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