Theory Refine_Monadic.Refine_Misc

section ‹Miscellanneous Lemmas and Tools›
theory Refine_Misc
imports 
  Automatic_Refinement.Automatic_Refinement
  Refine_Mono_Prover
begin

text ‹Basic configuration for monotonicity prover:›
lemmas [refine_mono] = monoI monotoneI[of "(≤)" "(≤)"]
lemmas [refine_mono] = TrueI le_funI order_refl

lemma case_prod_mono[refine_mono]: 
  "⟦⋀a b. p=(a,b) ⟹ f a b ≤ f' a b⟧ ⟹ case_prod f p ≤ case_prod f' p"
  by (auto split: prod.split)

lemma case_option_mono[refine_mono]:
  assumes "fn ≤ fn'"
  assumes "⋀v. x=Some v ⟹ fs v ≤ fs' v"
  shows "case_option fn fs x ≤ case_option fn' fs' x"
  using assms by (auto split: option.split)

lemma case_list_mono[refine_mono]:
  assumes "fn ≤ fn'"
  assumes "⋀x xs. l=x#xs ⟹ fc x xs ≤ fc' x xs"
  shows "case_list fn fc l ≤ case_list fn' fc' l"
  using assms by (auto split: list.split)

lemma if_mono[refine_mono]:
  assumes "b ⟹ m1 ≤ m1'"
  assumes "¬b ⟹ m2 ≤ m2'"
  shows "(if b then m1 else m2) ≤ (if b then m1' else m2')"
  using assms by auto

lemma let_mono[refine_mono]:
  "f x ≤ f' x' ⟹ Let x f ≤ Let x' f'" by auto


subsection ‹Uncategorized Lemmas›
lemma all_nat_split_at: "∀i::'a::linorder<k. P i ⟹ P k ⟹ ∀i>k. P i 
  ⟹ ∀i. P i"
  by (metis linorder_neq_iff)

subsection ‹Well-Foundedness›

lemma wf_no_infinite_down_chainI:
  assumes "⋀f. ⟦⋀i. (f (Suc i), f i)∈r⟧ ⟹ False"
  shows "wf r"
  by (metis assms wf_iff_no_infinite_down_chain)

