(* 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 ‹Complete Lattices› 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 ⊆ 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 ‹Introduction rule: the usual definition of complete lattice› 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 (⨆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 ⊆ 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 (⨅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 set_mp) 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 ‹Supremum› 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 ‹Infimum› 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 ‹Condition on ‹A›: infimum exists.› 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 ‹Infimum Laws› 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 ‹Supremum Laws› 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 ‹Fixed points of a lattice› definition "fps L f = {x ∈ carrier L. f x .=⇘_{L⇙}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 "(⨆⇘_{L⇙}A) ⊑⇘_{L⇙}f (⨆⇘_{L⇙}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 .=⇘_{L⇙}x" by (auto simp add: fps_def) moreover have "f x ⊑⇘_{L⇙}f (⨆⇘_{L⇙}A)" by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA) ultimately show "x ⊑⇘_{L⇙}f (⨆⇘_{L⇙}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 (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}(⨅⇘_{L⇙}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 .=⇘_{L⇙}x" by (auto simp add: fps_def) moreover have "f (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}f x" by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA) ultimately show "f (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}x" by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA) qed subsubsection ‹Least fixed points› 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 ‹Greatest fixed points› 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 ‹Complete lattices where ‹eq› is the Equality› 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 ⊆ 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 ⊆ 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 ‹Introduction rule: the usual definition of complete lattice› 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 set_rev_mp) 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 ‹Fixed points› 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 ‹Interval complete lattices› 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 ⊑⇘_{L⇙}b" shows "weak_complete_lattice (L ⦇ carrier := ⦃a..b⦄⇘_{L⇙}⦈)" proof - interpret L: weak_complete_lattice L by (simp add: assms) interpret weak_partial_order "L ⦇ carrier := ⦃a..b⦄⇘_{L⇙}⦈" proof - have "⦃a..b⦄⇘_{L⇙}⊆ carrier L" by (auto simp add: at_least_at_most_def) thus "weak_partial_order (L⦇carrier := ⦃a..b⦄⇘_{L⇙}⦈)" 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⦄⇘_{L⇙}⦈)" show "∃s. is_lub (L⦇carrier := ⦃a..b⦄⇘_{L⇙}⦈) 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 (rule_tac x="⨆⇘_{L⇙}A" in exI, rule least_UpperI, simp_all) show b:"⋀ x. x ∈ A ⟹ x ⊑⇘_{L⇙}⨆⇘_{L⇙}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⦄⇘_{L⇙}⦈) A ⟹ ⨆⇘_{L⇙}A ⊑⇘_{L⇙}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⦄⇘_{L⇙}" by (auto) from a show "⨆⇘_{L⇙}A ∈ ⦃a..b⦄⇘_{L⇙}" apply (rule_tac L.at_least_at_most_member) apply (auto) apply (meson L.at_least_at_most_closed L.sup_closed subset_trans) apply (meson False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed b all_not_in_conv assms(2) contra_subsetD subset_trans) apply (rule L.sup_least) apply (auto simp add: assms) using L.at_least_at_most_closed apply blast done qed qed show "∃s. is_glb (L⦇carrier := ⦃a..b⦄⇘_{L⇙}⦈) 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="⨅⇘_{L⇙}A" in exI, rule greatest_LowerI, simp_all) show b:"⋀x. x ∈ A ⟹ ⨅⇘_{L⇙}A ⊑⇘_{L⇙}x" using a L.at_least_at_most_closed by (force intro!: L.inf_lower) show "⋀y. y ∈ Lower (L⦇carrier := ⦃a..b⦄⇘_{L⇙}⦈) A ⟹ y ⊑⇘_{L⇙}⨅⇘_{L⇙}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⦄⇘_{L⇙}" by (auto) from a show "⨅⇘_{L⇙}A ∈ ⦃a..b⦄⇘_{L⇙}" apply (rule_tac L.at_least_at_most_member) apply (auto) apply (meson L.at_least_at_most_closed L.inf_closed subset_trans) apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans) apply (meson False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.le_trans b all_not_in_conv assms(3) contra_subsetD subset_trans) done qed qed qed qed subsection ‹Knaster-Tarski theorem and variants› text ‹The set of fixed points of a complete lattice is itself a complete lattice› theorem Knaster_Tarski: assumes "weak_complete_lattice L" "f ∈ carrier L → carrier L" "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 .=⇘_{L⇙}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 = "⨆⇘_{L⇙}A" have w: "f (⨆⇘_{L⇙}A) ∈ carrier L" by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2)) have pf_w: "(⨆⇘_{L⇙}A) ⊑⇘_{L⇙}f (⨆⇘_{L⇙}A)" by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3)) have f_top_chain: "f ` ⦃?w..⊤⇘_{L⇙}⦄⇘_{L⇙}⊆ ⦃?w..⊤⇘_{L⇙}⦄⇘_{L⇙}" proof (auto simp add: at_least_at_most_def) fix x assume b: "x ∈ carrier L" "⨆⇘_{L⇙}A ⊑⇘_{L⇙}x" from b show fx: "f x ∈ carrier L" using assms(2) by blast show "⨆⇘_{L⇙}A ⊑⇘_{L⇙}f x" proof - have "?w ⊑⇘_{L⇙}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 .=⇘_{L⇙}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 ⊑⇘_{L⇙}⨆⇘_{L⇙}A" by (simp add: AL L.sup_upper c(1)) ultimately show "y ⊑⇘_{L⇙}f (⨆⇘_{L⇙}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 ⊑⇘_{L⇙}⊤⇘_{L⇙}" by (simp add: fx) qed let ?L' = "L⦇ carrier := ⦃?w..⊤⇘_{L⇙}⦄⇘_{L⇙}⦈" 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⇘_{?L'⇙}f) A" proof (rule least_UpperI, simp_all) fix x assume "x ∈ Upper ?L'' A" hence "LFP⇘_{?L'⇙}f ⊑⇘_{?L'⇙}x" apply (rule_tac L'.LFP_lowerbound) apply (auto simp add: Upper_def) apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp) apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl) apply (auto) apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2)) done thus " LFP⇘_{?L'⇙}f ⊑⇘_{L⇙}x" by (simp) next fix x assume xA: "x ∈ A" show "x ⊑⇘_{L⇙}LFP⇘_{?L'⇙}f" proof - have "LFP⇘_{?L'⇙}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⇘_{?L'⇙}f ∈ fps L f" proof (auto simp add: fps_def) have "LFP⇘_{?L'⇙}f ∈ carrier ?L'" by (rule L'.LFP_closed) thus c:"LFP⇘_{?L'⇙}f ∈ carrier L" by (auto simp add: at_least_at_most_def) have "LFP⇘_{?L'⇙}f .=⇘_{?L'⇙}f (LFP⇘_{?L'⇙}f)" proof (rule "L'.LFP_weak_unfold", simp_all) show "f ∈ ⦃⨆⇘_{L⇙}A..⊤⇘_{L⇙}⦄⇘_{L⇙}→ ⦃⨆⇘_{L⇙}A..⊤⇘_{L⇙}⦄⇘_{L⇙}" apply (auto simp add: Pi_def at_least_at_most_def) using assms(2) apply blast apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2) using assms(2) apply blast done from assms(3) show "Mono⇘_{L⦇carrier := ⦃⨆⇘L⇙A..⊤⇘L⇙⦄⇘L⇙⦈⇙}f" apply (auto simp add: isotone_def) using L'.weak_partial_order_axioms apply blast apply (meson L.at_least_at_most_closed subsetCE) done qed thus "f (LFP⇘_{?L'⇙}f) .=⇘_{L⇙}LFP⇘_{?L'⇙}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 = "⨅⇘_{L⇙}A" have w: "f (⨅⇘_{L⇙}A) ∈ carrier L" by (simp add: AL funcset_carrier' assms(2)) have pf_w: "f (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}(⨅⇘_{L⇙}A)" by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3)) have f_bot_chain: "f ` ⦃⊥⇘_{L⇙}..?w⦄⇘_{L⇙}⊆ ⦃⊥⇘_{L⇙}..?w⦄⇘_{L⇙}" proof (auto simp add: at_least_at_most_def) fix x assume b: "x ∈ carrier L" "x ⊑⇘_{L⇙}⨅⇘_{L⇙}A" from b show fx: "f x ∈ carrier L" using assms(2) by blast show "f x ⊑⇘_{L⇙}⨅⇘_{L⇙}A" proof - have "f ?w ⊑⇘_{L⇙}?w" proof (rule_tac L.inf_greatest, simp_all add: AL w) fix y assume c: "y ∈ A" with assms have "y .=⇘_{L⇙}f y" by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq) moreover have "⨅⇘_{L⇙}A ⊑⇘_{L⇙}y" by (simp add: AL L.inf_lower c) ultimately show "f (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}y" by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp 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 "⊥⇘_{L⇙}⊑⇘_{L⇙}f x" by (simp add: fx) qed let ?L' = "L⦇ carrier := ⦃⊥⇘_{L⇙}..?w⦄⇘_{L⇙}⦈" 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⇘_{?L'⇙}f) A" proof (rule greatest_LowerI, simp_all) fix x assume "x ∈ Lower ?L'' A" hence "x ⊑⇘_{?L'⇙}GFP⇘_{?L'⇙}f" apply (rule_tac L'.GFP_upperbound) apply (auto simp add: Lower_def) apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest) apply (simp add: funcset_carrier' L.sym assms(2) fps_def) done thus "x ⊑⇘_{L⇙}GFP⇘_{?L'⇙}f" by (simp) next fix x assume xA: "x ∈ A" show "GFP⇘_{?L'⇙}f ⊑⇘_{L⇙}x" proof - have "GFP⇘_{?L'⇙}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⇘_{?L'⇙}f ∈ fps L f" proof (auto simp add: fps_def) have "GFP⇘_{?L'⇙}f ∈ carrier ?L'" by (rule L'.GFP_closed) thus c:"GFP⇘_{?L'⇙}f ∈ carrier L" by (auto simp add: at_least_at_most_def) have "GFP⇘_{?L'⇙}f .=⇘_{?L'⇙}f (GFP⇘_{?L'⇙}f)" proof (rule "L'.GFP_weak_unfold", simp_all) show "f ∈ ⦃⊥⇘_{L⇙}..?w⦄⇘_{L⇙}→ ⦃⊥⇘_{L⇙}..?w⦄⇘_{L⇙}" apply (auto simp add: Pi_def at_least_at_most_def) using assms(2) apply blast apply (simp add: funcset_carrier' assms(2)) apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2) done from assms(3) show "Mono⇘_{L⦇carrier := ⦃⊥⇘L⇙..?w⦄⇘L⇙⦈⇙}f" apply (auto simp add: isotone_def) using L'.weak_partial_order_axioms apply blast using L.at_least_at_most_closed apply (blast intro: funcset_carrier') done qed thus "f (GFP⇘_{?L'⇙}f) .=⇘_{L⇙}GFP⇘_{?L'⇙}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 "⊤⇘_{fpl L f⇙}.=⇘_{L⇙}GFP⇘_{L⇙}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 "⊤⇘_{fpl L f⇙}⊑⇘_{L⇙}GFP⇘_{L⇙}f" by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified]) show "GFP⇘_{L⇙}f ⊑⇘_{L⇙}⊤⇘_{fpl L f⇙}" proof - have "GFP⇘_{L⇙}f ∈ fps L f" by (rule L.GFP_fixed_point, simp_all add: assms) hence "GFP⇘_{L⇙}f ∈ carrier (fpl L f)" by simp hence "GFP⇘_{L⇙}f ⊑⇘_{fpl L f⇙}⊤⇘_{fpl L f⇙}" by (rule L'.top_higher) thus ?thesis by simp qed show "⊤⇘_{fpl L f⇙}∈ 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 "⊥⇘_{fpl L f⇙}.=⇘_{L⇙}LFP⇘_{L⇙}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⇘_{L⇙}f ⊑⇘_{L⇙}⊥⇘_{fpl L f⇙}" by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified]) show "⊥⇘_{fpl L f⇙}⊑⇘_{L⇙}LFP⇘_{L⇙}f" proof - have "LFP⇘_{L⇙}f ∈ fps L f" by (rule L.LFP_fixed_point, simp_all add: assms) hence "LFP⇘_{L⇙}f ∈ carrier (fpl L f)" by simp hence "⊥⇘_{fpl L f⇙}⊑⇘_{fpl L f⇙}LFP⇘_{L⇙}f" by (rule L'.bottom_lower) thus ?thesis by simp qed show "⊥⇘_{fpl L f⇙}∈ 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 ‹If a function is both idempotent and isotone then the image of the function forms a complete lattice› 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 "⊤⇘_{fpl L f⇙}.=⇘_{L⇙}f (⊤⇘_{L⇙})" "⊥⇘_{fpl L f⇙}.=⇘_{L⇙}f (⊥⇘_{L⇙})" 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 "⊤⇘_{fpl L f⇙}.=⇘_{L⇙}f (⊤⇘_{L⇙})" proof - from FA have "⊤⇘_{fpl L f⇙}∈ carrier L" proof - have "⊤⇘_{fpl L f⇙}∈ fps L f" using L'.top_closed by auto thus ?thesis using FA by blast qed moreover with assms have "f ⊤⇘_{L⇙}∈ 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 "⊥⇘_{fpl L f⇙}.=⇘_{L⇙}f (⊥⇘_{L⇙})" proof - from FA have "⊥⇘_{fpl L f⇙}∈ carrier L" proof - have "⊥⇘_{fpl L f⇙}∈ fps L f" using L'.bottom_closed by auto thus ?thesis using FA by blast qed moreover with assms have "f ⊥⇘_{L⇙}∈ 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 "⨅⇘_{fpl L f⇙}A .=⇘_{L⇙}f (⨅⇘_{L⇙}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 (⨅⇘_{L⇙}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: "⨅⇘_{fpl L f⇙}A ∈ fps L f" by (rule L'.inf_closed[simplified], simp add: assms) show ?thesis proof (rule L.weak_le_antisym) show ic: "⨅⇘_{fpl L f⇙}A ∈ carrier L" using FA infA by blast show fc: "f (⨅⇘_{L⇙}A) ∈ carrier L" using FA fA by blast show "f (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}⨅⇘_{fpl L f⇙}A" proof - have "⋀x. x ∈ A ⟹ f (⨅⇘_{L⇙}A) ⊑⇘_{L⇙}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 (⨅⇘_{L⇙}A) ⊑⇘_{fpl L f⇙}⨅⇘_{fpl L f⇙}A" by (rule_tac L'.inf_greatest, simp_all add: fA assms(3,5)) thus ?thesis by (simp) qed show "⨅⇘_{fpl L f⇙}A ⊑⇘_{L⇙}f (⨅⇘_{L⇙}A)" proof - have "⋀x. x ∈ A ⟹ ⨅⇘_{fpl L f⇙}A ⊑⇘_{fpl L f⇙}x" by (rule L'.inf_lower, simp_all add: assms) hence "⨅⇘_{fpl L f⇙}A ⊑⇘_{L⇙}(⨅⇘_{L⇙}A)" apply (rule_tac L.inf_greatest, simp_all add: A) using FA infA apply blast done hence 1:"f(⨅⇘_{fpl L f⇙}A) ⊑⇘_{L⇙}f(⨅⇘_{L⇙}A)" by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1) have 2:"⨅⇘_{fpl L f⇙}A ⊑⇘_{L⇙}f (⨅⇘_{fpl L f⇙}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 ‹Examples› subsubsection ‹The Powerset of a Set is a Complete Lattice› 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 ‹@{term "⋂ B"} is not the infimum of @{term B}: @{term "⋂ {} = UNIV"} which is in general bigger than @{term "A"}! › by (fastforce intro!: greatest_LowerI simp: Lower_def) then show "∃i. greatest ?L i (Lower ?L B)" .. qed text ‹Another example, that of the lattice of subgroups of a group, can be found in Group theory (Section~\ref{sec:subgroup-lattice}).› subsection ‹Limit preserving functions› 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 (⨆⇘_{X⇙}A) = (⨆⇘_{Y⇙}(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 (⨆⇘_{X⇙}A) = (⨆⇘_{Y⇙}(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 (⨅⇘_{X⇙}A) = (⨅⇘_{Y⇙}(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 (⨅⇘_{X⇙}A) = (⨅⇘_{Y⇙}(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 apply (simp add: join_pres_def weak_sup_pres_def, safe) apply (rename_tac x y) apply (drule_tac x="{x, y}" in spec) apply (auto simp add: join_def) done lemma inf_pres_is_meet_pres: assumes "weak_inf_pres X Y f" shows "meet_pres X Y f" using assms apply (simp add: meet_pres_def weak_inf_pres_def, safe) apply (rename_tac x y) apply (drule_tac x="{x, y}" in spec) apply (auto simp add: meet_def) done end