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