text ‹This lemma transfers well-foundedness over a simulation relation.›
lemma sim_wf:
  assumes WF: "wf (S'¯)"
  assumes STARTR: "(x0,x0')∈R"
  assumes SIM: "⋀s s' t. ⟦ (s,s')∈R; (s,t)∈S; (x0',s')∈S'⇧* ⟧ 
    ⟹ ∃t'. (s',t')∈S' ∧ (t,t')∈R"
  assumes CLOSED: "Domain S  ⊆ S⇧*``{x0}"
  shows "wf (S¯)"
proof (rule wf_no_infinite_down_chainI, simp)
  txt ‹
    Informal proof:
    Assume there is an infinite chain in ‹S›.
    Due to the closedness property of ‹S›, it can be extended to 
    start at ‹x0›.
    Now, we inductively construct an infinite chain in ‹S'›, such that
    each element of the new chain is in relation with the corresponding 
    element of the original chain:
      The first element is ‹x0'›. 
      For any element ‹i+1›, the simulation property yields the next
      element.
    This chain contradicts well-foundedness of ‹S'›.
›

  fix f
  assume CHAIN: "⋀i. (f i, f (Suc i))∈S"
  txt ‹Extend to start with ‹x0››
  obtain f' where CHAIN': "⋀i. (f' i, f' (Suc i))∈S" and [simp]: "f' 0 = x0"
  proof -
    {
      fix x
      assume S: "x = f 0"
      from CHAIN have "f 0 ∈ Domain S" by auto
      with CLOSED have "(x0,x)∈S⇧*" by (auto simp: S)
      then obtain g k where G0: "g 0 = x0" and X: "x = g k" 
        and CH: "(∀i<k. (g i, g (Suc i))∈S)"
      proof induct
        case base thus ?case by force
      next
        case (step y z) show ?case proof (rule step.hyps(3))
          fix g k 
          assume "g 0 = x0" and "y = g k" 
            and "∀i<k. (g i, g (Suc i))∈S"
          thus ?case using ‹(y,z)∈S›
            by (rule_tac step.prems[where g="g(Suc k := z)" and k="Suc k"])
              auto
        qed
      qed
      define f' where "f' i = (if i<k then g i else f (i-k))" for i
      have "∃f'. f' 0 = x0 ∧ (∀i. (f' i, f' (Suc i))∈S)"
        apply (rule_tac x=f' in exI)
        apply (unfold f'_def)
        apply (rule conjI)
        using S X G0 apply (auto) []
        apply (rule_tac k=k in all_nat_split_at)
        apply (auto)
        apply (simp add: CH)
        apply (subgoal_tac "k = Suc i")
        apply (simp add: S[symmetric] CH X)
        apply simp
        apply (simp add: CHAIN)
        apply (subgoal_tac "Suc i - k = Suc (i-k)")
        using CHAIN apply simp
        apply simp
        done
    }
    then obtain f' where "∀i. (f' i,f' (Suc i))∈S" and "f' 0 = x0" by blast
    thus ?thesis by (blast intro!: that)
  qed

  txt ‹Construct chain in ‹S'››
  define g' where "g' = rec_nat x0' (λi x. SOME x'. 
          (x,x')∈S' ∧ (f' (Suc i),x')∈R ∧ (x0', x')∈S'⇧* )"
  {
    fix i
    note [simp] = g'_def
    have "(g' i, g' (Suc i))∈S' ∧ (f' (Suc i),g' (Suc i))∈R 
      ∧ (x0',g' (Suc i))∈S'⇧*"
    proof (induct i)
      case 0 
      from SIM[OF STARTR] CHAIN'[of 0] obtain t' where 
        "(x0',t')∈S'" and "(f' (Suc 0),t')∈R" by auto
      moreover hence "(x0',t')∈S'⇧*" by auto
      ultimately show ?case
        by (auto intro: someI2 simp: STARTR)
    next
      case (Suc i)
      with SIM[OF _ CHAIN'[of "Suc i"]] 
      obtain t' where LS: "(g' (Suc i),t')∈S'" and "(f' (Suc (Suc i)),t')∈R"
        by auto
      moreover from LS Suc have "(x0', t')∈S'⇧*" by auto
      ultimately show ?case
        apply simp
        apply (rule_tac a="t'" in someI2)
        apply auto
        done
    qed
  } hence S'CHAIN: "∀i. (g' i, g'(Suc i))∈S'" by simp
  txt ‹This contradicts well-foundedness›
  with WF show False 
    by (erule_tac wf_no_infinite_down_chainE[where f=g']) simp
qed

text ‹Well-founded relation that approximates a finite set from below.›
definition "finite_psupset S ≡ { (Q',Q). Q⊂Q' ∧ Q' ⊆ S }"
lemma finite_psupset_wf[simp, intro]: "finite S ⟹ wf (finite_psupset S)"
  unfolding finite_psupset_def by (blast intro: wf_bounded_supset)

definition "less_than_bool ≡ {(a,b). a<(b::bool)}"
lemma wf_less_than_bool[simp, intro!]: "wf (less_than_bool)"
  unfolding less_than_bool_def
  by (auto simp: wf_def)
lemma less_than_bool_iff[simp]:
  "(x,y)∈less_than_bool ⟷ x=False ∧ y=True"  
  by (auto simp: less_than_bool_def)

definition "greater_bounded N ≡ inv_image less_than (λx. N-x)" 
lemma wf_greater_bounded[simp, intro!]: "wf (greater_bounded N)" by (auto simp: greater_bounded_def)

lemma greater_bounded_Suc_iff[simp]: "(Suc x,x)∈greater_bounded N ⟷ Suc x ≤ N"
  by (auto simp: greater_bounded_def)

    
    
subsection ‹Monotonicity and Orderings›

lemma mono_const[simp, intro!]: "mono (λ_. c)" by (auto intro: monoI)
lemma mono_if: "⟦mono S1; mono S2⟧ ⟹
  mono (λF s. if b s then S1 F s else S2 F s)"
  apply rule
  apply (rule le_funI)
  apply (auto dest: monoD[THEN le_funD])
  done

lemma mono_infI: "mono f ⟹ mono g ⟹ mono (inf f g)"
  unfolding inf_fun_def
  apply (rule monoI)
  apply (metis inf_mono monoD)
  done

lemma mono_infI': 
  "mono f ⟹ mono g ⟹ mono (λx. inf (f x) (g x) :: 'b::lattice)"
  by (rule mono_infI[unfolded inf_fun_def])

lemma mono_infArg: 
  fixes f :: "'a::lattice ⇒ 'b::order"
  shows "mono f ⟹ mono (λx. f (inf x X))"
  apply (rule monoI)
  apply (erule monoD)
  apply (metis inf_mono order_refl) 
  done

lemma mono_Sup:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "mono f ⟹ Sup (f`S) ≤ f (Sup S)"
  apply (rule Sup_least)
  apply (erule imageE)
  apply simp
  apply (erule monoD)
  apply (erule Sup_upper)
  done

lemma mono_SupI:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  assumes "mono f"
  assumes "S'⊆f`S"
  shows "Sup S' ≤ f (Sup S)"
  by (metis Sup_subset_mono assms mono_Sup order_trans)

lemma mono_Inf:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "mono f ⟹ f (Inf S) ≤ Inf (f`S)"
  apply (rule Inf_greatest)
  apply (erule imageE)
  apply simp
  apply (erule monoD)
  apply (erule Inf_lower)
  done

lemma mono_funpow: "mono (f::'a::order ⇒ 'a) ⟹ mono (f^^i)"
  apply (induct i)
  apply (auto intro!: monoI) 
  apply (auto dest: monoD)
  done

lemma mono_id[simp, intro!]:
  "mono id"
  "mono (λx. x)"
  by (auto intro: monoI)

declare SUP_insert[simp]

lemma (in semilattice_inf) le_infD1:
  "a ≤ inf b c ⟹ a ≤ b" by (rule le_infE)
lemma (in semilattice_inf) le_infD2:
  "a ≤ inf b c ⟹ a ≤ c" by (rule le_infE)
lemma (in semilattice_inf) inf_leI:
  "⟦ ⋀x. ⟦ x≤a; x≤b ⟧ ⟹ x≤c ⟧ ⟹ inf a b ≤ c"
  by (metis inf_le1 inf_le2)

lemma top_Sup: "(top::'a::complete_lattice)∈A ⟹ Sup A = top"
  by (metis Sup_upper top_le)
lemma bot_Inf: "(bot::'a::complete_lattice)∈A ⟹ Inf A = bot"
  by (metis Inf_lower le_bot)

lemma mono_compD: "mono f ⟹ x≤y ⟹ f o x ≤ f o y"
  apply (rule le_funI)
  apply (auto dest: monoD le_funD)
  done


subsubsection ‹Galois Connections›
locale galois_connection =
  fixes α::"'a::complete_lattice ⇒ 'b::complete_lattice" and γ
  assumes galois: "c ≤ γ(a) ⟷ α(c) ≤ a"
begin
  lemma αγ_defl: "α(γ(x)) ≤ x"
  proof -
    have "γ x ≤ γ x" by simp
    with galois show "α(γ(x)) ≤ x" by blast
  qed
  lemma γα_infl: "x ≤ γ(α(x))"
  proof -
    have "α x ≤ α x" by simp
    with galois show "x ≤ γ(α(x))" by blast
  qed
    
  lemma α_mono: "mono α"
  proof 
    fix x::'a and y::'a
    assume "x≤y"
    also note γα_infl[of y]
    finally show "α x ≤ α y" by (simp add: galois)
  qed

  lemma γ_mono: "mono γ"
    by rule (metis αγ_defl galois inf_absorb1 le_infE)

  lemma dist_γ[simp]: 
    "γ (inf a b) = inf (γ a) (γ b)"
    apply (rule order_antisym)
    apply (rule mono_inf[OF γ_mono])
    apply (simp add: galois)
    apply (simp add: galois[symmetric])
    done

  lemma dist_α[simp]: 
    "α (sup a b) = sup (α a) (α b)"
    by (metis (no_types) α_mono galois mono_sup order_antisym 
      sup_ge1 sup_ge2 sup_least)

end

subsubsection ‹Fixed Points›
lemma mono_lfp_eqI:
  assumes MONO: "mono f"
  assumes FIXP: "f a ≤ a"
  assumes LEAST: "⋀x. f x = x ⟹ a≤x"
  shows "lfp f = a"
  apply (rule antisym)
  apply (rule lfp_lowerbound)
  apply (rule FIXP)
  by (metis LEAST MONO lfp_unfold)

lemma mono_gfp_eqI:
  assumes MONO: "mono f"
  assumes FIXP: "a ≤ f a"
  assumes GREATEST: "⋀x. f x = x ⟹ x≤a"
  shows "gfp f = a"
  apply (rule antisym)
  apply (metis GREATEST MONO gfp_unfold)
  apply (rule gfp_upperbound)
  apply (rule FIXP)
  done

lemma lfp_le_gfp': "mono f ⟹ lfp f x ≤ gfp f x"
  by (rule le_funD[OF lfp_le_gfp])

(* Just a reformulation of lfp_induct *)
lemma lfp_induct':
  assumes M: "mono f"
  assumes IS: "⋀m. ⟦ m ≤ lfp f; m ≤ P ⟧ ⟹ f m ≤ P"
  shows "lfp f ≤ P"
  apply (rule lfp_induct[OF M])
  apply (rule IS)
  by simp_all

lemma lfp_gen_induct:
  ― ‹Induction lemma for generalized lfps›
  assumes M: "mono f"
  notes MONO'[refine_mono] = monoD[OF M]
  assumes I0: "m0 ≤ P"
  assumes IS: "⋀m. ⟦
      m ≤ lfp (λs. sup m0 (f s));  ― ‹Assume already established invariants›
      m ≤ P;                       ― ‹Assume invariant›
      f m ≤ lfp (λs. sup m0 (f s)) ― ‹Assume that step preserved est. invars›
    ⟧ ⟹ f m ≤ P"                 ― ‹Show that step preserves invariant›
  shows "lfp (λs. sup m0 (f s)) ≤ P"
  apply (rule lfp_induct')
  apply (meson MONO' monoI order_mono_setup.refl sup_mono)
  apply (rule sup_least)
  apply (rule I0)
  apply (rule IS, assumption+)
  apply (subst lfp_unfold)
  apply (meson MONO' monoI order_mono_setup.refl sup_mono)
  apply (rule le_supI2)
  apply (rule monoD[OF M])
  .



subsubsection ‹Connecting Complete Lattices and 
  Chain-Complete Partial Orders›
(* Note: Also connected by subclass now. However, we need both directions
  of embedding*)
lemma (in complete_lattice) is_ccpo: "class.ccpo Sup (≤) (<)"
  apply unfold_locales
  apply (erule Sup_upper)
  apply (erule Sup_least)
  done

lemma (in complete_lattice) is_dual_ccpo: "class.ccpo Inf (≥) (>)"
  apply unfold_locales
  apply (rule less_le_not_le)
  apply (rule order_refl)
  apply (erule (1) order_trans)
  apply (erule (1) order.antisym)
  apply (erule Inf_lower)
  apply (erule Inf_greatest)
  done

lemma dual_ccpo_mono_simp: "monotone (≥) (≥) f ⟷ mono f"
  unfolding monotone_def mono_def by auto
lemma dual_ccpo_monoI: "mono f ⟹ monotone (≥) (≥) f" 
  by (simp add: dual_ccpo_mono_simp) 
lemma dual_ccpo_monoD: "monotone (≥) (≥) f ⟹ mono f" 
  by (simp add: dual_ccpo_mono_simp) 

lemma ccpo_lfp_simp: "⋀f. mono f ⟹ ccpo.fixp Sup (≤) f = lfp f"
  apply (rule antisym)
  defer
  apply (rule lfp_lowerbound)
  apply (drule ccpo.fixp_unfold[OF is_ccpo , symmetric])
  apply simp

  apply (rule ccpo.fixp_lowerbound[OF is_ccpo], assumption)
  apply (simp add: lfp_unfold[symmetric])
  done

lemma ccpo_gfp_simp: "⋀f. mono f ⟹ ccpo.fixp Inf (≥) f = gfp f"
  apply (rule antisym)
  apply (rule gfp_upperbound)
  apply (drule ccpo.fixp_unfold[OF is_dual_ccpo dual_ccpo_monoI, symmetric])
  apply simp

  apply (rule ccpo.fixp_lowerbound[OF is_dual_ccpo dual_ccpo_monoI], assumption)
  apply (simp add: gfp_unfold[symmetric])
  done

abbreviation "chain_admissible P ≡ ccpo.admissible Sup (≤) P"
abbreviation "is_chain ≡ Complete_Partial_Order.chain (≤)"
lemmas chain_admissibleI[intro?] = ccpo.admissibleI[where lub=Sup and ord="(≤)"]


abbreviation "dual_chain_admissible P ≡ ccpo.admissible Inf (λx y. y≤x) P"
abbreviation "is_dual_chain ≡ Complete_Partial_Order.chain (λx y. y≤x)"
lemmas dual_chain_admissibleI[intro?] = 
  ccpo.admissibleI[where lub=Inf and ord="(λx y. y≤x)"]

lemma dual_chain_iff[simp]: "is_dual_chain C = is_chain C"
  unfolding chain_def
  apply auto
  done

lemmas chain_dualI = iffD1[OF dual_chain_iff]
lemmas dual_chainI = iffD2[OF dual_chain_iff]

lemma is_chain_empty[simp, intro!]: "is_chain {}"
  by (rule chainI) auto
lemma is_dual_chain_empty[simp, intro!]: "is_dual_chain {}"
  by (rule dual_chainI) auto

lemma point_chainI: "is_chain M ⟹ is_chain ((λf. f x)`M)"
  by (auto intro: chainI le_funI dest: chainD le_funD)


text ‹We transfer the admissible induction lemmas to complete
  lattices.›
lemma lfp_cadm_induct:
  "⟦chain_admissible P; P (Sup {}); mono f; ⋀x. P x ⟹ P (f x)⟧ ⟹ P (lfp f)"
  by (simp only:  ccpo_lfp_simp[symmetric])
     (rule ccpo.fixp_induct[OF is_ccpo])

lemma gfp_cadm_induct:
  "⟦dual_chain_admissible P; P (Inf {}); mono f; ⋀x. P x ⟹ P (f x)⟧ ⟹ P (gfp f)"
  by (simp only: dual_ccpo_mono_simp[symmetric] ccpo_gfp_simp[symmetric])
     (rule ccpo.fixp_induct[OF is_dual_ccpo])

subsubsection ‹Continuity and Kleene Fixed Point Theorem›
definition "cont f ≡ ∀C. C≠{} ⟶ f (Sup C) = Sup (f`C)"
definition "strict f ≡ f bot = bot"
definition "inf_distrib f ≡ strict f ∧ cont f"

lemma contI[intro?]: "⟦⋀C. C≠{} ⟹ f (Sup C) = Sup (f`C)⟧ ⟹ cont f" 
  unfolding cont_def by auto
lemma contD: "cont f ⟹ C≠{} ⟹ f (Sup C) = Sup (f ` C)"
  unfolding cont_def by auto
lemma contD': "cont f ⟹ C≠{} ⟹ f (Sup C) = Sup (f ` C)"
  by (fact contD)

lemma strictD[dest]: "strict f ⟹ f bot = bot" 
  unfolding strict_def by auto
― ‹We only add this lemma to the simpset for functions on the same type. 
    Otherwise, the simplifier tries it much too often.›
lemma strictD_simp[simp]: "strict f ⟹ f (bot::'a::bot) = (bot::'a)" 
  unfolding strict_def by auto

lemma strictI[intro?]: "f bot = bot ⟹ strict f"
  unfolding strict_def by auto

lemma inf_distribD[simp]: 
  "inf_distrib f ⟹ strict f"
  "inf_distrib f ⟹ cont f"
  unfolding inf_distrib_def by auto

lemma inf_distribI[intro?]: "⟦strict f; cont f⟧ ⟹ inf_distrib f"
  unfolding inf_distrib_def by auto

lemma inf_distribD'[simp]:
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "inf_distrib f ⟹ f (Sup C) = Sup (f`C)"
  apply (cases "C={}")
  apply (auto dest: inf_distribD contD')
  done

lemma inf_distribI':
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  assumes B: "⋀C. f (Sup C) = Sup (f`C)"
  shows "inf_distrib f"
  apply (rule)
  apply (rule)
  apply (rule B[of "{}", simplified])
  apply (rule)
  apply (rule B)
  done
  
lemma cont_is_mono[simp]: 
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "cont f ⟹ mono f"
  apply (rule monoI)
  apply (drule_tac C="{x,y}" in contD)
  apply (auto simp: le_iff_sup)
  done

lemma inf_distrib_is_mono[simp]: 
  fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
  shows "inf_distrib f ⟹ mono f"
  by simp

text ‹Only proven for complete lattices here. Also holds for CCPOs.›

theorem gen_kleene_lfp:
  fixes f:: "'a::complete_lattice ⇒ 'a"
  assumes CONT: "cont f"
  shows "lfp (λx. sup m (f x)) = (SUP i. (f^^i) m)"
proof (rule antisym)
  let ?f = "(λx. sup m (f x))"
  let ?K="{ (f^^i) m | i . True}"
  note MONO=cont_is_mono[OF CONT]
  note MONO'[refine_mono] = monoD[OF MONO]
  {
    fix i
    have "(f^^i) m ≤ lfp ?f"
      apply (induct i)
      apply simp
      apply (subst lfp_unfold)
      apply (meson MONO' monoI order_mono_setup.refl sup_mono) 
      apply simp
      
      apply (subst lfp_unfold)
      apply (meson MONO' monoI order_mono_setup.refl sup_mono) 
      apply simp
      by (metis MONO' le_supI2)
  } thus "(SUP i. (f^^i) m) ≤ lfp ?f" by (blast intro: SUP_least)
next
  let ?f = "(λx. sup m (f x))"
  show "lfp ?f ≤ (SUP i. (f^^i) m)"
    apply (rule lfp_lowerbound)
    apply (rule sup_least)
    apply (rule order_trans[OF _ SUP_upper[where i=0]], simp_all) []
    apply (simp add: contD [OF CONT])
    apply (rule Sup_subset_mono)
    apply (auto)
    apply (rule_tac x="Suc i" in range_eqI)
    apply simp
    done
qed

theorem kleene_lfp:
  fixes f:: "'a::complete_lattice ⇒ 'a"
  assumes CONT: "cont f"
  shows "lfp f = (SUP i. (f^^i) bot)"
  using gen_kleene_lfp[OF CONT,where m=bot] by simp

theorem (* Detailed proof *)
  fixes f:: "'a::complete_lattice ⇒ 'a"
  assumes CONT: "cont f"
  shows "lfp f = (SUP i. (f^^i) bot)"
proof (rule antisym)
  let ?K="{ (f^^i) bot | i . True}"
  note MONO=cont_is_mono[OF CONT]
  {
    fix i
    have "(f^^i) bot ≤ lfp f"
      apply (induct i)
      apply simp
      apply simp
      by (metis MONO lfp_unfold monoD)
  } thus "(SUP i. (f^^i) bot) ≤ lfp f" by (blast intro: SUP_least)
next
  show "lfp f ≤ (SUP i. (f^^i) bot)"
    apply (rule lfp_lowerbound)
    apply (simp add: contD [OF CONT])
    apply (rule Sup_subset_mono)
    apply auto
    apply (rule_tac x="Suc i" in range_eqI)
    apply auto
    done
qed

(* Alternative proof of gen_kleene_lfp that re-uses standard Kleene, but is more tedious *)
lemma SUP_funpow_contracting:
  fixes f :: "'a ⇒ ('a::complete_lattice)"
  assumes C: "cont f" 
  shows "f (SUP i. (f^^i) m) ≤ (SUP i. (f^^i) m)"
proof -
  have 1: "⋀i x. f ((f^^i) x) = (f^^(Suc i)) x"
    by simp

  have "f (SUP i. (f^^i) m) = (SUP i. f ((f ^^ i) m))"
    by (subst contD[OF C]) (simp_all add: image_comp)
  also have "… ≤ (SUP i. (f^^i) m)"
    apply (rule SUP_least)
    apply (simp, subst 1)
    apply (rule SUP_upper)
    ..
  finally show ?thesis .
qed

lemma gen_kleene_chain_conv:
  fixes f :: "'a::complete_lattice ⇒ 'a"
  assumes C: "cont f"
  shows "(SUP i. (f^^i) m) = (SUP i. ((λx. sup m (f x))^^i) bot)"
proof -
  let ?f' = "λx. sup m (f x)"
  show ?thesis
  proof (intro antisym SUP_least)
    from C have C': "cont ?f'"
      unfolding cont_def
      by (simp add: SUP_sup_distrib[symmetric])
  
    fix i
    show "(f ^^ i) m ≤ (SUP i. (?f' ^^ i) bot)"
    proof (induction i)
      case 0 show ?case
        by (rule order_trans[OF _ SUP_upper[where i=1]]) auto
    next
      case (Suc i)
      from cont_is_mono[OF C, THEN monoD, OF Suc]
      have "(f ^^ (Suc i)) m ≤ f (SUP i. ((λx. sup m (f x)) ^^ i) bot)"
        by simp
      also have "… ≤ sup m …" by simp
      also note SUP_funpow_contracting[OF C']
      finally show ?case .
    qed
  next
    fix i
    show "(?f'^^i) bot ≤ (SUP i. (f^^i) m)"
    proof (induction i)
      case 0 thus ?case by simp
    next
      case (Suc i)
      from monoD[OF cont_is_mono[OF C] Suc]
      have "(?f'^^Suc i) bot ≤ sup m (f (SUP i. (f ^^ i) m))" 
        by (simp add: le_supI2)
      also have "… ≤ (SUP i. (f ^^ i) m)"
        apply (rule sup_least)
        apply (rule order_trans[OF _ SUP_upper[where i=0]], simp_all) []
        apply (rule SUP_funpow_contracting[OF C])
        done
      finally show ?case .
    qed
  qed
qed
   
theorem 
  assumes C: "cont f"
  shows "lfp (λx. sup m (f x)) = (SUP i. (f^^i) m)"
  apply (subst gen_kleene_chain_conv[OF C])
  apply (rule kleene_lfp)
    using C
    unfolding cont_def
    apply (simp add: SUP_sup_distrib[symmetric])
  done



lemma (in galois_connection) dual_inf_dist_γ: "γ (Inf C) = Inf (γ`C)"
  apply (rule antisym)
  apply (rule Inf_greatest)
  apply clarify
  apply (rule monoD[OF γ_mono])
  apply (rule Inf_lower)
  apply simp

  apply (subst galois)
  apply (rule Inf_greatest)
  apply (subst galois[symmetric])
  apply (rule Inf_lower)
  apply simp
  done

lemma (in galois_connection) inf_dist_α: "inf_distrib α"
  apply (rule inf_distribI')
  apply (rule antisym)

  apply (subst galois[symmetric])
  apply (rule Sup_least)
  apply (subst galois)
  apply (rule Sup_upper)
  apply simp

  apply (rule Sup_least)
  apply clarify
  apply (rule monoD[OF α_mono])
  apply (rule Sup_upper)
  apply simp
  done

subsection ‹Maps›
subsubsection ‹Key-Value Set›
  
  lemma map_to_set_simps[simp]: 
    "map_to_set Map.empty = {}"
    "map_to_set [a↦b] = {(a,b)}"
    "map_to_set (m|`K) = map_to_set m ∩ K×UNIV"
    "map_to_set (m(x:=None)) = map_to_set m - {x}×UNIV"
    "map_to_set (m(x↦v)) = map_to_set m - {x}×UNIV ∪ {(x,v)}"
    "map_to_set m ∩ dom m×UNIV = map_to_set m"
    "m k = Some v ⟹ (k,v)∈map_to_set m"
    "single_valued (map_to_set m)"
    apply (simp_all)
    by (auto simp: map_to_set_def restrict_map_def split: if_split_asm
      intro: single_valuedI)
      
  lemma map_to_set_inj:     
    "(k,v)∈map_to_set m ⟹ (k,v')∈map_to_set m ⟹ v = v'"
    by (auto simp: map_to_set_def)


end