src/HOL/Algebra/Complete_Lattice.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 68488 dfbd80c3d180 child 68684 9a42b84f8838 permissions -rw-r--r--
More on Algebra by Paulo and Martin
     1 (*  Title:      HOL/Algebra/Complete_Lattice.thy

     2     Author:     Clemens Ballarin, started 7 November 2003

     3     Copyright:  Clemens Ballarin

     4

     5 Most congruence rules by Stephan Hohe.

     6 With additional contributions from Alasdair Armstrong and Simon Foster.

     7 *)

     8

     9 theory Complete_Lattice

    10 imports Lattice

    11 begin

    12

    13 section \<open>Complete Lattices\<close>

    14

    15 locale weak_complete_lattice = weak_partial_order +

    16   assumes sup_exists:

    17     "[| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"

    18     and inf_exists:

    19     "[| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"

    20

    21 sublocale weak_complete_lattice \<subseteq> weak_lattice

    22 proof

    23   fix x y

    24   assume a: "x \<in> carrier L" "y \<in> carrier L"

    25   thus "\<exists>s. is_lub L s {x, y}"

    26     by (rule_tac sup_exists[of "{x, y}"], auto)

    27   from a show "\<exists>s. is_glb L s {x, y}"

    28     by (rule_tac inf_exists[of "{x, y}"], auto)

    29 qed

    30

    31 text \<open>Introduction rule: the usual definition of complete lattice\<close>

    32

    33 lemma (in weak_partial_order) weak_complete_latticeI:

    34   assumes sup_exists:

    35     "!!A. [| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"

    36     and inf_exists:

    37     "!!A. [| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"

    38   shows "weak_complete_lattice L"

    39   by standard (auto intro: sup_exists inf_exists)

    40

    41 lemma (in weak_complete_lattice) dual_weak_complete_lattice:

    42   "weak_complete_lattice (inv_gorder L)"

    43 proof -

    44   interpret dual: weak_lattice "inv_gorder L"

    45     by (metis dual_weak_lattice)

    46   show ?thesis

    47     by (unfold_locales) (simp_all add:inf_exists sup_exists)

    48 qed

    49

    50 lemma (in weak_complete_lattice) supI:

    51   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]

    52   ==> P (\<Squnion>A)"

    53 proof (unfold sup_def)

    54   assume L: "A \<subseteq> carrier L"

    55     and P: "!!l. least L l (Upper L A) ==> P l"

    56   with sup_exists obtain s where "least L s (Upper L A)" by blast

    57   with L show "P (SOME l. least L l (Upper L A))"

    58   by (fast intro: someI2 weak_least_unique P)

    59 qed

    60

    61 lemma (in weak_complete_lattice) sup_closed [simp]:

    62   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"

    63   by (rule supI) simp_all

    64

    65 lemma (in weak_complete_lattice) sup_cong:

    66   assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"

    67   shows "\<Squnion> A .= \<Squnion> B"

    68 proof -

    69   have "\<And> x. is_lub L x A \<longleftrightarrow> is_lub L x B"

    70     by (rule least_Upper_cong_r, simp_all add: assms)

    71   moreover have "\<Squnion> B \<in> carrier L"

    72     by (simp add: assms(2))

    73   ultimately show ?thesis

    74     by (simp add: sup_def)

    75 qed

    76

    77 sublocale weak_complete_lattice \<subseteq> weak_bounded_lattice

    78   apply (unfold_locales)

    79   apply (metis Upper_empty empty_subsetI sup_exists)

    80   apply (metis Lower_empty empty_subsetI inf_exists)

    81 done

    82

    83 lemma (in weak_complete_lattice) infI:

    84   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]

    85   ==> P (\<Sqinter>A)"

    86 proof (unfold inf_def)

    87   assume L: "A \<subseteq> carrier L"

    88     and P: "!!l. greatest L l (Lower L A) ==> P l"

    89   with inf_exists obtain s where "greatest L s (Lower L A)" by blast

    90   with L show "P (SOME l. greatest L l (Lower L A))"

    91   by (fast intro: someI2 weak_greatest_unique P)

    92 qed

    93

    94 lemma (in weak_complete_lattice) inf_closed [simp]:

    95   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"

    96   by (rule infI) simp_all

    97

    98 lemma (in weak_complete_lattice) inf_cong:

    99   assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"

   100   shows "\<Sqinter> A .= \<Sqinter> B"

   101 proof -

   102   have "\<And> x. is_glb L x A \<longleftrightarrow> is_glb L x B"

   103     by (rule greatest_Lower_cong_r, simp_all add: assms)

   104   moreover have "\<Sqinter> B \<in> carrier L"

   105     by (simp add: assms(2))

   106   ultimately show ?thesis

   107     by (simp add: inf_def)

   108 qed

   109

   110 theorem (in weak_partial_order) weak_complete_lattice_criterion1:

   111   assumes top_exists: "\<exists>g. greatest L g (carrier L)"

   112     and inf_exists:

   113       "\<And>A. [| A \<subseteq> carrier L; A \<noteq> {} |] ==> \<exists>i. greatest L i (Lower L A)"

   114   shows "weak_complete_lattice L"

   115 proof (rule weak_complete_latticeI)

   116   from top_exists obtain top where top: "greatest L top (carrier L)" ..

   117   fix A

   118   assume L: "A \<subseteq> carrier L"

   119   let ?B = "Upper L A"

   120   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)

   121   then have B_non_empty: "?B \<noteq> {}" by fast

   122   have B_L: "?B \<subseteq> carrier L" by simp

   123   from inf_exists [OF B_L B_non_empty]

   124   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..

   125   then have bcarr: "b \<in> carrier L"

   126     by auto

   127   have "least L b (Upper L A)"

   128   proof (rule least_UpperI)

   129     show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"

   130       by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)

   131     show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"

   132       by (meson B_L b_inf_B greatest_Lower_below)

   133   qed (use bcarr L in auto)

   134   then show "\<exists>s. least L s (Upper L A)" ..

   135 next

   136   fix A

   137   assume L: "A \<subseteq> carrier L"

   138   show "\<exists>i. greatest L i (Lower L A)"

   139     by (metis L Lower_empty inf_exists top_exists)

   140 qed

   141

   142

   143 text \<open>Supremum\<close>

   144

   145 declare (in partial_order) weak_sup_of_singleton [simp del]

   146

   147 lemma (in partial_order) sup_of_singleton [simp]:

   148   "x \<in> carrier L ==> \<Squnion>{x} = x"

   149   using weak_sup_of_singleton unfolding eq_is_equal .

   150

   151 lemma (in upper_semilattice) join_assoc_lemma:

   152   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   153   shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"

   154   using weak_join_assoc_lemma L unfolding eq_is_equal .

   155

   156 lemma (in upper_semilattice) join_assoc:

   157   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   158   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"

   159   using weak_join_assoc L unfolding eq_is_equal .

   160

   161

   162 text \<open>Infimum\<close>

   163

   164 declare (in partial_order) weak_inf_of_singleton [simp del]

   165

   166 lemma (in partial_order) inf_of_singleton [simp]:

   167   "x \<in> carrier L ==> \<Sqinter>{x} = x"

   168   using weak_inf_of_singleton unfolding eq_is_equal .

   169

   170 text \<open>Condition on \<open>A\<close>: infimum exists.\<close>

   171

   172 lemma (in lower_semilattice) meet_assoc_lemma:

   173   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   174   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"

   175   using weak_meet_assoc_lemma L unfolding eq_is_equal .

   176

   177 lemma (in lower_semilattice) meet_assoc:

   178   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   179   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"

   180   using weak_meet_assoc L unfolding eq_is_equal .

   181

   182

   183 subsection \<open>Infimum Laws\<close>

   184

   185 context weak_complete_lattice

   186 begin

   187

   188 lemma inf_glb:

   189   assumes "A \<subseteq> carrier L"

   190   shows "greatest L (\<Sqinter>A) (Lower L A)"

   191 proof -

   192   obtain i where "greatest L i (Lower L A)"

   193     by (metis assms inf_exists)

   194   thus ?thesis

   195     by (metis inf_def someI_ex)

   196 qed

   197

   198 lemma inf_lower:

   199   assumes "A \<subseteq> carrier L" "x \<in> A"

   200   shows "\<Sqinter>A \<sqsubseteq> x"

   201   by (metis assms greatest_Lower_below inf_glb)

   202

   203 lemma inf_greatest:

   204   assumes "A \<subseteq> carrier L" "z \<in> carrier L"

   205           "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x)"

   206   shows "z \<sqsubseteq> \<Sqinter>A"

   207   by (metis Lower_memI assms greatest_le inf_glb)

   208

   209 lemma weak_inf_empty [simp]: "\<Sqinter>{} .= \<top>"

   210   by (metis Lower_empty empty_subsetI inf_glb top_greatest weak_greatest_unique)

   211

   212 lemma weak_inf_carrier [simp]: "\<Sqinter>carrier L .= \<bottom>"

   213   by (metis bottom_weak_eq inf_closed inf_lower subset_refl)

   214

   215 lemma weak_inf_insert [simp]:

   216   assumes "a \<in> carrier L" "A \<subseteq> carrier L"

   217   shows "\<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"

   218 proof (rule weak_le_antisym)

   219   show "\<Sqinter>insert a A \<sqsubseteq> a \<sqinter> \<Sqinter>A"

   220     by (simp add: assms inf_lower local.inf_greatest meet_le)

   221   show aA: "a \<sqinter> \<Sqinter>A \<in> carrier L"

   222     using assms by simp

   223   show "a \<sqinter> \<Sqinter>A \<sqsubseteq> \<Sqinter>insert a A"

   224     apply (rule inf_greatest)

   225     using assms apply (simp_all add: aA)

   226     by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)

   227   show "\<Sqinter>insert a A \<in> carrier L"

   228     using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)

   229 qed

   230

   231 subsection \<open>Supremum Laws\<close>

   232

   233 lemma sup_lub:

   234   assumes "A \<subseteq> carrier L"

   235   shows "least L (\<Squnion>A) (Upper L A)"

   236     by (metis Upper_is_closed assms least_closed least_cong supI sup_closed sup_exists weak_least_unique)

   237

   238 lemma sup_upper:

   239   assumes "A \<subseteq> carrier L" "x \<in> A"

   240   shows "x \<sqsubseteq> \<Squnion>A"

   241   by (metis assms least_Upper_above supI)

   242

   243 lemma sup_least:

   244   assumes "A \<subseteq> carrier L" "z \<in> carrier L"

   245           "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z)"

   246   shows "\<Squnion>A \<sqsubseteq> z"

   247   by (metis Upper_memI assms least_le sup_lub)

   248

   249 lemma weak_sup_empty [simp]: "\<Squnion>{} .= \<bottom>"

   250   by (metis Upper_empty bottom_least empty_subsetI sup_lub weak_least_unique)

   251

   252 lemma weak_sup_carrier [simp]: "\<Squnion>carrier L .= \<top>"

   253   by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)

   254

   255 lemma weak_sup_insert [simp]:

   256   assumes "a \<in> carrier L" "A \<subseteq> carrier L"

   257   shows "\<Squnion>insert a A .= a \<squnion> \<Squnion>A"

   258 proof (rule weak_le_antisym)

   259   show aA: "a \<squnion> \<Squnion>A \<in> carrier L"

   260     using assms by simp

   261   show "\<Squnion>insert a A \<sqsubseteq> a \<squnion> \<Squnion>A"

   262     apply (rule sup_least)

   263     using assms apply (simp_all add: aA)

   264     by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)

   265   show "a \<squnion> \<Squnion>A \<sqsubseteq> \<Squnion>insert a A"

   266     by (simp add: assms join_le local.sup_least sup_upper)

   267   show "\<Squnion>insert a A \<in> carrier L"

   268     using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)

   269 qed

   270

   271 end

   272

   273

   274 subsection \<open>Fixed points of a lattice\<close>

   275

   276 definition "fps L f = {x \<in> carrier L. f x .=\<^bsub>L\<^esub> x}"

   277

   278 abbreviation "fpl L f \<equiv> L\<lparr>carrier := fps L f\<rparr>"

   279

   280 lemma (in weak_partial_order)

   281   use_fps: "x \<in> fps L f \<Longrightarrow> f x .= x"

   282   by (simp add: fps_def)

   283

   284 lemma fps_carrier [simp]:

   285   "fps L f \<subseteq> carrier L"

   286   by (auto simp add: fps_def)

   287

   288 lemma (in weak_complete_lattice) fps_sup_image:

   289   assumes "f \<in> carrier L \<rightarrow> carrier L" "A \<subseteq> fps L f"

   290   shows "\<Squnion> (f  A) .= \<Squnion> A"

   291 proof -

   292   from assms(2) have AL: "A \<subseteq> carrier L"

   293     by (auto simp add: fps_def)

   294   show ?thesis

   295   proof (rule sup_cong, simp_all add: AL)

   296     from assms(1) AL show "f  A \<subseteq> carrier L"

   297       by auto

   298     then have *: "\<And>b. \<lbrakk>A \<subseteq> {x \<in> carrier L. f x .= x}; b \<in> A\<rbrakk> \<Longrightarrow> \<exists>a\<in>f  A. b .= a"

   299       by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)

   300     from assms(2) show "f  A {.=} A"

   301       by (auto simp add: fps_def intro: set_eqI2 [OF _ *])

   302   qed

   303 qed

   304

   305 lemma (in weak_complete_lattice) fps_idem:

   306   assumes "f \<in> carrier L \<rightarrow> carrier L" "Idem f"

   307   shows "fps L f {.=} f  carrier L"

   308 proof (rule set_eqI2)

   309   show "\<And>a. a \<in> fps L f \<Longrightarrow> \<exists>b\<in>f  carrier L. a .= b"

   310     using assms by (force simp add: fps_def intro: local.sym)

   311   show "\<And>b. b \<in> f  carrier L \<Longrightarrow> \<exists>a\<in>fps L f. b .= a"

   312     using assms by (force simp add: idempotent_def fps_def)

   313 qed

   314

   315 context weak_complete_lattice

   316 begin

   317

   318 lemma weak_sup_pre_fixed_point:

   319   assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"

   320   shows "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"

   321 proof (rule sup_least)

   322   from assms(3) show AL: "A \<subseteq> carrier L"

   323     by (auto simp add: fps_def)

   324   thus fA: "f (\<Squnion>A) \<in> carrier L"

   325     by (simp add: assms funcset_carrier[of f L L])

   326   fix x

   327   assume xA: "x \<in> A"

   328   hence "x \<in> fps L f"

   329     using assms subsetCE by blast

   330   hence "f x .=\<^bsub>L\<^esub> x"

   331     by (auto simp add: fps_def)

   332   moreover have "f x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"

   333     by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA)

   334   ultimately show "x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"

   335     by (meson AL fA assms(1) funcset_carrier le_cong local.refl subsetCE xA)

   336 qed

   337

   338 lemma weak_sup_post_fixed_point:

   339   assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"

   340   shows "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"

   341 proof (rule inf_greatest)

   342   from assms(3) show AL: "A \<subseteq> carrier L"

   343     by (auto simp add: fps_def)

   344   thus fA: "f (\<Sqinter>A) \<in> carrier L"

   345     by (simp add: assms funcset_carrier[of f L L])

   346   fix x

   347   assume xA: "x \<in> A"

   348   hence "x \<in> fps L f"

   349     using assms subsetCE by blast

   350   hence "f x .=\<^bsub>L\<^esub> x"

   351     by (auto simp add: fps_def)

   352   moreover have "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f x"

   353     by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA)

   354   ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> x"

   355     by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA)

   356 qed

   357

   358

   359 subsubsection \<open>Least fixed points\<close>

   360

   361 lemma LFP_closed [intro, simp]:

   362   "LFP f \<in> carrier L"

   363   by (metis (lifting) LEAST_FP_def inf_closed mem_Collect_eq subsetI)

   364

   365 lemma LFP_lowerbound:

   366   assumes "x \<in> carrier L" "f x \<sqsubseteq> x"

   367   shows "LFP f \<sqsubseteq> x"

   368   by (auto intro:inf_lower assms simp add:LEAST_FP_def)

   369

   370 lemma LFP_greatest:

   371   assumes "x \<in> carrier L"

   372           "(\<And>u. \<lbrakk> u \<in> carrier L; f u \<sqsubseteq> u \<rbrakk> \<Longrightarrow> x \<sqsubseteq> u)"

   373   shows "x \<sqsubseteq> LFP f"

   374   by (auto simp add:LEAST_FP_def intro:inf_greatest assms)

   375

   376 lemma LFP_lemma2:

   377   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"

   378   shows "f (LFP f) \<sqsubseteq> LFP f"

   379 proof (rule LFP_greatest)

   380   have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"

   381     using assms by (auto simp add: Pi_def)

   382   with assms show "f (LFP f) \<in> carrier L"

   383     by blast

   384   show "\<And>u. \<lbrakk>u \<in> carrier L; f u \<sqsubseteq> u\<rbrakk> \<Longrightarrow> f (LFP f) \<sqsubseteq> u"

   385     by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)

   386 qed

   387

   388 lemma LFP_lemma3:

   389   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"

   390   shows "LFP f \<sqsubseteq> f (LFP f)"

   391   using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)

   392

   393 lemma LFP_weak_unfold:

   394   "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f .= f (LFP f)"

   395   by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)

   396

   397 lemma LFP_fixed_point [intro]:

   398   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"

   399   shows "LFP f \<in> fps L f"

   400 proof -

   401   have "f (LFP f) \<in> carrier L"

   402     using assms(2) by blast

   403   with assms show ?thesis

   404     by (simp add: LFP_weak_unfold fps_def local.sym)

   405 qed

   406

   407 lemma LFP_least_fixed_point:

   408   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"

   409   shows "LFP f \<sqsubseteq> x"

   410   using assms by (force intro: LFP_lowerbound simp add: fps_def)

   411

   412 lemma LFP_idem:

   413   assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"

   414   shows "LFP f .= (f \<bottom>)"

   415 proof (rule weak_le_antisym)

   416   from assms(1) show fb: "f \<bottom> \<in> carrier L"

   417     by (rule funcset_mem, simp)

   418   from assms show mf: "LFP f \<in> carrier L"

   419     by blast

   420   show "LFP f \<sqsubseteq> f \<bottom>"

   421   proof -

   422     have "f (f \<bottom>) .= f \<bottom>"

   423       by (auto simp add: fps_def fb assms(3) idempotent)

   424     moreover have "f (f \<bottom>) \<in> carrier L"

   425       by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)

   426     ultimately show ?thesis

   427       by (auto intro: LFP_lowerbound simp add: fb)

   428   qed

   429   show "f \<bottom> \<sqsubseteq> LFP f"

   430   proof -

   431     have "f \<bottom> \<sqsubseteq> f (LFP f)"

   432       by (auto intro: use_iso1[of _ f] simp add: assms)

   433     moreover have "... .= LFP f"

   434       using assms(1) assms(2) fps_def by force

   435     moreover from assms(1) have "f (LFP f) \<in> carrier L"

   436       by (auto)

   437     ultimately show ?thesis

   438       using fb by blast

   439   qed

   440 qed

   441

   442

   443 subsubsection \<open>Greatest fixed points\<close>

   444

   445 lemma GFP_closed [intro, simp]:

   446   "GFP f \<in> carrier L"

   447   by (auto intro:sup_closed simp add:GREATEST_FP_def)

   448

   449 lemma GFP_upperbound:

   450   assumes "x \<in> carrier L" "x \<sqsubseteq> f x"

   451   shows "x \<sqsubseteq> GFP f"

   452   by (auto intro:sup_upper assms simp add:GREATEST_FP_def)

   453

   454 lemma GFP_least:

   455   assumes "x \<in> carrier L"

   456           "(\<And>u. \<lbrakk> u \<in> carrier L; u \<sqsubseteq> f u \<rbrakk> \<Longrightarrow> u \<sqsubseteq> x)"

   457   shows "GFP f \<sqsubseteq> x"

   458   by (auto simp add:GREATEST_FP_def intro:sup_least assms)

   459

   460 lemma GFP_lemma2:

   461   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"

   462   shows "GFP f \<sqsubseteq> f (GFP f)"

   463 proof (rule GFP_least)

   464   have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"

   465     using assms by (auto simp add: Pi_def)

   466   with assms show "f (GFP f) \<in> carrier L"

   467     by blast

   468   show "\<And>u. \<lbrakk>u \<in> carrier L; u \<sqsubseteq> f u\<rbrakk> \<Longrightarrow> u \<sqsubseteq> f (GFP f)"

   469     by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)

   470 qed

   471

   472 lemma GFP_lemma3:

   473   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"

   474   shows "f (GFP f) \<sqsubseteq> GFP f"

   475   by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)

   476

   477 lemma GFP_weak_unfold:

   478   "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> GFP f .= f (GFP f)"

   479   by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)

   480

   481 lemma (in weak_complete_lattice) GFP_fixed_point [intro]:

   482   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"

   483   shows "GFP f \<in> fps L f"

   484   using assms

   485 proof -

   486   have "f (GFP f) \<in> carrier L"

   487     using assms(2) by blast

   488   with assms show ?thesis

   489     by (simp add: GFP_weak_unfold fps_def local.sym)

   490 qed

   491

   492 lemma GFP_greatest_fixed_point:

   493   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"

   494   shows "x \<sqsubseteq> GFP f"

   495   using assms

   496   by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)

   497

   498 lemma GFP_idem:

   499   assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"

   500   shows "GFP f .= (f \<top>)"

   501 proof (rule weak_le_antisym)

   502   from assms(1) show fb: "f \<top> \<in> carrier L"

   503     by (rule funcset_mem, simp)

   504   from assms show mf: "GFP f \<in> carrier L"

   505     by blast

   506   show "f \<top> \<sqsubseteq> GFP f"

   507   proof -

   508     have "f (f \<top>) .= f \<top>"

   509       by (auto simp add: fps_def fb assms(3) idempotent)

   510     moreover have "f (f \<top>) \<in> carrier L"

   511       by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)

   512     ultimately show ?thesis

   513       by (rule_tac GFP_upperbound, simp_all add: fb local.sym)

   514   qed

   515   show "GFP f \<sqsubseteq> f \<top>"

   516   proof -

   517     have "GFP f \<sqsubseteq> f (GFP f)"

   518       by (simp add: GFP_lemma2 assms(1) assms(2))

   519     moreover have "... \<sqsubseteq> f \<top>"

   520       by (auto intro: use_iso1[of _ f] simp add: assms)

   521     moreover from assms(1) have "f (GFP f) \<in> carrier L"

   522       by (auto)

   523     ultimately show ?thesis

   524       using fb local.le_trans by blast

   525   qed

   526 qed

   527

   528 end

   529

   530

   531 subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close>

   532

   533 locale complete_lattice = partial_order +

   534   assumes sup_exists:

   535     "[| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"

   536     and inf_exists:

   537     "[| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"

   538

   539 sublocale complete_lattice \<subseteq> lattice

   540 proof

   541   fix x y

   542   assume a: "x \<in> carrier L" "y \<in> carrier L"

   543   thus "\<exists>s. is_lub L s {x, y}"

   544     by (rule_tac sup_exists[of "{x, y}"], auto)

   545   from a show "\<exists>s. is_glb L s {x, y}"

   546     by (rule_tac inf_exists[of "{x, y}"], auto)

   547 qed

   548

   549 sublocale complete_lattice \<subseteq> weak?: weak_complete_lattice

   550   by standard (auto intro: sup_exists inf_exists)

   551

   552 lemma complete_lattice_lattice [simp]:

   553   assumes "complete_lattice X"

   554   shows "lattice X"

   555 proof -

   556   interpret c: complete_lattice X

   557     by (simp add: assms)

   558   show ?thesis

   559     by (unfold_locales)

   560 qed

   561

   562 text \<open>Introduction rule: the usual definition of complete lattice\<close>

   563

   564 lemma (in partial_order) complete_latticeI:

   565   assumes sup_exists:

   566     "!!A. [| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"

   567     and inf_exists:

   568     "!!A. [| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"

   569   shows "complete_lattice L"

   570   by standard (auto intro: sup_exists inf_exists)

   571

   572 theorem (in partial_order) complete_lattice_criterion1:

   573   assumes top_exists: "\<exists>g. greatest L g (carrier L)"

   574     and inf_exists:

   575       "!!A. [| A \<subseteq> carrier L; A \<noteq> {} |] ==> \<exists>i. greatest L i (Lower L A)"

   576   shows "complete_lattice L"

   577 proof (rule complete_latticeI)

   578   from top_exists obtain top where top: "greatest L top (carrier L)" ..

   579   fix A

   580   assume L: "A \<subseteq> carrier L"

   581   let ?B = "Upper L A"

   582   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)

   583   then have B_non_empty: "?B \<noteq> {}" by fast

   584   have B_L: "?B \<subseteq> carrier L" by simp

   585   from inf_exists [OF B_L B_non_empty]

   586   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..

   587   then have bcarr: "b \<in> carrier L"

   588     by blast

   589   have "least L b (Upper L A)"

   590   proof (rule least_UpperI)

   591     show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"

   592       by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)

   593     show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"

   594       by (auto elim: greatest_Lower_below [OF b_inf_B])

   595   qed (use L bcarr in auto)

   596   then show "\<exists>s. least L s (Upper L A)" ..

   597 next

   598   fix A

   599   assume L: "A \<subseteq> carrier L"

   600   show "\<exists>i. greatest L i (Lower L A)"

   601   proof (cases "A = {}")

   602     case True then show ?thesis

   603       by (simp add: top_exists)

   604   next

   605     case False with L show ?thesis

   606       by (rule inf_exists)

   607   qed

   608 qed

   609

   610 (* TODO: prove dual version *)

   611

   612 subsection \<open>Fixed points\<close>

   613

   614 context complete_lattice

   615 begin

   616

   617 lemma LFP_unfold:

   618   "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f = f (LFP f)"

   619   using eq_is_equal weak.LFP_weak_unfold by auto

   620

   621 lemma LFP_const:

   622   "t \<in> carrier L \<Longrightarrow> LFP (\<lambda> x. t) = t"

   623   by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)

   624

   625 lemma LFP_id:

   626   "LFP id = \<bottom>"

   627   by (simp add: local.le_antisym weak.LFP_lowerbound)

   628

   629 lemma GFP_unfold:

   630   "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> GFP f = f (GFP f)"

   631   using eq_is_equal weak.GFP_weak_unfold by auto

   632

   633 lemma GFP_const:

   634   "t \<in> carrier L \<Longrightarrow> GFP (\<lambda> x. t) = t"

   635   by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)

   636

   637 lemma GFP_id:

   638   "GFP id = \<top>"

   639   using weak.GFP_upperbound by auto

   640

   641 end

   642

   643

   644 subsection \<open>Interval complete lattices\<close>

   645

   646 context weak_complete_lattice

   647 begin

   648

   649   lemma at_least_at_most_Sup: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"

   650     by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)

   651

   652   lemma at_least_at_most_Inf: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"

   653     by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)

   654

   655 end

   656

   657 lemma weak_complete_lattice_interval:

   658   assumes "weak_complete_lattice L" "a \<in> carrier L" "b \<in> carrier L" "a \<sqsubseteq>\<^bsub>L\<^esub> b"

   659   shows "weak_complete_lattice (L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>)"

   660 proof -

   661   interpret L: weak_complete_lattice L

   662     by (simp add: assms)

   663   interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"

   664   proof -

   665     have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"

   666       by (auto simp add: at_least_at_most_def)

   667     thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"

   668       by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)

   669   qed

   670

   671   show ?thesis

   672   proof

   673     fix A

   674     assume a: "A \<subseteq> carrier (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"

   675     show "\<exists>s. is_lub (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"

   676     proof (cases "A = {}")

   677       case True

   678       thus ?thesis

   679         by (rule_tac x="a" in exI, auto simp add: least_def assms)

   680     next

   681       case False

   682       show ?thesis

   683       proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)

   684         show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"

   685           using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)

   686         show "\<And>y. y \<in> Upper (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"

   687           using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)

   688         from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"

   689           by (auto)

   690         from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"

   691           apply (rule_tac L.at_least_at_most_member)

   692           apply (auto)

   693           apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)

   694           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)

   695           apply (rule L.sup_least)

   696           apply (auto simp add: assms)

   697           using L.at_least_at_most_closed apply blast

   698         done

   699       qed

   700     qed

   701     show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"

   702     proof (cases "A = {}")

   703       case True

   704       thus ?thesis

   705         by (rule_tac x="b" in exI, auto simp add: greatest_def assms)

   706     next

   707       case False

   708       show ?thesis

   709       proof (rule_tac x="\<Sqinter>\<^bsub>L\<^esub> A" in exI, rule greatest_LowerI, simp_all)

   710         show b:"\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"

   711           using a L.at_least_at_most_closed by (force intro!: L.inf_lower)

   712         show "\<And>y. y \<in> Lower (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> y \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"

   713            using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)

   714         from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"

   715           by (auto)

   716         from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"

   717           apply (rule_tac L.at_least_at_most_member)

   718           apply (auto)

   719           apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)

   720           apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)

   721           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)

   722         done

   723       qed

   724     qed

   725   qed

   726 qed

   727

   728

   729 subsection \<open>Knaster-Tarski theorem and variants\<close>

   730

   731 text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>

   732

   733 theorem Knaster_Tarski:

   734   assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"

   735   shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")

   736 proof -

   737   interpret L: weak_complete_lattice L

   738     by (simp add: assms)

   739   interpret weak_partial_order ?L'

   740   proof -

   741     have "{x \<in> carrier L. f x .=\<^bsub>L\<^esub> x} \<subseteq> carrier L"

   742       by (auto)

   743     thus "weak_partial_order ?L'"

   744       by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)

   745   qed

   746   show ?thesis

   747   proof (unfold_locales, simp_all)

   748     fix A

   749     assume A: "A \<subseteq> fps L f"

   750     show "\<exists>s. is_lub (fpl L f) s A"

   751     proof

   752       from A have AL: "A \<subseteq> carrier L"

   753         by (meson fps_carrier subset_eq)

   754

   755       let ?w = "\<Squnion>\<^bsub>L\<^esub> A"

   756       have w: "f (\<Squnion>\<^bsub>L\<^esub>A) \<in> carrier L"

   757         by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2))

   758

   759       have pf_w: "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"

   760         by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3))

   761

   762       have f_top_chain: "f  \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<subseteq> \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"

   763       proof (auto simp add: at_least_at_most_def)

   764         fix x

   765         assume b: "x \<in> carrier L" "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"

   766         from b show fx: "f x \<in> carrier L"

   767           using assms(2) by blast

   768         show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f x"

   769         proof -

   770           have "?w \<sqsubseteq>\<^bsub>L\<^esub> f ?w"

   771           proof (rule_tac L.sup_least, simp_all add: AL w)

   772             fix y

   773             assume c: "y \<in> A"

   774             hence y: "y \<in> fps L f"

   775               using A subsetCE by blast

   776             with assms have "y .=\<^bsub>L\<^esub> f y"

   777             proof -

   778               from y have "y \<in> carrier L"

   779                 by (simp add: fps_def)

   780               moreover hence "f y \<in> carrier L"

   781                 by (rule_tac funcset_mem[of f "carrier L"], simp_all add: assms)

   782               ultimately show ?thesis using y

   783                 by (rule_tac L.sym, simp_all add: L.use_fps)

   784             qed

   785             moreover have "y \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"

   786               by (simp add: AL L.sup_upper c(1))

   787             ultimately show "y \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"

   788               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)

   789           qed

   790           thus ?thesis

   791             by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) b(1) b(2) use_iso2)

   792         qed

   793

   794         show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>L\<^esub>"

   795           by (simp add: fx)

   796       qed

   797

   798       let ?L' = "L\<lparr> carrier := \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rparr>"

   799

   800       interpret L': weak_complete_lattice ?L'

   801         by (auto intro: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)

   802

   803       let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"

   804

   805       show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"

   806       proof (rule least_UpperI, simp_all)

   807         fix x

   808         assume "x \<in> Upper ?L'' A"

   809         hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"

   810           apply (rule_tac L'.LFP_lowerbound)

   811           apply (auto simp add: Upper_def)

   812           apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)

   813           apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)

   814           apply (auto)

   815           apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))

   816         done

   817         thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"

   818           by (simp)

   819       next

   820         fix x

   821         assume xA: "x \<in> A"

   822         show "x \<sqsubseteq>\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"

   823         proof -

   824           have "LFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"

   825             by blast

   826           thus ?thesis

   827             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)

   828         qed

   829       next

   830         show "A \<subseteq> fps L f"

   831           by (simp add: A)

   832       next

   833         show "LFP\<^bsub>?L'\<^esub> f \<in> fps L f"

   834         proof (auto simp add: fps_def)

   835           have "LFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"

   836             by (rule L'.LFP_closed)

   837           thus c:"LFP\<^bsub>?L'\<^esub> f \<in> carrier L"

   838              by (auto simp add: at_least_at_most_def)

   839           have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"

   840           proof (rule "L'.LFP_weak_unfold", simp_all)

   841             show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"

   842               apply (auto simp add: Pi_def at_least_at_most_def)

   843               using assms(2) apply blast

   844               apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)

   845               using assms(2) apply blast

   846             done

   847             from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"

   848               apply (auto simp add: isotone_def)

   849               using L'.weak_partial_order_axioms apply blast

   850               apply (meson L.at_least_at_most_closed subsetCE)

   851             done

   852           qed

   853           thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"

   854             by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)

   855         qed

   856       qed

   857     qed

   858     show "\<exists>i. is_glb (L\<lparr>carrier := fps L f\<rparr>) i A"

   859     proof

   860       from A have AL: "A \<subseteq> carrier L"

   861         by (meson fps_carrier subset_eq)

   862

   863       let ?w = "\<Sqinter>\<^bsub>L\<^esub> A"

   864       have w: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> carrier L"

   865         by (simp add: AL funcset_carrier' assms(2))

   866

   867       have pf_w: "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"

   868         by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3))

   869

   870       have f_bot_chain: "f  \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<subseteq> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"

   871       proof (auto simp add: at_least_at_most_def)

   872         fix x

   873         assume b: "x \<in> carrier L" "x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"

   874         from b show fx: "f x \<in> carrier L"

   875           using assms(2) by blast

   876         show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"

   877         proof -

   878           have "f ?w \<sqsubseteq>\<^bsub>L\<^esub> ?w"

   879           proof (rule_tac L.inf_greatest, simp_all add: AL w)

   880             fix y

   881             assume c: "y \<in> A"

   882             with assms have "y .=\<^bsub>L\<^esub> f y"

   883               by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq)

   884             moreover have "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"

   885               by (simp add: AL L.inf_lower c)

   886             ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> y"

   887               by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)

   888           qed

   889           thus ?thesis

   890             by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)

   891         qed

   892

   893         show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"

   894           by (simp add: fx)

   895       qed

   896

   897       let ?L' = "L\<lparr> carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rparr>"

   898

   899       interpret L': weak_complete_lattice ?L'

   900         by (auto intro!: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)

   901

   902       let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"

   903

   904       show "is_glb ?L'' (GFP\<^bsub>?L'\<^esub> f) A"

   905       proof (rule greatest_LowerI, simp_all)

   906         fix x

   907         assume "x \<in> Lower ?L'' A"

   908         hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"

   909           apply (rule_tac L'.GFP_upperbound)

   910           apply (auto simp add: Lower_def)

   911           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)

   912           apply (simp add: funcset_carrier' L.sym assms(2) fps_def)

   913         done

   914         thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"

   915           by (simp)

   916       next

   917         fix x

   918         assume xA: "x \<in> A"

   919         show "GFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"

   920         proof -

   921           have "GFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"

   922             by blast

   923           thus ?thesis

   924             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)

   925         qed

   926       next

   927         show "A \<subseteq> fps L f"

   928           by (simp add: A)

   929       next

   930         show "GFP\<^bsub>?L'\<^esub> f \<in> fps L f"

   931         proof (auto simp add: fps_def)

   932           have "GFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"

   933             by (rule L'.GFP_closed)

   934           thus c:"GFP\<^bsub>?L'\<^esub> f \<in> carrier L"

   935              by (auto simp add: at_least_at_most_def)

   936           have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"

   937           proof (rule "L'.GFP_weak_unfold", simp_all)

   938             show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"

   939               apply (auto simp add: Pi_def at_least_at_most_def)

   940               using assms(2) apply blast

   941               apply (simp add: funcset_carrier' assms(2))

   942               apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)

   943             done

   944             from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"

   945               apply (auto simp add: isotone_def)

   946               using L'.weak_partial_order_axioms apply blast

   947               using L.at_least_at_most_closed apply (blast intro: funcset_carrier')

   948             done

   949           qed

   950           thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"

   951             by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)

   952         qed

   953       qed

   954     qed

   955   qed

   956 qed

   957

   958 theorem Knaster_Tarski_top:

   959   assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"

   960   shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"

   961 proof -

   962   interpret L: weak_complete_lattice L

   963     by (simp add: assms)

   964   interpret L': weak_complete_lattice "fpl L f"

   965     by (rule Knaster_Tarski, simp_all add: assms)

   966   show ?thesis

   967   proof (rule L.weak_le_antisym, simp_all)

   968     show "\<top>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"

   969       by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])

   970     show "GFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>fpl L f\<^esub>"

   971     proof -

   972       have "GFP\<^bsub>L\<^esub> f \<in> fps L f"

   973         by (rule L.GFP_fixed_point, simp_all add: assms)

   974       hence "GFP\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"

   975         by simp

   976       hence "GFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<top>\<^bsub>fpl L f\<^esub>"

   977         by (rule L'.top_higher)

   978       thus ?thesis

   979         by simp

   980     qed

   981     show "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"

   982     proof -

   983       have "carrier (fpl L f) \<subseteq> carrier L"

   984         by (auto simp add: fps_def)

   985       with L'.top_closed show ?thesis

   986         by blast

   987     qed

   988   qed

   989 qed

   990

   991 theorem Knaster_Tarski_bottom:

   992   assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"

   993   shows "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"

   994 proof -

   995   interpret L: weak_complete_lattice L

   996     by (simp add: assms)

   997   interpret L': weak_complete_lattice "fpl L f"

   998     by (rule Knaster_Tarski, simp_all add: assms)

   999   show ?thesis

  1000   proof (rule L.weak_le_antisym, simp_all)

  1001     show "LFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<bottom>\<^bsub>fpl L f\<^esub>"

  1002       by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])

  1003     show "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"

  1004     proof -

  1005       have "LFP\<^bsub>L\<^esub> f \<in> fps L f"

  1006         by (rule L.LFP_fixed_point, simp_all add: assms)

  1007       hence "LFP\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"

  1008         by simp

  1009       hence "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>fpl L f\<^esub> LFP\<^bsub>L\<^esub> f"

  1010         by (rule L'.bottom_lower)

  1011       thus ?thesis

  1012         by simp

  1013     qed

  1014     show "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"

  1015     proof -

  1016       have "carrier (fpl L f) \<subseteq> carrier L"

  1017         by (auto simp add: fps_def)

  1018       with L'.bottom_closed show ?thesis

  1019         by blast

  1020     qed

  1021   qed

  1022 qed

  1023

  1024 text \<open>If a function is both idempotent and isotone then the image of the function forms a complete lattice\<close>

  1025

  1026 theorem Knaster_Tarski_idem:

  1027   assumes "complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "idempotent L f"

  1028   shows "complete_lattice (L\<lparr>carrier := f  carrier L\<rparr>)"

  1029 proof -

  1030   interpret L: complete_lattice L

  1031     by (simp add: assms)

  1032   have "fps L f = f  carrier L"

  1033     using L.weak.fps_idem[OF assms(2) assms(4)]

  1034     by (simp add: L.set_eq_is_eq)

  1035   then interpret L': weak_complete_lattice "(L\<lparr>carrier := f  carrier L\<rparr>)"

  1036     by (metis Knaster_Tarski L.weak.weak_complete_lattice_axioms assms(2) assms(3))

  1037   show ?thesis

  1038     using L'.sup_exists L'.inf_exists

  1039     by (unfold_locales, auto simp add: L.eq_is_equal)

  1040 qed

  1041

  1042 theorem Knaster_Tarski_idem_extremes:

  1043   assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \<in> carrier L \<rightarrow> carrier L"

  1044   shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)" "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"

  1045 proof -

  1046   interpret L: weak_complete_lattice "L"

  1047     by (simp_all add: assms)

  1048   interpret L': weak_complete_lattice "fpl L f"

  1049     by (rule Knaster_Tarski, simp_all add: assms)

  1050   have FA: "fps L f \<subseteq> carrier L"

  1051     by (auto simp add: fps_def)

  1052   show "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)"

  1053   proof -

  1054     from FA have "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"

  1055     proof -

  1056       have "\<top>\<^bsub>fpl L f\<^esub> \<in> fps L f"

  1057         using L'.top_closed by auto

  1058       thus ?thesis

  1059         using FA by blast

  1060     qed

  1061     moreover with assms have "f \<top>\<^bsub>L\<^esub> \<in> carrier L"

  1062       by (auto)

  1063

  1064     ultimately show ?thesis

  1065       using L.trans[OF Knaster_Tarski_top[of L f] L.GFP_idem[of f]]

  1066       by (simp_all add: assms)

  1067   qed

  1068   show "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"

  1069   proof -

  1070     from FA have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"

  1071     proof -

  1072       have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> fps L f"

  1073         using L'.bottom_closed by auto

  1074       thus ?thesis

  1075         using FA by blast

  1076     qed

  1077     moreover with assms have "f \<bottom>\<^bsub>L\<^esub> \<in> carrier L"

  1078       by (auto)

  1079

  1080     ultimately show ?thesis

  1081       using L.trans[OF Knaster_Tarski_bottom[of L f] L.LFP_idem[of f]]

  1082       by (simp_all add: assms)

  1083   qed

  1084 qed

  1085

  1086 theorem Knaster_Tarski_idem_inf_eq:

  1087   assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \<in> carrier L \<rightarrow> carrier L"

  1088           "A \<subseteq> fps L f"

  1089   shows "\<Sqinter>\<^bsub>fpl L f\<^esub> A .=\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub> A)"

  1090 proof -

  1091   interpret L: weak_complete_lattice "L"

  1092     by (simp_all add: assms)

  1093   interpret L': weak_complete_lattice "fpl L f"

  1094     by (rule Knaster_Tarski, simp_all add: assms)

  1095   have FA: "fps L f \<subseteq> carrier L"

  1096     by (auto simp add: fps_def)

  1097   have A: "A \<subseteq> carrier L"

  1098     using FA assms(5) by blast

  1099   have fA: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> fps L f"

  1100     by (metis (no_types, lifting) A L.idempotent L.inf_closed PiE assms(3) assms(4) fps_def mem_Collect_eq)

  1101   have infA: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> fps L f"

  1102     by (rule L'.inf_closed[simplified], simp add: assms)

  1103   show ?thesis

  1104   proof (rule L.weak_le_antisym)

  1105     show ic: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> carrier L"

  1106       using FA infA by blast

  1107     show fc: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> carrier L"

  1108       using FA fA by blast

  1109     show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>fpl L f\<^esub>A"

  1110     proof -

  1111       have "\<And>x. x \<in> A \<Longrightarrow> f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> x"

  1112         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)

  1113       hence "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<Sqinter>\<^bsub>fpl L f\<^esub>A"

  1114         by (rule_tac L'.inf_greatest, simp_all add: fA assms(3,5))

  1115       thus ?thesis

  1116         by (simp)

  1117     qed

  1118     show "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub>A)"

  1119     proof -

  1120       have "\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>fpl L f\<^esub> x"

  1121         by (rule L'.inf_lower, simp_all add: assms)

  1122       hence "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub>A)"

  1123         apply (rule_tac L.inf_greatest, simp_all add: A)

  1124         using FA infA apply blast

  1125         done

  1126       hence 1:"f(\<Sqinter>\<^bsub>fpl L f\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f(\<Sqinter>\<^bsub>L\<^esub>A)"

  1127         by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)

  1128       have 2:"\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>fpl L f\<^esub>A)"

  1129         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)

  1130

  1131       show ?thesis

  1132         using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)

  1133     qed

  1134   qed

  1135 qed

  1136

  1137 subsection \<open>Examples\<close>

  1138

  1139 subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>

  1140

  1141 theorem powerset_is_complete_lattice:

  1142   "complete_lattice \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>"

  1143   (is "complete_lattice ?L")

  1144 proof (rule partial_order.complete_latticeI)

  1145   show "partial_order ?L"

  1146     by standard auto

  1147 next

  1148   fix B

  1149   assume "B \<subseteq> carrier ?L"

  1150   then have "least ?L (\<Union> B) (Upper ?L B)"

  1151     by (fastforce intro!: least_UpperI simp: Upper_def)

  1152   then show "\<exists>s. least ?L s (Upper ?L B)" ..

  1153 next

  1154   fix B

  1155   assume "B \<subseteq> carrier ?L"

  1156   then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"

  1157     txt \<open>@{term "\<Inter> B"} is not the infimum of @{term B}:

  1158       @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! \<close>

  1159     by (fastforce intro!: greatest_LowerI simp: Lower_def)

  1160   then show "\<exists>i. greatest ?L i (Lower ?L B)" ..

  1161 qed

  1162

  1163 text \<open>Another example, that of the lattice of subgroups of a group,

  1164   can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>

  1165

  1166

  1167 subsection \<open>Limit preserving functions\<close>

  1168

  1169 definition weak_sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where

  1170 "weak_sup_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. A \<noteq> {} \<longrightarrow> f (\<Squnion>\<^bsub>X\<^esub> A) = (\<Squnion>\<^bsub>Y\<^esub> (f  A)))"

  1171

  1172 definition sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where

  1173 "sup_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. f (\<Squnion>\<^bsub>X\<^esub> A) = (\<Squnion>\<^bsub>Y\<^esub> (f  A)))"

  1174

  1175 definition weak_inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where

  1176 "weak_inf_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. A \<noteq> {} \<longrightarrow> f (\<Sqinter>\<^bsub>X\<^esub> A) = (\<Sqinter>\<^bsub>Y\<^esub> (f  A)))"

  1177

  1178 definition inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where

  1179 "inf_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. f (\<Sqinter>\<^bsub>X\<^esub> A) = (\<Sqinter>\<^bsub>Y\<^esub> (f  A)))"

  1180

  1181 lemma weak_sup_pres:

  1182   "sup_pres X Y f \<Longrightarrow> weak_sup_pres X Y f"

  1183   by (simp add: sup_pres_def weak_sup_pres_def)

  1184

  1185 lemma weak_inf_pres:

  1186   "inf_pres X Y f \<Longrightarrow> weak_inf_pres X Y f"

  1187   by (simp add: inf_pres_def weak_inf_pres_def)

  1188

  1189 lemma sup_pres_is_join_pres:

  1190   assumes "weak_sup_pres X Y f"

  1191   shows "join_pres X Y f"

  1192   using assms

  1193   apply (simp add: join_pres_def weak_sup_pres_def, safe)

  1194   apply (rename_tac x y)

  1195   apply (drule_tac x="{x, y}" in spec)

  1196   apply (auto simp add: join_def)

  1197 done

  1198

  1199 lemma inf_pres_is_meet_pres:

  1200   assumes "weak_inf_pres X Y f"

  1201   shows "meet_pres X Y f"

  1202   using assms

  1203   apply (simp add: meet_pres_def weak_inf_pres_def, safe)

  1204   apply (rename_tac x y)

  1205   apply (drule_tac x="{x, y}" in spec)

  1206   apply (auto simp add: meet_def)

  1207 done

  1208

  1209 end