# Theory Complete_Lattice_Prop

Up to index of Isabelle/HOL/LatticeProperties

theory Complete_Lattice_Prop
imports WellFoundedTransitive
`header {* Fixpoints and Complete Lattices *}(*    Author: Viorel Preoteasa*)theory Complete_Lattice_Propimports WellFoundedTransitivebegintext{*This theory introduces some results about fixpoints of functions on complete lattices. The main result is that a monotonic function mapping momotonic functions to monotonic functions has the least fixpoint monotonic.*}context complete_lattice beginlemma inf_Inf: assumes nonempty: "A ≠ {}"   shows "inf x (Inf A) = Inf ((inf x) ` A)"  apply (rule antisym, simp_all)  apply (rule Inf_greatest)  apply (simp add: image_def, safe, simp)  apply (rule_tac y = "Inf A" in order_trans, simp_all)  apply (rule Inf_lower, simp)  apply (cut_tac nonempty)  apply safe  apply (erule notE)  apply (rule_tac y = "inf x xa" in order_trans)  apply (rule Inf_lower, simp add: image_def, blast)  apply simp  apply (rule Inf_greatest)  apply (rule_tac y = "inf x xa" in order_trans)  apply (rule Inf_lower)  apply (simp add: image_def)  by autoend(*Monotonic applications which map monotonic to monotonic have monotonic fixpoints*)definition  "mono_mono F = (mono F ∧ (∀ f . mono f --> mono (F f)))"theorem lfp_mono [simp]:  "mono_mono F ==> mono (lfp F)"  apply (simp add: mono_mono_def)  apply (rule_tac f="F" and P = "mono" in lfp_ordinal_induct)  apply (simp_all add: mono_def)  apply (intro allI impI SUP_least)  apply (rule_tac y = "f y" in order_trans)  apply (auto intro: SUP_upper)  donelemma gfp_ordinal_induct:  fixes f :: "'a::complete_lattice => 'a"  assumes mono: "mono f"  and P_f: "!!S. P S ==> P (f S)"  and P_Union: "!!M. ∀S∈M. P S ==> P (Inf M)"  shows "P (gfp f)"proof -  let ?M = "{S. gfp f ≤ S ∧ P S}"  have "P (Inf ?M)" using P_Union by simp  also have "Inf ?M = gfp f"  proof (rule antisym)    show "gfp f ≤ Inf ?M" by (blast intro: Inf_greatest)    hence "f (gfp f) ≤ f (Inf ?M)" by (rule mono [THEN monoD])    hence "gfp f ≤ f (Inf ?M)" using mono [THEN gfp_unfold] by simp    hence "f (Inf ?M) ∈ ?M" using P_f P_Union by simp    hence "Inf ?M ≤ f (Inf ?M)" by (rule Inf_lower)    thus "Inf ?M ≤ gfp f" by (rule gfp_upperbound)  qed  finally show ?thesis .qed theorem gfp_mono [simp]:  "mono_mono F ==> mono (gfp F)"  apply (simp add: mono_mono_def)  apply (rule_tac f="F" and P = "mono" in gfp_ordinal_induct)  apply (simp_all, safe)  apply (simp_all add: mono_def)  apply (intro allI impI INF_greatest)  apply (rule_tac y = "f x" in order_trans)  apply (auto intro: INF_lower)  donecontext complete_lattice begindefinition  "Sup_less x (w::'b::well_founded) = Sup {y ::'a . ∃ v < w . y = x v}"lemma Sup_less_upper:  "v < w ==> P v ≤ Sup_less P w"  by (simp add: Sup_less_def, rule Sup_upper, blast)lemma Sup_less_least:  "(!! v . v < w ==> P v ≤ Q) ==> Sup_less P w ≤ Q"  by (simp add: Sup_less_def, rule Sup_least, blast)endlemma Sup_less_fun_eq:  "((Sup_less P w) i) = (Sup_less (λ v . P v i)) w"  apply (simp add: Sup_less_def Sup_fun_def SUP_def)  by (rule_tac f = Sup in arg_cong, auto)theorem fp_wf_induction:  "f x  = x ==> mono f ==> (∀ w . (y w) ≤ f (Sup_less y w)) ==> Sup (range y) ≤ x"  apply (rule Sup_least)  apply (simp add: image_def, safe, simp)  apply (rule less_induct1, simp_all)  apply (rule_tac y = "f (Sup_less y xa)" in order_trans, simp)  apply (drule_tac x = "Sup_less y xa" and y = "x" in monoD)  by (simp add: Sup_less_least, auto)end`