src/HOL/Algebra/Lattice.thy
 author haftmann Fri Apr 20 11:21:42 2007 +0200 (2007-04-20) changeset 22744 5cbe966d67a2 parent 22265 3c5c6bdf61de child 23350 50c5b0912a0c permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     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