src/HOL/Algebra/Complete_Lattice.thy
author paulson <lp15@cam.ac.uk>
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