Theory 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])
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:
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));
m ≤ P;
f m ≤ lfp (λs. sup m0 (f s))
⟧ ⟹ f m ≤ P"
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›
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
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
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
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