src/HOL/Algebra/Lattice.thy
author ballarin
Fri May 14 19:29:22 2004 +0200 (2004-05-14)
changeset 14751 0d7850e27fed
parent 14706 71590b7733b7
child 15328 35951e6a7855
permissions -rw-r--r--
Change of theory hierarchy: Group is now based in Lattice.
     1 (*
     2   Title:     HOL/Algebra/Lattice.thy
     3   Id:        $Id$
     4   Author:    Clemens Ballarin, started 7 November 2003
     5   Copyright: Clemens Ballarin
     6 *)
     7 
     8 header {* Orders and Lattices *}
     9 
    10 theory Lattice = Main:
    11 
    12 text {* Object with a carrier set. *}
    13 
    14 record 'a partial_object =
    15   carrier :: "'a set"
    16 
    17 subsection {* Partial Orders *}
    18 
    19 record 'a order = "'a partial_object" +
    20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    21 
    22 locale partial_order = struct L +
    23   assumes refl [intro, simp]:
    24                   "x \<in> carrier L ==> x \<sqsubseteq> x"
    25     and anti_sym [intro]:
    26                   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    27     and trans [trans]:
    28                   "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
    29                    x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    30 
    31 constdefs (structure L)
    32   less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    33   "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    34 
    35   -- {* Upper and lower bounds of a set. *}
    36   Upper :: "[_, 'a set] => 'a set"
    37   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
    38                 carrier L"
    39 
    40   Lower :: "[_, 'a set] => 'a set"
    41   "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
    42                 carrier L"
    43 
    44   -- {* Least and greatest, as predicate. *}
    45   least :: "[_, 'a, 'a set] => bool"
    46   "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    47 
    48   greatest :: "[_, 'a, 'a set] => bool"
    49   "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    50 
    51   -- {* Supremum and infimum *}
    52   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    53   "\<Squnion>A == THE x. least L x (Upper L A)"
    54 
    55   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
    56   "\<Sqinter>A == THE x. greatest L x (Lower L A)"
    57 
    58   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    59   "x \<squnion> y == sup L {x, y}"
    60 
    61   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
    62   "x \<sqinter> y == inf L {x, y}"
    63 
    64 
    65 subsubsection {* Upper *}
    66 
    67 lemma Upper_closed [intro, simp]:
    68   "Upper L A \<subseteq> carrier L"
    69   by (unfold Upper_def) clarify
    70 
    71 lemma UpperD [dest]:
    72   includes struct L
    73   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
    74   by (unfold Upper_def) blast
    75 
    76 lemma Upper_memI:
    77   includes struct L
    78   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
    79   by (unfold Upper_def) blast
    80 
    81 lemma Upper_antimono:
    82   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
    83   by (unfold Upper_def) blast
    84 
    85 
    86 subsubsection {* Lower *}
    87 
    88 lemma Lower_closed [intro, simp]:
    89   "Lower L A \<subseteq> carrier L"
    90   by (unfold Lower_def) clarify
    91 
    92 lemma LowerD [dest]:
    93   includes struct L
    94   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
    95   by (unfold Lower_def) blast
    96 
    97 lemma Lower_memI:
    98   includes struct L
    99   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   100   by (unfold Lower_def) blast
   101 
   102 lemma Lower_antimono:
   103   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   104   by (unfold Lower_def) blast
   105 
   106 
   107 subsubsection {* least *}
   108 
   109 lemma least_carrier [intro, simp]:
   110   shows "least L l A ==> l \<in> carrier L"
   111   by (unfold least_def) fast
   112 
   113 lemma least_mem:
   114   "least L l A ==> l \<in> A"
   115   by (unfold least_def) fast
   116 
   117 lemma (in partial_order) least_unique:
   118   "[| least L x A; least L y A |] ==> x = y"
   119   by (unfold least_def) blast
   120 
   121 lemma least_le:
   122   includes struct L
   123   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   124   by (unfold least_def) fast
   125 
   126 lemma least_UpperI:
   127   includes struct L
   128   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   129     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   130     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   131   shows "least L s (Upper L A)"
   132 proof -
   133   have "Upper L A \<subseteq> carrier L" by simp
   134   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   135   moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   136   ultimately show ?thesis by (simp add: least_def)
   137 qed
   138 
   139 
   140 subsubsection {* greatest *}
   141 
   142 lemma greatest_carrier [intro, simp]:
   143   shows "greatest L l A ==> l \<in> carrier L"
   144   by (unfold greatest_def) fast
   145 
   146 lemma greatest_mem:
   147   "greatest L l A ==> l \<in> A"
   148   by (unfold greatest_def) fast
   149 
   150 lemma (in partial_order) greatest_unique:
   151   "[| greatest L x A; greatest L y A |] ==> x = y"
   152   by (unfold greatest_def) blast
   153 
   154 lemma greatest_le:
   155   includes struct L
   156   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   157   by (unfold greatest_def) fast
   158 
   159 lemma greatest_LowerI:
   160   includes struct L
   161   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   162     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   163     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   164   shows "greatest L i (Lower L A)"
   165 proof -
   166   have "Lower L A \<subseteq> carrier L" by simp
   167   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   168   moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   169   ultimately show ?thesis by (simp add: greatest_def)
   170 qed
   171 
   172 
   173 subsection {* Lattices *}
   174 
   175 locale lattice = partial_order +
   176   assumes sup_of_two_exists:
   177     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   178     and inf_of_two_exists:
   179     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   180 
   181 lemma least_Upper_above:
   182   includes struct L
   183   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   184   by (unfold least_def) blast
   185 
   186 lemma greatest_Lower_above:
   187   includes struct L
   188   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   189   by (unfold greatest_def) blast
   190 
   191 
   192 subsubsection {* Supremum *}
   193 
   194 lemma (in lattice) joinI:
   195   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   196   ==> P (x \<squnion> y)"
   197 proof (unfold join_def sup_def)
   198   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   199     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   200   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   201   with L show "P (THE l. least L l (Upper L {x, y}))"
   202     by (fast intro: theI2 least_unique P)
   203 qed
   204 
   205 lemma (in lattice) join_closed [simp]:
   206   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   207   by (rule joinI) (rule least_carrier)
   208 
   209 lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   210   "x \<in> carrier L ==> least L x (Upper L {x})"
   211   by (rule least_UpperI) fast+
   212 
   213 lemma (in partial_order) sup_of_singleton [simp]:
   214   includes struct L
   215   shows "x \<in> carrier L ==> \<Squnion>{x} = x"
   216   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   217 
   218 
   219 text {* Condition on @{text A}: supremum exists. *}
   220 
   221 lemma (in lattice) sup_insertI:
   222   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   223   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   224   ==> P (\<Squnion>(insert x A))"
   225 proof (unfold sup_def)
   226   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   227     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   228     and least_a: "least L a (Upper L A)"
   229   from L least_a have La: "a \<in> carrier L" by simp
   230   from L sup_of_two_exists least_a
   231   obtain s where least_s: "least L s (Upper L {a, x})" by blast
   232   show "P (THE l. least L l (Upper L (insert x A)))"
   233   proof (rule theI2)
   234     show "least L s (Upper L (insert x A))"
   235     proof (rule least_UpperI)
   236       fix z
   237       assume "z \<in> insert x A"
   238       then show "z \<sqsubseteq> s"
   239       proof
   240         assume "z = x" then show ?thesis
   241           by (simp add: least_Upper_above [OF least_s] L La)
   242       next
   243         assume "z \<in> A"
   244         with L least_s least_a show ?thesis
   245           by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   246       qed
   247     next
   248       fix y
   249       assume y: "y \<in> Upper L (insert x A)"
   250       show "s \<sqsubseteq> y"
   251       proof (rule least_le [OF least_s], rule Upper_memI)
   252 	fix z
   253 	assume z: "z \<in> {a, x}"
   254 	then show "z \<sqsubseteq> y"
   255 	proof
   256           have y': "y \<in> Upper L A"
   257             apply (rule subsetD [where A = "Upper L (insert x A)"])
   258             apply (rule Upper_antimono) apply clarify apply assumption
   259             done
   260           assume "z = a"
   261           with y' least_a show ?thesis by (fast dest: least_le)
   262 	next
   263 	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
   264           with y L show ?thesis by blast
   265 	qed
   266       qed (rule Upper_closed [THEN subsetD])
   267     next
   268       from L show "insert x A \<subseteq> carrier L" by simp
   269       from least_s show "s \<in> carrier L" by simp
   270     qed
   271   next
   272     fix l
   273     assume least_l: "least L l (Upper L (insert x A))"
   274     show "l = s"
   275     proof (rule least_unique)
   276       show "least L s (Upper L (insert x A))"
   277       proof (rule least_UpperI)
   278         fix z
   279         assume "z \<in> insert x A"
   280         then show "z \<sqsubseteq> s"
   281 	proof
   282           assume "z = x" then show ?thesis
   283             by (simp add: least_Upper_above [OF least_s] L La)
   284 	next
   285           assume "z \<in> A"
   286           with L least_s least_a show ?thesis
   287             by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   288 	qed
   289       next
   290         fix y
   291         assume y: "y \<in> Upper L (insert x A)"
   292         show "s \<sqsubseteq> y"
   293         proof (rule least_le [OF least_s], rule Upper_memI)
   294           fix z
   295           assume z: "z \<in> {a, x}"
   296           then show "z \<sqsubseteq> y"
   297           proof
   298             have y': "y \<in> Upper L A"
   299 	      apply (rule subsetD [where A = "Upper L (insert x A)"])
   300 	      apply (rule Upper_antimono) apply clarify apply assumption
   301 	      done
   302             assume "z = a"
   303             with y' least_a show ?thesis by (fast dest: least_le)
   304 	  next
   305             assume "z \<in> {x}"
   306             with y L show ?thesis by blast
   307           qed
   308         qed (rule Upper_closed [THEN subsetD])
   309       next
   310         from L show "insert x A \<subseteq> carrier L" by simp
   311         from least_s show "s \<in> carrier L" by simp
   312       qed
   313     qed
   314   qed
   315 qed
   316 
   317 lemma (in lattice) finite_sup_least:
   318   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   319 proof (induct set: Finites)
   320   case empty
   321   then show ?case by simp
   322 next
   323   case (insert A x)
   324   show ?case
   325   proof (cases "A = {}")
   326     case True
   327     with insert show ?thesis by (simp add: sup_of_singletonI)
   328   next
   329     case False
   330     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   331     with _ show ?thesis
   332       by (rule sup_insertI) (simp_all add: insert [simplified])
   333   qed
   334 qed
   335 
   336 lemma (in lattice) finite_sup_insertI:
   337   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   338     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   339   shows "P (\<Squnion> (insert x A))"
   340 proof (cases "A = {}")
   341   case True with P and xA show ?thesis
   342     by (simp add: sup_of_singletonI)
   343 next
   344   case False with P and xA show ?thesis
   345     by (simp add: sup_insertI finite_sup_least)
   346 qed
   347 
   348 lemma (in lattice) finite_sup_closed:
   349   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   350 proof (induct set: Finites)
   351   case empty then show ?case by simp
   352 next
   353   case (insert A x) then show ?case
   354     by - (rule finite_sup_insertI, simp_all)
   355 qed
   356 
   357 lemma (in lattice) join_left:
   358   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   359   by (rule joinI [folded join_def]) (blast dest: least_mem)
   360 
   361 lemma (in lattice) join_right:
   362   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   363   by (rule joinI [folded join_def]) (blast dest: least_mem)
   364 
   365 lemma (in lattice) sup_of_two_least:
   366   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   367 proof (unfold sup_def)
   368   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   369   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   370   with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
   371   by (fast intro: theI2 least_unique)  (* blast fails *)
   372 qed
   373 
   374 lemma (in lattice) join_le:
   375   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   376     and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   377   shows "x \<squnion> y \<sqsubseteq> z"
   378 proof (rule joinI)
   379   fix s
   380   assume "least L s (Upper L {x, y})"
   381   with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   382 qed
   383 
   384 lemma (in lattice) join_assoc_lemma:
   385   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   386   shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   387 proof (rule finite_sup_insertI)
   388   -- {* The textbook argument in Jacobson I, p 457 *}
   389   fix s
   390   assume sup: "least L s (Upper L {x, y, z})"
   391   show "x \<squnion> (y \<squnion> z) = s"
   392   proof (rule anti_sym)
   393     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   394       by (fastsimp intro!: join_le elim: least_Upper_above)
   395   next
   396     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   397     by (erule_tac least_le)
   398       (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
   399   qed (simp_all add: L least_carrier [OF sup])
   400 qed (simp_all add: L)
   401 
   402 lemma join_comm:
   403   includes struct L
   404   shows "x \<squnion> y = y \<squnion> x"
   405   by (unfold join_def) (simp add: insert_commute)
   406 
   407 lemma (in lattice) join_assoc:
   408   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   409   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   410 proof -
   411   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   412   also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)
   413   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
   414   also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)
   415   finally show ?thesis .
   416 qed
   417 
   418 
   419 subsubsection {* Infimum *}
   420 
   421 lemma (in lattice) meetI:
   422   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   423   x \<in> carrier L; y \<in> carrier L |]
   424   ==> P (x \<sqinter> y)"
   425 proof (unfold meet_def inf_def)
   426   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   427     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   428   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   429   with L show "P (THE g. greatest L g (Lower L {x, y}))"
   430   by (fast intro: theI2 greatest_unique P)
   431 qed
   432 
   433 lemma (in lattice) meet_closed [simp]:
   434   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   435   by (rule meetI) (rule greatest_carrier)
   436 
   437 lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   438   "x \<in> carrier L ==> greatest L x (Lower L {x})"
   439   by (rule greatest_LowerI) fast+
   440 
   441 lemma (in partial_order) inf_of_singleton [simp]:
   442   includes struct L
   443   shows "x \<in> carrier L ==> \<Sqinter> {x} = x"
   444   by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   445 
   446 text {* Condition on A: infimum exists. *}
   447 
   448 lemma (in lattice) inf_insertI:
   449   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   450   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   451   ==> P (\<Sqinter>(insert x A))"
   452 proof (unfold inf_def)
   453   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   454     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
   455     and greatest_a: "greatest L a (Lower L A)"
   456   from L greatest_a have La: "a \<in> carrier L" by simp
   457   from L inf_of_two_exists greatest_a
   458   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   459   show "P (THE g. greatest L g (Lower L (insert x A)))"
   460   proof (rule theI2)
   461     show "greatest L i (Lower L (insert x A))"
   462     proof (rule greatest_LowerI)
   463       fix z
   464       assume "z \<in> insert x A"
   465       then show "i \<sqsubseteq> z"
   466       proof
   467         assume "z = x" then show ?thesis
   468           by (simp add: greatest_Lower_above [OF greatest_i] L La)
   469       next
   470         assume "z \<in> A"
   471         with L greatest_i greatest_a show ?thesis
   472           by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
   473       qed
   474     next
   475       fix y
   476       assume y: "y \<in> Lower L (insert x A)"
   477       show "y \<sqsubseteq> i"
   478       proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   479 	fix z
   480 	assume z: "z \<in> {a, x}"
   481 	then show "y \<sqsubseteq> z"
   482 	proof
   483           have y': "y \<in> Lower L A"
   484             apply (rule subsetD [where A = "Lower L (insert x A)"])
   485             apply (rule Lower_antimono) apply clarify apply assumption
   486             done
   487           assume "z = a"
   488           with y' greatest_a show ?thesis by (fast dest: greatest_le)
   489 	next
   490           assume "z \<in> {x}"
   491           with y L show ?thesis by blast
   492 	qed
   493       qed (rule Lower_closed [THEN subsetD])
   494     next
   495       from L show "insert x A \<subseteq> carrier L" by simp
   496       from greatest_i show "i \<in> carrier L" by simp
   497     qed
   498   next
   499     fix g
   500     assume greatest_g: "greatest L g (Lower L (insert x A))"
   501     show "g = i"
   502     proof (rule greatest_unique)
   503       show "greatest L i (Lower L (insert x A))"
   504       proof (rule greatest_LowerI)
   505         fix z
   506         assume "z \<in> insert x A"
   507         then show "i \<sqsubseteq> z"
   508 	proof
   509           assume "z = x" then show ?thesis
   510             by (simp add: greatest_Lower_above [OF greatest_i] L La)
   511 	next
   512           assume "z \<in> A"
   513           with L greatest_i greatest_a show ?thesis
   514             by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
   515         qed
   516       next
   517         fix y
   518         assume y: "y \<in> Lower L (insert x A)"
   519         show "y \<sqsubseteq> i"
   520         proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   521           fix z
   522           assume z: "z \<in> {a, x}"
   523           then show "y \<sqsubseteq> z"
   524           proof
   525             have y': "y \<in> Lower L A"
   526 	      apply (rule subsetD [where A = "Lower L (insert x A)"])
   527 	      apply (rule Lower_antimono) apply clarify apply assumption
   528 	      done
   529             assume "z = a"
   530             with y' greatest_a show ?thesis by (fast dest: greatest_le)
   531 	  next
   532             assume "z \<in> {x}"
   533             with y L show ?thesis by blast
   534 	  qed
   535         qed (rule Lower_closed [THEN subsetD])
   536       next
   537         from L show "insert x A \<subseteq> carrier L" by simp
   538         from greatest_i show "i \<in> carrier L" by simp
   539       qed
   540     qed
   541   qed
   542 qed
   543 
   544 lemma (in lattice) finite_inf_greatest:
   545   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   546 proof (induct set: Finites)
   547   case empty then show ?case by simp
   548 next
   549   case (insert A x)
   550   show ?case
   551   proof (cases "A = {}")
   552     case True
   553     with insert show ?thesis by (simp add: inf_of_singletonI)
   554   next
   555     case False
   556     from insert show ?thesis
   557     proof (rule_tac inf_insertI)
   558       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
   559     qed simp_all
   560   qed
   561 qed
   562 
   563 lemma (in lattice) finite_inf_insertI:
   564   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   565     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   566   shows "P (\<Sqinter> (insert x A))"
   567 proof (cases "A = {}")
   568   case True with P and xA show ?thesis
   569     by (simp add: inf_of_singletonI)
   570 next
   571   case False with P and xA show ?thesis
   572     by (simp add: inf_insertI finite_inf_greatest)
   573 qed
   574 
   575 lemma (in lattice) finite_inf_closed:
   576   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   577 proof (induct set: Finites)
   578   case empty then show ?case by simp
   579 next
   580   case (insert A x) then show ?case
   581     by (rule_tac finite_inf_insertI) (simp_all)
   582 qed
   583 
   584 lemma (in lattice) meet_left:
   585   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   586   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   587 
   588 lemma (in lattice) meet_right:
   589   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   590   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   591 
   592 lemma (in lattice) inf_of_two_greatest:
   593   "[| x \<in> carrier L; y \<in> carrier L |] ==>
   594   greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   595 proof (unfold inf_def)
   596   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   597   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   598   with L
   599   show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
   600   by (fast intro: theI2 greatest_unique)  (* blast fails *)
   601 qed
   602 
   603 lemma (in lattice) meet_le:
   604   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   605     and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   606   shows "z \<sqsubseteq> x \<sqinter> y"
   607 proof (rule meetI)
   608   fix i
   609   assume "greatest L i (Lower L {x, y})"
   610   with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   611 qed
   612 
   613 lemma (in lattice) meet_assoc_lemma:
   614   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   615   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   616 proof (rule finite_inf_insertI)
   617   txt {* The textbook argument in Jacobson I, p 457 *}
   618   fix i
   619   assume inf: "greatest L i (Lower L {x, y, z})"
   620   show "x \<sqinter> (y \<sqinter> z) = i"
   621   proof (rule anti_sym)
   622     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   623       by (fastsimp intro!: meet_le elim: greatest_Lower_above)
   624   next
   625     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
   626     by (erule_tac greatest_le)
   627       (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
   628   qed (simp_all add: L greatest_carrier [OF inf])
   629 qed (simp_all add: L)
   630 
   631 lemma meet_comm:
   632   includes struct L
   633   shows "x \<sqinter> y = y \<sqinter> x"
   634   by (unfold meet_def) (simp add: insert_commute)
   635 
   636 lemma (in lattice) meet_assoc:
   637   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   638   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   639 proof -
   640   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   641   also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma)
   642   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
   643   also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma)
   644   finally show ?thesis .
   645 qed
   646 
   647 
   648 subsection {* Total Orders *}
   649 
   650 locale total_order = lattice +
   651   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   652 
   653 text {* Introduction rule: the usual definition of total order *}
   654 
   655 lemma (in partial_order) total_orderI:
   656   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   657   shows "total_order L"
   658 proof (rule total_order.intro)
   659   show "lattice_axioms L"
   660   proof (rule lattice_axioms.intro)
   661     fix x y
   662     assume L: "x \<in> carrier L"  "y \<in> carrier L"
   663     show "EX s. least L s (Upper L {x, y})"
   664     proof -
   665       note total L
   666       moreover
   667       {
   668         assume "x \<sqsubseteq> y"
   669         with L have "least L y (Upper L {x, y})"
   670           by (rule_tac least_UpperI) auto
   671       }
   672       moreover
   673       {
   674         assume "y \<sqsubseteq> x"
   675         with L have "least L x (Upper L {x, y})"
   676           by (rule_tac least_UpperI) auto
   677       }
   678       ultimately show ?thesis by blast
   679     qed
   680   next
   681     fix x y
   682     assume L: "x \<in> carrier L"  "y \<in> carrier L"
   683     show "EX i. greatest L i (Lower L {x, y})"
   684     proof -
   685       note total L
   686       moreover
   687       {
   688         assume "y \<sqsubseteq> x"
   689         with L have "greatest L y (Lower L {x, y})"
   690           by (rule_tac greatest_LowerI) auto
   691       }
   692       moreover
   693       {
   694         assume "x \<sqsubseteq> y"
   695         with L have "greatest L x (Lower L {x, y})"
   696           by (rule_tac greatest_LowerI) auto
   697       }
   698       ultimately show ?thesis by blast
   699     qed
   700   qed
   701 qed (assumption | rule total_order_axioms.intro)+
   702 
   703 
   704 subsection {* Complete lattices *}
   705 
   706 locale complete_lattice = lattice +
   707   assumes sup_exists:
   708     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   709     and inf_exists:
   710     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   711 
   712 text {* Introduction rule: the usual definition of complete lattice *}
   713 
   714 lemma (in partial_order) complete_latticeI:
   715   assumes sup_exists:
   716     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   717     and inf_exists:
   718     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   719   shows "complete_lattice L"
   720 proof (rule complete_lattice.intro)
   721   show "lattice_axioms L"
   722     by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
   723 qed (assumption | rule complete_lattice_axioms.intro)+
   724 
   725 constdefs (structure L)
   726   top :: "_ => 'a" ("\<top>\<index>")
   727   "\<top> == sup L (carrier L)"
   728 
   729   bottom :: "_ => 'a" ("\<bottom>\<index>")
   730   "\<bottom> == inf L (carrier L)"
   731 
   732 
   733 lemma (in complete_lattice) supI:
   734   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   735   ==> P (\<Squnion>A)"
   736 proof (unfold sup_def)
   737   assume L: "A \<subseteq> carrier L"
   738     and P: "!!l. least L l (Upper L A) ==> P l"
   739   with sup_exists obtain s where "least L s (Upper L A)" by blast
   740   with L show "P (THE l. least L l (Upper L A))"
   741   by (fast intro: theI2 least_unique P)
   742 qed
   743 
   744 lemma (in complete_lattice) sup_closed [simp]:
   745   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
   746   by (rule supI) simp_all
   747 
   748 lemma (in complete_lattice) top_closed [simp, intro]:
   749   "\<top> \<in> carrier L"
   750   by (unfold top_def) simp
   751 
   752 lemma (in complete_lattice) infI:
   753   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
   754   ==> P (\<Sqinter>A)"
   755 proof (unfold inf_def)
   756   assume L: "A \<subseteq> carrier L"
   757     and P: "!!l. greatest L l (Lower L A) ==> P l"
   758   with inf_exists obtain s where "greatest L s (Lower L A)" by blast
   759   with L show "P (THE l. greatest L l (Lower L A))"
   760   by (fast intro: theI2 greatest_unique P)
   761 qed
   762 
   763 lemma (in complete_lattice) inf_closed [simp]:
   764   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
   765   by (rule infI) simp_all
   766 
   767 lemma (in complete_lattice) bottom_closed [simp, intro]:
   768   "\<bottom> \<in> carrier L"
   769   by (unfold bottom_def) simp
   770 
   771 text {* Jacobson: Theorem 8.1 *}
   772 
   773 lemma Lower_empty [simp]:
   774   "Lower L {} = carrier L"
   775   by (unfold Lower_def) simp
   776 
   777 lemma Upper_empty [simp]:
   778   "Upper L {} = carrier L"
   779   by (unfold Upper_def) simp
   780 
   781 theorem (in partial_order) complete_lattice_criterion1:
   782   assumes top_exists: "EX g. greatest L g (carrier L)"
   783     and inf_exists:
   784       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
   785   shows "complete_lattice L"
   786 proof (rule complete_latticeI)
   787   from top_exists obtain top where top: "greatest L top (carrier L)" ..
   788   fix A
   789   assume L: "A \<subseteq> carrier L"
   790   let ?B = "Upper L A"
   791   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
   792   then have B_non_empty: "?B ~= {}" by fast
   793   have B_L: "?B \<subseteq> carrier L" by simp
   794   from inf_exists [OF B_L B_non_empty]
   795   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   796   have "least L b (Upper L A)"
   797 apply (rule least_UpperI)
   798    apply (rule greatest_le [where A = "Lower L ?B"])
   799     apply (rule b_inf_B)
   800    apply (rule Lower_memI)
   801     apply (erule UpperD)
   802      apply assumption
   803     apply (rule L)
   804    apply (fast intro: L [THEN subsetD])
   805   apply (erule greatest_Lower_above [OF b_inf_B])
   806   apply simp
   807  apply (rule L)
   808 apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)
   809 done
   810   then show "EX s. least L s (Upper L A)" ..
   811 next
   812   fix A
   813   assume L: "A \<subseteq> carrier L"
   814   show "EX i. greatest L i (Lower L A)"
   815   proof (cases "A = {}")
   816     case True then show ?thesis
   817       by (simp add: top_exists)
   818   next
   819     case False with L show ?thesis
   820       by (rule inf_exists)
   821   qed
   822 qed
   823 
   824 (* TODO: prove dual version *)
   825 
   826 subsection {* Examples *}
   827 
   828 subsubsection {* Powerset of a set is a complete lattice *}
   829 
   830 theorem powerset_is_complete_lattice:
   831   "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
   832   (is "complete_lattice ?L")
   833 proof (rule partial_order.complete_latticeI)
   834   show "partial_order ?L"
   835     by (rule partial_order.intro) auto
   836 next
   837   fix B
   838   assume "B \<subseteq> carrier ?L"
   839   then have "least ?L (\<Union> B) (Upper ?L B)"
   840     by (fastsimp intro!: least_UpperI simp: Upper_def)
   841   then show "EX s. least ?L s (Upper ?L B)" ..
   842 next
   843   fix B
   844   assume "B \<subseteq> carrier ?L"
   845   then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
   846     txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
   847       @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
   848     by (fastsimp intro!: greatest_LowerI simp: Lower_def)
   849   then show "EX i. greatest ?L i (Lower ?L B)" ..
   850 qed
   851 
   852 text {* An other example, that of the lattice of subgroups of a group,
   853   can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
   854 
   855 end