# 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
```