Quelle  Complete_Lattice.thy

(*  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 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 ‹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 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 ‹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 (intro exI 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
        show "⊔🪙L🪙A ∈ {a..b}🪙L🪙"
        proof (rule_tac L.at_least_at_most_member)
          show 1: "⊔🪙L🪙A ∈ carrier L"
            by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
          show "a ⊑🪙L🪙 ⊔🪙L🪙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 "⊔🪙L🪙A ⊑🪙L🪙 b"
          proof (rule L.sup_least)
            show "A ⊆ carrier L" "∧x. x ∈ A ==> x ⊑🪙L🪙 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}🪙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
        show "⊓🪙L🪙A ∈ {a..b}🪙L🪙"
        proof (rule_tac L.at_least_at_most_member)
          show 1: "⊓🪙L🪙A ∈ carrier L"
            by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans)
          show "a ⊑🪙L🪙 ⊓🪙L🪙A"
            by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
          show "⊓🪙L🪙A ⊑🪙L🪙 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 ‹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" 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 .=🪙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: "x ∈ Upper ?L'' A"
        have "LFP🪙?L'🪙 f ⊑🪙?L'🪙 x"
        proof (rule L'.LFP_lowerbound, simp_all)
          show "x ∈ {⊔🪙L🪙A..⊤🪙L🪙}🪙L🪙"
            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 ⊑🪙L🪙 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🪙?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)
            have "∧x. [x ∈ carrier L; ⊔🪙L🪙A ⊑🪙L🪙 x] ==> ⊔🪙L🪙A ⊑🪙L🪙 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 ∈ {⊔🪙L🪙A..⊤🪙L🪙}🪙L🪙 → {⊔🪙L🪙A..⊤🪙L🪙}🪙L🪙"
              by (auto simp add: Pi_def at_least_at_most_def)
            show "Mono🪙L(carrier := {⊔🪙L🪙A..⊤🪙L🪙}🪙L🪙)🪙 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🪙?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 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 "⊥🪙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"
        then have x: "∀y. y ∈ A ∧ y ∈ fps L f ⟶ x ⊑🪙L🪙 y" "x ∈ fps L f"
          by (auto simp add: Lower_def)
        have "x ⊑🪙?L'🪙 GFP🪙?L'🪙 f"
          unfolding Lower_def
        proof (rule_tac L'.GFP_upperbound; simp)
          show "x ∈ {⊥🪙L🪙..⊓🪙L🪙A}🪙L🪙"
            by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier)
          show "x ⊑🪙L🪙 f x"
            using x by (simp add: funcset_carrier' L.sym assms(2) fps_def)
        qed
        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)
            have "∧x. [x ∈ carrier L; x ⊑🪙L🪙 ⊓🪙L🪙A] ==> f x ⊑🪙L🪙 ⊓🪙L🪙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 ∈ {⊥🪙L🪙..?w}🪙L🪙 → {⊥🪙L🪙..?w}🪙L🪙"
              by (auto simp add: Pi_def at_least_at_most_def)
            have "∧x y. [x ∈ {⊥🪙L🪙..⊓🪙L🪙A}🪙L🪙; y ∈ {⊥🪙L🪙..⊓🪙L🪙A}🪙L🪙; x ⊑🪙L🪙 y] ==> f x ⊑🪙L🪙 f y"
              by (meson L.at_least_at_most_closed subsetD use_iso1  assms(3)) 
            with L'.weak_partial_order_axioms show "Mono🪙L(carrier := {⊥🪙L🪙..?w}🪙L🪙)🪙 f"
              by (auto simp add: isotone_def)
          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 *: "⊓🪙fpl L f🪙A ∈ carrier L"
        using FA infA by blast
      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)"
        by (rule_tac L.inf_greatest, simp_all add: A *)
      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 ‹🍋‹∩ B› is not the infimum of 🍋‹B›:
      🍋‹∩ {} = UNIV› which is in general bigger than 🍋‹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 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