Theory Mutual_CCPO_Recursion

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

chapter ‹Mutual CCPO Recursion ‹fixed_point››

theory Mutual_CCPO_Recursion
  imports
    "HOL-Library.Complete_Partial_Order2"
    "AutoCorres_Utils"
  keywords "fixed_point" :: thy_goal_stmt
begin

section ‹Relate orders between locale and type classes›

lemma gfp_lub_fun: "gfp.lub_fun = Inf"
  unfolding fun_lub_def fun_eq_iff Inf_apply image_def by simp

lemma gfp_le_fun: "gfp.le_fun = (≥)"
  unfolding fun_ord_def le_fun_def fun_eq_iff Inf_apply image_def by simp

lemma
  shows fst_prod_lub: "fst (prod_lub luba lubb S) = luba (fst ` S)"
    and snd_prod_lub: "snd (prod_lub luba lubb S) = lubb (snd ` S)"
  by (auto simp: prod_lub_def)

lemma fun_lub_app: "fun_lub lub S x = lub ((λf. f x) ` S)"
  by (auto simp: fun_lub_def image_def)

lemma ccpo_Inf: "class.ccpo (Inf :: 'a::complete_lattice set ⇒ _) (≥) (mk_less (≥))"
  by (rule cont_intro)

lemma ccpo_Sup: "class.ccpo (Sup :: 'a::complete_lattice set ⇒ _) (≤) (mk_less (≤))"
  by (rule cont_intro)

lemma ccpo_flat: "class.ccpo (flat_lub b) (flat_ord b) (mk_less (flat_ord b))"
  using Partial_Function.ccpo[OF flat_interpretation] .

lemma monotone_pair[partial_function_mono]:
  "monotone R orda f ⟹ monotone R ordb g ⟹ monotone R (rel_prod orda ordb) (λx. (f x, g x))"
  by (simp add: monotone_def)

lemma monotone_fst'[partial_function_mono]:
  "monotone orda (rel_prod ordb ordc) f ⟹ monotone orda ordb (λx. fst (f x))"
  by (auto simp add: monotone_def rel_prod_sel)

lemma monotone_snd'[partial_function_mono]:
  "monotone orda (rel_prod ordb ordc) f ⟹ monotone orda ordc (λx. snd (f x))"
  by (auto simp add: monotone_def rel_prod_sel)

lemma monotone_id_fun_elim[partial_function_mono]:
  "monotone (≥) ord (λx. x) ⟹ monotone (≥) (fun_ord ord) (λx. x)"
  by (auto simp add: monotone_def le_fun_def fun_ord_def)

lemma monotone_id[partial_function_mono]: "monotone ord ord (λx. x)"
  by (auto simp add: monotone_def)

lemma monotone_abs:
  "(⋀x. monotone R Q (λf. F f x)) ⟹ monotone R (fun_ord Q) (λf x. F f x)"
  by (simp add: monotone_def fun_ord_def)

lemma monotone_fun_ord_applyD:
  "monotone orda (fun_ord ordb) f ⟹ monotone orda ordb (λy. f y x)"
  by(auto simp add: monotone_def fun_ord_def)

lemma admissible_snd:
  "cont luba orda (prod_lub lubb Inf) (rel_prod ordb (≥)) F ⟹
    ccpo.admissible luba orda (λx. snd (F x))"
  unfolding ccpo.admissible_def cont_def prod_eq_iff
  by (auto simp: prod_lub_def)

lemma cont_apply_gfp: "cont gfp.lub_fun gfp.le_fun Inf (≤) (λx. x c)"
  by (rule cont_applyI) (simp add: cont_def)

lemma mcont_mem_gfp:
  "mcont gfp.lub_fun gfp.le_fun (Inf) (≥) F ⟹ gfp.admissible (λA. x ∈ F A)"
  by (auto simp: mcont_def cont_def ccpo.admissible_def)

lemma mcont2mcont_call:
  "mcont luba orda (fun_lub lubb) (fun_ord ordb) F ⟹ mcont luba orda lubb ordb (λx. F x c)"
  by (auto simp: mcont_def monotone_def cont_def fun_lub_def fun_ord_def le_fun_def fun_eq_iff)
     (simp add: image_def)

lemma preorder_fun_ord [partial_function_mono]: "class.preorder R (mk_less R) ⟹ class.preorder (fun_ord R) (mk_less (fun_ord R))"
  by (force simp: class.preorder_def fun_ord_def mk_less_def)

lemma preorder_monotone_const'[partial_function_mono]: 
 "class.preorder leq (mk_less leq) ⟹ monotone ord leq (λ_. c)"
  by (rule preorder.monotone_const)

declare preorder_rel_prodI [partial_function_mono]
declare gfp.preorder [partial_function_mono]
declare lfp.preorder [partial_function_mono]

lemma option_ord_preorder [partial_function_mono]: "class.preorder option_ord (mk_less option_ord)" 
  by simp

section ‹Prove admissibility of ‹corresXF››

lemma not_imp_not_iff: "(¬A ⟶ ¬B) ⟷ (B ⟶ A)"
  by auto

lemma mcont_fun_lub_call:
  "mcont luba orda (fun_lub lubb) (fun_ord ordb) f ⟹
     mcont luba orda lubb ordb (λy. f y x)"
  by (simp add: mcont_fun_lub_apply)

lemma chain_disj_of_subsingleton:
  "Complete_Partial_Order.chain ord {r. P r} ⟹
    Complete_Partial_Order.chain ord {r. Q r} ⟹
    (⋀r q. P r ⟹ Q q ⟹ r = q) ⟹
    Complete_Partial_Order.chain ord {r. P r ∨ Q r}"
  by (auto simp: chain_def)

