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
 ballarin@65099  1 (* Title: HOL/Algebra/Complete_Lattice.thy  ballarin@65099  2  Author: Clemens Ballarin, started 7 November 2003  ballarin@65099  3  Copyright: Clemens Ballarin  ballarin@65099  4 ballarin@65099  5 Most congruence rules by Stephan Hohe.  ballarin@65099  6 With additional contributions from Alasdair Armstrong and Simon Foster.  ballarin@65099  7 *)  ballarin@65099  8 ballarin@65099  9 theory Complete_Lattice  ballarin@66579  10 imports Lattice  ballarin@65099  11 begin  ballarin@65099  12 ballarin@65099  13 section \Complete Lattices\  ballarin@65099  14 ballarin@65099  15 locale weak_complete_lattice = weak_partial_order +  ballarin@65099  16  assumes sup_exists:  wenzelm@67091  17  "[| A \ carrier L |] ==> \s. least L s (Upper L A)"  ballarin@65099  18  and inf_exists:  wenzelm@67091  19  "[| A \ carrier L |] ==> \i. greatest L i (Lower L A)"  ballarin@65099  20 ballarin@65099  21 sublocale weak_complete_lattice \ weak_lattice  ballarin@65099  22 proof  ballarin@65099  23  fix x y  ballarin@65099  24  assume a: "x \ carrier L" "y \ carrier L"  ballarin@65099  25  thus "\s. is_lub L s {x, y}"  ballarin@65099  26  by (rule_tac sup_exists[of "{x, y}"], auto)  ballarin@65099  27  from a show "\s. is_glb L s {x, y}"  ballarin@65099  28  by (rule_tac inf_exists[of "{x, y}"], auto)  ballarin@65099  29 qed  ballarin@65099  30 ballarin@65099  31 text \Introduction rule: the usual definition of complete lattice\  ballarin@65099  32 ballarin@65099  33 lemma (in weak_partial_order) weak_complete_latticeI:  ballarin@65099  34  assumes sup_exists:  wenzelm@67091  35  "!!A. [| A \ carrier L |] ==> \s. least L s (Upper L A)"  ballarin@65099  36  and inf_exists:  wenzelm@67091  37  "!!A. [| A \ carrier L |] ==> \i. greatest L i (Lower L A)"  ballarin@65099  38  shows "weak_complete_lattice L"  ballarin@65099  39  by standard (auto intro: sup_exists inf_exists)  ballarin@65099  40 ballarin@65099  41 lemma (in weak_complete_lattice) dual_weak_complete_lattice:  ballarin@65099  42  "weak_complete_lattice (inv_gorder L)"  ballarin@65099  43 proof -  ballarin@65099  44  interpret dual: weak_lattice "inv_gorder L"  ballarin@65099  45  by (metis dual_weak_lattice)  ballarin@65099  46  show ?thesis  lp15@68488  47  by (unfold_locales) (simp_all add:inf_exists sup_exists)  ballarin@65099  48 qed  ballarin@65099  49 ballarin@65099  50 lemma (in weak_complete_lattice) supI:  ballarin@65099  51  "[| !!l. least L l (Upper L A) ==> P l; A \ carrier L |]  ballarin@65099  52  ==> P (\A)"  ballarin@65099  53 proof (unfold sup_def)  ballarin@65099  54  assume L: "A \ carrier L"  ballarin@65099  55  and P: "!!l. least L l (Upper L A) ==> P l"  ballarin@65099  56  with sup_exists obtain s where "least L s (Upper L A)" by blast  ballarin@65099  57  with L show "P (SOME l. least L l (Upper L A))"  ballarin@65099  58  by (fast intro: someI2 weak_least_unique P)  ballarin@65099  59 qed  ballarin@65099  60 ballarin@65099  61 lemma (in weak_complete_lattice) sup_closed [simp]:  ballarin@65099  62  "A \ carrier L ==> \A \ carrier L"  ballarin@65099  63  by (rule supI) simp_all  ballarin@65099  64 ballarin@65099  65 lemma (in weak_complete_lattice) sup_cong:  ballarin@65099  66  assumes "A \ carrier L" "B \ carrier L" "A {.=} B"  ballarin@65099  67  shows "\ A .= \ B"  ballarin@65099  68 proof -  ballarin@65099  69  have "\ x. is_lub L x A \ is_lub L x B"  ballarin@65099  70  by (rule least_Upper_cong_r, simp_all add: assms)  ballarin@65099  71  moreover have "\ B \ carrier L"  ballarin@65099  72  by (simp add: assms(2))  ballarin@65099  73  ultimately show ?thesis  ballarin@65099  74  by (simp add: sup_def)  ballarin@65099  75 qed  ballarin@65099  76 ballarin@65099  77 sublocale weak_complete_lattice \ weak_bounded_lattice  ballarin@65099  78  apply (unfold_locales)  ballarin@65099  79  apply (metis Upper_empty empty_subsetI sup_exists)  ballarin@65099  80  apply (metis Lower_empty empty_subsetI inf_exists)  ballarin@65099  81 done  ballarin@65099  82 ballarin@65099  83 lemma (in weak_complete_lattice) infI:  ballarin@65099  84  "[| !!i. greatest L i (Lower L A) ==> P i; A \ carrier L |]  ballarin@65099  85  ==> P (\A)"  ballarin@65099  86 proof (unfold inf_def)  ballarin@65099  87  assume L: "A \ carrier L"  ballarin@65099  88  and P: "!!l. greatest L l (Lower L A) ==> P l"  ballarin@65099  89  with inf_exists obtain s where "greatest L s (Lower L A)" by blast  ballarin@65099  90  with L show "P (SOME l. greatest L l (Lower L A))"  ballarin@65099  91  by (fast intro: someI2 weak_greatest_unique P)  ballarin@65099  92 qed  ballarin@65099  93 ballarin@65099  94 lemma (in weak_complete_lattice) inf_closed [simp]:  ballarin@65099  95  "A \ carrier L ==> \A \ carrier L"  ballarin@65099  96  by (rule infI) simp_all  ballarin@65099  97 ballarin@65099  98 lemma (in weak_complete_lattice) inf_cong:  ballarin@65099  99  assumes "A \ carrier L" "B \ carrier L" "A {.=} B"  ballarin@65099  100  shows "\ A .= \ B"  ballarin@65099  101 proof -  ballarin@65099  102  have "\ x. is_glb L x A \ is_glb L x B"  ballarin@65099  103  by (rule greatest_Lower_cong_r, simp_all add: assms)  ballarin@65099  104  moreover have "\ B \ carrier L"  ballarin@65099  105  by (simp add: assms(2))  ballarin@65099  106  ultimately show ?thesis  ballarin@65099  107  by (simp add: inf_def)  ballarin@65099  108 qed  ballarin@65099  109 ballarin@65099  110 theorem (in weak_partial_order) weak_complete_lattice_criterion1:  wenzelm@67091  111  assumes top_exists: "\g. greatest L g (carrier L)"  ballarin@65099  112  and inf_exists:  wenzelm@67091  113  "\A. [| A \ carrier L; A \ {} |] ==> \i. greatest L i (Lower L A)"  ballarin@65099  114  shows "weak_complete_lattice L"  ballarin@65099  115 proof (rule weak_complete_latticeI)  ballarin@65099  116  from top_exists obtain top where top: "greatest L top (carrier L)" ..  ballarin@65099  117  fix A  ballarin@65099  118  assume L: "A \ carrier L"  ballarin@65099  119  let ?B = "Upper L A"  ballarin@65099  120  from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)  wenzelm@67091  121  then have B_non_empty: "?B \ {}" by fast  ballarin@65099  122  have B_L: "?B \ carrier L" by simp  ballarin@65099  123  from inf_exists [OF B_L B_non_empty]  ballarin@65099  124  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..  lp15@68488  125  then have bcarr: "b \ carrier L"  lp15@68488  126  by auto  ballarin@65099  127  have "least L b (Upper L A)"  lp15@68488  128  proof (rule least_UpperI)  lp15@68488  129  show "\x. x \ A \ x \ b"  lp15@68488  130  by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)  lp15@68488  131  show "\y. y \ Upper L A \ b \ y"  lp15@68488  132  by (meson B_L b_inf_B greatest_Lower_below)  lp15@68488  133  qed (use bcarr L in auto)  wenzelm@67091  134  then show "\s. least L s (Upper L A)" ..  ballarin@65099  135 next  ballarin@65099  136  fix A  ballarin@65099  137  assume L: "A \ carrier L"  wenzelm@67091  138  show "\i. greatest L i (Lower L A)"  lp15@68488  139  by (metis L Lower_empty inf_exists top_exists)  ballarin@65099  140 qed  ballarin@65099  141 ballarin@65099  142 ballarin@65099  143 text \Supremum\  ballarin@65099  144 ballarin@65099  145 declare (in partial_order) weak_sup_of_singleton [simp del]  ballarin@65099  146 ballarin@65099  147 lemma (in partial_order) sup_of_singleton [simp]:  ballarin@65099  148  "x \ carrier L ==> \{x} = x"  ballarin@65099  149  using weak_sup_of_singleton unfolding eq_is_equal .  ballarin@65099  150 ballarin@65099  151 lemma (in upper_semilattice) join_assoc_lemma:  ballarin@65099  152  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@65099  153  shows "x \ (y \ z) = \{x, y, z}"  ballarin@65099  154  using weak_join_assoc_lemma L unfolding eq_is_equal .  ballarin@65099  155 ballarin@65099  156 lemma (in upper_semilattice) join_assoc:  ballarin@65099  157  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@65099  158  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@65099  159  using weak_join_assoc L unfolding eq_is_equal .  ballarin@65099  160 ballarin@65099  161 ballarin@65099  162 text \Infimum\  ballarin@65099  163 ballarin@65099  164 declare (in partial_order) weak_inf_of_singleton [simp del]  ballarin@65099  165 ballarin@65099  166 lemma (in partial_order) inf_of_singleton [simp]:  ballarin@65099  167  "x \ carrier L ==> \{x} = x"  ballarin@65099  168  using weak_inf_of_singleton unfolding eq_is_equal .  ballarin@65099  169 ballarin@65099  170 text \Condition on \A\: infimum exists.\  ballarin@65099  171 ballarin@65099  172 lemma (in lower_semilattice) meet_assoc_lemma:  ballarin@65099  173  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@65099  174  shows "x \ (y \ z) = \{x, y, z}"  ballarin@65099  175  using weak_meet_assoc_lemma L unfolding eq_is_equal .  ballarin@65099  176 ballarin@65099  177 lemma (in lower_semilattice) meet_assoc:  ballarin@65099  178  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@65099  179  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@65099  180  using weak_meet_assoc L unfolding eq_is_equal .  ballarin@65099  181 ballarin@65099  182 ballarin@65099  183 subsection \Infimum Laws\  ballarin@65099  184 ballarin@65099  185 context weak_complete_lattice  ballarin@65099  186 begin  ballarin@65099  187 ballarin@65099  188 lemma inf_glb:  ballarin@65099  189  assumes "A \ carrier L"  ballarin@65099  190  shows "greatest L (\A) (Lower L A)"  ballarin@65099  191 proof -  ballarin@65099  192  obtain i where "greatest L i (Lower L A)"  ballarin@65099  193  by (metis assms inf_exists)  ballarin@65099  194  thus ?thesis  lp15@68488  195  by (metis inf_def someI_ex)  ballarin@65099  196 qed  ballarin@65099  197 ballarin@65099  198 lemma inf_lower:  ballarin@65099  199  assumes "A \ carrier L" "x \ A"  ballarin@65099  200  shows "\A \ x"  ballarin@65099  201  by (metis assms greatest_Lower_below inf_glb)  ballarin@65099  202 ballarin@65099  203 lemma inf_greatest:  ballarin@65099  204  assumes "A \ carrier L" "z \ carrier L"  ballarin@65099  205  "(\x. x \ A \ z \ x)"  ballarin@65099  206  shows "z \ \A"  ballarin@65099  207  by (metis Lower_memI assms greatest_le inf_glb)  ballarin@65099  208 ballarin@65099  209 lemma weak_inf_empty [simp]: "\{} .= \"  ballarin@65099  210  by (metis Lower_empty empty_subsetI inf_glb top_greatest weak_greatest_unique)  ballarin@65099  211 ballarin@65099  212 lemma weak_inf_carrier [simp]: "\carrier L .= \"  ballarin@65099  213  by (metis bottom_weak_eq inf_closed inf_lower subset_refl)  ballarin@65099  214 ballarin@65099  215 lemma weak_inf_insert [simp]:  lp15@68488  216  assumes "a \ carrier L" "A \ carrier L"  lp15@68488  217  shows "\insert a A .= a \ \A"  lp15@68488  218 proof (rule weak_le_antisym)  lp15@68488  219  show "\insert a A \ a \ \A"  lp15@68488  220  by (simp add: assms inf_lower local.inf_greatest meet_le)  lp15@68488  221  show aA: "a \ \A \ carrier L"  lp15@68488  222  using assms by simp  lp15@68488  223  show "a \ \A \ \insert a A"  lp15@68488  224  apply (rule inf_greatest)  lp15@68488  225  using assms apply (simp_all add: aA)  lp15@68488  226  by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)  lp15@68488  227  show "\insert a A \ carrier L"  lp15@68488  228  using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)  lp15@68488  229 qed  ballarin@65099  230 ballarin@65099  231 subsection \Supremum Laws\  ballarin@65099  232 ballarin@65099  233 lemma sup_lub:  ballarin@65099  234  assumes "A \ carrier L"  ballarin@65099  235  shows "least L (\A) (Upper L A)"  ballarin@65099  236  by (metis Upper_is_closed assms least_closed least_cong supI sup_closed sup_exists weak_least_unique)  ballarin@65099  237 ballarin@65099  238 lemma sup_upper:  ballarin@65099  239  assumes "A \ carrier L" "x \ A"  ballarin@65099  240  shows "x \ \A"  ballarin@65099  241  by (metis assms least_Upper_above supI)  ballarin@65099  242 ballarin@65099  243 lemma sup_least:  ballarin@65099  244  assumes "A \ carrier L" "z \ carrier L"  ballarin@65099  245  "(\x. x \ A \ x \ z)"  ballarin@65099  246  shows "\A \ z"  ballarin@65099  247  by (metis Upper_memI assms least_le sup_lub)  ballarin@65099  248 ballarin@65099  249 lemma weak_sup_empty [simp]: "\{} .= \"  ballarin@65099  250  by (metis Upper_empty bottom_least empty_subsetI sup_lub weak_least_unique)  ballarin@65099  251 ballarin@65099  252 lemma weak_sup_carrier [simp]: "\carrier L .= \"  ballarin@65099  253  by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)  ballarin@65099  254 ballarin@65099  255 lemma weak_sup_insert [simp]:  lp15@68488  256  assumes "a \ carrier L" "A \ carrier L"  lp15@68488  257  shows "\insert a A .= a \ \A"  lp15@68488  258 proof (rule weak_le_antisym)  lp15@68488  259  show aA: "a \ \A \ carrier L"  lp15@68488  260  using assms by simp  lp15@68488  261  show "\insert a A \ a \ \A"  lp15@68488  262  apply (rule sup_least)  lp15@68488  263  using assms apply (simp_all add: aA)  lp15@68488  264  by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)  lp15@68488  265  show "a \ \A \ \insert a A"  lp15@68488  266  by (simp add: assms join_le local.sup_least sup_upper)  lp15@68488  267  show "\insert a A \ carrier L"  lp15@68488  268  using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)  lp15@68488  269 qed  ballarin@65099  270 ballarin@65099  271 end  ballarin@65099  272 ballarin@65099  273 ballarin@65099  274 subsection \Fixed points of a lattice\  ballarin@65099  275 ballarin@65099  276 definition "fps L f = {x \ carrier L. f x .=\<^bsub>L\<^esub> x}"  ballarin@65099  277 ballarin@65099  278 abbreviation "fpl L f \ L\carrier := fps L f\"  ballarin@65099  279 ballarin@65099  280 lemma (in weak_partial_order)  ballarin@65099  281  use_fps: "x \ fps L f \ f x .= x"  ballarin@65099  282  by (simp add: fps_def)  ballarin@65099  283 ballarin@65099  284 lemma fps_carrier [simp]:  ballarin@65099  285  "fps L f \ carrier L"  ballarin@65099  286  by (auto simp add: fps_def)  ballarin@65099  287 ballarin@65099  288 lemma (in weak_complete_lattice) fps_sup_image:  ballarin@65099  289  assumes "f \ carrier L \ carrier L" "A \ fps L f"  ballarin@65099  290  shows "\ (f  A) .= \ A"  ballarin@65099  291 proof -  ballarin@65099  292  from assms(2) have AL: "A \ carrier L"  ballarin@65099  293  by (auto simp add: fps_def)  ballarin@65099  294  show ?thesis  ballarin@65099  295  proof (rule sup_cong, simp_all add: AL)  ballarin@65099  296  from assms(1) AL show "f  A \ carrier L"  lp15@68488  297  by auto  lp15@68488  298  then have *: "\b. \A \ {x \ carrier L. f x .= x}; b \ A\ \ \a\f  A. b .= a"  lp15@68488  299  by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)  ballarin@65099  300  from assms(2) show "f  A {.=} A"  lp15@68488  301  by (auto simp add: fps_def intro: set_eqI2 [OF _ *])  ballarin@65099  302  qed  ballarin@65099  303 qed  ballarin@65099  304 ballarin@65099  305 lemma (in weak_complete_lattice) fps_idem:  lp15@68488  306  assumes "f \ carrier L \ carrier L" "Idem f"  lp15@68488  307  shows "fps L f {.=} f  carrier L"  lp15@68488  308 proof (rule set_eqI2)  lp15@68488  309  show "\a. a \ fps L f \ \b\f  carrier L. a .= b"  lp15@68488  310  using assms by (force simp add: fps_def intro: local.sym)  lp15@68488  311  show "\b. b \ f  carrier L \ \a\fps L f. b .= a"  lp15@68488  312  using assms by (force simp add: idempotent_def fps_def)  lp15@68488  313 qed  ballarin@65099  314 ballarin@65099  315 context weak_complete_lattice  ballarin@65099  316 begin  ballarin@65099  317 ballarin@65099  318 lemma weak_sup_pre_fixed_point:  ballarin@65099  319  assumes "f \ carrier L \ carrier L" "isotone L L f" "A \ fps L f"  ballarin@65099  320  shows "(\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub> A)"  ballarin@65099  321 proof (rule sup_least)  ballarin@65099  322  from assms(3) show AL: "A \ carrier L"  ballarin@65099  323  by (auto simp add: fps_def)  ballarin@65099  324  thus fA: "f (\A) \ carrier L"  ballarin@65099  325  by (simp add: assms funcset_carrier[of f L L])  ballarin@65099  326  fix x  ballarin@65099  327  assume xA: "x \ A"  ballarin@65099  328  hence "x \ fps L f"  ballarin@65099  329  using assms subsetCE by blast  ballarin@65099  330  hence "f x .=\<^bsub>L\<^esub> x"  ballarin@65099  331  by (auto simp add: fps_def)  ballarin@65099  332  moreover have "f x \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"  ballarin@65099  333  by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA)  ballarin@65099  334  ultimately show "x \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"  ballarin@65099  335  by (meson AL fA assms(1) funcset_carrier le_cong local.refl subsetCE xA)  ballarin@65099  336 qed  ballarin@65099  337 ballarin@65099  338 lemma weak_sup_post_fixed_point:  ballarin@65099  339  assumes "f \ carrier L \ carrier L" "isotone L L f" "A \ fps L f"  ballarin@65099  340  shows "f (\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub> A)"  ballarin@65099  341 proof (rule inf_greatest)  ballarin@65099  342  from assms(3) show AL: "A \ carrier L"  ballarin@65099  343  by (auto simp add: fps_def)  ballarin@65099  344  thus fA: "f (\A) \ carrier L"  ballarin@65099  345  by (simp add: assms funcset_carrier[of f L L])  ballarin@65099  346  fix x  ballarin@65099  347  assume xA: "x \ A"  ballarin@65099  348  hence "x \ fps L f"  ballarin@65099  349  using assms subsetCE by blast  ballarin@65099  350  hence "f x .=\<^bsub>L\<^esub> x"  ballarin@65099  351  by (auto simp add: fps_def)  ballarin@65099  352  moreover have "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> f x"  ballarin@65099  353  by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA)  ballarin@65099  354  ultimately show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> x"  ballarin@65099  355  by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA)  ballarin@65099  356 qed  ballarin@65099  357 ballarin@65099  358 ballarin@65099  359 subsubsection \Least fixed points\  ballarin@65099  360 ballarin@65099  361 lemma LFP_closed [intro, simp]:  ballarin@66580  362  "LFP f \ carrier L"  ballarin@66580  363  by (metis (lifting) LEAST_FP_def inf_closed mem_Collect_eq subsetI)  ballarin@65099  364 ballarin@65099  365 lemma LFP_lowerbound:  ballarin@65099  366  assumes "x \ carrier L" "f x \ x"  ballarin@66580  367  shows "LFP f \ x"  ballarin@66580  368  by (auto intro:inf_lower assms simp add:LEAST_FP_def)  ballarin@65099  369 ballarin@65099  370 lemma LFP_greatest:  ballarin@65099  371  assumes "x \ carrier L"  ballarin@65099  372  "(\u. \ u \ carrier L; f u \ u \ \ x \ u)"  ballarin@66580  373  shows "x \ LFP f"  ballarin@66580  374  by (auto simp add:LEAST_FP_def intro:inf_greatest assms)  ballarin@65099  375 ballarin@65099  376 lemma LFP_lemma2:  ballarin@65099  377  assumes "Mono f" "f \ carrier L \ carrier L"  ballarin@66580  378  shows "f (LFP f) \ LFP f"  lp15@68488  379 proof (rule LFP_greatest)  lp15@68488  380  have f: "\x. x \ carrier L \ f x \ carrier L"  lp15@68488  381  using assms by (auto simp add: Pi_def)  lp15@68488  382  with assms show "f (LFP f) \ carrier L"  lp15@68488  383  by blast  lp15@68488  384  show "\u. \u \ carrier L; f u \ u\ \ f (LFP f) \ u"  lp15@68488  385  by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)  lp15@68488  386 qed  ballarin@65099  387 ballarin@65099  388 lemma LFP_lemma3:  ballarin@65099  389  assumes "Mono f" "f \ carrier L \ carrier L"  ballarin@66580  390  shows "LFP f \ f (LFP f)"  lp15@68488  391  using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)  ballarin@65099  392 ballarin@65099  393 lemma LFP_weak_unfold:  ballarin@66580  394  "\ Mono f; f \ carrier L \ carrier L \ \ LFP f .= f (LFP f)"  ballarin@65099  395  by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)  ballarin@65099  396 ballarin@65099  397 lemma LFP_fixed_point [intro]:  ballarin@65099  398  assumes "Mono f" "f \ carrier L \ carrier L"  ballarin@66580  399  shows "LFP f \ fps L f"  ballarin@65099  400 proof -  ballarin@66580  401  have "f (LFP f) \ carrier L"  ballarin@65099  402  using assms(2) by blast  ballarin@65099  403  with assms show ?thesis  ballarin@65099  404  by (simp add: LFP_weak_unfold fps_def local.sym)  ballarin@65099  405 qed  ballarin@65099  406 ballarin@65099  407 lemma LFP_least_fixed_point:  ballarin@65099  408  assumes "Mono f" "f \ carrier L \ carrier L" "x \ fps L f"  ballarin@66580  409  shows "LFP f \ x"  ballarin@65099  410  using assms by (force intro: LFP_lowerbound simp add: fps_def)  ballarin@65099  411   ballarin@65099  412 lemma LFP_idem:  ballarin@65099  413  assumes "f \ carrier L \ carrier L" "Mono f" "Idem f"  ballarin@66580  414  shows "LFP f .= (f \)"  ballarin@65099  415 proof (rule weak_le_antisym)  ballarin@65099  416  from assms(1) show fb: "f \ \ carrier L"  ballarin@65099  417  by (rule funcset_mem, simp)  ballarin@66580  418  from assms show mf: "LFP f \ carrier L"  ballarin@65099  419  by blast  ballarin@66580  420  show "LFP f \ f \"  ballarin@65099  421  proof -  ballarin@65099  422  have "f (f \) .= f \"  ballarin@65099  423  by (auto simp add: fps_def fb assms(3) idempotent)  ballarin@65099  424  moreover have "f (f \) \ carrier L"  ballarin@65099  425  by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)  ballarin@65099  426  ultimately show ?thesis  ballarin@65099  427  by (auto intro: LFP_lowerbound simp add: fb)  ballarin@65099  428  qed  ballarin@66580  429  show "f \ \ LFP f"  ballarin@65099  430  proof -  ballarin@66580  431  have "f \ \ f (LFP f)"  ballarin@65099  432  by (auto intro: use_iso1[of _ f] simp add: assms)  ballarin@66580  433  moreover have "... .= LFP f"  ballarin@65099  434  using assms(1) assms(2) fps_def by force  ballarin@66580  435  moreover from assms(1) have "f (LFP f) \ carrier L"  ballarin@65099  436  by (auto)  ballarin@65099  437  ultimately show ?thesis  ballarin@65099  438  using fb by blast  ballarin@65099  439  qed  ballarin@65099  440 qed  ballarin@65099  441 ballarin@65099  442 ballarin@65099  443 subsubsection \Greatest fixed points\  ballarin@65099  444   ballarin@65099  445 lemma GFP_closed [intro, simp]:  ballarin@66580  446  "GFP f \ carrier L"  ballarin@66580  447  by (auto intro:sup_closed simp add:GREATEST_FP_def)  ballarin@65099  448   ballarin@65099  449 lemma GFP_upperbound:  ballarin@65099  450  assumes "x \ carrier L" "x \ f x"  ballarin@66580  451  shows "x \ GFP f"  ballarin@66580  452  by (auto intro:sup_upper assms simp add:GREATEST_FP_def)  ballarin@65099  453 ballarin@65099  454 lemma GFP_least:  ballarin@65099  455  assumes "x \ carrier L"  ballarin@65099  456  "(\u. \ u \ carrier L; u \ f u \ \ u \ x)"  ballarin@66580  457  shows "GFP f \ x"  ballarin@66580  458  by (auto simp add:GREATEST_FP_def intro:sup_least assms)  ballarin@65099  459 ballarin@65099  460 lemma GFP_lemma2:  ballarin@65099  461  assumes "Mono f" "f \ carrier L \ carrier L"  ballarin@66580  462  shows "GFP f \ f (GFP f)"  lp15@68488  463 proof (rule GFP_least)  lp15@68488  464  have f: "\x. x \ carrier L \ f x \ carrier L"  lp15@68488  465  using assms by (auto simp add: Pi_def)  lp15@68488  466  with assms show "f (GFP f) \ carrier L"  lp15@68488  467  by blast  lp15@68488  468  show "\u. \u \ carrier L; u \ f u\ \ u \ f (GFP f)"  lp15@68488  469  by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)  lp15@68488  470 qed  ballarin@65099  471 ballarin@65099  472 lemma GFP_lemma3:  ballarin@65099  473  assumes "Mono f" "f \ carrier L \ carrier L"  ballarin@66580  474  shows "f (GFP f) \ GFP f"  ballarin@65099  475  by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)  ballarin@65099  476   ballarin@65099  477 lemma GFP_weak_unfold:  ballarin@66580  478  "\ Mono f; f \ carrier L \ carrier L \ \ GFP f .= f (GFP f)"  ballarin@65099  479  by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)  ballarin@65099  480 ballarin@65099  481 lemma (in weak_complete_lattice) GFP_fixed_point [intro]:  ballarin@65099  482  assumes "Mono f" "f \ carrier L \ carrier L"  ballarin@66580  483  shows "GFP f \ fps L f"  ballarin@65099  484  using assms  ballarin@65099  485 proof -  ballarin@66580  486  have "f (GFP f) \ carrier L"  ballarin@65099  487  using assms(2) by blast  ballarin@65099  488  with assms show ?thesis  ballarin@65099  489  by (simp add: GFP_weak_unfold fps_def local.sym)  ballarin@65099  490 qed  ballarin@65099  491 ballarin@65099  492 lemma GFP_greatest_fixed_point:  ballarin@65099  493  assumes "Mono f" "f \ carrier L \ carrier L" "x \ fps L f"  ballarin@66580  494  shows "x \ GFP f"  ballarin@65099  495  using assms  ballarin@65099  496  by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)  ballarin@65099  497   ballarin@65099  498 lemma GFP_idem:  ballarin@65099  499  assumes "f \ carrier L \ carrier L" "Mono f" "Idem f"  ballarin@66580  500  shows "GFP f .= (f \)"  ballarin@65099  501 proof (rule weak_le_antisym)  ballarin@65099  502  from assms(1) show fb: "f \ \ carrier L"  ballarin@65099  503  by (rule funcset_mem, simp)  ballarin@66580  504  from assms show mf: "GFP f \ carrier L"  ballarin@65099  505  by blast  ballarin@66580  506  show "f \ \ GFP f"  ballarin@65099  507  proof -  ballarin@65099  508  have "f (f \) .= f \"  ballarin@65099  509  by (auto simp add: fps_def fb assms(3) idempotent)  ballarin@65099  510  moreover have "f (f \) \ carrier L"  ballarin@65099  511  by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)  ballarin@65099  512  ultimately show ?thesis  ballarin@65099  513  by (rule_tac GFP_upperbound, simp_all add: fb local.sym)  ballarin@65099  514  qed  ballarin@66580  515  show "GFP f \ f \"  ballarin@65099  516  proof -  ballarin@66580  517  have "GFP f \ f (GFP f)"  ballarin@65099  518  by (simp add: GFP_lemma2 assms(1) assms(2))  ballarin@65099  519  moreover have "... \ f \"  ballarin@65099  520  by (auto intro: use_iso1[of _ f] simp add: assms)  ballarin@66580  521  moreover from assms(1) have "f (GFP f) \ carrier L"  ballarin@65099  522  by (auto)  ballarin@65099  523  ultimately show ?thesis  ballarin@65099  524  using fb local.le_trans by blast  ballarin@65099  525  qed  ballarin@65099  526 qed  ballarin@65099  527 ballarin@65099  528 end  ballarin@65099  529 ballarin@65099  530 wenzelm@67226  531 subsection \Complete lattices where \eq\ is the Equality\  ballarin@65099  532 ballarin@65099  533 locale complete_lattice = partial_order +  ballarin@65099  534  assumes sup_exists:  wenzelm@67091  535  "[| A \ carrier L |] ==> \s. least L s (Upper L A)"  ballarin@65099  536  and inf_exists:  wenzelm@67091  537  "[| A \ carrier L |] ==> \i. greatest L i (Lower L A)"  ballarin@65099  538 ballarin@65099  539 sublocale complete_lattice \ lattice  ballarin@65099  540 proof  ballarin@65099  541  fix x y  ballarin@65099  542  assume a: "x \ carrier L" "y \ carrier L"  ballarin@65099  543  thus "\s. is_lub L s {x, y}"  ballarin@65099  544  by (rule_tac sup_exists[of "{x, y}"], auto)  ballarin@65099  545  from a show "\s. is_glb L s {x, y}"  ballarin@65099  546  by (rule_tac inf_exists[of "{x, y}"], auto)  ballarin@65099  547 qed  ballarin@65099  548 ballarin@65099  549 sublocale complete_lattice \ weak?: weak_complete_lattice  ballarin@65099  550  by standard (auto intro: sup_exists inf_exists)  ballarin@65099  551 ballarin@65099  552 lemma complete_lattice_lattice [simp]:  ballarin@65099  553  assumes "complete_lattice X"  ballarin@65099  554  shows "lattice X"  ballarin@65099  555 proof -  ballarin@65099  556  interpret c: complete_lattice X  ballarin@65099  557  by (simp add: assms)  ballarin@65099  558  show ?thesis  ballarin@65099  559  by (unfold_locales)  ballarin@65099  560 qed  ballarin@65099  561 ballarin@65099  562 text \Introduction rule: the usual definition of complete lattice\  ballarin@65099  563 ballarin@65099  564 lemma (in partial_order) complete_latticeI:  ballarin@65099  565  assumes sup_exists:  wenzelm@67091  566  "!!A. [| A \ carrier L |] ==> \s. least L s (Upper L A)"  ballarin@65099  567  and inf_exists:  wenzelm@67091  568  "!!A. [| A \ carrier L |] ==> \i. greatest L i (Lower L A)"  ballarin@65099  569  shows "complete_lattice L"  ballarin@65099  570  by standard (auto intro: sup_exists inf_exists)  ballarin@65099  571 ballarin@65099  572 theorem (in partial_order) complete_lattice_criterion1:  wenzelm@67091  573  assumes top_exists: "\g. greatest L g (carrier L)"  ballarin@65099  574  and inf_exists:  wenzelm@67091  575  "!!A. [| A \ carrier L; A \ {} |] ==> \i. greatest L i (Lower L A)"  ballarin@65099  576  shows "complete_lattice L"  ballarin@65099  577 proof (rule complete_latticeI)  ballarin@65099  578  from top_exists obtain top where top: "greatest L top (carrier L)" ..  ballarin@65099  579  fix A  ballarin@65099  580  assume L: "A \ carrier L"  ballarin@65099  581  let ?B = "Upper L A"  ballarin@65099  582  from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)  wenzelm@67091  583  then have B_non_empty: "?B \ {}" by fast  ballarin@65099  584  have B_L: "?B \ carrier L" by simp  ballarin@65099  585  from inf_exists [OF B_L B_non_empty]  ballarin@65099  586  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..  lp15@68488  587  then have bcarr: "b \ carrier L"  lp15@68488  588  by blast  ballarin@65099  589  have "least L b (Upper L A)"  lp15@68488  590  proof (rule least_UpperI)  lp15@68488  591  show "\x. x \ A \ x \ b"  lp15@68488  592  by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)  lp15@68488  593  show "\y. y \ Upper L A \ b \ y"  lp15@68488  594  by (auto elim: greatest_Lower_below [OF b_inf_B])  lp15@68488  595  qed (use L bcarr in auto)  wenzelm@67091  596  then show "\s. least L s (Upper L A)" ..  ballarin@65099  597 next  ballarin@65099  598  fix A  ballarin@65099  599  assume L: "A \ carrier L"  wenzelm@67091  600  show "\i. greatest L i (Lower L A)"  ballarin@65099  601  proof (cases "A = {}")  ballarin@65099  602  case True then show ?thesis  ballarin@65099  603  by (simp add: top_exists)  ballarin@65099  604  next  ballarin@65099  605  case False with L show ?thesis  ballarin@65099  606  by (rule inf_exists)  ballarin@65099  607  qed  ballarin@65099  608 qed  ballarin@65099  609 ballarin@65099  610 (* TODO: prove dual version *)  ballarin@65099  611 ballarin@65099  612 subsection \Fixed points\  ballarin@65099  613 ballarin@65099  614 context complete_lattice  ballarin@65099  615 begin  ballarin@65099  616 ballarin@65099  617 lemma LFP_unfold:  ballarin@66580  618  "\ Mono f; f \ carrier L \ carrier L \ \ LFP f = f (LFP f)"  ballarin@65099  619  using eq_is_equal weak.LFP_weak_unfold by auto  ballarin@65099  620 ballarin@65099  621 lemma LFP_const:  ballarin@66580  622  "t \ carrier L \ LFP (\ x. t) = t"  ballarin@65099  623  by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)  ballarin@65099  624 ballarin@65099  625 lemma LFP_id:  ballarin@66580  626  "LFP id = \"  ballarin@65099  627  by (simp add: local.le_antisym weak.LFP_lowerbound)  ballarin@65099  628 ballarin@65099  629 lemma GFP_unfold:  ballarin@66580  630  "\ Mono f; f \ carrier L \ carrier L \ \ GFP f = f (GFP f)"  ballarin@65099  631  using eq_is_equal weak.GFP_weak_unfold by auto  ballarin@65099  632 ballarin@65099  633 lemma GFP_const:  ballarin@66580  634  "t \ carrier L \ GFP (\ x. t) = t"  ballarin@65099  635  by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)  ballarin@65099  636 ballarin@65099  637 lemma GFP_id:  ballarin@66580  638  "GFP id = \"  ballarin@65099  639  using weak.GFP_upperbound by auto  ballarin@65099  640 ballarin@65099  641 end  ballarin@65099  642 ballarin@65099  643 ballarin@65099  644 subsection \Interval complete lattices\  ballarin@65099  645   ballarin@65099  646 context weak_complete_lattice  ballarin@65099  647 begin  ballarin@65099  648 lp15@68488  649  lemma at_least_at_most_Sup: "\ a \ carrier L; b \ carrier L; a \ b \ \ \ \a..b\ .= b"  lp15@68488  650  by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)  ballarin@65099  651 lp15@68488  652  lemma at_least_at_most_Inf: "\ a \ carrier L; b \ carrier L; a \ b \ \ \ \a..b\ .= a"  lp15@68488  653  by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)  ballarin@65099  654 ballarin@65099  655 end  ballarin@65099  656 ballarin@65099  657 lemma weak_complete_lattice_interval:  ballarin@65099  658  assumes "weak_complete_lattice L" "a \ carrier L" "b \ carrier L" "a \\<^bsub>L\<^esub> b"  ballarin@65099  659  shows "weak_complete_lattice (L \ carrier := \a..b\\<^bsub>L\<^esub> \)"  ballarin@65099  660 proof -  ballarin@65099  661  interpret L: weak_complete_lattice L  ballarin@65099  662  by (simp add: assms)  ballarin@65099  663  interpret weak_partial_order "L \ carrier := \a..b\\<^bsub>L\<^esub> \"  ballarin@65099  664  proof -  ballarin@65099  665  have "\a..b\\<^bsub>L\<^esub> \ carrier L"  lp15@68488  666  by (auto simp add: at_least_at_most_def)  ballarin@65099  667  thus "weak_partial_order (L\carrier := \a..b\\<^bsub>L\<^esub>\)"  ballarin@65099  668  by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)  ballarin@65099  669  qed  ballarin@65099  670 ballarin@65099  671  show ?thesis  ballarin@65099  672  proof  ballarin@65099  673  fix A  ballarin@65099  674  assume a: "A \ carrier (L\carrier := \a..b\\<^bsub>L\<^esub>\)"  ballarin@65099  675  show "\s. is_lub (L\carrier := \a..b\\<^bsub>L\<^esub>\) s A"  ballarin@65099  676  proof (cases "A = {}")  ballarin@65099  677  case True  ballarin@65099  678  thus ?thesis  ballarin@65099  679  by (rule_tac x="a" in exI, auto simp add: least_def assms)  ballarin@65099  680  next  ballarin@65099  681  case False  ballarin@65099  682  show ?thesis  ballarin@65099  683  proof (rule_tac x="\\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)  ballarin@65099  684  show b:"\ x. x \ A \ x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"  ballarin@65099  685  using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)  ballarin@65099  686  show "\y. y \ Upper (L\carrier := \a..b\\<^bsub>L\<^esub>\) A \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> y"  ballarin@65099  687  using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)  ballarin@65099  688  from a show "A \ \a..b\\<^bsub>L\<^esub>"  ballarin@65099  689  by (auto)  ballarin@65099  690  from a show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>"  ballarin@65099  691  apply (rule_tac L.at_least_at_most_member)  ballarin@65099  692  apply (auto)  ballarin@65099  693  apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)  ballarin@65099  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)  ballarin@65099  695  apply (rule L.sup_least)  ballarin@65099  696  apply (auto simp add: assms)  ballarin@65099  697  using L.at_least_at_most_closed apply blast  ballarin@65099  698  done  ballarin@65099  699  qed  ballarin@65099  700  qed  ballarin@65099  701  show "\s. is_glb (L\carrier := \a..b\\<^bsub>L\<^esub>\) s A"  ballarin@65099  702  proof (cases "A = {}")  ballarin@65099  703  case True  ballarin@65099  704  thus ?thesis  ballarin@65099  705  by (rule_tac x="b" in exI, auto simp add: greatest_def assms)  ballarin@65099  706  next  ballarin@65099  707  case False  ballarin@65099  708  show ?thesis  ballarin@65099  709  proof (rule_tac x="\\<^bsub>L\<^esub> A" in exI, rule greatest_LowerI, simp_all)  ballarin@65099  710  show b:"\x. x \ A \ \\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> x"  ballarin@65099  711  using a L.at_least_at_most_closed by (force intro!: L.inf_lower)  ballarin@65099  712  show "\y. y \ Lower (L\carrier := \a..b\\<^bsub>L\<^esub>\) A \ y \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"  ballarin@65099  713  using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)  ballarin@65099  714  from a show "A \ \a..b\\<^bsub>L\<^esub>"  ballarin@65099  715  by (auto)  ballarin@65099  716  from a show "\\<^bsub>L\<^esub>A \ \a..b\\<^bsub>L\<^esub>"  ballarin@65099  717  apply (rule_tac L.at_least_at_most_member)  ballarin@65099  718  apply (auto)  ballarin@65099  719  apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)  ballarin@65099  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)  ballarin@65099  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)  ballarin@65099  722  done  ballarin@65099  723  qed  ballarin@65099  724  qed  ballarin@65099  725  qed  ballarin@65099  726 qed  ballarin@65099  727 ballarin@65099  728 ballarin@65099  729 subsection \Knaster-Tarski theorem and variants\  ballarin@65099  730   ballarin@65099  731 text \The set of fixed points of a complete lattice is itself a complete lattice\  ballarin@65099  732 ballarin@65099  733 theorem Knaster_Tarski:  ballarin@65099  734  assumes "weak_complete_lattice L" "f \ carrier L \ carrier L" "isotone L L f"  ballarin@65099  735  shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")  ballarin@65099  736 proof -  ballarin@65099  737  interpret L: weak_complete_lattice L  ballarin@65099  738  by (simp add: assms)  ballarin@65099  739  interpret weak_partial_order ?L'  ballarin@65099  740  proof -  ballarin@65099  741  have "{x \ carrier L. f x .=\<^bsub>L\<^esub> x} \ carrier L"  ballarin@65099  742  by (auto)  ballarin@65099  743  thus "weak_partial_order ?L'"  ballarin@65099  744  by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)  ballarin@65099  745  qed  ballarin@65099  746  show ?thesis  ballarin@65099  747  proof (unfold_locales, simp_all)  ballarin@65099  748  fix A  ballarin@65099  749  assume A: "A \ fps L f"  ballarin@65099  750  show "\s. is_lub (fpl L f) s A"  ballarin@65099  751  proof  ballarin@65099  752  from A have AL: "A \ carrier L"  ballarin@65099  753  by (meson fps_carrier subset_eq)  ballarin@65099  754 ballarin@65099  755  let ?w = "\\<^bsub>L\<^esub> A"  ballarin@65099  756  have w: "f (\\<^bsub>L\<^esub>A) \ carrier L"  ballarin@65099  757  by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2))  ballarin@65099  758 ballarin@65099  759  have pf_w: "(\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub> A)"  ballarin@65099  760  by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3))  ballarin@65099  761 ballarin@65099  762  have f_top_chain: "f  \?w..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \ \?w..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>"  ballarin@65099  763  proof (auto simp add: at_least_at_most_def)  ballarin@65099  764  fix x  ballarin@65099  765  assume b: "x \ carrier L" "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> x"  ballarin@65099  766  from b show fx: "f x \ carrier L"  ballarin@65099  767  using assms(2) by blast  ballarin@65099  768  show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> f x"  ballarin@65099  769  proof -  ballarin@65099  770  have "?w \\<^bsub>L\<^esub> f ?w"  ballarin@65099  771  proof (rule_tac L.sup_least, simp_all add: AL w)  ballarin@65099  772  fix y  ballarin@65099  773  assume c: "y \ A"  ballarin@65099  774  hence y: "y \ fps L f"  ballarin@65099  775  using A subsetCE by blast  ballarin@65099  776  with assms have "y .=\<^bsub>L\<^esub> f y"  ballarin@65099  777  proof -  ballarin@65099  778  from y have "y \ carrier L"  ballarin@65099  779  by (simp add: fps_def)  ballarin@65099  780  moreover hence "f y \ carrier L"  ballarin@65099  781  by (rule_tac funcset_mem[of f "carrier L"], simp_all add: assms)  ballarin@65099  782  ultimately show ?thesis using y  ballarin@65099  783  by (rule_tac L.sym, simp_all add: L.use_fps)  ballarin@65099  784  qed  ballarin@65099  785  moreover have "y \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"  ballarin@65099  786  by (simp add: AL L.sup_upper c(1))  ballarin@65099  787  ultimately show "y \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"  ballarin@65099  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)  ballarin@65099  789  qed  ballarin@65099  790  thus ?thesis  ballarin@65099  791  by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) b(1) b(2) use_iso2)  ballarin@65099  792  qed  ballarin@65099  793   ballarin@65099  794  show "f x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>"  ballarin@65099  795  by (simp add: fx)  ballarin@65099  796  qed  ballarin@65099  797   ballarin@65099  798  let ?L' = "L\ carrier := \?w..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \"  ballarin@65099  799 ballarin@65099  800  interpret L': weak_complete_lattice ?L'  ballarin@65099  801  by (auto intro: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)  ballarin@65099  802 ballarin@65099  803  let ?L'' = "L\ carrier := fps L f \"  ballarin@65099  804 ballarin@66580  805  show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"  ballarin@65099  806  proof (rule least_UpperI, simp_all)  ballarin@65099  807  fix x  ballarin@65099  808  assume "x \ Upper ?L'' A"  ballarin@66580  809  hence "LFP\<^bsub>?L'\<^esub> f \\<^bsub>?L'\<^esub> x"  ballarin@65099  810  apply (rule_tac L'.LFP_lowerbound)  ballarin@65099  811  apply (auto simp add: Upper_def)  ballarin@65099  812  apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)  ballarin@65099  813  apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)  ballarin@65099  814  apply (auto)  ballarin@65099  815  apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))  ballarin@65099  816  done  ballarin@66580  817  thus " LFP\<^bsub>?L'\<^esub> f \\<^bsub>L\<^esub> x"  ballarin@65099  818  by (simp)  ballarin@65099  819  next  ballarin@65099  820  fix x  ballarin@65099  821  assume xA: "x \ A"  ballarin@66580  822  show "x \\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"  ballarin@65099  823  proof -  ballarin@66580  824  have "LFP\<^bsub>?L'\<^esub> f \ carrier ?L'"  ballarin@65099  825  by blast  ballarin@65099  826  thus ?thesis  ballarin@65099  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)  ballarin@65099  828  qed  ballarin@65099  829  next  ballarin@65099  830  show "A \ fps L f"  ballarin@65099  831  by (simp add: A)  ballarin@65099  832  next  ballarin@66580  833  show "LFP\<^bsub>?L'\<^esub> f \ fps L f"  ballarin@65099  834  proof (auto simp add: fps_def)  ballarin@66580  835  have "LFP\<^bsub>?L'\<^esub> f \ carrier ?L'"  ballarin@65099  836  by (rule L'.LFP_closed)  ballarin@66580  837  thus c:"LFP\<^bsub>?L'\<^esub> f \ carrier L"  ballarin@65099  838  by (auto simp add: at_least_at_most_def)  ballarin@66580  839  have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"  ballarin@65099  840  proof (rule "L'.LFP_weak_unfold", simp_all)  ballarin@65099  841  show "f \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>"  ballarin@65099  842  apply (auto simp add: Pi_def at_least_at_most_def)  ballarin@65099  843  using assms(2) apply blast  ballarin@65099  844  apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)  ballarin@65099  845  using assms(2) apply blast  ballarin@65099  846  done  ballarin@65099  847  from assms(3) show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>\\<^esub> f"  ballarin@65099  848  apply (auto simp add: isotone_def)  ballarin@65099  849  using L'.weak_partial_order_axioms apply blast  ballarin@65099  850  apply (meson L.at_least_at_most_closed subsetCE)  ballarin@65099  851  done  ballarin@65099  852  qed  ballarin@66580  853  thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"  ballarin@65099  854  by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)  ballarin@65099  855  qed  ballarin@65099  856  qed  ballarin@65099  857  qed  ballarin@65099  858  show "\i. is_glb (L\carrier := fps L f\) i A"  ballarin@65099  859  proof  ballarin@65099  860  from A have AL: "A \ carrier L"  ballarin@65099  861  by (meson fps_carrier subset_eq)  ballarin@65099  862 ballarin@65099  863  let ?w = "\\<^bsub>L\<^esub> A"  ballarin@65099  864  have w: "f (\\<^bsub>L\<^esub>A) \ carrier L"  ballarin@65099  865  by (simp add: AL funcset_carrier' assms(2))  ballarin@65099  866 ballarin@65099  867  have pf_w: "f (\\<^bsub>L\<^esub> A) \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub> A)"  ballarin@65099  868  by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3))  ballarin@65099  869 ballarin@65099  870  have f_bot_chain: "f  \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>"  ballarin@65099  871  proof (auto simp add: at_least_at_most_def)  ballarin@65099  872  fix x  ballarin@65099  873  assume b: "x \ carrier L" "x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"  ballarin@65099  874  from b show fx: "f x \ carrier L"  ballarin@65099  875  using assms(2) by blast  ballarin@65099  876  show "f x \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A"  ballarin@65099  877  proof -  ballarin@65099  878  have "f ?w \\<^bsub>L\<^esub> ?w"  ballarin@65099  879  proof (rule_tac L.inf_greatest, simp_all add: AL w)  ballarin@65099  880  fix y  ballarin@65099  881  assume c: "y \ A"  ballarin@65099  882  with assms have "y .=\<^bsub>L\<^esub> f y"  ballarin@65099  883  by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq)  ballarin@65099  884  moreover have "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> y"  ballarin@65099  885  by (simp add: AL L.inf_lower c)  ballarin@65099  886  ultimately show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> y"  ballarin@65099  887  by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)  ballarin@65099  888  qed  ballarin@65099  889  thus ?thesis  ballarin@65099  890  by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)  ballarin@65099  891  qed  ballarin@65099  892   ballarin@65099  893  show "\\<^bsub>L\<^esub> \\<^bsub>L\<^esub> f x"  ballarin@65099  894  by (simp add: fx)  ballarin@65099  895  qed  ballarin@65099  896   ballarin@65099  897  let ?L' = "L\ carrier := \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \"  ballarin@65099  898 ballarin@65099  899  interpret L': weak_complete_lattice ?L'  ballarin@65099  900  by (auto intro!: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)  ballarin@65099  901 ballarin@65099  902  let ?L'' = "L\ carrier := fps L f \"  ballarin@65099  903 ballarin@66580  904  show "is_glb ?L'' (GFP\<^bsub>?L'\<^esub> f) A"  ballarin@65099  905  proof (rule greatest_LowerI, simp_all)  ballarin@65099  906  fix x  ballarin@65099  907  assume "x \ Lower ?L'' A"  ballarin@66580  908  hence "x \\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"  ballarin@65099  909  apply (rule_tac L'.GFP_upperbound)  ballarin@65099  910  apply (auto simp add: Lower_def)  ballarin@65099  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)  ballarin@65099  912  apply (simp add: funcset_carrier' L.sym assms(2) fps_def)  ballarin@65099  913  done  ballarin@66580  914  thus "x \\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"  ballarin@65099  915  by (simp)  ballarin@65099  916  next  ballarin@65099  917  fix x  ballarin@65099  918  assume xA: "x \ A"  ballarin@66580  919  show "GFP\<^bsub>?L'\<^esub> f \\<^bsub>L\<^esub> x"  ballarin@65099  920  proof -  ballarin@66580  921  have "GFP\<^bsub>?L'\<^esub> f \ carrier ?L'"  ballarin@65099  922  by blast  ballarin@65099  923  thus ?thesis  ballarin@65099  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)  ballarin@65099  925  qed  ballarin@65099  926  next  ballarin@65099  927  show "A \ fps L f"  ballarin@65099  928  by (simp add: A)  ballarin@65099  929  next  ballarin@66580  930  show "GFP\<^bsub>?L'\<^esub> f \ fps L f"  ballarin@65099  931  proof (auto simp add: fps_def)  ballarin@66580  932  have "GFP\<^bsub>?L'\<^esub> f \ carrier ?L'"  ballarin@65099  933  by (rule L'.GFP_closed)  ballarin@66580  934  thus c:"GFP\<^bsub>?L'\<^esub> f \ carrier L"  ballarin@65099  935  by (auto simp add: at_least_at_most_def)  ballarin@66580  936  have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"  ballarin@65099  937  proof (rule "L'.GFP_weak_unfold", simp_all)  ballarin@65099  938  show "f \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub> \ \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>"  ballarin@65099  939  apply (auto simp add: Pi_def at_least_at_most_def)  ballarin@65099  940  using assms(2) apply blast  ballarin@65099  941  apply (simp add: funcset_carrier' assms(2))  ballarin@65099  942  apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)  ballarin@65099  943  done  ballarin@65099  944  from assms(3) show "Mono\<^bsub>L\carrier := \\\<^bsub>L\<^esub>..?w\\<^bsub>L\<^esub>\\<^esub> f"  ballarin@65099  945  apply (auto simp add: isotone_def)  ballarin@65099  946  using L'.weak_partial_order_axioms apply blast  ballarin@65099  947  using L.at_least_at_most_closed apply (blast intro: funcset_carrier')  ballarin@65099  948  done  ballarin@65099  949  qed  ballarin@66580  950  thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"  ballarin@65099  951  by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)  ballarin@65099  952  qed  ballarin@65099  953  qed  ballarin@65099  954  qed  ballarin@65099  955  qed  ballarin@65099  956 qed  ballarin@65099  957 ballarin@65099  958 theorem Knaster_Tarski_top:  ballarin@65099  959  assumes "weak_complete_lattice L" "isotone L L f" "f \ carrier L \ carrier L"  ballarin@66580  960  shows "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"  ballarin@65099  961 proof -  ballarin@65099  962  interpret L: weak_complete_lattice L  ballarin@65099  963  by (simp add: assms)  ballarin@65099  964  interpret L': weak_complete_lattice "fpl L f"  ballarin@65099  965  by (rule Knaster_Tarski, simp_all add: assms)  ballarin@65099  966  show ?thesis  ballarin@65099  967  proof (rule L.weak_le_antisym, simp_all)  ballarin@66580  968  show "\\<^bsub>fpl L f\<^esub> \\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"  ballarin@65099  969  by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])  ballarin@66580  970  show "GFP\<^bsub>L\<^esub> f \\<^bsub>L\<^esub> \\<^bsub>fpl L f\<^esub>"  ballarin@65099  971  proof -  ballarin@66580  972  have "GFP\<^bsub>L\<^esub> f \ fps L f"  ballarin@65099  973  by (rule L.GFP_fixed_point, simp_all add: assms)  ballarin@66580  974  hence "GFP\<^bsub>L\<^esub> f \ carrier (fpl L f)"  ballarin@65099  975  by simp  ballarin@66580  976  hence "GFP\<^bsub>L\<^esub> f \\<^bsub>fpl L f\<^esub> \\<^bsub>fpl L f\<^esub>"  ballarin@65099  977  by (rule L'.top_higher)  ballarin@65099  978  thus ?thesis  ballarin@65099  979  by simp  ballarin@65099  980  qed  ballarin@65099  981  show "\\<^bsub>fpl L f\<^esub> \ carrier L"  ballarin@65099  982  proof -  ballarin@65099  983  have "carrier (fpl L f) \ carrier L"  ballarin@65099  984  by (auto simp add: fps_def)  ballarin@65099  985  with L'.top_closed show ?thesis  ballarin@65099  986  by blast  ballarin@65099  987  qed  ballarin@65099  988  qed  ballarin@65099  989 qed  ballarin@65099  990 ballarin@65099  991 theorem Knaster_Tarski_bottom:  ballarin@65099  992  assumes "weak_complete_lattice L" "isotone L L f" "f \ carrier L \ carrier L"  ballarin@66580  993  shows "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"  ballarin@65099  994 proof -  ballarin@65099  995  interpret L: weak_complete_lattice L  ballarin@65099  996  by (simp add: assms)  ballarin@65099  997  interpret L': weak_complete_lattice "fpl L f"  ballarin@65099  998  by (rule Knaster_Tarski, simp_all add: assms)  ballarin@65099  999  show ?thesis  ballarin@65099  1000  proof (rule L.weak_le_antisym, simp_all)  ballarin@66580  1001  show "LFP\<^bsub>L\<^esub> f \\<^bsub>L\<^esub> \\<^bsub>fpl L f\<^esub>"  ballarin@65099  1002  by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])  ballarin@66580  1003  show "\\<^bsub>fpl L f\<^esub> \\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"  ballarin@65099  1004  proof -  ballarin@66580  1005  have "LFP\<^bsub>L\<^esub> f \ fps L f"  ballarin@65099  1006  by (rule L.LFP_fixed_point, simp_all add: assms)  ballarin@66580  1007  hence "LFP\<^bsub>L\<^esub> f \ carrier (fpl L f)"  ballarin@65099  1008  by simp  ballarin@66580  1009  hence "\\<^bsub>fpl L f\<^esub> \\<^bsub>fpl L f\<^esub> LFP\<^bsub>L\<^esub> f"  ballarin@65099  1010  by (rule L'.bottom_lower)  ballarin@65099  1011  thus ?thesis  ballarin@65099  1012  by simp  ballarin@65099  1013  qed  ballarin@65099  1014  show "\\<^bsub>fpl L f\<^esub> \ carrier L"  ballarin@65099  1015  proof -  ballarin@65099  1016  have "carrier (fpl L f) \ carrier L"  ballarin@65099  1017  by (auto simp add: fps_def)  ballarin@65099  1018  with L'.bottom_closed show ?thesis  ballarin@65099  1019  by blast  ballarin@65099  1020  qed  ballarin@65099  1021  qed  ballarin@65099  1022 qed  ballarin@65099  1023 ballarin@65099  1024 text \If a function is both idempotent and isotone then the image of the function forms a complete lattice\  ballarin@65099  1025   ballarin@65099  1026 theorem Knaster_Tarski_idem:  ballarin@65099  1027  assumes "complete_lattice L" "f \ carrier L \ carrier L" "isotone L L f" "idempotent L f"  ballarin@65099  1028  shows "complete_lattice (L\carrier := f  carrier L\)"  ballarin@65099  1029 proof -  ballarin@65099  1030  interpret L: complete_lattice L  ballarin@65099  1031  by (simp add: assms)  ballarin@65099  1032  have "fps L f = f  carrier L"  ballarin@65099  1033  using L.weak.fps_idem[OF assms(2) assms(4)]  ballarin@65099  1034  by (simp add: L.set_eq_is_eq)  ballarin@65099  1035  then interpret L': weak_complete_lattice "(L\carrier := f  carrier L\)"  ballarin@65099  1036  by (metis Knaster_Tarski L.weak.weak_complete_lattice_axioms assms(2) assms(3))  ballarin@65099  1037  show ?thesis  ballarin@65099  1038  using L'.sup_exists L'.inf_exists  ballarin@65099  1039  by (unfold_locales, auto simp add: L.eq_is_equal)  ballarin@65099  1040 qed  ballarin@65099  1041 ballarin@65099  1042 theorem Knaster_Tarski_idem_extremes:  ballarin@65099  1043  assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \ carrier L \ carrier L"  ballarin@65099  1044  shows "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)" "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)"  ballarin@65099  1045 proof -  ballarin@65099  1046  interpret L: weak_complete_lattice "L"  ballarin@65099  1047  by (simp_all add: assms)  ballarin@65099  1048  interpret L': weak_complete_lattice "fpl L f"  ballarin@65099  1049  by (rule Knaster_Tarski, simp_all add: assms)  ballarin@65099  1050  have FA: "fps L f \ carrier L"  ballarin@65099  1051  by (auto simp add: fps_def)  ballarin@65099  1052  show "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)"  ballarin@65099  1053  proof -  ballarin@65099  1054  from FA have "\\<^bsub>fpl L f\<^esub> \ carrier L"  ballarin@65099  1055  proof -  ballarin@65099  1056  have "\\<^bsub>fpl L f\<^esub> \ fps L f"  ballarin@65099  1057  using L'.top_closed by auto  ballarin@65099  1058  thus ?thesis  ballarin@65099  1059  using FA by blast  ballarin@65099  1060  qed  ballarin@65099  1061  moreover with assms have "f \\<^bsub>L\<^esub> \ carrier L"  ballarin@65099  1062  by (auto)  ballarin@65099  1063 ballarin@65099  1064  ultimately show ?thesis  ballarin@65099  1065  using L.trans[OF Knaster_Tarski_top[of L f] L.GFP_idem[of f]]  ballarin@65099  1066  by (simp_all add: assms)  ballarin@65099  1067  qed  ballarin@65099  1068  show "\\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>)"  ballarin@65099  1069  proof -  ballarin@65099  1070  from FA have "\\<^bsub>fpl L f\<^esub> \ carrier L"  ballarin@65099  1071  proof -  ballarin@65099  1072  have "\\<^bsub>fpl L f\<^esub> \ fps L f"  ballarin@65099  1073  using L'.bottom_closed by auto  ballarin@65099  1074  thus ?thesis  ballarin@65099  1075  using FA by blast  ballarin@65099  1076  qed  ballarin@65099  1077  moreover with assms have "f \\<^bsub>L\<^esub> \ carrier L"  ballarin@65099  1078  by (auto)  ballarin@65099  1079 ballarin@65099  1080  ultimately show ?thesis  ballarin@65099  1081  using L.trans[OF Knaster_Tarski_bottom[of L f] L.LFP_idem[of f]]  ballarin@65099  1082  by (simp_all add: assms)  ballarin@65099  1083  qed  ballarin@65099  1084 qed  ballarin@65099  1085 ballarin@66187  1086 theorem Knaster_Tarski_idem_inf_eq:  ballarin@66187  1087  assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \ carrier L \ carrier L"  ballarin@66187  1088  "A \ fps L f"  ballarin@66187  1089  shows "\\<^bsub>fpl L f\<^esub> A .=\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub> A)"  ballarin@66187  1090 proof -  ballarin@66187  1091  interpret L: weak_complete_lattice "L"  ballarin@66187  1092  by (simp_all add: assms)  ballarin@66187  1093  interpret L': weak_complete_lattice "fpl L f"  ballarin@66187  1094  by (rule Knaster_Tarski, simp_all add: assms)  ballarin@66187  1095  have FA: "fps L f \ carrier L"  ballarin@66187  1096  by (auto simp add: fps_def)  ballarin@66187  1097  have A: "A \ carrier L"  ballarin@66187  1098  using FA assms(5) by blast  ballarin@66187  1099  have fA: "f (\\<^bsub>L\<^esub>A) \ fps L f"  ballarin@66187  1100  by (metis (no_types, lifting) A L.idempotent L.inf_closed PiE assms(3) assms(4) fps_def mem_Collect_eq)  ballarin@66187  1101  have infA: "\\<^bsub>fpl L f\<^esub>A \ fps L f"  ballarin@66187  1102  by (rule L'.inf_closed[simplified], simp add: assms)  ballarin@66187  1103  show ?thesis  ballarin@66187  1104  proof (rule L.weak_le_antisym)  ballarin@66187  1105  show ic: "\\<^bsub>fpl L f\<^esub>A \ carrier L"  ballarin@66187  1106  using FA infA by blast  ballarin@66187  1107  show fc: "f (\\<^bsub>L\<^esub>A) \ carrier L"  ballarin@66187  1108  using FA fA by blast  ballarin@66187  1109  show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> \\<^bsub>fpl L f\<^esub>A"  ballarin@66187  1110  proof -  ballarin@66187  1111  have "\x. x \ A \ f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> x"  ballarin@66187  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)  ballarin@66187  1113  hence "f (\\<^bsub>L\<^esub>A) \\<^bsub>fpl L f\<^esub> \\<^bsub>fpl L f\<^esub>A"  ballarin@66187  1114  by (rule_tac L'.inf_greatest, simp_all add: fA assms(3,5))  ballarin@66187  1115  thus ?thesis  ballarin@66187  1116  by (simp)  ballarin@66187  1117  qed  ballarin@66187  1118  show "\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> f (\\<^bsub>L\<^esub>A)"  ballarin@66187  1119  proof -  ballarin@66187  1120  have "\x. x \ A \ \\<^bsub>fpl L f\<^esub>A \\<^bsub>fpl L f\<^esub> x"  ballarin@66187  1121  by (rule L'.inf_lower, simp_all add: assms)  ballarin@66187  1122  hence "\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> (\\<^bsub>L\<^esub>A)"  ballarin@66187  1123  apply (rule_tac L.inf_greatest, simp_all add: A)  ballarin@66187  1124  using FA infA apply blast  ballarin@66187  1125  done  ballarin@66187  1126  hence 1:"f(\\<^bsub>fpl L f\<^esub>A) \\<^bsub>L\<^esub> f(\\<^bsub>L\<^esub>A)"  ballarin@66187  1127  by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)  ballarin@66187  1128  have 2:"\\<^bsub>fpl L f\<^esub>A \\<^bsub>L\<^esub> f (\\<^bsub>fpl L f\<^esub>A)"  ballarin@66187  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)  ballarin@66187  1130   ballarin@66187  1131  show ?thesis  ballarin@66187  1132  using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)  ballarin@66187  1133  qed  ballarin@66187  1134  qed  ballarin@66187  1135 qed  ballarin@65099  1136 ballarin@65099  1137 subsection \Examples\  ballarin@65099  1138 ballarin@65099  1139 subsubsection \The Powerset of a Set is a Complete Lattice\  ballarin@65099  1140 ballarin@65099  1141 theorem powerset_is_complete_lattice:  nipkow@67399  1142  "complete_lattice \carrier = Pow A, eq = (=), le = (\)\"  ballarin@65099  1143  (is "complete_lattice ?L")  ballarin@65099  1144 proof (rule partial_order.complete_latticeI)  ballarin@65099  1145  show "partial_order ?L"  ballarin@65099  1146  by standard auto  ballarin@65099  1147 next  ballarin@65099  1148  fix B  ballarin@65099  1149  assume "B \ carrier ?L"  ballarin@65099  1150  then have "least ?L (\ B) (Upper ?L B)"  ballarin@65099  1151  by (fastforce intro!: least_UpperI simp: Upper_def)  wenzelm@67091  1152  then show "\s. least ?L s (Upper ?L B)" ..  ballarin@65099  1153 next  ballarin@65099  1154  fix B  ballarin@65099  1155  assume "B \ carrier ?L"  ballarin@65099  1156  then have "greatest ?L (\ B \ A) (Lower ?L B)"  ballarin@65099  1157  txt \@{term "\ B"} is not the infimum of @{term B}:  ballarin@65099  1158  @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! \  ballarin@65099  1159  by (fastforce intro!: greatest_LowerI simp: Lower_def)  wenzelm@67091  1160  then show "\i. greatest ?L i (Lower ?L B)" ..  ballarin@65099  1161 qed  ballarin@65099  1162 ballarin@66579  1163 text \Another example, that of the lattice of subgroups of a group,  ballarin@66579  1164  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\  ballarin@65099  1165 ballarin@65099  1166 ballarin@65099  1167 subsection \Limit preserving functions\  ballarin@65099  1168 ballarin@65099  1169 definition weak_sup_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where  ballarin@65099  1170 "weak_sup_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. A \ {} \ f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f  A)))"  ballarin@65099  1171 ballarin@65099  1172 definition sup_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where  ballarin@65099  1173 "sup_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f  A)))"  ballarin@65099  1174 ballarin@65099  1175 definition weak_inf_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where  ballarin@65099  1176 "weak_inf_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. A \ {} \ f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f  A)))"  ballarin@65099  1177 ballarin@65099  1178 definition inf_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where  ballarin@65099  1179 "inf_pres X Y f \ complete_lattice X \ complete_lattice Y \ (\ A \ carrier X. f (\\<^bsub>X\<^esub> A) = (\\<^bsub>Y\<^esub> (f  A)))"  ballarin@65099  1180 ballarin@65099  1181 lemma weak_sup_pres:  ballarin@65099  1182  "sup_pres X Y f \ weak_sup_pres X Y f"  ballarin@65099  1183  by (simp add: sup_pres_def weak_sup_pres_def)  ballarin@65099  1184 ballarin@65099  1185 lemma weak_inf_pres:  ballarin@65099  1186  "inf_pres X Y f \ weak_inf_pres X Y f"  ballarin@65099  1187  by (simp add: inf_pres_def weak_inf_pres_def)  ballarin@65099  1188 ballarin@65099  1189 lemma sup_pres_is_join_pres:  ballarin@65099  1190  assumes "weak_sup_pres X Y f"  ballarin@65099  1191  shows "join_pres X Y f"  ballarin@65099  1192  using assms  ballarin@65099  1193  apply (simp add: join_pres_def weak_sup_pres_def, safe)  ballarin@65099  1194  apply (rename_tac x y)  ballarin@65099  1195  apply (drule_tac x="{x, y}" in spec)  ballarin@65099  1196  apply (auto simp add: join_def)  ballarin@65099  1197 done  ballarin@65099  1198 ballarin@65099  1199 lemma inf_pres_is_meet_pres:  ballarin@65099  1200  assumes "weak_inf_pres X Y f"  ballarin@65099  1201  shows "meet_pres X Y f"  ballarin@65099  1202  using assms  ballarin@65099  1203  apply (simp add: meet_pres_def weak_inf_pres_def, safe)  ballarin@65099  1204  apply (rename_tac x y)  ballarin@65099  1205  apply (drule_tac x="{x, y}" in spec)  ballarin@65099  1206  apply (auto simp add: meet_def)  ballarin@65099  1207 done  ballarin@65099  1208 ballarin@65099  1209 end