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