(* Title: HOL/Algebra/Complete_Lattice.thy
Author: Clemens Ballarin, started 7 November 2003
Copyright: Clemens Ballarin
Most congruence rules by Stephan Hohe.
With additional contributions from Alasdair Armstrong and Simon Foster.
*)
theory Complete_Lattice
imports Lattice
begin
section \<open>Complete Lattices\<close>
locale weak_complete_lattice = weak_partial_order +
assumes sup_exists:
"[| A \ carrier L |] ==> \s. least L s (Upper L A)"
and inf_exists:
"[| A \ carrier L |] ==> \i. greatest L i (Lower L A)"
sublocale weak_complete_lattice \<subseteq> weak_lattice
proof
fix x y
assume a: "x \ carrier L" "y \ carrier L"
thus "\s. is_lub L s {x, y}"
by (rule_tac sup_exists[of "{x, y}"], auto)
from a show "\s. is_glb L s {x, y}"
by (rule_tac inf_exists[of "{x, y}"], auto)
qed
text \<open>Introduction rule: the usual definition of complete lattice\<close>
lemma (in weak_partial_order) weak_complete_latticeI:
assumes sup_exists:
"!!A. [| A \ carrier L |] ==> \s. least L s (Upper L A)"
and inf_exists:
"!!A. [| A \ carrier L |] ==> \i. greatest L i (Lower L A)"
shows "weak_complete_lattice L"
by standard (auto intro: sup_exists inf_exists)
lemma (in weak_complete_lattice) dual_weak_complete_lattice:
"weak_complete_lattice (inv_gorder L)"
proof -
interpret dual: weak_lattice "inv_gorder L"
by (metis dual_weak_lattice)
show ?thesis
by (unfold_locales) (simp_all add:inf_exists sup_exists)
qed
lemma (in weak_complete_lattice) supI:
"[| !!l. least L l (Upper L A) ==> P l; A \ carrier L |]
==> P (\<Squnion>A)"
proof (unfold sup_def)
assume L: "A \ carrier L"
and P: "!!l. least L l (Upper L A) ==> P l"
with sup_exists obtain s where "least L s (Upper L A)" by blast
with L show "P (SOME l. least L l (Upper L A))"
by (fast intro: someI2 weak_least_unique P)
qed
lemma (in weak_complete_lattice) sup_closed [simp]:
"A \ carrier L ==> \A \ carrier L"
by (rule supI) simp_all
lemma (in weak_complete_lattice) sup_cong:
assumes "A \ carrier L" "B \ carrier L" "A {.=} B"
shows "\ A .= \ B"
proof -
have "\ x. is_lub L x A \ is_lub L x B"
by (rule least_Upper_cong_r, simp_all add: assms)
moreover have "\ B \ carrier L"
by (simp add: assms(2))
ultimately show ?thesis
by (simp add: sup_def)
qed
sublocale weak_complete_lattice \<subseteq> weak_bounded_lattice
apply (unfold_locales)
apply (metis Upper_empty empty_subsetI sup_exists)
apply (metis Lower_empty empty_subsetI inf_exists)
done
lemma (in weak_complete_lattice) infI:
"[| !!i. greatest L i (Lower L A) ==> P i; A \ carrier L |]
==> P (\<Sqinter>A)"
proof (unfold inf_def)
assume L: "A \ carrier L"
and P: "!!l. greatest L l (Lower L A) ==> P l"
with inf_exists obtain s where "greatest L s (Lower L A)" by blast
with L show "P (SOME l. greatest L l (Lower L A))"
by (fast intro: someI2 weak_greatest_unique P)
qed
lemma (in weak_complete_lattice) inf_closed [simp]:
"A \ carrier L ==> \A \ carrier L"
by (rule infI) simp_all
lemma (in weak_complete_lattice) inf_cong:
assumes "A \ carrier L" "B \ carrier L" "A {.=} B"
shows "\ A .= \ B"
proof -
have "\ x. is_glb L x A \ is_glb L x B"
by (rule greatest_Lower_cong_r, simp_all add: assms)
moreover have "\ B \ carrier L"
by (simp add: assms(2))
ultimately show ?thesis
by (simp add: inf_def)
qed
theorem (in weak_partial_order) weak_complete_lattice_criterion1:
assumes top_exists: "\g. greatest L g (carrier L)"
and inf_exists:
"\A. [| A \ carrier L; A \ {} |] ==> \i. greatest L i (Lower L A)"
shows "weak_complete_lattice L"
proof (rule weak_complete_latticeI)
from top_exists obtain top where top: "greatest L top (carrier L)" ..
fix A
assume L: "A \ carrier L"
let ?B = "Upper L A"
from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)
then have B_non_empty: "?B \ {}" by fast
have B_L: "?B \ carrier L" by simp
from inf_exists [OF B_L B_non_empty]
obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
then have bcarr: "b \ carrier L"
by auto
have "least L b (Upper L A)"
proof (rule least_UpperI)
show "\x. x \ A \ x \ b"
by (meson L Lower_memI Upper_memD b_inf_B greatest_le subsetD)
show "\y. y \ Upper L A \ b \ y"
by (meson B_L b_inf_B greatest_Lower_below)
qed (use bcarr L in auto)
then show "\s. least L s (Upper L A)" ..
next
fix A
assume L: "A \ carrier L"
show "\i. greatest L i (Lower L A)"
by (metis L Lower_empty inf_exists top_exists)
qed
text \<open>Supremum\<close>
declare (in partial_order) weak_sup_of_singleton [simp del]
lemma (in partial_order) sup_of_singleton [simp]:
"x \ carrier L ==> \{x} = x"
using weak_sup_of_singleton unfolding eq_is_equal .
lemma (in upper_semilattice) join_assoc_lemma:
assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"
shows "x \ (y \ z) = \{x, y, z}"
using weak_join_assoc_lemma L unfolding eq_is_equal .
lemma (in upper_semilattice) join_assoc:
assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"
shows "(x \ y) \ z = x \ (y \ z)"
using weak_join_assoc L unfolding eq_is_equal .
text \<open>Infimum\<close>
declare (in partial_order) weak_inf_of_singleton [simp del]
lemma (in partial_order) inf_of_singleton [simp]:
"x \ carrier L ==> \{x} = x"
using weak_inf_of_singleton unfolding eq_is_equal .
text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
lemma (in lower_semilattice) meet_assoc_lemma:
assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"
shows "x \ (y \ z) = \{x, y, z}"
using weak_meet_assoc_lemma L unfolding eq_is_equal .
lemma (in lower_semilattice) meet_assoc:
assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"
shows "(x \ y) \ z = x \ (y \ z)"
using weak_meet_assoc L unfolding eq_is_equal .
subsection \<open>Infimum Laws\<close>
context weak_complete_lattice
begin
lemma inf_glb:
assumes "A \ carrier L"
shows "greatest L (\A) (Lower L A)"
proof -
obtain i where "greatest L i (Lower L A)"
by (metis assms inf_exists)
thus ?thesis
by (metis inf_def someI_ex)
qed
lemma inf_lower:
assumes "A \ carrier L" "x \ A"
shows "\A \ x"
by (metis assms greatest_Lower_below inf_glb)
lemma inf_greatest:
assumes "A \ carrier L" "z \ carrier L"
"(\x. x \ A \ z \ x)"
shows "z \ \A"
by (metis Lower_memI assms greatest_le inf_glb)
lemma weak_inf_empty [simp]: "\{} .= \"
by (metis Lower_empty empty_subsetI inf_glb top_greatest weak_greatest_unique)
lemma weak_inf_carrier [simp]: "\carrier L .= \"
by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
lemma weak_inf_insert [simp]:
assumes "a \ carrier L" "A \ carrier L"
shows "\insert a A .= a \ \A"
proof (rule weak_le_antisym)
show "\insert a A \ a \ \A"
by (simp add: assms inf_lower local.inf_greatest meet_le)
show aA: "a \ \A \ carrier L"
using assms by simp
show "a \ \A \ \insert a A"
apply (rule inf_greatest)
using assms apply (simp_all add: aA)
by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)
show "\insert a A \ carrier L"
using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
qed
subsection \<open>Supremum Laws\<close>
lemma sup_lub:
assumes "A \ carrier L"
shows "least L (\A) (Upper L A)"
by (metis Upper_is_closed assms least_closed least_cong supI sup_closed sup_exists weak_least_unique)
lemma sup_upper:
assumes "A \ carrier L" "x \ A"
shows "x \ \A"
by (metis assms least_Upper_above supI)
lemma sup_least:
assumes "A \ carrier L" "z \ carrier L"
"(\x. x \ A \ x \ z)"
shows "\A \ z"
by (metis Upper_memI assms least_le sup_lub)
lemma weak_sup_empty [simp]: "\{} .= \"
by (metis Upper_empty bottom_least empty_subsetI sup_lub weak_least_unique)
lemma weak_sup_carrier [simp]: "\carrier L .= \"
by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
lemma weak_sup_insert [simp]:
assumes "a \ carrier L" "A \ carrier L"
shows "\insert a A .= a \ \A"
proof (rule weak_le_antisym)
show aA: "a \ \A \ carrier L"
using assms by simp
show "\insert a A \ a \ \A"
apply (rule sup_least)
using assms apply (simp_all add: aA)
by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)
show "a \ \A \ \insert a A"
by (simp add: assms join_le local.sup_least sup_upper)
show "\insert a A \ carrier L"
using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
qed
end
subsection \<open>Fixed points of a lattice\<close>
definition "fps L f = {x \ carrier L. f x .=\<^bsub>L\<^esub> x}"
abbreviation "fpl L f \ L\carrier := fps L f\"
lemma (in weak_partial_order)
use_fps: "x \ fps L f \ f x .= x"
by (simp add: fps_def)
lemma fps_carrier [simp]:
"fps L f \ carrier L"
by (auto simp add: fps_def)
lemma (in weak_complete_lattice) fps_sup_image:
assumes "f \ carrier L \ carrier L" "A \ fps L f"
shows "\ (f ` A) .= \ A"
proof -
from assms(2) have AL: "A \ carrier L"
by (auto simp add: fps_def)
show ?thesis
proof (rule sup_cong, simp_all add: AL)
from assms(1) AL show "f ` A \ carrier L"
by auto
then have *: "\b. \A \ {x \ carrier L. f x .= x}; b \ A\ \ \a\f ` A. b .= a"
by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)
from assms(2) show "f ` A {.=} A"
by (auto simp add: fps_def intro: set_eqI2 [OF _ *])
qed
qed
lemma (in weak_complete_lattice) fps_idem:
assumes "f \ carrier L \ carrier L" "Idem f"
shows "fps L f {.=} f ` carrier L"
proof (rule set_eqI2)
show "\a. a \ fps L f \ \b\f ` carrier L. a .= b"
using assms by (force simp add: fps_def intro: local.sym)
show "\b. b \ f ` carrier L \ \a\fps L f. b .= a"
using assms by (force simp add: idempotent_def fps_def)
qed
context weak_complete_lattice
begin
lemma weak_sup_pre_fixed_point:
assumes "f \ carrier L \ carrier L" "isotone L L f" "A \ fps L f"
shows "(\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub> A)"
proof (rule sup_least)
from assms(3) show AL: "A \ carrier L"
by (auto simp add: fps_def)
thus fA: "f (\A) \ carrier L"
by (simp add: assms funcset_carrier[of f L L])
fix x
assume xA: "x \ A"
hence "x \ fps L f"
using assms subsetCE by blast
hence "f x .=\<^bsub>L\<^esub> x"
by (auto simp add: fps_def)
moreover have "f x \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"
by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA)
ultimately show "x \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"
by (meson AL fA assms(1) funcset_carrier le_cong local.refl subsetCE xA)
qed
lemma weak_sup_post_fixed_point:
assumes "f \ carrier L \ carrier L" "isotone L L f" "A \ fps L f"
shows "f (\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub> A)"
proof (rule inf_greatest)
from assms(3) show AL: "A \ carrier L"
by (auto simp add: fps_def)
thus fA: "f (\A) \ carrier L"
by (simp add: assms funcset_carrier[of f L L])
fix x
assume xA: "x \ A"
hence "x \ fps L f"
using assms subsetCE by blast
hence "f x .=\<^bsub>L\<^esub> x"
by (auto simp add: fps_def)
moreover have "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> f x"
by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA)
ultimately show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> x"
by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA)
qed
subsubsection \<open>Least fixed points\<close>
lemma LFP_closed [intro, simp]:
"LFP f \ carrier L"
by (metis (lifting) LEAST_FP_def inf_closed mem_Collect_eq subsetI)
lemma LFP_lowerbound:
assumes "x \ carrier L" "f x \ x"
shows "LFP f \ x"
by (auto intro:inf_lower assms simp add:LEAST_FP_def)
lemma LFP_greatest:
assumes "x \ carrier L"
"(\u. \ u \ carrier L; f u \ u \ \ x \ u)"
shows "x \ LFP f"
by (auto simp add:LEAST_FP_def intro:inf_greatest assms)
lemma LFP_lemma2:
assumes "Mono f" "f \ carrier L \ carrier L"
shows "f (LFP f) \ LFP f"
proof (rule LFP_greatest)
have f: "\x. x \ carrier L \ f x \ carrier L"
using assms by (auto simp add: Pi_def)
with assms show "f (LFP f) \ carrier L"
by blast
show "\u. \u \ carrier L; f u \ u\ \ f (LFP f) \ u"
by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)
qed
lemma LFP_lemma3:
assumes "Mono f" "f \ carrier L \ carrier L"
shows "LFP f \ f (LFP f)"
using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
lemma LFP_weak_unfold:
"\ Mono f; f \ carrier L \ carrier L \ \ LFP f .= f (LFP f)"
by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)
lemma LFP_fixed_point [intro]:
assumes "Mono f" "f \ carrier L \ carrier L"
shows "LFP f \ fps L f"
proof -
have "f (LFP f) \ carrier L"
using assms(2) by blast
with assms show ?thesis
by (simp add: LFP_weak_unfold fps_def local.sym)
qed
lemma LFP_least_fixed_point:
assumes "Mono f" "f \ carrier L \ carrier L" "x \ fps L f"
shows "LFP f \ x"
using assms by (force intro: LFP_lowerbound simp add: fps_def)
lemma LFP_idem:
assumes "f \ carrier L \ carrier L" "Mono f" "Idem f"
shows "LFP f .= (f \)"
proof (rule weak_le_antisym)
from assms(1) show fb: "f \ \ carrier L"
by (rule funcset_mem, simp)
from assms show mf: "LFP f \ carrier L"
by blast
show "LFP f \ f \"
proof -
have "f (f \) .= f \"
by (auto simp add: fps_def fb assms(3) idempotent)
moreover have "f (f \) \ carrier L"
by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
ultimately show ?thesis
by (auto intro: LFP_lowerbound simp add: fb)
qed
show "f \ \ LFP f"
proof -
have "f \ \ f (LFP f)"
by (auto intro: use_iso1[of _ f] simp add: assms)
moreover have "... .= LFP f"
using assms(1) assms(2) fps_def by force
moreover from assms(1) have "f (LFP f) \ carrier L"
by (auto)
ultimately show ?thesis
using fb by blast
qed
qed
subsubsection \<open>Greatest fixed points\<close>
lemma GFP_closed [intro, simp]:
"GFP f \ carrier L"
by (auto intro:sup_closed simp add:GREATEST_FP_def)
lemma GFP_upperbound:
assumes "x \ carrier L" "x \ f x"
shows "x \ GFP f"
by (auto intro:sup_upper assms simp add:GREATEST_FP_def)
lemma GFP_least:
assumes "x \ carrier L"
"(\u. \ u \ carrier L; u \ f u \ \ u \ x)"
shows "GFP f \ x"
by (auto simp add:GREATEST_FP_def intro:sup_least assms)
lemma GFP_lemma2:
assumes "Mono f" "f \ carrier L \ carrier L"
shows "GFP f \ f (GFP f)"
proof (rule GFP_least)
have f: "\x. x \ carrier L \ f x \ carrier L"
using assms by (auto simp add: Pi_def)
with assms show "f (GFP f) \ carrier L"
by blast
show "\u. \u \ carrier L; u \ f u\ \ u \ f (GFP f)"
by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)
qed
lemma GFP_lemma3:
assumes "Mono f" "f \ carrier L \ carrier L"
shows "f (GFP f) \ GFP f"
by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)
lemma GFP_weak_unfold:
"\ Mono f; f \ carrier L \ carrier L \ \ GFP f .= f (GFP f)"
by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)
lemma (in weak_complete_lattice) GFP_fixed_point [intro]:
assumes "Mono f" "f \ carrier L \ carrier L"
shows "GFP f \ fps L f"
using assms
proof -
have "f (GFP f) \ carrier L"
using assms(2) by blast
with assms show ?thesis
by (simp add: GFP_weak_unfold fps_def local.sym)
qed
lemma GFP_greatest_fixed_point:
assumes "Mono f" "f \ carrier L \ carrier L" "x \ fps L f"
shows "x \ GFP f"
using assms
by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)
lemma GFP_idem:
assumes "f \ carrier L \ carrier L" "Mono f" "Idem f"
shows "GFP f .= (f \)"
proof (rule weak_le_antisym)
from assms(1) show fb: "f \ \ carrier L"
by (rule funcset_mem, simp)
from assms show mf: "GFP f \ carrier L"
by blast
show "f \ \ GFP f"
proof -
have "f (f \) .= f \"
by (auto simp add: fps_def fb assms(3) idempotent)
moreover have "f (f \) \ carrier L"
by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
ultimately show ?thesis
by (rule_tac GFP_upperbound, simp_all add: fb local.sym)
qed
show "GFP f \ f \"
proof -
have "GFP f \ f (GFP f)"
by (simp add: GFP_lemma2 assms(1) assms(2))
moreover have "... \ f \"
by (auto intro: use_iso1[of _ f] simp add: assms)
moreover from assms(1) have "f (GFP f) \ carrier L"
by (auto)
ultimately show ?thesis
using fb local.le_trans by blast
qed
qed
end
subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close>
locale complete_lattice = partial_order +
assumes sup_exists:
"[| A \ carrier L |] ==> \s. least L s (Upper L A)"
and inf_exists:
"[| A \ carrier L |] ==> \i. greatest L i (Lower L A)"
sublocale complete_lattice \<subseteq> lattice
proof
fix x y
assume a: "x \ carrier L" "y \ carrier L"
thus "\s. is_lub L s {x, y}"
by (rule_tac sup_exists[of "{x, y}"], auto)
from a show "\s. is_glb L s {x, y}"
by (rule_tac inf_exists[of "{x, y}"], auto)
qed
sublocale complete_lattice \<subseteq> weak?: weak_complete_lattice
by standard (auto intro: sup_exists inf_exists)
lemma complete_lattice_lattice [simp]:
assumes "complete_lattice X"
shows "lattice X"
proof -
interpret c: complete_lattice X
by (simp add: assms)
show ?thesis
by (unfold_locales)
qed
text \<open>Introduction rule: the usual definition of complete lattice\<close>
lemma (in partial_order) complete_latticeI:
assumes sup_exists:
"!!A. [| A \ carrier L |] ==> \s. least L s (Upper L A)"
and inf_exists:
"!!A. [| A \ carrier L |] ==> \i. greatest L i (Lower L A)"
shows "complete_lattice L"
by standard (auto intro: sup_exists inf_exists)
theorem (in partial_order) complete_lattice_criterion1:
assumes top_exists: "\g. greatest L g (carrier L)"
and inf_exists:
"!!A. [| A \ carrier L; A \ {} |] ==> \i. greatest L i (Lower L A)"
shows "complete_lattice L"
proof (rule complete_latticeI)
from top_exists obtain top where top: "greatest L top (carrier L)" ..
fix A
assume L: "A \ carrier L"
let ?B = "Upper L A"
from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)
then have B_non_empty: "?B \ {}" by fast
have B_L: "?B \ carrier L" by simp
from inf_exists [OF B_L B_non_empty]
obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
then have bcarr: "b \ carrier L"
by blast
have "least L b (Upper L A)"
proof (rule least_UpperI)
show "\x. x \ A \ x \ b"
by (meson L Lower_memI Upper_memD b_inf_B greatest_le rev_subsetD)
show "\y. y \ Upper L A \ b \ y"
by (auto elim: greatest_Lower_below [OF b_inf_B])
qed (use L bcarr in auto)
then show "\s. least L s (Upper L A)" ..
next
fix A
assume L: "A \ carrier L"
show "\i. greatest L i (Lower L A)"
proof (cases "A = {}")
case True then show ?thesis
by (simp add: top_exists)
next
case False with L show ?thesis
by (rule inf_exists)
qed
qed
(* TODO: prove dual version *)
subsection \<open>Fixed points\<close>
context complete_lattice
begin
lemma LFP_unfold:
"\ Mono f; f \ carrier L \ carrier L \ \ LFP f = f (LFP f)"
using eq_is_equal weak.LFP_weak_unfold by auto
lemma LFP_const:
"t \ carrier L \ LFP (\ x. t) = t"
by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)
lemma LFP_id:
"LFP id = \"
by (simp add: local.le_antisym weak.LFP_lowerbound)
lemma GFP_unfold:
"\ Mono f; f \ carrier L \ carrier L \ \ GFP f = f (GFP f)"
using eq_is_equal weak.GFP_weak_unfold by auto
lemma GFP_const:
"t \ carrier L \ GFP (\ x. t) = t"
by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)
lemma GFP_id:
"GFP id = \"
using weak.GFP_upperbound by auto
end
subsection \<open>Interval complete lattices\<close>
context weak_complete_lattice
begin
lemma at_least_at_most_Sup: "\ a \ carrier L; b \ carrier L; a \ b \ \ \ \a..b\ .= b"
by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)
lemma at_least_at_most_Inf: "\ a \ carrier L; b \ carrier L; a \ b \ \ \ \a..b\ .= a"
by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)
end
lemma weak_complete_lattice_interval:
assumes "weak_complete_lattice L" "a \ carrier L" "b \ carrier L" "a \\<^bsub>L\<^esub> b"
shows "weak_complete_lattice (L \ carrier := \a..b\\<^bsub>L\<^esub> \)"
proof -
interpret L: weak_complete_lattice L
by (simp add: assms)
interpret weak_partial_order "L \ carrier := \a..b\\<^bsub>L\<^esub> \"
proof -
have "\a..b\\<^bsub>L\<^esub> \ carrier L"
by (auto simp add: at_least_at_most_def)
thus "weak_partial_order (L\carrier := \a..b\\<^bsub>L\<^esub>\)"
by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
qed
show ?thesis
proof
fix A
assume a: "A \ carrier (L\carrier := \a..b\\<^bsub>L\<^esub>\)"
show "\s. is_lub (L\carrier := \a..b\\<^bsub>L\<^esub>\) s A"
proof (cases "A = {}")
case True
thus ?thesis
by (rule_tac x="a" in exI, auto simp add: least_def assms)
next
case False
show ?thesis
proof (intro exI least_UpperI, simp_all)
show b:"\ x. x \ A \ x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
show "\y. y \ Upper (L\carrier := \a..b\\<^bsub>L\<^esub>\) A \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> y"
using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
from a show *: "A \ \a..b\\<^bsub>L\<^esub>"
by auto
show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>"
proof (rule_tac L.at_least_at_most_member)
show 1: "\\<^bsub>L\<^esub>A \ carrier L"
by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
show "a \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) subsetD subset_trans)
show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> b"
proof (rule L.sup_least)
show "A \ carrier L" "\x. x \ A \ x \\<^bsub>L\<^esub> b"
using * L.at_least_at_most_closed by blast+
qed (simp add: assms)
qed
qed
qed
show "\s. is_glb (L\carrier := \a..b\\<^bsub>L\<^esub>\) s A"
proof (cases "A = {}")
case True
thus ?thesis
by (rule_tac x="b" in exI, auto simp add: greatest_def assms)
next
case False
show ?thesis
proof (rule_tac x="\\<^bsub>L\<^esub> A" in exI, rule greatest_LowerI, simp_all)
show b:"\x. x \ A \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> x"
using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
show "\y. y \ Lower (L\carrier := \a..b\\<^bsub>L\<^esub>\) A \ y \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
from a show *: "A \ \a..b\\<^bsub>L\<^esub>"
by auto
show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>"
proof (rule_tac L.at_least_at_most_member)
show 1: "\\<^bsub>L\<^esub>A \ carrier L"
by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans)
show "a \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> b"
by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) subsetD subset_trans)
qed
qed
qed
qed
qed
subsection \<open>Knaster-Tarski theorem and variants\<close>
text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
theorem Knaster_Tarski:
assumes "weak_complete_lattice L" and f: "f \ carrier L \ carrier L" and "isotone L L f"
shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
proof -
interpret L: weak_complete_lattice L
by (simp add: assms)
interpret weak_partial_order ?L'
proof -
have "{x \ carrier L. f x .=\<^bsub>L\<^esub> x} \ carrier L"
by (auto)
thus "weak_partial_order ?L'"
by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
qed
show ?thesis
proof (unfold_locales, simp_all)
fix A
assume A: "A \ fps L f"
show "\s. is_lub (fpl L f) s A"
proof
from A have AL: "A \ carrier L"
by (meson fps_carrier subset_eq)
let ?w = "\\<^bsub>L\<^esub> A"
have w: "f (\\<^bsub>L\<^esub>A) \ carrier L"
by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2))
have pf_w: "(\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub> A)"
by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3))
have f_top_chain: "f ` \?w..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \ \?w..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>"
proof (auto simp add: at_least_at_most_def)
fix x
assume b: "x \ carrier L" "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> x"
from b show fx: "f x \ carrier L"
using assms(2) by blast
show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> f x"
proof -
have "?w \\<^bsub>L\<^esub> f ?w"
proof (rule_tac L.sup_least, simp_all add: AL w)
fix y
assume c: "y \ A"
hence y: "y \ fps L f"
using A subsetCE by blast
with assms have "y .=\<^bsub>L\<^esub> f y"
proof -
from y have "y \ carrier L"
by (simp add: fps_def)
moreover hence "f y \ carrier L"
by (rule_tac funcset_mem[of f "carrier L"], simp_all add: assms)
ultimately show ?thesis using y
by (rule_tac L.sym, simp_all add: L.use_fps)
qed
moreover have "y \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
by (simp add: AL L.sup_upper c(1))
ultimately show "y \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"
by (meson fps_def AL funcset_mem L.refl L.weak_complete_lattice_axioms assms(2) assms(3) c(1) isotone_def rev_subsetD weak_complete_lattice.sup_closed weak_partial_order.le_cong)
qed
thus ?thesis
by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) b(1) b(2) use_iso2)
qed
show "f x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>"
by (simp add: fx)
qed
let ?L' = "L\ carrier := \?w..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \"
interpret L': weak_complete_lattice ?L'
by (auto intro: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
let ?L'' = "L\ carrier := fps L f \"
show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
proof (rule least_UpperI, simp_all)
fix x
assume x: "x \ Upper ?L'' A"
have "LFP\<^bsub>?L'\<^esub> f \\<^bsub>?L'\<^esub> x"
proof (rule L'.LFP_lowerbound, simp_all)
show "x \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>"
using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least rev_subsetD)
with x show "f x \\<^bsub>L\<^esub> x"
by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
qed
thus " LFP\<^bsub>?L'\<^esub> f \\<^bsub>L\<^esub> x"
by (simp)
next
fix x
assume xA: "x \ A"
show "x \\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
proof -
have "LFP\<^bsub>?L'\<^esub> f \ carrier ?L'"
by blast
thus ?thesis
by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed L.sup_upper xA subsetCE)
qed
next
show "A \ fps L f"
by (simp add: A)
next
show "LFP\<^bsub>?L'\<^esub> f \ fps L f"
proof (auto simp add: fps_def)
have "LFP\<^bsub>?L'\<^esub> f \ carrier ?L'"
by (rule L'.LFP_closed)
thus c:"LFP\<^bsub>?L'\<^esub> f \ carrier L"
by (auto simp add: at_least_at_most_def)
have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
proof (rule "L'.LFP_weak_unfold", simp_all)
have "\x. \x \ carrier L; \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> x\ \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> f x"
by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
with f show "f \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>"
by (auto simp add: Pi_def at_least_at_most_def)
show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>\\<^esub> f"
using L'.weak_partial_order_axioms assms(3)
by (auto simp add: isotone_def) (meson L.at_least_at_most_closed subsetCE)
qed
thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)
qed
qed
qed
show "\i. is_glb (L\carrier := fps L f\) i A"
proof
from A have AL: "A \ carrier L"
by (meson fps_carrier subset_eq)
let ?w = "\\<^bsub>L\<^esub> A"
have w: "f (\\<^bsub>L\<^esub>A) \ carrier L"
by (simp add: AL funcset_carrier' assms(2))
have pf_w: "f (\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub> A)"
by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3))
have f_bot_chain: "f ` \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>"
proof (auto simp add: at_least_at_most_def)
fix x
assume b: "x \ carrier L" "x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
from b show fx: "f x \ carrier L"
using assms(2) by blast
show "f x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
proof -
have "f ?w \\<^bsub>L\<^esub> ?w"
proof (rule_tac L.inf_greatest, simp_all add: AL w)
fix y
assume c: "y \ A"
with assms have "y .=\<^bsub>L\<^esub> f y"
by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq)
moreover have "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> y"
by (simp add: AL L.inf_lower c)
ultimately show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> y"
by (meson AL L.inf_closed L.le_trans c pf_w rev_subsetD w)
qed
thus ?thesis
by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
qed
show "\\<^bsub>L\<^esub> \\<^bsub>L\<^esub> f x"
by (simp add: fx)
qed
let ?L' = "L\ carrier := \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \"
interpret L': weak_complete_lattice ?L'
by (auto intro!: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
let ?L'' = "L\ carrier := fps L f \"
show "is_glb ?L'' (GFP\<^bsub>?L'\<^esub> f) A"
proof (rule greatest_LowerI, simp_all)
fix x
assume "x \ Lower ?L'' A"
then have x: "\y. y \ A \ y \ fps L f \ x \\<^bsub>L\<^esub> y" "x \ fps L f"
by (auto simp add: Lower_def)
have "x \\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
unfolding Lower_def
proof (rule_tac L'.GFP_upperbound; simp)
show "x \ \\\<^bsub>L\<^esub>..\\<^bsub>L\<^esub>A\\<^bsub>L\<^esub>"
by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier)
show "x \\<^bsub>L\<^esub> f x"
using x by (simp add: funcset_carrier' L.sym assms(2) fps_def)
qed
thus "x \\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
by (simp)
next
fix x
assume xA: "x \ A"
show "GFP\<^bsub>?L'\<^esub> f \\<^bsub>L\<^esub> x"
proof -
have "GFP\<^bsub>?L'\<^esub> f \ carrier ?L'"
by blast
thus ?thesis
by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.inf_lower L.le_trans subsetCE xA)
qed
next
show "A \ fps L f"
by (simp add: A)
next
show "GFP\<^bsub>?L'\<^esub> f \ fps L f"
proof (auto simp add: fps_def)
have "GFP\<^bsub>?L'\<^esub> f \ carrier ?L'"
by (rule L'.GFP_closed)
thus c:"GFP\<^bsub>?L'\<^esub> f \ carrier L"
by (auto simp add: at_least_at_most_def)
have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
proof (rule "L'.GFP_weak_unfold", simp_all)
have "\x. \x \ carrier L; x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A\ \ f x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"
by (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
with assms(2) show "f \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>"
by (auto simp add: Pi_def at_least_at_most_def)
have "\x y. \x \ \\\<^bsub>L\<^esub>..\\<^bsub>L\<^esub>A\\<^bsub>L\<^esub>; y \ \\\<^bsub>L\<^esub>..\\<^bsub>L\<^esub>A\\<^bsub>L\<^esub>; x \\<^bsub>L\<^esub> y\ \ f x \\<^bsub>L\<^esub> f y"
by (meson L.at_least_at_most_closed subsetD use_iso1 assms(3))
with L'.weak_partial_order_axioms show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>\\<^esub> f"
by (auto simp add: isotone_def)
qed
thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)
qed
qed
qed
qed
qed
theorem Knaster_Tarski_top:
assumes "weak_complete_lattice L" "isotone L L f" "f \ carrier L \ carrier L"
shows "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"
proof -
interpret L: weak_complete_lattice L
by (simp add: assms)
interpret L': weak_complete_lattice "fpl L f"
by (rule Knaster_Tarski, simp_all add: assms)
show ?thesis
proof (rule L.weak_le_antisym, simp_all)
show "\\<^bsub>fpl L f\<^esub> \\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"
by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])
show "GFP\<^bsub>L\<^esub> f \\<^bsub>L\<^esub> \\<^bsub>fpl L f\<^esub>"
proof -
have "GFP\<^bsub>L\<^esub> f \ fps L f"
by (rule L.GFP_fixed_point, simp_all add: assms)
hence "GFP\<^bsub>L\<^esub> f \ carrier (fpl L f)"
by simp
hence "GFP\<^bsub>L\<^esub> f \\<^bsub>fpl L f\<^esub> \\<^bsub>fpl L f\<^esub>"
by (rule L'.top_higher)
thus ?thesis
by simp
qed
show "\\<^bsub>fpl L f\<^esub> \ carrier L"
proof -
have "carrier (fpl L f) \ carrier L"
by (auto simp add: fps_def)
with L'.top_closed show ?thesis
by blast
qed
qed
qed
theorem Knaster_Tarski_bottom:
assumes "weak_complete_lattice L" "isotone L L f" "f \ carrier L \ carrier L"
shows "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"
proof -
interpret L: weak_complete_lattice L
by (simp add: assms)
interpret L': weak_complete_lattice "fpl L f"
by (rule Knaster_Tarski, simp_all add: assms)
show ?thesis
proof (rule L.weak_le_antisym, simp_all)
show "LFP\<^bsub>L\<^esub> f \\<^bsub>L\<^esub> \\<^bsub>fpl L f\<^esub>"
by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])
show "\\<^bsub>fpl L f\<^esub> \\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"
proof -
have "LFP\<^bsub>L\<^esub> f \ fps L f"
by (rule L.LFP_fixed_point, simp_all add: assms)
hence "LFP\<^bsub>L\<^esub> f \ carrier (fpl L f)"
by simp
hence "\\<^bsub>fpl L f\<^esub> \\<^bsub>fpl L f\<^esub> LFP\<^bsub>L\<^esub> f"
by (rule L'.bottom_lower)
thus ?thesis
by simp
qed
show "\\<^bsub>fpl L f\<^esub> \ carrier L"
proof -
have "carrier (fpl L f) \ carrier L"
by (auto simp add: fps_def)
with L'.bottom_closed show ?thesis
by blast
qed
qed
qed
text \<open>If a function is both idempotent and isotone then the image of the function forms a complete lattice\<close>
theorem Knaster_Tarski_idem:
assumes "complete_lattice L" "f \ carrier L \ carrier L" "isotone L L f" "idempotent L f"
shows "complete_lattice (L\carrier := f ` carrier L\)"
proof -
interpret L: complete_lattice L
by (simp add: assms)
have "fps L f = f ` carrier L"
using L.weak.fps_idem[OF assms(2) assms(4)]
by (simp add: L.set_eq_is_eq)
then interpret L': weak_complete_lattice "(L\carrier := f ` carrier L\)"
by (metis Knaster_Tarski L.weak.weak_complete_lattice_axioms assms(2) assms(3))
show ?thesis
using L'.sup_exists L'.inf_exists
by (unfold_locales, auto simp add: L.eq_is_equal)
qed
theorem Knaster_Tarski_idem_extremes:
assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \ carrier L \ carrier L"
shows "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)" "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)"
proof -
interpret L: weak_complete_lattice "L"
by (simp_all add: assms)
interpret L': weak_complete_lattice "fpl L f"
by (rule Knaster_Tarski, simp_all add: assms)
have FA: "fps L f \ carrier L"
by (auto simp add: fps_def)
show "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)"
proof -
from FA have "\\<^bsub>fpl L f\<^esub> \ carrier L"
proof -
have "\\<^bsub>fpl L f\<^esub> \ fps L f"
using L'.top_closed by auto
thus ?thesis
using FA by blast
qed
moreover with assms have "f \\<^bsub>L\<^esub> \ carrier L"
by (auto)
ultimately show ?thesis
using L.trans[OF Knaster_Tarski_top[of L f] L.GFP_idem[of f]]
by (simp_all add: assms)
qed
show "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)"
proof -
from FA have "\\<^bsub>fpl L f\<^esub> \ carrier L"
proof -
have "\\<^bsub>fpl L f\<^esub> \ fps L f"
using L'.bottom_closed by auto
thus ?thesis
using FA by blast
qed
moreover with assms have "f \\<^bsub>L\<^esub> \ carrier L"
by (auto)
ultimately show ?thesis
using L.trans[OF Knaster_Tarski_bottom[of L f] L.LFP_idem[of f]]
by (simp_all add: assms)
qed
qed
theorem Knaster_Tarski_idem_inf_eq:
assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \ carrier L \ carrier L"
"A \ fps L f"
shows "\\<^bsub>fpl L f\<^esub> A .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub> A)"
proof -
interpret L: weak_complete_lattice "L"
by (simp_all add: assms)
interpret L': weak_complete_lattice "fpl L f"
by (rule Knaster_Tarski, simp_all add: assms)
have FA: "fps L f \ carrier L"
by (auto simp add: fps_def)
have A: "A \ carrier L"
using FA assms(5) by blast
have fA: "f (\\<^bsub>L\<^esub>A) \ fps L f"
by (metis (no_types, lifting) A L.idempotent L.inf_closed PiE assms(3) assms(4) fps_def mem_Collect_eq)
have infA: "\\<^bsub>fpl L f\<^esub>A \ fps L f"
by (rule L'.inf_closed[simplified], simp add: assms)
show ?thesis
proof (rule L.weak_le_antisym)
show ic: "\\<^bsub>fpl L f\<^esub>A \ carrier L"
using FA infA by blast
show fc: "f (\\<^bsub>L\<^esub>A) \ carrier L"
using FA fA by blast
show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> \\<^bsub>fpl L f\<^esub>A"
proof -
have "\x. x \ A \ f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> x"
by (meson A FA L.inf_closed L.inf_lower L.le_trans L.weak_sup_post_fixed_point assms(2) assms(4) assms(5) fA subsetCE)
hence "f (\\<^bsub>L\<^esub>A) \\<^bsub>fpl L f\<^esub> \\<^bsub>fpl L f\<^esub>A"
by (rule_tac L'.inf_greatest, simp_all add: fA assms(3,5))
thus ?thesis
by (simp)
qed
show "\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"
proof -
have *: "\\<^bsub>fpl L f\<^esub>A \ carrier L"
using FA infA by blast
have "\x. x \ A \ \\<^bsub>fpl L f\<^esub>A \\<^bsub>fpl L f\<^esub> x"
by (rule L'.inf_lower, simp_all add: assms)
hence "\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub>A)"
by (rule_tac L.inf_greatest, simp_all add: A *)
hence 1:"f(\\<^bsub>fpl L f\<^esub>A) \\<^bsub>L\<^esub> f(\\<^bsub>L\<^esub>A)"
by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)
have 2:"\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> f (\\<^bsub>fpl L f\<^esub>A)"
by (metis (no_types, lifting) FA L.sym L.use_fps L.weak_complete_lattice_axioms PiE assms(4) infA subsetCE weak_complete_lattice_def weak_partial_order.weak_refl)
show ?thesis
using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)
qed
qed
qed
subsection \<open>Examples\<close>
subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
theorem powerset_is_complete_lattice:
"complete_lattice \carrier = Pow A, eq = (=), le = (\)\"
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"
by standard auto
next
fix B
assume "B \ carrier ?L"
then have "least ?L (\ B) (Upper ?L B)"
by (fastforce intro!: least_UpperI simp: Upper_def)
then show "\s. least ?L s (Upper ?L B)" ..
next
fix B
assume "B \ carrier ?L"
then have "greatest ?L (\ B \ A) (Lower ?L B)"
txt \<open>\<^term>\<open>\<Inter> B\<close> is not the infimum of \<^term>\<open>B\<close>:
\<^term>\<open>\<Inter> {} = UNIV\<close> which is in general bigger than \<^term>\<open>A\<close>! \<close>
by (fastforce intro!: greatest_LowerI simp: Lower_def)
then show "\i. greatest ?L i (Lower ?L B)" ..
qed
text \<open>Another example, that of the lattice of subgroups of a group,
can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
subsection \<open>Limit preserving functions\<close>
definition weak_sup_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where
"weak_sup_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. A \ {} \ f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f ` A)))"
definition sup_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where
"sup_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f ` A)))"
definition weak_inf_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where
"weak_inf_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. A \ {} \ f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f ` A)))"
definition inf_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where
"inf_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f ` A)))"
lemma weak_sup_pres:
"sup_pres X Y f \ weak_sup_pres X Y f"
by (simp add: sup_pres_def weak_sup_pres_def)
lemma weak_inf_pres:
"inf_pres X Y f \ weak_inf_pres X Y f"
by (simp add: inf_pres_def weak_inf_pres_def)
lemma sup_pres_is_join_pres:
assumes "weak_sup_pres X Y f"
shows "join_pres X Y f"
using assms by (auto simp: join_pres_def weak_sup_pres_def join_def)
lemma inf_pres_is_meet_pres:
assumes "weak_inf_pres X Y f"
shows "meet_pres X Y f"
using assms by (auto simp: meet_pres_def weak_inf_pres_def meet_def)
end
¤ Dauer der Verarbeitung: 0.50 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