definition subsingleton_set :: "'a set ⇒ bool" where
  "subsingleton_set P ⟷ (∀a∈P. ∀b∈P. a = b)"

lemma subsingleton_set_empty[iff]: "subsingleton_set {}"
  by (simp add: subsingleton_set_def)

lemma subsingleton_set_singleton[iff]: "subsingleton_set {x}"
  by (simp add: subsingleton_set_def)

context ccpo
begin

lemma subsingleton_sets_imp_chain:
  "subsingleton_set (⋃ Ps) ⟹ Complete_Partial_Order.chain (≤) (⋃ Ps)"
  by (auto simp: subsingleton_set_def Complete_Partial_Order.chain_def Ball_def)

lemma Sup_of_subsingleton_sets_eq:
  assumes Ps: "subsingleton_set (⋃ Ps)" and P: "P ∈ Ps" and a: "a ∈ P"
  shows "Sup (⋃ Ps) = a" 
proof (intro order.antisym ccpo_Sup_least ccpo_Sup_upper subsingleton_sets_imp_chain[OF Ps])
  fix x :: 'a assume "x ∈ ⋃ Ps"
  then obtain Q where "Q ∈ Ps" "x ∈ Q" by auto
  with Ps P a show "x ≤ a"
    by (auto simp add: subsingleton_set_def Ball_def)
qed (use P a in blast)

lemma monotone_Sup_of_subsingleton_sets:
  assumes Ps: "⋀F. subsingleton_set (⋃ (Ps F))"
    and *: "⋀F G. ord F G ⟹ sim_set (sim_set (≤)) (Ps F) (Ps G)"
  shows "monotone ord (≤) (λF. Sup (⋃ (Ps F)))"
proof (intro monotoneI ccpo_Sup_least subsingleton_sets_imp_chain[OF Ps])
  fix F G x assume "ord F G" "x ∈ ⋃ (Ps F)"
  with *[of F G] obtain y where "x ≤ y" "y ∈ ⋃ (Ps G)"
    by (fastforce simp: sim_set_def)
  then show "x ≤ Sup (⋃ (Ps G))"
    apply (intro order_trans[OF ‹x ≤ y›])
    apply (intro ccpo_Sup_upper subsingleton_sets_imp_chain[OF Ps])
    apply auto
    done
qed

lemma ccpo_refl: "x ≤ x" ..

lemma fixp_unfold_def:
  fixes f :: "'a ⇒ 'a"
  assumes def: "F ≡ ccpo.fixp Sup (≤) f"
  assumes f: "monotone (≤) (≤) f"
  shows "F = f F"
  by (unfold def) (rule fixp_unfold[OF f])

lemma fixp_induct_def:
  fixes f :: "'a ⇒ 'a"
  assumes def: "F ≡ ccpo.fixp Sup (≤) f"
  assumes mono: "monotone (≤) (≤) f"
  assumes adm: "ccpo.admissible Sup (≤) P"
  assumes bot: "P (Sup {})"
  assumes step: "⋀x. P x ⟹ P (f x)"
  shows "P F"
  by (unfold def) (rule fixp_induct[OF adm mono bot step])

lemma induct_Sup_of_subsingleton_sets:
  assumes Ps: "subsingleton_set (⋃ Ps)"
    and adm: "ccpo.admissible Sup (≤) P"
    and bot: "P (Sup {})"
    and step: "⋀p x. p ∈ Ps ⟹ x ∈ p ⟹ P x"
  shows "P (Sup (⋃ Ps))"
proof cases
  assume *: "(⋃ Ps) = {}" from bot show ?thesis unfolding * .
next
  assume *: "(⋃ Ps) ≠ {}"
  show ?thesis
    by (intro ccpo.admissibleD[OF adm subsingleton_sets_imp_chain[OF Ps] *])
       (blast intro: step)
qed

lemma induct_Sup_of_subsingleton_sets_def:
  assumes F: "F ≡ Sup (⋃ Ps)"
  assumes Ps: "subsingleton_set (⋃ Ps)"
    and adm: "ccpo.admissible Sup (≤) P"
    and bot: "P (Sup {})"
    and step: "⋀p x. p ∈ Ps ⟹ x ∈ p ⟹ P x"
  shows "P F"
  unfolding F by (rule induct_Sup_of_subsingleton_sets; fact)

end

lemma flat_lub_empty: "flat_lub x {} = x"
  by (simp add: flat_lub_def)

lemma monotone_bind_option[partial_function_mono]:
  "monotone ord option_ord f ⟹ (⋀a. monotone ord option_ord (λx. g x a)) ⟹
    monotone ord option_ord (λx. Option.bind (f x) (g x))"
  by (fastforce simp: monotone_def flat_ord_def bind_eq_None_conv)

lemma (in ccpo) admissible_ord: "ccpo.admissible Sup (≤) (λx. x ≤ b)"
  by (clarsimp simp add: ccpo.admissible_def intro!: ccpo_Sup_least)

ML_file ‹mutual_ccpo_recursion.ML›

setup ‹
  (Mutual_CCPO_Rec.add_ccpo "option" Mutual_CCPO_Rec.synth_option
    #> Mutual_CCPO_Rec.add_ccpo "lfp" Mutual_CCPO_Rec.synth_lfp
    #> Mutual_CCPO_Rec.add_ccpo "gfp" Mutual_CCPO_Rec.synth_gfp)
  |> Context.theory_map ›

no_notation top ("⊤")
no_notation bot ("⊥")
no_notation sup (infixl "⊔" 65)
no_notation inf (infixl "⊓" 70)

hide_const (open) cont

end