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