src/HOL/Algebra/Lattice.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 67443 3abf6a722518
child 69700 7a92cbec7030
permissions -rw-r--r--
More on Algebra by Paulo and Martin
     1 (*  Title:      HOL/Algebra/Lattice.thy
     2     Author:     Clemens Ballarin, started 7 November 2003
     3     Copyright:  Clemens Ballarin
     4 
     5 Most congruence rules by Stephan Hohe.
     6 With additional contributions from Alasdair Armstrong and Simon Foster.
     7 *)
     8 
     9 theory Lattice
    10 imports Order
    11 begin
    12 
    13 section \<open>Lattices\<close>
    14   
    15 subsection \<open>Supremum and infimum\<close>
    16 
    17 definition
    18   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    19   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
    20 
    21 definition
    22   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
    23   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
    24 
    25 definition supr :: 
    26   "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
    27   where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)"
    28 
    29 definition infi :: 
    30   "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
    31   where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
    32 
    33 syntax
    34   "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10)
    35   "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10)
    36   "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
    37   "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
    38 
    39 translations
    40   "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
    41   "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
    42   "SSUP\<^bsub>L\<^esub> x. B"     == "CONST supr L CONST UNIV (%x. B)"
    43   "SSUP\<^bsub>L\<^esub> x:A. B"   == "CONST supr L A (%x. B)"
    44 
    45 definition
    46   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    47   where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
    48 
    49 definition
    50   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
    51   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
    52 
    53 definition
    54   LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
    55   "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    \<comment> \<open>least fixed point\<close>
    56 
    57 definition
    58   GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
    59   "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    \<comment> \<open>greatest fixed point\<close>
    60 
    61 
    62 subsection \<open>Dual operators\<close>
    63 
    64 lemma sup_dual [simp]: 
    65   "\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A"
    66   by (simp add: sup_def inf_def)
    67 
    68 lemma inf_dual [simp]: 
    69   "\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A"
    70   by (simp add: sup_def inf_def)
    71 
    72 lemma join_dual [simp]:
    73   "p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q"
    74   by (simp add:join_def meet_def)
    75 
    76 lemma meet_dual [simp]:
    77   "p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q"
    78   by (simp add:join_def meet_def)
    79 
    80 lemma top_dual [simp]:
    81   "\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>"
    82   by (simp add: top_def bottom_def)
    83 
    84 lemma bottom_dual [simp]:
    85   "\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>"
    86   by (simp add: top_def bottom_def)
    87 
    88 lemma LFP_dual [simp]:
    89   "LEAST_FP (inv_gorder L) f = GREATEST_FP L f"
    90   by (simp add:LEAST_FP_def GREATEST_FP_def)
    91 
    92 lemma GFP_dual [simp]:
    93   "GREATEST_FP (inv_gorder L) f = LEAST_FP L f"
    94   by (simp add:LEAST_FP_def GREATEST_FP_def)
    95 
    96 
    97 subsection \<open>Lattices\<close>
    98 
    99 locale weak_upper_semilattice = weak_partial_order +
   100   assumes sup_of_two_exists:
   101     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})"
   102 
   103 locale weak_lower_semilattice = weak_partial_order +
   104   assumes inf_of_two_exists:
   105     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})"
   106 
   107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
   108 
   109 lemma (in weak_lattice) dual_weak_lattice:
   110   "weak_lattice (inv_gorder L)"
   111 proof -
   112   interpret dual: weak_partial_order "inv_gorder L"
   113     by (metis dual_weak_order)
   114 
   115   show ?thesis
   116     apply (unfold_locales)
   117     apply (simp_all add: inf_of_two_exists sup_of_two_exists)
   118   done
   119 qed
   120 
   121 
   122 subsubsection \<open>Supremum\<close>
   123 
   124 lemma (in weak_upper_semilattice) joinI:
   125   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   126   ==> P (x \<squnion> y)"
   127 proof (unfold join_def sup_def)
   128   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   129     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   130   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   131   with L show "P (SOME l. least L l (Upper L {x, y}))"
   132     by (fast intro: someI2 P)
   133 qed
   134 
   135 lemma (in weak_upper_semilattice) join_closed [simp]:
   136   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   137   by (rule joinI) (rule least_closed)
   138 
   139 lemma (in weak_upper_semilattice) join_cong_l:
   140   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   141     and xx': "x .= x'"
   142   shows "x \<squnion> y .= x' \<squnion> y"
   143 proof (rule joinI, rule joinI)
   144   fix a b
   145   from xx' carr
   146       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   147 
   148   assume leasta: "least L a (Upper L {x, y})"
   149   assume "least L b (Upper L {x', y})"
   150   with carr
   151       have leastb: "least L b (Upper L {x, y})"
   152       by (simp add: least_Upper_cong_r[OF _ _ seq])
   153 
   154   from leasta leastb
   155       show "a .= b" by (rule weak_least_unique)
   156 qed (rule carr)+
   157 
   158 lemma (in weak_upper_semilattice) join_cong_r:
   159   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   160     and yy': "y .= y'"
   161   shows "x \<squnion> y .= x \<squnion> y'"
   162 proof (rule joinI, rule joinI)
   163   fix a b
   164   have "{x, y} = {y, x}" by fast
   165   also from carr yy'
   166       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   167   also have "{y', x} = {x, y'}" by fast
   168   finally
   169       have seq: "{x, y} {.=} {x, y'}" .
   170 
   171   assume leasta: "least L a (Upper L {x, y})"
   172   assume "least L b (Upper L {x, y'})"
   173   with carr
   174       have leastb: "least L b (Upper L {x, y})"
   175       by (simp add: least_Upper_cong_r[OF _ _ seq])
   176 
   177   from leasta leastb
   178       show "a .= b" by (rule weak_least_unique)
   179 qed (rule carr)+
   180 
   181 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   182   "x \<in> carrier L ==> least L x (Upper L {x})"
   183   by (rule least_UpperI) auto
   184 
   185 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
   186   "x \<in> carrier L ==> \<Squnion>{x} .= x"
   187   unfolding sup_def
   188   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
   189 
   190 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
   191   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
   192   unfolding sup_def
   193   by (rule someI2) (auto intro: sup_of_singletonI)
   194 
   195 text \<open>Condition on \<open>A\<close>: supremum exists.\<close>
   196 
   197 lemma (in weak_upper_semilattice) sup_insertI:
   198   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   199   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   200   ==> P (\<Squnion>(insert x A))"
   201 proof (unfold sup_def)
   202   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   203     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   204     and least_a: "least L a (Upper L A)"
   205   from L least_a have La: "a \<in> carrier L" by simp
   206   from L sup_of_two_exists least_a
   207   obtain s where least_s: "least L s (Upper L {a, x})" by blast
   208   show "P (SOME l. least L l (Upper L (insert x A)))"
   209   proof (rule someI2)
   210     show "least L s (Upper L (insert x A))"
   211     proof (rule least_UpperI)
   212       fix z
   213       assume "z \<in> insert x A"
   214       then show "z \<sqsubseteq> s"
   215       proof
   216         assume "z = x" then show ?thesis
   217           by (simp add: least_Upper_above [OF least_s] L La)
   218       next
   219         assume "z \<in> A"
   220         with L least_s least_a show ?thesis
   221           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
   222       qed
   223     next
   224       fix y
   225       assume y: "y \<in> Upper L (insert x A)"
   226       show "s \<sqsubseteq> y"
   227       proof (rule least_le [OF least_s], rule Upper_memI)
   228         fix z
   229         assume z: "z \<in> {a, x}"
   230         then show "z \<sqsubseteq> y"
   231         proof
   232           have y': "y \<in> Upper L A"
   233             apply (rule subsetD [where A = "Upper L (insert x A)"])
   234              apply (rule Upper_antimono)
   235              apply blast
   236             apply (rule y)
   237             done
   238           assume "z = a"
   239           with y' least_a show ?thesis by (fast dest: least_le)
   240         next
   241           assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
   242           with y L show ?thesis by blast
   243         qed
   244       qed (rule Upper_closed [THEN subsetD, OF y])
   245     next
   246       from L show "insert x A \<subseteq> carrier L" by simp
   247       from least_s show "s \<in> carrier L" by simp
   248     qed
   249   qed (rule P)
   250 qed
   251 
   252 lemma (in weak_upper_semilattice) finite_sup_least:
   253   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> least L (\<Squnion>A) (Upper L A)"
   254 proof (induct set: finite)
   255   case empty
   256   then show ?case by simp
   257 next
   258   case (insert x A)
   259   show ?case
   260   proof (cases "A = {}")
   261     case True
   262     with insert show ?thesis
   263       by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
   264         (* The above step is hairy; least_cong can make simp loop.
   265         Would want special version of simp to apply least_cong. *)
   266   next
   267     case False
   268     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   269     with _ show ?thesis
   270       by (rule sup_insertI) (simp_all add: insert [simplified])
   271   qed
   272 qed
   273 
   274 lemma (in weak_upper_semilattice) finite_sup_insertI:
   275   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   276     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   277   shows "P (\<Squnion> (insert x A))"
   278 proof (cases "A = {}")
   279   case True with P and xA show ?thesis
   280     by (simp add: finite_sup_least)
   281 next
   282   case False with P and xA show ?thesis
   283     by (simp add: sup_insertI finite_sup_least)
   284 qed
   285 
   286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
   287   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Squnion>A \<in> carrier L"
   288 proof (induct set: finite)
   289   case empty then show ?case by simp
   290 next
   291   case insert then show ?case
   292     by - (rule finite_sup_insertI, simp_all)
   293 qed
   294 
   295 lemma (in weak_upper_semilattice) join_left:
   296   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   297   by (rule joinI [folded join_def]) (blast dest: least_mem)
   298 
   299 lemma (in weak_upper_semilattice) join_right:
   300   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   301   by (rule joinI [folded join_def]) (blast dest: least_mem)
   302 
   303 lemma (in weak_upper_semilattice) sup_of_two_least:
   304   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   305 proof (unfold sup_def)
   306   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   307   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   308   with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
   309   by (fast intro: someI2 weak_least_unique)  (* blast fails *)
   310 qed
   311 
   312 lemma (in weak_upper_semilattice) join_le:
   313   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   314     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   315   shows "x \<squnion> y \<sqsubseteq> z"
   316 proof (rule joinI [OF _ x y])
   317   fix s
   318   assume "least L s (Upper L {x, y})"
   319   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   320 qed
   321 
   322 lemma (in weak_lattice) weak_le_iff_meet:
   323   assumes "x \<in> carrier L" "y \<in> carrier L"
   324   shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y"
   325   by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)
   326   
   327 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   328   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   329   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
   330 proof (rule finite_sup_insertI)
   331   \<comment> \<open>The textbook argument in Jacobson I, p 457\<close>
   332   fix s
   333   assume sup: "least L s (Upper L {x, y, z})"
   334   show "x \<squnion> (y \<squnion> z) .= s"
   335   proof (rule weak_le_antisym)
   336     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   337       by (fastforce intro!: join_le elim: least_Upper_above)
   338   next
   339     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   340     by (erule_tac least_le)
   341       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
   342   qed (simp_all add: L least_closed [OF sup])
   343 qed (simp_all add: L)
   344 
   345 text \<open>Commutativity holds for \<open>=\<close>.\<close>
   346 
   347 lemma join_comm:
   348   fixes L (structure)
   349   shows "x \<squnion> y = y \<squnion> x"
   350   by (unfold join_def) (simp add: insert_commute)
   351 
   352 lemma (in weak_upper_semilattice) weak_join_assoc:
   353   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   354   shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
   355 proof -
   356   (* FIXME: could be simplified by improved simp: uniform use of .=,
   357      omit [symmetric] in last step. *)
   358   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   359   also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
   360   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
   361   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
   362   finally show ?thesis by (simp add: L)
   363 qed
   364 
   365 
   366 subsubsection \<open>Infimum\<close>
   367 
   368 lemma (in weak_lower_semilattice) meetI:
   369   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   370   x \<in> carrier L; y \<in> carrier L |]
   371   ==> P (x \<sqinter> y)"
   372 proof (unfold meet_def inf_def)
   373   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   374     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   375   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   376   with L show "P (SOME g. greatest L g (Lower L {x, y}))"
   377   by (fast intro: someI2 weak_greatest_unique P)
   378 qed
   379 
   380 lemma (in weak_lower_semilattice) meet_closed [simp]:
   381   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   382   by (rule meetI) (rule greatest_closed)
   383 
   384 lemma (in weak_lower_semilattice) meet_cong_l:
   385   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   386     and xx': "x .= x'"
   387   shows "x \<sqinter> y .= x' \<sqinter> y"
   388 proof (rule meetI, rule meetI)
   389   fix a b
   390   from xx' carr
   391       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   392 
   393   assume greatesta: "greatest L a (Lower L {x, y})"
   394   assume "greatest L b (Lower L {x', y})"
   395   with carr
   396       have greatestb: "greatest L b (Lower L {x, y})"
   397       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
   398 
   399   from greatesta greatestb
   400       show "a .= b" by (rule weak_greatest_unique)
   401 qed (rule carr)+
   402 
   403 lemma (in weak_lower_semilattice) meet_cong_r:
   404   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   405     and yy': "y .= y'"
   406   shows "x \<sqinter> y .= x \<sqinter> y'"
   407 proof (rule meetI, rule meetI)
   408   fix a b
   409   have "{x, y} = {y, x}" by fast
   410   also from carr yy'
   411       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   412   also have "{y', x} = {x, y'}" by fast
   413   finally
   414       have seq: "{x, y} {.=} {x, y'}" .
   415 
   416   assume greatesta: "greatest L a (Lower L {x, y})"
   417   assume "greatest L b (Lower L {x, y'})"
   418   with carr
   419       have greatestb: "greatest L b (Lower L {x, y})"
   420       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
   421 
   422   from greatesta greatestb
   423       show "a .= b" by (rule weak_greatest_unique)
   424 qed (rule carr)+
   425 
   426 lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   427   "x \<in> carrier L ==> greatest L x (Lower L {x})"
   428   by (rule greatest_LowerI) auto
   429 
   430 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
   431   "x \<in> carrier L ==> \<Sqinter>{x} .= x"
   432   unfolding inf_def
   433   by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
   434 
   435 lemma (in weak_partial_order) inf_of_singleton_closed:
   436   "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
   437   unfolding inf_def
   438   by (rule someI2) (auto intro: inf_of_singletonI)
   439 
   440 text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
   441 
   442 lemma (in weak_lower_semilattice) inf_insertI:
   443   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   444   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   445   ==> P (\<Sqinter>(insert x A))"
   446 proof (unfold inf_def)
   447   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   448     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
   449     and greatest_a: "greatest L a (Lower L A)"
   450   from L greatest_a have La: "a \<in> carrier L" by simp
   451   from L inf_of_two_exists greatest_a
   452   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   453   show "P (SOME g. greatest L g (Lower L (insert x A)))"
   454   proof (rule someI2)
   455     show "greatest L i (Lower L (insert x A))"
   456     proof (rule greatest_LowerI)
   457       fix z
   458       assume "z \<in> insert x A"
   459       then show "i \<sqsubseteq> z"
   460       proof
   461         assume "z = x" then show ?thesis
   462           by (simp add: greatest_Lower_below [OF greatest_i] L La)
   463       next
   464         assume "z \<in> A"
   465         with L greatest_i greatest_a show ?thesis
   466           by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
   467       qed
   468     next
   469       fix y
   470       assume y: "y \<in> Lower L (insert x A)"
   471       show "y \<sqsubseteq> i"
   472       proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   473         fix z
   474         assume z: "z \<in> {a, x}"
   475         then show "y \<sqsubseteq> z"
   476         proof
   477           have y': "y \<in> Lower L A"
   478             apply (rule subsetD [where A = "Lower L (insert x A)"])
   479             apply (rule Lower_antimono)
   480              apply blast
   481             apply (rule y)
   482             done
   483           assume "z = a"
   484           with y' greatest_a show ?thesis by (fast dest: greatest_le)
   485         next
   486           assume "z \<in> {x}"
   487           with y L show ?thesis by blast
   488         qed
   489       qed (rule Lower_closed [THEN subsetD, OF y])
   490     next
   491       from L show "insert x A \<subseteq> carrier L" by simp
   492       from greatest_i show "i \<in> carrier L" by simp
   493     qed
   494   qed (rule P)
   495 qed
   496 
   497 lemma (in weak_lower_semilattice) finite_inf_greatest:
   498   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   499 proof (induct set: finite)
   500   case empty then show ?case by simp
   501 next
   502   case (insert x A)
   503   show ?case
   504   proof (cases "A = {}")
   505     case True
   506     with insert show ?thesis
   507       by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
   508         inf_of_singleton_closed inf_of_singletonI)
   509   next
   510     case False
   511     from insert show ?thesis
   512     proof (rule_tac inf_insertI)
   513       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
   514     qed simp_all
   515   qed
   516 qed
   517 
   518 lemma (in weak_lower_semilattice) finite_inf_insertI:
   519   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   520     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   521   shows "P (\<Sqinter> (insert x A))"
   522 proof (cases "A = {}")
   523   case True with P and xA show ?thesis
   524     by (simp add: finite_inf_greatest)
   525 next
   526   case False with P and xA show ?thesis
   527     by (simp add: inf_insertI finite_inf_greatest)
   528 qed
   529 
   530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
   531   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Sqinter>A \<in> carrier L"
   532 proof (induct set: finite)
   533   case empty then show ?case by simp
   534 next
   535   case insert then show ?case
   536     by (rule_tac finite_inf_insertI) (simp_all)
   537 qed
   538 
   539 lemma (in weak_lower_semilattice) meet_left:
   540   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   541   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   542 
   543 lemma (in weak_lower_semilattice) meet_right:
   544   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   545   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   546 
   547 lemma (in weak_lower_semilattice) inf_of_two_greatest:
   548   "[| x \<in> carrier L; y \<in> carrier L |] ==>
   549   greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
   550 proof (unfold inf_def)
   551   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   552   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   553   with L
   554   show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
   555   by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
   556 qed
   557 
   558 lemma (in weak_lower_semilattice) meet_le:
   559   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   560     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   561   shows "z \<sqsubseteq> x \<sqinter> y"
   562 proof (rule meetI [OF _ x y])
   563   fix i
   564   assume "greatest L i (Lower L {x, y})"
   565   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   566 qed
   567 
   568 lemma (in weak_lattice) weak_le_iff_join:
   569   assumes "x \<in> carrier L" "y \<in> carrier L"
   570   shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)"
   571   by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl)
   572   
   573 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
   574   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   575   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
   576 proof (rule finite_inf_insertI)
   577   txt \<open>The textbook argument in Jacobson I, p 457\<close>
   578   fix i
   579   assume inf: "greatest L i (Lower L {x, y, z})"
   580   show "x \<sqinter> (y \<sqinter> z) .= i"
   581   proof (rule weak_le_antisym)
   582     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   583       by (fastforce intro!: meet_le elim: greatest_Lower_below)
   584   next
   585     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
   586     by (erule_tac greatest_le)
   587       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
   588   qed (simp_all add: L greatest_closed [OF inf])
   589 qed (simp_all add: L)
   590 
   591 lemma meet_comm:
   592   fixes L (structure)
   593   shows "x \<sqinter> y = y \<sqinter> x"
   594   by (unfold meet_def) (simp add: insert_commute)
   595 
   596 lemma (in weak_lower_semilattice) weak_meet_assoc:
   597   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   598   shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
   599 proof -
   600   (* FIXME: improved simp, see weak_join_assoc above *)
   601   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   602   also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
   603   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
   604   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   605   finally show ?thesis by (simp add: L)
   606 qed
   607 
   608 text \<open>Total orders are lattices.\<close>
   609 
   610 sublocale weak_total_order \<subseteq> weak?: weak_lattice
   611 proof
   612   fix x y
   613   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   614   show "\<exists>s. least L s (Upper L {x, y})"
   615   proof -
   616     note total L
   617     moreover
   618     {
   619       assume "x \<sqsubseteq> y"
   620       with L have "least L y (Upper L {x, y})"
   621         by (rule_tac least_UpperI) auto
   622     }
   623     moreover
   624     {
   625       assume "y \<sqsubseteq> x"
   626       with L have "least L x (Upper L {x, y})"
   627         by (rule_tac least_UpperI) auto
   628     }
   629     ultimately show ?thesis by blast
   630   qed
   631 next
   632   fix x y
   633   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   634   show "\<exists>i. greatest L i (Lower L {x, y})"
   635   proof -
   636     note total L
   637     moreover
   638     {
   639       assume "y \<sqsubseteq> x"
   640       with L have "greatest L y (Lower L {x, y})"
   641         by (rule_tac greatest_LowerI) auto
   642     }
   643     moreover
   644     {
   645       assume "x \<sqsubseteq> y"
   646       with L have "greatest L x (Lower L {x, y})"
   647         by (rule_tac greatest_LowerI) auto
   648     }
   649     ultimately show ?thesis by blast
   650   qed
   651 qed
   652 
   653 
   654 subsection \<open>Weak Bounded Lattices\<close>
   655 
   656 locale weak_bounded_lattice = 
   657   weak_lattice + 
   658   weak_partial_order_bottom + 
   659   weak_partial_order_top
   660 begin
   661 
   662 lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>"
   663   by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)
   664 
   665 lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x"
   666   by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)
   667 
   668 lemma bottom_weak_eq:
   669   "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>"
   670   by (metis bottom_closed bottom_lower weak_le_antisym)
   671 
   672 lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>"
   673   by (metis join_closed join_left top_closed top_higher weak_le_antisym)
   674 
   675 lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x"
   676   by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)
   677 
   678 lemma top_weak_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>"
   679   by (metis top_closed top_higher weak_le_antisym)
   680 
   681 end
   682 
   683 sublocale weak_bounded_lattice \<subseteq> weak_partial_order ..
   684 
   685 
   686 subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close>
   687 
   688 locale upper_semilattice = partial_order +
   689   assumes sup_of_two_exists:
   690     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})"
   691 
   692 sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice
   693   by unfold_locales (rule sup_of_two_exists)
   694 
   695 locale lower_semilattice = partial_order +
   696   assumes inf_of_two_exists:
   697     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})"
   698 
   699 sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice
   700   by unfold_locales (rule inf_of_two_exists)
   701 
   702 locale lattice = upper_semilattice + lower_semilattice
   703 
   704 sublocale lattice \<subseteq> weak_lattice ..
   705 
   706 lemma (in lattice) dual_lattice:
   707   "lattice (inv_gorder L)"
   708 proof -
   709   interpret dual: weak_lattice "inv_gorder L"
   710     by (metis dual_weak_lattice)
   711 
   712   show ?thesis
   713     apply (unfold_locales)
   714     apply (simp_all add: inf_of_two_exists sup_of_two_exists)
   715     apply (simp add:eq_is_equal)
   716   done
   717 qed
   718   
   719 lemma (in lattice) le_iff_join:
   720   assumes "x \<in> carrier L" "y \<in> carrier L"
   721   shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)"
   722   by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)
   723 
   724 lemma (in lattice) le_iff_meet:
   725   assumes "x \<in> carrier L" "y \<in> carrier L"
   726   shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y"
   727   by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)
   728 
   729 text \<open> Total orders are lattices. \<close>
   730 
   731 sublocale total_order \<subseteq> weak?: lattice
   732   by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)
   733     
   734 text \<open>Functions that preserve joins and meets\<close>
   735   
   736 definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   737 "join_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<squnion>\<^bsub>X\<^esub> y) = f x \<squnion>\<^bsub>Y\<^esub> f y)"
   738 
   739 definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   740 "meet_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<sqinter>\<^bsub>X\<^esub> y) = f x \<sqinter>\<^bsub>Y\<^esub> f y)"
   741 
   742 lemma join_pres_isotone:
   743   assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f"
   744   shows "isotone X Y f"
   745   using assms
   746   apply (rule_tac isotoneI)
   747   apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)
   748   using lattice_def partial_order_def upper_semilattice_def apply blast
   749   using lattice_def partial_order_def upper_semilattice_def apply blast
   750   apply fastforce
   751 done
   752 
   753 lemma meet_pres_isotone:
   754   assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f"
   755   shows "isotone X Y f"
   756   using assms
   757   apply (rule_tac isotoneI)
   758   apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)
   759   using lattice_def partial_order_def upper_semilattice_def apply blast
   760   using lattice_def partial_order_def upper_semilattice_def apply blast
   761   apply fastforce
   762 done
   763 
   764 
   765 subsection \<open>Bounded Lattices\<close>
   766 
   767 locale bounded_lattice = 
   768   lattice + 
   769   weak_partial_order_bottom + 
   770   weak_partial_order_top
   771 
   772 sublocale bounded_lattice \<subseteq> weak_bounded_lattice ..
   773 
   774 context bounded_lattice
   775 begin
   776 
   777 lemma bottom_eq:  
   778   "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>"
   779   by (metis bottom_closed bottom_lower le_antisym)
   780 
   781 lemma top_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>"
   782   by (metis le_antisym top_closed top_higher)
   783 
   784 end
   785 
   786 end