src/HOL/Algebra/Lattice.thy
 author haftmann Fri Jun 17 16:12:49 2005 +0200 (2005-06-17) changeset 16417 9bc16273c2d4 parent 16325 a6431098a929 child 19286 83404ccd270a permissions -rw-r--r--
migrated theory headers to new format
     1 (*

     2   Title:     HOL/Algebra/Lattice.thy

     3   Id:        $Id$

     4   Author:    Clemens Ballarin, started 7 November 2003

     5   Copyright: Clemens Ballarin

     6 *)

     7

     8 header {* Orders and Lattices *}

     9

    10 theory Lattice imports Main begin

    11

    12 text {* Object with a carrier set. *}

    13

    14 record 'a partial_object =

    15   carrier :: "'a set"

    16

    17 subsection {* Partial Orders *}

    18

    19 record 'a order = "'a partial_object" +

    20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)

    21

    22 locale partial_order = struct L +

    23   assumes refl [intro, simp]:

    24                   "x \<in> carrier L ==> x \<sqsubseteq> x"

    25     and anti_sym [intro]:

    26                   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"

    27     and trans [trans]:

    28                   "[| x \<sqsubseteq> y; y \<sqsubseteq> z;

    29                    x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"

    30

    31 constdefs (structure L)

    32   less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)

    33   "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"

    34

    35   -- {* Upper and lower bounds of a set. *}

    36   Upper :: "[_, 'a set] => 'a set"

    37   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>

    38                 carrier L"

    39

    40   Lower :: "[_, 'a set] => 'a set"

    41   "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>

    42                 carrier L"

    43

    44   -- {* Least and greatest, as predicate. *}

    45   least :: "[_, 'a, 'a set] => bool"

    46   "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"

    47

    48   greatest :: "[_, 'a, 'a set] => bool"

    49   "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"

    50

    51   -- {* Supremum and infimum *}

    52   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)

    53   "\<Squnion>A == THE x. least L x (Upper L A)"

    54

    55   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)

    56   "\<Sqinter>A == THE x. greatest L x (Lower L A)"

    57

    58   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)

    59   "x \<squnion> y == sup L {x, y}"

    60

    61   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)

    62   "x \<sqinter> y == inf L {x, y}"

    63

    64

    65 subsubsection {* Upper *}

    66

    67 lemma Upper_closed [intro, simp]:

    68   "Upper L A \<subseteq> carrier L"

    69   by (unfold Upper_def) clarify

    70

    71 lemma UpperD [dest]:

    72   includes struct L

    73   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"

    74   by (unfold Upper_def) blast

    75

    76 lemma Upper_memI:

    77   includes struct L

    78   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"

    79   by (unfold Upper_def) blast

    80

    81 lemma Upper_antimono:

    82   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"

    83   by (unfold Upper_def) blast

    84

    85

    86 subsubsection {* Lower *}

    87

    88 lemma Lower_closed [intro, simp]:

    89   "Lower L A \<subseteq> carrier L"

    90   by (unfold Lower_def) clarify

    91

    92 lemma LowerD [dest]:

    93   includes struct L

    94   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"

    95   by (unfold Lower_def) blast

    96

    97 lemma Lower_memI:

    98   includes struct L

    99   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"

   100   by (unfold Lower_def) blast

   101

   102 lemma Lower_antimono:

   103   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"

   104   by (unfold Lower_def) blast

   105

   106

   107 subsubsection {* least *}

   108

   109 lemma least_carrier [intro, simp]:

   110   shows "least L l A ==> l \<in> carrier L"

   111   by (unfold least_def) fast

   112

   113 lemma least_mem:

   114   "least L l A ==> l \<in> A"

   115   by (unfold least_def) fast

   116

   117 lemma (in partial_order) least_unique:

   118   "[| least L x A; least L y A |] ==> x = y"

   119   by (unfold least_def) blast

   120

   121 lemma least_le:

   122   includes struct L

   123   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"

   124   by (unfold least_def) fast

   125

   126 lemma least_UpperI:

   127   includes struct L

   128   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"

   129     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"

   130     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"

   131   shows "least L s (Upper L A)"

   132 proof -

   133   have "Upper L A \<subseteq> carrier L" by simp

   134   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)

   135   moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast

   136   ultimately show ?thesis by (simp add: least_def)

   137 qed

   138

   139

   140 subsubsection {* greatest *}

   141

   142 lemma greatest_carrier [intro, simp]:

   143   shows "greatest L l A ==> l \<in> carrier L"

   144   by (unfold greatest_def) fast

   145

   146 lemma greatest_mem:

   147   "greatest L l A ==> l \<in> A"

   148   by (unfold greatest_def) fast

   149

   150 lemma (in partial_order) greatest_unique:

   151   "[| greatest L x A; greatest L y A |] ==> x = y"

   152   by (unfold greatest_def) blast

   153

   154 lemma greatest_le:

   155   includes struct L

   156   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"

   157   by (unfold greatest_def) fast

   158

   159 lemma greatest_LowerI:

   160   includes struct L

   161   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"

   162     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"

   163     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"

   164   shows "greatest L i (Lower L A)"

   165 proof -

   166   have "Lower L A \<subseteq> carrier L" by simp

   167   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)

   168   moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast

   169   ultimately show ?thesis by (simp add: greatest_def)

   170 qed

   171

   172

   173 subsection {* Lattices *}

   174

   175 locale lattice = partial_order +

   176   assumes sup_of_two_exists:

   177     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"

   178     and inf_of_two_exists:

   179     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"

   180

   181 lemma least_Upper_above:

   182   includes struct L

   183   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"

   184   by (unfold least_def) blast

   185

   186 lemma greatest_Lower_above:

   187   includes struct L

   188   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"

   189   by (unfold greatest_def) blast

   190

   191

   192 subsubsection {* Supremum *}

   193

   194 lemma (in lattice) joinI:

   195   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]

   196   ==> P (x \<squnion> y)"

   197 proof (unfold join_def sup_def)

   198   assume L: "x \<in> carrier L"  "y \<in> carrier L"

   199     and P: "!!l. least L l (Upper L {x, y}) ==> P l"

   200   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast

   201   with L show "P (THE l. least L l (Upper L {x, y}))"

   202     by (fast intro: theI2 least_unique P)

   203 qed

   204

   205 lemma (in lattice) join_closed [simp]:

   206   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"

   207   by (rule joinI) (rule least_carrier)

   208

   209 lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)

   210   "x \<in> carrier L ==> least L x (Upper L {x})"

   211   by (rule least_UpperI) fast+

   212

   213 lemma (in partial_order) sup_of_singleton [simp]:

   214   includes struct L

   215   shows "x \<in> carrier L ==> \<Squnion>{x} = x"

   216   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)

   217

   218

   219 text {* Condition on @{text A}: supremum exists. *}

   220

   221 lemma (in lattice) sup_insertI:

   222   "[| !!s. least L s (Upper L (insert x A)) ==> P s;

   223   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]

   224   ==> P (\<Squnion>(insert x A))"

   225 proof (unfold sup_def)

   226   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"

   227     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"

   228     and least_a: "least L a (Upper L A)"

   229   from L least_a have La: "a \<in> carrier L" by simp

   230   from L sup_of_two_exists least_a

   231   obtain s where least_s: "least L s (Upper L {a, x})" by blast

   232   show "P (THE l. least L l (Upper L (insert x A)))"

   233   proof (rule theI2)

   234     show "least L s (Upper L (insert x A))"

   235     proof (rule least_UpperI)

   236       fix z

   237       assume "z \<in> insert x A"

   238       then show "z \<sqsubseteq> s"

   239       proof

   240         assume "z = x" then show ?thesis

   241           by (simp add: least_Upper_above [OF least_s] L La)

   242       next

   243         assume "z \<in> A"

   244         with L least_s least_a show ?thesis

   245           by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)

   246       qed

   247     next

   248       fix y

   249       assume y: "y \<in> Upper L (insert x A)"

   250       show "s \<sqsubseteq> y"

   251       proof (rule least_le [OF least_s], rule Upper_memI)

   252 	fix z

   253 	assume z: "z \<in> {a, x}"

   254 	then show "z \<sqsubseteq> y"

   255 	proof

   256           have y': "y \<in> Upper L A"

   257             apply (rule subsetD [where A = "Upper L (insert x A)"])

   258             apply (rule Upper_antimono) apply clarify apply assumption

   259             done

   260           assume "z = a"

   261           with y' least_a show ?thesis by (fast dest: least_le)

   262 	next

   263 	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)

   264           with y L show ?thesis by blast

   265 	qed

   266       qed (rule Upper_closed [THEN subsetD])

   267     next

   268       from L show "insert x A \<subseteq> carrier L" by simp

   269       from least_s show "s \<in> carrier L" by simp

   270     qed

   271   next

   272     fix l

   273     assume least_l: "least L l (Upper L (insert x A))"

   274     show "l = s"

   275     proof (rule least_unique)

   276       show "least L s (Upper L (insert x A))"

   277       proof (rule least_UpperI)

   278         fix z

   279         assume "z \<in> insert x A"

   280         then show "z \<sqsubseteq> s"

   281 	proof

   282           assume "z = x" then show ?thesis

   283             by (simp add: least_Upper_above [OF least_s] L La)

   284 	next

   285           assume "z \<in> A"

   286           with L least_s least_a show ?thesis

   287             by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)

   288 	qed

   289       next

   290         fix y

   291         assume y: "y \<in> Upper L (insert x A)"

   292         show "s \<sqsubseteq> y"

   293         proof (rule least_le [OF least_s], rule Upper_memI)

   294           fix z

   295           assume z: "z \<in> {a, x}"

   296           then show "z \<sqsubseteq> y"

   297           proof

   298             have y': "y \<in> Upper L A"

   299 	      apply (rule subsetD [where A = "Upper L (insert x A)"])

   300 	      apply (rule Upper_antimono) apply clarify apply assumption

   301 	      done

   302             assume "z = a"

   303             with y' least_a show ?thesis by (fast dest: least_le)

   304 	  next

   305             assume "z \<in> {x}"

   306             with y L show ?thesis by blast

   307           qed

   308         qed (rule Upper_closed [THEN subsetD])

   309       next

   310         from L show "insert x A \<subseteq> carrier L" by simp

   311         from least_s show "s \<in> carrier L" by simp

   312       qed

   313     qed

   314   qed

   315 qed

   316

   317 lemma (in lattice) finite_sup_least:

   318   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"

   319 proof (induct set: Finites)

   320   case empty

   321   then show ?case by simp

   322 next

   323   case (insert x A)

   324   show ?case

   325   proof (cases "A = {}")

   326     case True

   327     with insert show ?thesis by (simp add: sup_of_singletonI)

   328   next

   329     case False

   330     with insert have "least L (\<Squnion>A) (Upper L A)" by simp

   331     with _ show ?thesis

   332       by (rule sup_insertI) (simp_all add: insert [simplified])

   333   qed

   334 qed

   335

   336 lemma (in lattice) finite_sup_insertI:

   337   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"

   338     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"

   339   shows "P (\<Squnion> (insert x A))"

   340 proof (cases "A = {}")

   341   case True with P and xA show ?thesis

   342     by (simp add: sup_of_singletonI)

   343 next

   344   case False with P and xA show ?thesis

   345     by (simp add: sup_insertI finite_sup_least)

   346 qed

   347

   348 lemma (in lattice) finite_sup_closed:

   349   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"

   350 proof (induct set: Finites)

   351   case empty then show ?case by simp

   352 next

   353   case insert then show ?case

   354     by - (rule finite_sup_insertI, simp_all)

   355 qed

   356

   357 lemma (in lattice) join_left:

   358   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"

   359   by (rule joinI [folded join_def]) (blast dest: least_mem)

   360

   361 lemma (in lattice) join_right:

   362   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"

   363   by (rule joinI [folded join_def]) (blast dest: least_mem)

   364

   365 lemma (in lattice) sup_of_two_least:

   366   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"

   367 proof (unfold sup_def)

   368   assume L: "x \<in> carrier L"  "y \<in> carrier L"

   369   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast

   370   with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"

   371   by (fast intro: theI2 least_unique)  (* blast fails *)

   372 qed

   373

   374 lemma (in lattice) join_le:

   375   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"

   376     and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   377   shows "x \<squnion> y \<sqsubseteq> z"

   378 proof (rule joinI)

   379   fix s

   380   assume "least L s (Upper L {x, y})"

   381   with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)

   382 qed

   383

   384 lemma (in lattice) join_assoc_lemma:

   385   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   386   shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"

   387 proof (rule finite_sup_insertI)

   388   -- {* The textbook argument in Jacobson I, p 457 *}

   389   fix s

   390   assume sup: "least L s (Upper L {x, y, z})"

   391   show "x \<squnion> (y \<squnion> z) = s"

   392   proof (rule anti_sym)

   393     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"

   394       by (fastsimp intro!: join_le elim: least_Upper_above)

   395   next

   396     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"

   397     by (erule_tac least_le)

   398       (blast intro!: Upper_memI intro: trans join_left join_right join_closed)

   399   qed (simp_all add: L least_carrier [OF sup])

   400 qed (simp_all add: L)

   401

   402 lemma join_comm:

   403   includes struct L

   404   shows "x \<squnion> y = y \<squnion> x"

   405   by (unfold join_def) (simp add: insert_commute)

   406

   407 lemma (in lattice) join_assoc:

   408   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   409   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"

   410 proof -

   411   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)

   412   also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)

   413   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)

   414   also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)

   415   finally show ?thesis .

   416 qed

   417

   418

   419 subsubsection {* Infimum *}

   420

   421 lemma (in lattice) meetI:

   422   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;

   423   x \<in> carrier L; y \<in> carrier L |]

   424   ==> P (x \<sqinter> y)"

   425 proof (unfold meet_def inf_def)

   426   assume L: "x \<in> carrier L"  "y \<in> carrier L"

   427     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"

   428   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast

   429   with L show "P (THE g. greatest L g (Lower L {x, y}))"

   430   by (fast intro: theI2 greatest_unique P)

   431 qed

   432

   433 lemma (in lattice) meet_closed [simp]:

   434   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"

   435   by (rule meetI) (rule greatest_carrier)

   436

   437 lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)

   438   "x \<in> carrier L ==> greatest L x (Lower L {x})"

   439   by (rule greatest_LowerI) fast+

   440

   441 lemma (in partial_order) inf_of_singleton [simp]:

   442   includes struct L

   443   shows "x \<in> carrier L ==> \<Sqinter> {x} = x"

   444   by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)

   445

   446 text {* Condition on A: infimum exists. *}

   447

   448 lemma (in lattice) inf_insertI:

   449   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;

   450   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]

   451   ==> P (\<Sqinter>(insert x A))"

   452 proof (unfold inf_def)

   453   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"

   454     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"

   455     and greatest_a: "greatest L a (Lower L A)"

   456   from L greatest_a have La: "a \<in> carrier L" by simp

   457   from L inf_of_two_exists greatest_a

   458   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast

   459   show "P (THE g. greatest L g (Lower L (insert x A)))"

   460   proof (rule theI2)

   461     show "greatest L i (Lower L (insert x A))"

   462     proof (rule greatest_LowerI)

   463       fix z

   464       assume "z \<in> insert x A"

   465       then show "i \<sqsubseteq> z"

   466       proof

   467         assume "z = x" then show ?thesis

   468           by (simp add: greatest_Lower_above [OF greatest_i] L La)

   469       next

   470         assume "z \<in> A"

   471         with L greatest_i greatest_a show ?thesis

   472           by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)

   473       qed

   474     next

   475       fix y

   476       assume y: "y \<in> Lower L (insert x A)"

   477       show "y \<sqsubseteq> i"

   478       proof (rule greatest_le [OF greatest_i], rule Lower_memI)

   479 	fix z

   480 	assume z: "z \<in> {a, x}"

   481 	then show "y \<sqsubseteq> z"

   482 	proof

   483           have y': "y \<in> Lower L A"

   484             apply (rule subsetD [where A = "Lower L (insert x A)"])

   485             apply (rule Lower_antimono) apply clarify apply assumption

   486             done

   487           assume "z = a"

   488           with y' greatest_a show ?thesis by (fast dest: greatest_le)

   489 	next

   490           assume "z \<in> {x}"

   491           with y L show ?thesis by blast

   492 	qed

   493       qed (rule Lower_closed [THEN subsetD])

   494     next

   495       from L show "insert x A \<subseteq> carrier L" by simp

   496       from greatest_i show "i \<in> carrier L" by simp

   497     qed

   498   next

   499     fix g

   500     assume greatest_g: "greatest L g (Lower L (insert x A))"

   501     show "g = i"

   502     proof (rule greatest_unique)

   503       show "greatest L i (Lower L (insert x A))"

   504       proof (rule greatest_LowerI)

   505         fix z

   506         assume "z \<in> insert x A"

   507         then show "i \<sqsubseteq> z"

   508 	proof

   509           assume "z = x" then show ?thesis

   510             by (simp add: greatest_Lower_above [OF greatest_i] L La)

   511 	next

   512           assume "z \<in> A"

   513           with L greatest_i greatest_a show ?thesis

   514             by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)

   515         qed

   516       next

   517         fix y

   518         assume y: "y \<in> Lower L (insert x A)"

   519         show "y \<sqsubseteq> i"

   520         proof (rule greatest_le [OF greatest_i], rule Lower_memI)

   521           fix z

   522           assume z: "z \<in> {a, x}"

   523           then show "y \<sqsubseteq> z"

   524           proof

   525             have y': "y \<in> Lower L A"

   526 	      apply (rule subsetD [where A = "Lower L (insert x A)"])

   527 	      apply (rule Lower_antimono) apply clarify apply assumption

   528 	      done

   529             assume "z = a"

   530             with y' greatest_a show ?thesis by (fast dest: greatest_le)

   531 	  next

   532             assume "z \<in> {x}"

   533             with y L show ?thesis by blast

   534 	  qed

   535         qed (rule Lower_closed [THEN subsetD])

   536       next

   537         from L show "insert x A \<subseteq> carrier L" by simp

   538         from greatest_i show "i \<in> carrier L" by simp

   539       qed

   540     qed

   541   qed

   542 qed

   543

   544 lemma (in lattice) finite_inf_greatest:

   545   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"

   546 proof (induct set: Finites)

   547   case empty then show ?case by simp

   548 next

   549   case (insert x A)

   550   show ?case

   551   proof (cases "A = {}")

   552     case True

   553     with insert show ?thesis by (simp add: inf_of_singletonI)

   554   next

   555     case False

   556     from insert show ?thesis

   557     proof (rule_tac inf_insertI)

   558       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp

   559     qed simp_all

   560   qed

   561 qed

   562

   563 lemma (in lattice) finite_inf_insertI:

   564   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"

   565     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"

   566   shows "P (\<Sqinter> (insert x A))"

   567 proof (cases "A = {}")

   568   case True with P and xA show ?thesis

   569     by (simp add: inf_of_singletonI)

   570 next

   571   case False with P and xA show ?thesis

   572     by (simp add: inf_insertI finite_inf_greatest)

   573 qed

   574

   575 lemma (in lattice) finite_inf_closed:

   576   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"

   577 proof (induct set: Finites)

   578   case empty then show ?case by simp

   579 next

   580   case insert then show ?case

   581     by (rule_tac finite_inf_insertI) (simp_all)

   582 qed

   583

   584 lemma (in lattice) meet_left:

   585   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"

   586   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)

   587

   588 lemma (in lattice) meet_right:

   589   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"

   590   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)

   591

   592 lemma (in lattice) inf_of_two_greatest:

   593   "[| x \<in> carrier L; y \<in> carrier L |] ==>

   594   greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"

   595 proof (unfold inf_def)

   596   assume L: "x \<in> carrier L"  "y \<in> carrier L"

   597   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast

   598   with L

   599   show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"

   600   by (fast intro: theI2 greatest_unique)  (* blast fails *)

   601 qed

   602

   603 lemma (in lattice) meet_le:

   604   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"

   605     and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   606   shows "z \<sqsubseteq> x \<sqinter> y"

   607 proof (rule meetI)

   608   fix i

   609   assume "greatest L i (Lower L {x, y})"

   610   with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)

   611 qed

   612

   613 lemma (in lattice) meet_assoc_lemma:

   614   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   615   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"

   616 proof (rule finite_inf_insertI)

   617   txt {* The textbook argument in Jacobson I, p 457 *}

   618   fix i

   619   assume inf: "greatest L i (Lower L {x, y, z})"

   620   show "x \<sqinter> (y \<sqinter> z) = i"

   621   proof (rule anti_sym)

   622     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"

   623       by (fastsimp intro!: meet_le elim: greatest_Lower_above)

   624   next

   625     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"

   626     by (erule_tac greatest_le)

   627       (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)

   628   qed (simp_all add: L greatest_carrier [OF inf])

   629 qed (simp_all add: L)

   630

   631 lemma meet_comm:

   632   includes struct L

   633   shows "x \<sqinter> y = y \<sqinter> x"

   634   by (unfold meet_def) (simp add: insert_commute)

   635

   636 lemma (in lattice) meet_assoc:

   637   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"

   638   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"

   639 proof -

   640   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)

   641   also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma)

   642   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)

   643   also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma)

   644   finally show ?thesis .

   645 qed

   646

   647

   648 subsection {* Total Orders *}

   649

   650 locale total_order = lattice +

   651   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"

   652

   653 text {* Introduction rule: the usual definition of total order *}

   654

   655 lemma (in partial_order) total_orderI:

   656   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"

   657   shows "total_order L"

   658 proof (rule total_order.intro)

   659   show "lattice_axioms L"

   660   proof (rule lattice_axioms.intro)

   661     fix x y

   662     assume L: "x \<in> carrier L"  "y \<in> carrier L"

   663     show "EX s. least L s (Upper L {x, y})"

   664     proof -

   665       note total L

   666       moreover

   667       {

   668         assume "x \<sqsubseteq> y"

   669         with L have "least L y (Upper L {x, y})"

   670           by (rule_tac least_UpperI) auto

   671       }

   672       moreover

   673       {

   674         assume "y \<sqsubseteq> x"

   675         with L have "least L x (Upper L {x, y})"

   676           by (rule_tac least_UpperI) auto

   677       }

   678       ultimately show ?thesis by blast

   679     qed

   680   next

   681     fix x y

   682     assume L: "x \<in> carrier L"  "y \<in> carrier L"

   683     show "EX i. greatest L i (Lower L {x, y})"

   684     proof -

   685       note total L

   686       moreover

   687       {

   688         assume "y \<sqsubseteq> x"

   689         with L have "greatest L y (Lower L {x, y})"

   690           by (rule_tac greatest_LowerI) auto

   691       }

   692       moreover

   693       {

   694         assume "x \<sqsubseteq> y"

   695         with L have "greatest L x (Lower L {x, y})"

   696           by (rule_tac greatest_LowerI) auto

   697       }

   698       ultimately show ?thesis by blast

   699     qed

   700   qed

   701 qed (assumption | rule total_order_axioms.intro)+

   702

   703

   704 subsection {* Complete lattices *}

   705

   706 locale complete_lattice = lattice +

   707   assumes sup_exists:

   708     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"

   709     and inf_exists:

   710     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"

   711

   712 text {* Introduction rule: the usual definition of complete lattice *}

   713

   714 lemma (in partial_order) complete_latticeI:

   715   assumes sup_exists:

   716     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"

   717     and inf_exists:

   718     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"

   719   shows "complete_lattice L"

   720 proof (rule complete_lattice.intro)

   721   show "lattice_axioms L"

   722     by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+

   723 qed (assumption | rule complete_lattice_axioms.intro)+

   724

   725 constdefs (structure L)

   726   top :: "_ => 'a" ("\<top>\<index>")

   727   "\<top> == sup L (carrier L)"

   728

   729   bottom :: "_ => 'a" ("\<bottom>\<index>")

   730   "\<bottom> == inf L (carrier L)"

   731

   732

   733 lemma (in complete_lattice) supI:

   734   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]

   735   ==> P (\<Squnion>A)"

   736 proof (unfold sup_def)

   737   assume L: "A \<subseteq> carrier L"

   738     and P: "!!l. least L l (Upper L A) ==> P l"

   739   with sup_exists obtain s where "least L s (Upper L A)" by blast

   740   with L show "P (THE l. least L l (Upper L A))"

   741   by (fast intro: theI2 least_unique P)

   742 qed

   743

   744 lemma (in complete_lattice) sup_closed [simp]:

   745   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"

   746   by (rule supI) simp_all

   747

   748 lemma (in complete_lattice) top_closed [simp, intro]:

   749   "\<top> \<in> carrier L"

   750   by (unfold top_def) simp

   751

   752 lemma (in complete_lattice) infI:

   753   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]

   754   ==> P (\<Sqinter>A)"

   755 proof (unfold inf_def)

   756   assume L: "A \<subseteq> carrier L"

   757     and P: "!!l. greatest L l (Lower L A) ==> P l"

   758   with inf_exists obtain s where "greatest L s (Lower L A)" by blast

   759   with L show "P (THE l. greatest L l (Lower L A))"

   760   by (fast intro: theI2 greatest_unique P)

   761 qed

   762

   763 lemma (in complete_lattice) inf_closed [simp]:

   764   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"

   765   by (rule infI) simp_all

   766

   767 lemma (in complete_lattice) bottom_closed [simp, intro]:

   768   "\<bottom> \<in> carrier L"

   769   by (unfold bottom_def) simp

   770

   771 text {* Jacobson: Theorem 8.1 *}

   772

   773 lemma Lower_empty [simp]:

   774   "Lower L {} = carrier L"

   775   by (unfold Lower_def) simp

   776

   777 lemma Upper_empty [simp]:

   778   "Upper L {} = carrier L"

   779   by (unfold Upper_def) simp

   780

   781 theorem (in partial_order) complete_lattice_criterion1:

   782   assumes top_exists: "EX g. greatest L g (carrier L)"

   783     and inf_exists:

   784       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"

   785   shows "complete_lattice L"

   786 proof (rule complete_latticeI)

   787   from top_exists obtain top where top: "greatest L top (carrier L)" ..

   788   fix A

   789   assume L: "A \<subseteq> carrier L"

   790   let ?B = "Upper L A"

   791   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)

   792   then have B_non_empty: "?B ~= {}" by fast

   793   have B_L: "?B \<subseteq> carrier L" by simp

   794   from inf_exists [OF B_L B_non_empty]

   795   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..

   796   have "least L b (Upper L A)"

   797 apply (rule least_UpperI)

   798    apply (rule greatest_le [where A = "Lower L ?B"])

   799     apply (rule b_inf_B)

   800    apply (rule Lower_memI)

   801     apply (erule UpperD)

   802      apply assumption

   803     apply (rule L)

   804    apply (fast intro: L [THEN subsetD])

   805   apply (erule greatest_Lower_above [OF b_inf_B])

   806   apply simp

   807  apply (rule L)

   808 apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)

   809 done

   810   then show "EX s. least L s (Upper L A)" ..

   811 next

   812   fix A

   813   assume L: "A \<subseteq> carrier L"

   814   show "EX i. greatest L i (Lower L A)"

   815   proof (cases "A = {}")

   816     case True then show ?thesis

   817       by (simp add: top_exists)

   818   next

   819     case False with L show ?thesis

   820       by (rule inf_exists)

   821   qed

   822 qed

   823

   824 (* TODO: prove dual version *)

   825

   826 subsection {* Examples *}

   827

   828 subsubsection {* Powerset of a set is a complete lattice *}

   829

   830 theorem powerset_is_complete_lattice:

   831   "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"

   832   (is "complete_lattice ?L")

   833 proof (rule partial_order.complete_latticeI)

   834   show "partial_order ?L"

   835     by (rule partial_order.intro) auto

   836 next

   837   fix B

   838   assume "B \<subseteq> carrier ?L"

   839   then have "least ?L (\<Union> B) (Upper ?L B)"

   840     by (fastsimp intro!: least_UpperI simp: Upper_def)

   841   then show "EX s. least ?L s (Upper ?L B)" ..

   842 next

   843   fix B

   844   assume "B \<subseteq> carrier ?L"

   845   then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"

   846     txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:

   847       @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}

   848     by (fastsimp intro!: greatest_LowerI simp: Lower_def)

   849   then show "EX i. greatest ?L i (Lower ?L B)" ..

   850 qed

   851

   852 text {* An other example, that of the lattice of subgroups of a group,

   853   can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}

   854

   855 end