Quelle Complete_Lattice.thy Sprache: Isabelle

(*  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

quality100%

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.