# Theory LatticeProperties.Complete_Lattice_Prop

```section ‹Fixpoints and Complete Lattices›

(*
Author: Viorel Preoteasa
*)

theory Complete_Lattice_Prop
imports WellFoundedTransitive
begin

text‹
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 begin

lemma inf_Inf: assumes nonempty: "A ≠ {}"
shows "inf x (Inf A) = Inf ((inf x) ` A)"
using assms by (auto simp add: INF_inf_const1 nonempty)

end

(*
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 (rule_tac f="F" and P = "mono" in lfp_ordinal_induct)
apply (intro allI impI SUP_least)
apply (rule_tac y = "f y" in order_trans)
apply (auto intro: SUP_upper)
done

lemma 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 (rule_tac f="F" and P = "mono" in gfp_ordinal_induct)
apply (simp_all, safe)
apply (intro allI impI INF_greatest)
apply (rule_tac y = "f x" in order_trans)
apply (auto intro: INF_lower)
done

context complete_lattice begin

definition
"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)

end

lemma Sup_less_fun_eq:
"((Sup_less P w) i) = (Sup_less (λ v . P v i)) w"
apply (rule arg_cong [of _ _ Sup])
apply auto
done

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)