src/HOL/Algebra/Lattice.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30363 9b8d9b6ef803
child 32960 69916a850301
permissions -rw-r--r--
simplified method setup;
     1 (*
     2   Title:     HOL/Algebra/Lattice.thy
     3   Author:    Clemens Ballarin, started 7 November 2003
     4   Copyright: Clemens Ballarin
     5 
     6 Most congruence rules by Stephan Hohe.
     7 *)
     8 
     9 theory Lattice imports Congruence begin
    10 
    11 section {* Orders and Lattices *}
    12 
    13 subsection {* Partial Orders *}
    14 
    15 record 'a gorder = "'a eq_object" +
    16   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    17 
    18 locale weak_partial_order = equivalence L for L (structure) +
    19   assumes le_refl [intro, simp]:
    20       "x \<in> carrier L ==> x \<sqsubseteq> x"
    21     and weak_le_anti_sym [intro]:
    22       "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
    23     and le_trans [trans]:
    24       "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    25     and le_cong:
    26       "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
    27 
    28 constdefs (structure L)
    29   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    30   "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
    31 
    32 
    33 subsubsection {* The order relation *}
    34 
    35 context weak_partial_order begin
    36 
    37 lemma le_cong_l [intro, trans]:
    38   "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    39   by (auto intro: le_cong [THEN iffD2])
    40 
    41 lemma le_cong_r [intro, trans]:
    42   "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    43   by (auto intro: le_cong [THEN iffD1])
    44 
    45 lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
    46   by (simp add: le_cong_l)
    47 
    48 end
    49 
    50 lemma weak_llessI:
    51   fixes R (structure)
    52   assumes "x \<sqsubseteq> y" and "~(x .= y)"
    53   shows "x \<sqsubset> y"
    54   using assms unfolding lless_def by simp
    55 
    56 lemma lless_imp_le:
    57   fixes R (structure)
    58   assumes "x \<sqsubset> y"
    59   shows "x \<sqsubseteq> y"
    60   using assms unfolding lless_def by simp
    61 
    62 lemma weak_lless_imp_not_eq:
    63   fixes R (structure)
    64   assumes "x \<sqsubset> y"
    65   shows "\<not> (x .= y)"
    66   using assms unfolding lless_def by simp
    67 
    68 lemma weak_llessE:
    69   fixes R (structure)
    70   assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
    71   shows "P"
    72   using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
    73 
    74 lemma (in weak_partial_order) lless_cong_l [trans]:
    75   assumes xx': "x .= x'"
    76     and xy: "x' \<sqsubset> y"
    77     and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
    78   shows "x \<sqsubset> y"
    79   using assms unfolding lless_def by (auto intro: trans sym)
    80 
    81 lemma (in weak_partial_order) lless_cong_r [trans]:
    82   assumes xy: "x \<sqsubset> y"
    83     and  yy': "y .= y'"
    84     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
    85   shows "x \<sqsubset> y'"
    86   using assms unfolding lless_def by (auto intro: trans sym)
    87 
    88 
    89 lemma (in weak_partial_order) lless_antisym:
    90   assumes "a \<in> carrier L" "b \<in> carrier L"
    91     and "a \<sqsubset> b" "b \<sqsubset> a"
    92   shows "P"
    93   using assms
    94   by (elim weak_llessE) auto
    95 
    96 lemma (in weak_partial_order) lless_trans [trans]:
    97   assumes "a \<sqsubset> b" "b \<sqsubset> c"
    98     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
    99   shows "a \<sqsubset> c"
   100   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
   101 
   102 
   103 subsubsection {* Upper and lower bounds of a set *}
   104 
   105 constdefs (structure L)
   106   Upper :: "[_, 'a set] => 'a set"
   107   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
   108 
   109   Lower :: "[_, 'a set] => 'a set"
   110   "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
   111 
   112 lemma Upper_closed [intro!, simp]:
   113   "Upper L A \<subseteq> carrier L"
   114   by (unfold Upper_def) clarify
   115 
   116 lemma Upper_memD [dest]:
   117   fixes L (structure)
   118   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   119   by (unfold Upper_def) blast
   120 
   121 lemma (in weak_partial_order) Upper_elemD [dest]:
   122   "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   123   unfolding Upper_def elem_def
   124   by (blast dest: sym)
   125 
   126 lemma Upper_memI:
   127   fixes L (structure)
   128   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   129   by (unfold Upper_def) blast
   130 
   131 lemma (in weak_partial_order) Upper_elemI:
   132   "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
   133   unfolding Upper_def by blast
   134 
   135 lemma Upper_antimono:
   136   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   137   by (unfold Upper_def) blast
   138 
   139 lemma (in weak_partial_order) Upper_is_closed [simp]:
   140   "A \<subseteq> carrier L ==> is_closed (Upper L A)"
   141   by (rule is_closedI) (blast intro: Upper_memI)+
   142 
   143 lemma (in weak_partial_order) Upper_mem_cong:
   144   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   145     and aa': "a .= a'"
   146     and aelem: "a \<in> Upper L A"
   147   shows "a' \<in> Upper L A"
   148 proof (rule Upper_memI[OF _ a'carr])
   149   fix y
   150   assume yA: "y \<in> A"
   151   hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
   152   also note aa'
   153   finally
   154       show "y \<sqsubseteq> a'"
   155       by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
   156 qed
   157 
   158 lemma (in weak_partial_order) Upper_cong:
   159   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   160     and AA': "A {.=} A'"
   161   shows "Upper L A = Upper L A'"
   162 unfolding Upper_def
   163 apply rule
   164  apply (rule, clarsimp) defer 1
   165  apply (rule, clarsimp) defer 1
   166 proof -
   167   fix x a'
   168   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   169     and a'A': "a' \<in> A'"
   170   assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
   171 
   172   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   173   from this obtain a
   174       where aA: "a \<in> A"
   175       and a'a: "a' .= a"
   176       by auto
   177   note [simp] = subsetD[OF Acarr aA] carr
   178 
   179   note a'a
   180   also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
   181   finally show "a' \<sqsubseteq> x" by simp
   182 next
   183   fix x a
   184   assume carr: "x \<in> carrier L" "a \<in> carrier L"
   185     and aA: "a \<in> A"
   186   assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
   187 
   188   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   189   from this obtain a'
   190       where a'A': "a' \<in> A'"
   191       and aa': "a .= a'"
   192       by auto
   193   note [simp] = subsetD[OF A'carr a'A'] carr
   194 
   195   note aa'
   196   also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
   197   finally show "a \<sqsubseteq> x" by simp
   198 qed
   199 
   200 lemma Lower_closed [intro!, simp]:
   201   "Lower L A \<subseteq> carrier L"
   202   by (unfold Lower_def) clarify
   203 
   204 lemma Lower_memD [dest]:
   205   fixes L (structure)
   206   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   207   by (unfold Lower_def) blast
   208 
   209 lemma Lower_memI:
   210   fixes L (structure)
   211   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   212   by (unfold Lower_def) blast
   213 
   214 lemma Lower_antimono:
   215   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   216   by (unfold Lower_def) blast
   217 
   218 lemma (in weak_partial_order) Lower_is_closed [simp]:
   219   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
   220   by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
   221 
   222 lemma (in weak_partial_order) Lower_mem_cong:
   223   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   224     and aa': "a .= a'"
   225     and aelem: "a \<in> Lower L A"
   226   shows "a' \<in> Lower L A"
   227 using assms Lower_closed[of L A]
   228 by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
   229 
   230 lemma (in weak_partial_order) Lower_cong:
   231   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   232     and AA': "A {.=} A'"
   233   shows "Lower L A = Lower L A'"
   234 using Lower_memD[of y]
   235 unfolding Lower_def
   236 apply safe
   237  apply clarsimp defer 1
   238  apply clarsimp defer 1
   239 proof -
   240   fix x a'
   241   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   242     and a'A': "a' \<in> A'"
   243   assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
   244   hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
   245 
   246   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   247   from this obtain a
   248       where aA: "a \<in> A"
   249       and a'a: "a' .= a"
   250       by auto
   251 
   252   from aA and subsetD[OF Acarr aA]
   253       have "x \<sqsubseteq> a" by (rule aLxCond)
   254   also note a'a[symmetric]
   255   finally
   256       show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
   257 next
   258   fix x a
   259   assume carr: "x \<in> carrier L" "a \<in> carrier L"
   260     and aA: "a \<in> A"
   261   assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
   262   hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
   263 
   264   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   265   from this obtain a'
   266       where a'A': "a' \<in> A'"
   267       and aa': "a .= a'"
   268       by auto
   269   from a'A' and subsetD[OF A'carr a'A']
   270       have "x \<sqsubseteq> a'" by (rule a'LxCond)
   271   also note aa'[symmetric]
   272   finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
   273 qed
   274 
   275 
   276 subsubsection {* Least and greatest, as predicate *}
   277 
   278 constdefs (structure L)
   279   least :: "[_, 'a, 'a set] => bool"
   280   "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
   281 
   282   greatest :: "[_, 'a, 'a set] => bool"
   283   "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
   284 
   285 text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
   286   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
   287 
   288 lemma least_closed [intro, simp]:
   289   "least L l A ==> l \<in> carrier L"
   290   by (unfold least_def) fast
   291 
   292 lemma least_mem:
   293   "least L l A ==> l \<in> A"
   294   by (unfold least_def) fast
   295 
   296 lemma (in weak_partial_order) weak_least_unique:
   297   "[| least L x A; least L y A |] ==> x .= y"
   298   by (unfold least_def) blast
   299 
   300 lemma least_le:
   301   fixes L (structure)
   302   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   303   by (unfold least_def) fast
   304 
   305 lemma (in weak_partial_order) least_cong:
   306   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   307   by (unfold least_def) (auto dest: sym)
   308 
   309 text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
   310   @{term "A {.=} A'"} *}
   311 
   312 lemma (in weak_partial_order) least_Upper_cong_l:
   313   assumes "x .= x'"
   314     and "x \<in> carrier L" "x' \<in> carrier L"
   315     and "A \<subseteq> carrier L"
   316   shows "least L x (Upper L A) = least L x' (Upper L A)"
   317   apply (rule least_cong) using assms by auto
   318 
   319 lemma (in weak_partial_order) least_Upper_cong_r:
   320   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
   321     and AA': "A {.=} A'"
   322   shows "least L x (Upper L A) = least L x (Upper L A')"
   323 apply (subgoal_tac "Upper L A = Upper L A'", simp)
   324 by (rule Upper_cong) fact+
   325 
   326 lemma least_UpperI:
   327   fixes L (structure)
   328   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   329     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   330     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   331   shows "least L s (Upper L A)"
   332 proof -
   333   have "Upper L A \<subseteq> carrier L" by simp
   334   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   335   moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   336   ultimately show ?thesis by (simp add: least_def)
   337 qed
   338 
   339 lemma least_Upper_above:
   340   fixes L (structure)
   341   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   342   by (unfold least_def) blast
   343 
   344 lemma greatest_closed [intro, simp]:
   345   "greatest L l A ==> l \<in> carrier L"
   346   by (unfold greatest_def) fast
   347 
   348 lemma greatest_mem:
   349   "greatest L l A ==> l \<in> A"
   350   by (unfold greatest_def) fast
   351 
   352 lemma (in weak_partial_order) weak_greatest_unique:
   353   "[| greatest L x A; greatest L y A |] ==> x .= y"
   354   by (unfold greatest_def) blast
   355 
   356 lemma greatest_le:
   357   fixes L (structure)
   358   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   359   by (unfold greatest_def) fast
   360 
   361 lemma (in weak_partial_order) greatest_cong:
   362   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   363   greatest L x A = greatest L x' A"
   364   by (unfold greatest_def) (auto dest: sym)
   365 
   366 text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
   367   @{term "A {.=} A'"} *}
   368 
   369 lemma (in weak_partial_order) greatest_Lower_cong_l:
   370   assumes "x .= x'"
   371     and "x \<in> carrier L" "x' \<in> carrier L"
   372     and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
   373   shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
   374   apply (rule greatest_cong) using assms by auto
   375 
   376 lemma (in weak_partial_order) greatest_Lower_cong_r:
   377   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
   378     and AA': "A {.=} A'"
   379   shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
   380 apply (subgoal_tac "Lower L A = Lower L A'", simp)
   381 by (rule Lower_cong) fact+
   382 
   383 lemma greatest_LowerI:
   384   fixes L (structure)
   385   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   386     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   387     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   388   shows "greatest L i (Lower L A)"
   389 proof -
   390   have "Lower L A \<subseteq> carrier L" by simp
   391   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   392   moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   393   ultimately show ?thesis by (simp add: greatest_def)
   394 qed
   395 
   396 lemma greatest_Lower_below:
   397   fixes L (structure)
   398   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   399   by (unfold greatest_def) blast
   400 
   401 text {* Supremum and infimum *}
   402 
   403 constdefs (structure L)
   404   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   405   "\<Squnion>A == SOME x. least L x (Upper L A)"
   406 
   407   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   408   "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
   409 
   410   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   411   "x \<squnion> y == \<Squnion> {x, y}"
   412 
   413   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   414   "x \<sqinter> y == \<Sqinter> {x, y}"
   415 
   416 
   417 subsection {* Lattices *}
   418 
   419 locale weak_upper_semilattice = weak_partial_order +
   420   assumes sup_of_two_exists:
   421     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   422 
   423 locale weak_lower_semilattice = weak_partial_order +
   424   assumes inf_of_two_exists:
   425     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   426 
   427 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
   428 
   429 
   430 subsubsection {* Supremum *}
   431 
   432 lemma (in weak_upper_semilattice) joinI:
   433   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   434   ==> P (x \<squnion> y)"
   435 proof (unfold join_def sup_def)
   436   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   437     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   438   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   439   with L show "P (SOME l. least L l (Upper L {x, y}))"
   440     by (fast intro: someI2 P)
   441 qed
   442 
   443 lemma (in weak_upper_semilattice) join_closed [simp]:
   444   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   445   by (rule joinI) (rule least_closed)
   446 
   447 lemma (in weak_upper_semilattice) join_cong_l:
   448   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   449     and xx': "x .= x'"
   450   shows "x \<squnion> y .= x' \<squnion> y"
   451 proof (rule joinI, rule joinI)
   452   fix a b
   453   from xx' carr
   454       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   455 
   456   assume leasta: "least L a (Upper L {x, y})"
   457   assume "least L b (Upper L {x', y})"
   458   with carr
   459       have leastb: "least L b (Upper L {x, y})"
   460       by (simp add: least_Upper_cong_r[OF _ _ seq])
   461 
   462   from leasta leastb
   463       show "a .= b" by (rule weak_least_unique)
   464 qed (rule carr)+
   465 
   466 lemma (in weak_upper_semilattice) join_cong_r:
   467   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   468     and yy': "y .= y'"
   469   shows "x \<squnion> y .= x \<squnion> y'"
   470 proof (rule joinI, rule joinI)
   471   fix a b
   472   have "{x, y} = {y, x}" by fast
   473   also from carr yy'
   474       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   475   also have "{y', x} = {x, y'}" by fast
   476   finally
   477       have seq: "{x, y} {.=} {x, y'}" .
   478 
   479   assume leasta: "least L a (Upper L {x, y})"
   480   assume "least L b (Upper L {x, y'})"
   481   with carr
   482       have leastb: "least L b (Upper L {x, y})"
   483       by (simp add: least_Upper_cong_r[OF _ _ seq])
   484 
   485   from leasta leastb
   486       show "a .= b" by (rule weak_least_unique)
   487 qed (rule carr)+
   488 
   489 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   490   "x \<in> carrier L ==> least L x (Upper L {x})"
   491   by (rule least_UpperI) auto
   492 
   493 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
   494   "x \<in> carrier L ==> \<Squnion>{x} .= x"
   495   unfolding sup_def
   496   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
   497 
   498 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
   499   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
   500   unfolding sup_def
   501   by (rule someI2) (auto intro: sup_of_singletonI)
   502 
   503 text {* Condition on @{text A}: supremum exists. *}
   504 
   505 lemma (in weak_upper_semilattice) sup_insertI:
   506   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   507   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   508   ==> P (\<Squnion>(insert x A))"
   509 proof (unfold sup_def)
   510   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   511     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   512     and least_a: "least L a (Upper L A)"
   513   from L least_a have La: "a \<in> carrier L" by simp
   514   from L sup_of_two_exists least_a
   515   obtain s where least_s: "least L s (Upper L {a, x})" by blast
   516   show "P (SOME l. least L l (Upper L (insert x A)))"
   517   proof (rule someI2)
   518     show "least L s (Upper L (insert x A))"
   519     proof (rule least_UpperI)
   520       fix z
   521       assume "z \<in> insert x A"
   522       then show "z \<sqsubseteq> s"
   523       proof
   524         assume "z = x" then show ?thesis
   525           by (simp add: least_Upper_above [OF least_s] L La)
   526       next
   527         assume "z \<in> A"
   528         with L least_s least_a show ?thesis
   529           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
   530       qed
   531     next
   532       fix y
   533       assume y: "y \<in> Upper L (insert x A)"
   534       show "s \<sqsubseteq> y"
   535       proof (rule least_le [OF least_s], rule Upper_memI)
   536 	fix z
   537 	assume z: "z \<in> {a, x}"
   538 	then show "z \<sqsubseteq> y"
   539 	proof
   540           have y': "y \<in> Upper L A"
   541             apply (rule subsetD [where A = "Upper L (insert x A)"])
   542              apply (rule Upper_antimono)
   543 	     apply blast
   544 	    apply (rule y)
   545             done
   546           assume "z = a"
   547           with y' least_a show ?thesis by (fast dest: least_le)
   548 	next
   549 	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
   550           with y L show ?thesis by blast
   551 	qed
   552       qed (rule Upper_closed [THEN subsetD, OF y])
   553     next
   554       from L show "insert x A \<subseteq> carrier L" by simp
   555       from least_s show "s \<in> carrier L" by simp
   556     qed
   557   qed (rule P)
   558 qed
   559 
   560 lemma (in weak_upper_semilattice) finite_sup_least:
   561   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   562 proof (induct set: finite)
   563   case empty
   564   then show ?case by simp
   565 next
   566   case (insert x A)
   567   show ?case
   568   proof (cases "A = {}")
   569     case True
   570     with insert show ?thesis
   571       by simp (simp add: least_cong [OF weak_sup_of_singleton]
   572 	sup_of_singleton_closed sup_of_singletonI)
   573 	(* The above step is hairy; least_cong can make simp loop.
   574 	Would want special version of simp to apply least_cong. *)
   575   next
   576     case False
   577     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   578     with _ show ?thesis
   579       by (rule sup_insertI) (simp_all add: insert [simplified])
   580   qed
   581 qed
   582 
   583 lemma (in weak_upper_semilattice) finite_sup_insertI:
   584   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   585     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   586   shows "P (\<Squnion> (insert x A))"
   587 proof (cases "A = {}")
   588   case True with P and xA show ?thesis
   589     by (simp add: finite_sup_least)
   590 next
   591   case False with P and xA show ?thesis
   592     by (simp add: sup_insertI finite_sup_least)
   593 qed
   594 
   595 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
   596   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   597 proof (induct set: finite)
   598   case empty then show ?case by simp
   599 next
   600   case insert then show ?case
   601     by - (rule finite_sup_insertI, simp_all)
   602 qed
   603 
   604 lemma (in weak_upper_semilattice) join_left:
   605   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   606   by (rule joinI [folded join_def]) (blast dest: least_mem)
   607 
   608 lemma (in weak_upper_semilattice) join_right:
   609   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   610   by (rule joinI [folded join_def]) (blast dest: least_mem)
   611 
   612 lemma (in weak_upper_semilattice) sup_of_two_least:
   613   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   614 proof (unfold sup_def)
   615   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   616   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   617   with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
   618   by (fast intro: someI2 weak_least_unique)  (* blast fails *)
   619 qed
   620 
   621 lemma (in weak_upper_semilattice) join_le:
   622   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   623     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   624   shows "x \<squnion> y \<sqsubseteq> z"
   625 proof (rule joinI [OF _ x y])
   626   fix s
   627   assume "least L s (Upper L {x, y})"
   628   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   629 qed
   630 
   631 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   632   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   633   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
   634 proof (rule finite_sup_insertI)
   635   -- {* The textbook argument in Jacobson I, p 457 *}
   636   fix s
   637   assume sup: "least L s (Upper L {x, y, z})"
   638   show "x \<squnion> (y \<squnion> z) .= s"
   639   proof (rule weak_le_anti_sym)
   640     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   641       by (fastsimp intro!: join_le elim: least_Upper_above)
   642   next
   643     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   644     by (erule_tac least_le)
   645       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
   646   qed (simp_all add: L least_closed [OF sup])
   647 qed (simp_all add: L)
   648 
   649 text {* Commutativity holds for @{text "="}. *}
   650 
   651 lemma join_comm:
   652   fixes L (structure)
   653   shows "x \<squnion> y = y \<squnion> x"
   654   by (unfold join_def) (simp add: insert_commute)
   655 
   656 lemma (in weak_upper_semilattice) weak_join_assoc:
   657   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   658   shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
   659 proof -
   660   (* FIXME: could be simplified by improved simp: uniform use of .=,
   661      omit [symmetric] in last step. *)
   662   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   663   also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
   664   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
   665   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
   666   finally show ?thesis by (simp add: L)
   667 qed
   668 
   669 
   670 subsubsection {* Infimum *}
   671 
   672 lemma (in weak_lower_semilattice) meetI:
   673   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   674   x \<in> carrier L; y \<in> carrier L |]
   675   ==> P (x \<sqinter> y)"
   676 proof (unfold meet_def inf_def)
   677   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   678     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   679   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   680   with L show "P (SOME g. greatest L g (Lower L {x, y}))"
   681   by (fast intro: someI2 weak_greatest_unique P)
   682 qed
   683 
   684 lemma (in weak_lower_semilattice) meet_closed [simp]:
   685   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   686   by (rule meetI) (rule greatest_closed)
   687 
   688 lemma (in weak_lower_semilattice) meet_cong_l:
   689   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   690     and xx': "x .= x'"
   691   shows "x \<sqinter> y .= x' \<sqinter> y"
   692 proof (rule meetI, rule meetI)
   693   fix a b
   694   from xx' carr
   695       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   696 
   697   assume greatesta: "greatest L a (Lower L {x, y})"
   698   assume "greatest L b (Lower L {x', y})"
   699   with carr
   700       have greatestb: "greatest L b (Lower L {x, y})"
   701       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
   702 
   703   from greatesta greatestb
   704       show "a .= b" by (rule weak_greatest_unique)
   705 qed (rule carr)+
   706 
   707 lemma (in weak_lower_semilattice) meet_cong_r:
   708   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   709     and yy': "y .= y'"
   710   shows "x \<sqinter> y .= x \<sqinter> y'"
   711 proof (rule meetI, rule meetI)
   712   fix a b
   713   have "{x, y} = {y, x}" by fast
   714   also from carr yy'
   715       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   716   also have "{y', x} = {x, y'}" by fast
   717   finally
   718       have seq: "{x, y} {.=} {x, y'}" .
   719 
   720   assume greatesta: "greatest L a (Lower L {x, y})"
   721   assume "greatest L b (Lower L {x, y'})"
   722   with carr
   723       have greatestb: "greatest L b (Lower L {x, y})"
   724       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
   725 
   726   from greatesta greatestb
   727       show "a .= b" by (rule weak_greatest_unique)
   728 qed (rule carr)+
   729 
   730 lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   731   "x \<in> carrier L ==> greatest L x (Lower L {x})"
   732   by (rule greatest_LowerI) auto
   733 
   734 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
   735   "x \<in> carrier L ==> \<Sqinter>{x} .= x"
   736   unfolding inf_def
   737   by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
   738 
   739 lemma (in weak_partial_order) inf_of_singleton_closed:
   740   "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
   741   unfolding inf_def
   742   by (rule someI2) (auto intro: inf_of_singletonI)
   743 
   744 text {* Condition on @{text A}: infimum exists. *}
   745 
   746 lemma (in weak_lower_semilattice) inf_insertI:
   747   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   748   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   749   ==> P (\<Sqinter>(insert x A))"
   750 proof (unfold inf_def)
   751   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   752     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
   753     and greatest_a: "greatest L a (Lower L A)"
   754   from L greatest_a have La: "a \<in> carrier L" by simp
   755   from L inf_of_two_exists greatest_a
   756   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   757   show "P (SOME g. greatest L g (Lower L (insert x A)))"
   758   proof (rule someI2)
   759     show "greatest L i (Lower L (insert x A))"
   760     proof (rule greatest_LowerI)
   761       fix z
   762       assume "z \<in> insert x A"
   763       then show "i \<sqsubseteq> z"
   764       proof
   765         assume "z = x" then show ?thesis
   766           by (simp add: greatest_Lower_below [OF greatest_i] L La)
   767       next
   768         assume "z \<in> A"
   769         with L greatest_i greatest_a show ?thesis
   770           by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
   771       qed
   772     next
   773       fix y
   774       assume y: "y \<in> Lower L (insert x A)"
   775       show "y \<sqsubseteq> i"
   776       proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   777 	fix z
   778 	assume z: "z \<in> {a, x}"
   779 	then show "y \<sqsubseteq> z"
   780 	proof
   781           have y': "y \<in> Lower L A"
   782             apply (rule subsetD [where A = "Lower L (insert x A)"])
   783             apply (rule Lower_antimono)
   784 	     apply blast
   785 	    apply (rule y)
   786             done
   787           assume "z = a"
   788           with y' greatest_a show ?thesis by (fast dest: greatest_le)
   789 	next
   790           assume "z \<in> {x}"
   791           with y L show ?thesis by blast
   792 	qed
   793       qed (rule Lower_closed [THEN subsetD, OF y])
   794     next
   795       from L show "insert x A \<subseteq> carrier L" by simp
   796       from greatest_i show "i \<in> carrier L" by simp
   797     qed
   798   qed (rule P)
   799 qed
   800 
   801 lemma (in weak_lower_semilattice) finite_inf_greatest:
   802   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   803 proof (induct set: finite)
   804   case empty then show ?case by simp
   805 next
   806   case (insert x A)
   807   show ?case
   808   proof (cases "A = {}")
   809     case True
   810     with insert show ?thesis
   811       by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
   812 	inf_of_singleton_closed inf_of_singletonI)
   813   next
   814     case False
   815     from insert show ?thesis
   816     proof (rule_tac inf_insertI)
   817       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
   818     qed simp_all
   819   qed
   820 qed
   821 
   822 lemma (in weak_lower_semilattice) finite_inf_insertI:
   823   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   824     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   825   shows "P (\<Sqinter> (insert x A))"
   826 proof (cases "A = {}")
   827   case True with P and xA show ?thesis
   828     by (simp add: finite_inf_greatest)
   829 next
   830   case False with P and xA show ?thesis
   831     by (simp add: inf_insertI finite_inf_greatest)
   832 qed
   833 
   834 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
   835   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   836 proof (induct set: finite)
   837   case empty then show ?case by simp
   838 next
   839   case insert then show ?case
   840     by (rule_tac finite_inf_insertI) (simp_all)
   841 qed
   842 
   843 lemma (in weak_lower_semilattice) meet_left:
   844   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   845   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   846 
   847 lemma (in weak_lower_semilattice) meet_right:
   848   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   849   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   850 
   851 lemma (in weak_lower_semilattice) inf_of_two_greatest:
   852   "[| x \<in> carrier L; y \<in> carrier L |] ==>
   853   greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   854 proof (unfold inf_def)
   855   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   856   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   857   with L
   858   show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
   859   by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
   860 qed
   861 
   862 lemma (in weak_lower_semilattice) meet_le:
   863   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   864     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   865   shows "z \<sqsubseteq> x \<sqinter> y"
   866 proof (rule meetI [OF _ x y])
   867   fix i
   868   assume "greatest L i (Lower L {x, y})"
   869   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   870 qed
   871 
   872 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
   873   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   874   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
   875 proof (rule finite_inf_insertI)
   876   txt {* The textbook argument in Jacobson I, p 457 *}
   877   fix i
   878   assume inf: "greatest L i (Lower L {x, y, z})"
   879   show "x \<sqinter> (y \<sqinter> z) .= i"
   880   proof (rule weak_le_anti_sym)
   881     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   882       by (fastsimp intro!: meet_le elim: greatest_Lower_below)
   883   next
   884     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
   885     by (erule_tac greatest_le)
   886       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
   887   qed (simp_all add: L greatest_closed [OF inf])
   888 qed (simp_all add: L)
   889 
   890 lemma meet_comm:
   891   fixes L (structure)
   892   shows "x \<sqinter> y = y \<sqinter> x"
   893   by (unfold meet_def) (simp add: insert_commute)
   894 
   895 lemma (in weak_lower_semilattice) weak_meet_assoc:
   896   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   897   shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
   898 proof -
   899   (* FIXME: improved simp, see weak_join_assoc above *)
   900   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   901   also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
   902   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
   903   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   904   finally show ?thesis by (simp add: L)
   905 qed
   906 
   907 
   908 subsection {* Total Orders *}
   909 
   910 locale weak_total_order = weak_partial_order +
   911   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   912 
   913 text {* Introduction rule: the usual definition of total order *}
   914 
   915 lemma (in weak_partial_order) weak_total_orderI:
   916   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   917   shows "weak_total_order L"
   918   proof qed (rule total)
   919 
   920 text {* Total orders are lattices. *}
   921 
   922 sublocale weak_total_order < weak: weak_lattice
   923 proof
   924   fix x y
   925   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   926   show "EX s. least L s (Upper L {x, y})"
   927   proof -
   928     note total L
   929     moreover
   930     {
   931       assume "x \<sqsubseteq> y"
   932       with L have "least L y (Upper L {x, y})"
   933         by (rule_tac least_UpperI) auto
   934     }
   935     moreover
   936     {
   937       assume "y \<sqsubseteq> x"
   938       with L have "least L x (Upper L {x, y})"
   939         by (rule_tac least_UpperI) auto
   940     }
   941     ultimately show ?thesis by blast
   942   qed
   943 next
   944   fix x y
   945   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   946   show "EX i. greatest L i (Lower L {x, y})"
   947   proof -
   948     note total L
   949     moreover
   950     {
   951       assume "y \<sqsubseteq> x"
   952       with L have "greatest L y (Lower L {x, y})"
   953         by (rule_tac greatest_LowerI) auto
   954     }
   955     moreover
   956     {
   957       assume "x \<sqsubseteq> y"
   958       with L have "greatest L x (Lower L {x, y})"
   959         by (rule_tac greatest_LowerI) auto
   960     }
   961     ultimately show ?thesis by blast
   962   qed
   963 qed
   964 
   965 
   966 subsection {* Complete Lattices *}
   967 
   968 locale weak_complete_lattice = weak_lattice +
   969   assumes sup_exists:
   970     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   971     and inf_exists:
   972     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   973 
   974 text {* Introduction rule: the usual definition of complete lattice *}
   975 
   976 lemma (in weak_partial_order) weak_complete_latticeI:
   977   assumes sup_exists:
   978     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   979     and inf_exists:
   980     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   981   shows "weak_complete_lattice L"
   982   proof qed (auto intro: sup_exists inf_exists)
   983 
   984 constdefs (structure L)
   985   top :: "_ => 'a" ("\<top>\<index>")
   986   "\<top> == sup L (carrier L)"
   987 
   988   bottom :: "_ => 'a" ("\<bottom>\<index>")
   989   "\<bottom> == inf L (carrier L)"
   990 
   991 
   992 lemma (in weak_complete_lattice) supI:
   993   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   994   ==> P (\<Squnion>A)"
   995 proof (unfold sup_def)
   996   assume L: "A \<subseteq> carrier L"
   997     and P: "!!l. least L l (Upper L A) ==> P l"
   998   with sup_exists obtain s where "least L s (Upper L A)" by blast
   999   with L show "P (SOME l. least L l (Upper L A))"
  1000   by (fast intro: someI2 weak_least_unique P)
  1001 qed
  1002 
  1003 lemma (in weak_complete_lattice) sup_closed [simp]:
  1004   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
  1005   by (rule supI) simp_all
  1006 
  1007 lemma (in weak_complete_lattice) top_closed [simp, intro]:
  1008   "\<top> \<in> carrier L"
  1009   by (unfold top_def) simp
  1010 
  1011 lemma (in weak_complete_lattice) infI:
  1012   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
  1013   ==> P (\<Sqinter>A)"
  1014 proof (unfold inf_def)
  1015   assume L: "A \<subseteq> carrier L"
  1016     and P: "!!l. greatest L l (Lower L A) ==> P l"
  1017   with inf_exists obtain s where "greatest L s (Lower L A)" by blast
  1018   with L show "P (SOME l. greatest L l (Lower L A))"
  1019   by (fast intro: someI2 weak_greatest_unique P)
  1020 qed
  1021 
  1022 lemma (in weak_complete_lattice) inf_closed [simp]:
  1023   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
  1024   by (rule infI) simp_all
  1025 
  1026 lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
  1027   "\<bottom> \<in> carrier L"
  1028   by (unfold bottom_def) simp
  1029 
  1030 text {* Jacobson: Theorem 8.1 *}
  1031 
  1032 lemma Lower_empty [simp]:
  1033   "Lower L {} = carrier L"
  1034   by (unfold Lower_def) simp
  1035 
  1036 lemma Upper_empty [simp]:
  1037   "Upper L {} = carrier L"
  1038   by (unfold Upper_def) simp
  1039 
  1040 theorem (in weak_partial_order) weak_complete_lattice_criterion1:
  1041   assumes top_exists: "EX g. greatest L g (carrier L)"
  1042     and inf_exists:
  1043       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
  1044   shows "weak_complete_lattice L"
  1045 proof (rule weak_complete_latticeI)
  1046   from top_exists obtain top where top: "greatest L top (carrier L)" ..
  1047   fix A
  1048   assume L: "A \<subseteq> carrier L"
  1049   let ?B = "Upper L A"
  1050   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
  1051   then have B_non_empty: "?B ~= {}" by fast
  1052   have B_L: "?B \<subseteq> carrier L" by simp
  1053   from inf_exists [OF B_L B_non_empty]
  1054   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
  1055   have "least L b (Upper L A)"
  1056 apply (rule least_UpperI)
  1057    apply (rule greatest_le [where A = "Lower L ?B"])
  1058     apply (rule b_inf_B)
  1059    apply (rule Lower_memI)
  1060     apply (erule Upper_memD [THEN conjunct1])
  1061      apply assumption
  1062     apply (rule L)
  1063    apply (fast intro: L [THEN subsetD])
  1064   apply (erule greatest_Lower_below [OF b_inf_B])
  1065   apply simp
  1066  apply (rule L)
  1067 apply (rule greatest_closed [OF b_inf_B])
  1068 done
  1069   then show "EX s. least L s (Upper L A)" ..
  1070 next
  1071   fix A
  1072   assume L: "A \<subseteq> carrier L"
  1073   show "EX i. greatest L i (Lower L A)"
  1074   proof (cases "A = {}")
  1075     case True then show ?thesis
  1076       by (simp add: top_exists)
  1077   next
  1078     case False with L show ?thesis
  1079       by (rule inf_exists)
  1080   qed
  1081 qed
  1082 
  1083 (* TODO: prove dual version *)
  1084 
  1085 
  1086 subsection {* Orders and Lattices where @{text eq} is the Equality *}
  1087 
  1088 locale partial_order = weak_partial_order +
  1089   assumes eq_is_equal: "op .= = op ="
  1090 begin
  1091 
  1092 declare weak_le_anti_sym [rule del]
  1093 
  1094 lemma le_anti_sym [intro]:
  1095   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
  1096   using weak_le_anti_sym unfolding eq_is_equal .
  1097 
  1098 lemma lless_eq:
  1099   "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
  1100   unfolding lless_def by (simp add: eq_is_equal)
  1101 
  1102 lemma lless_asym:
  1103   assumes "a \<in> carrier L" "b \<in> carrier L"
  1104     and "a \<sqsubset> b" "b \<sqsubset> a"
  1105   shows "P"
  1106   using assms unfolding lless_eq by auto
  1107 
  1108 end
  1109 
  1110 
  1111 text {* Least and greatest, as predicate *}
  1112 
  1113 lemma (in partial_order) least_unique:
  1114   "[| least L x A; least L y A |] ==> x = y"
  1115   using weak_least_unique unfolding eq_is_equal .
  1116 
  1117 lemma (in partial_order) greatest_unique:
  1118   "[| greatest L x A; greatest L y A |] ==> x = y"
  1119   using weak_greatest_unique unfolding eq_is_equal .
  1120 
  1121 
  1122 text {* Lattices *}
  1123 
  1124 locale upper_semilattice = partial_order +
  1125   assumes sup_of_two_exists:
  1126     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
  1127 
  1128 sublocale upper_semilattice < weak: weak_upper_semilattice
  1129   proof qed (rule sup_of_two_exists)
  1130 
  1131 locale lower_semilattice = partial_order +
  1132   assumes inf_of_two_exists:
  1133     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
  1134 
  1135 sublocale lower_semilattice < weak: weak_lower_semilattice
  1136   proof qed (rule inf_of_two_exists)
  1137 
  1138 locale lattice = upper_semilattice + lower_semilattice
  1139 
  1140 
  1141 text {* Supremum *}
  1142 
  1143 declare (in partial_order) weak_sup_of_singleton [simp del]
  1144 
  1145 lemma (in partial_order) sup_of_singleton [simp]:
  1146   "x \<in> carrier L ==> \<Squnion>{x} = x"
  1147   using weak_sup_of_singleton unfolding eq_is_equal .
  1148 
  1149 lemma (in upper_semilattice) join_assoc_lemma:
  1150   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  1151   shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
  1152   using weak_join_assoc_lemma L unfolding eq_is_equal .
  1153 
  1154 lemma (in upper_semilattice) join_assoc:
  1155   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  1156   shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
  1157   using weak_join_assoc L unfolding eq_is_equal .
  1158 
  1159 
  1160 text {* Infimum *}
  1161 
  1162 declare (in partial_order) weak_inf_of_singleton [simp del]
  1163 
  1164 lemma (in partial_order) inf_of_singleton [simp]:
  1165   "x \<in> carrier L ==> \<Sqinter>{x} = x"
  1166   using weak_inf_of_singleton unfolding eq_is_equal .
  1167 
  1168 text {* Condition on @{text A}: infimum exists. *}
  1169 
  1170 lemma (in lower_semilattice) meet_assoc_lemma:
  1171   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  1172   shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
  1173   using weak_meet_assoc_lemma L unfolding eq_is_equal .
  1174 
  1175 lemma (in lower_semilattice) meet_assoc:
  1176   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  1177   shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
  1178   using weak_meet_assoc L unfolding eq_is_equal .
  1179 
  1180 
  1181 text {* Total Orders *}
  1182 
  1183 locale total_order = partial_order +
  1184   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  1185 
  1186 sublocale total_order < weak: weak_total_order
  1187   proof qed (rule total_order_total)
  1188 
  1189 text {* Introduction rule: the usual definition of total order *}
  1190 
  1191 lemma (in partial_order) total_orderI:
  1192   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  1193   shows "total_order L"
  1194   proof qed (rule total)
  1195 
  1196 text {* Total orders are lattices. *}
  1197 
  1198 sublocale total_order < weak: lattice
  1199   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
  1200 
  1201 
  1202 text {* Complete lattices *}
  1203 
  1204 locale complete_lattice = lattice +
  1205   assumes sup_exists:
  1206     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
  1207     and inf_exists:
  1208     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
  1209 
  1210 sublocale complete_lattice < weak: weak_complete_lattice
  1211   proof qed (auto intro: sup_exists inf_exists)
  1212 
  1213 text {* Introduction rule: the usual definition of complete lattice *}
  1214 
  1215 lemma (in partial_order) complete_latticeI:
  1216   assumes sup_exists:
  1217     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
  1218     and inf_exists:
  1219     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
  1220   shows "complete_lattice L"
  1221   proof qed (auto intro: sup_exists inf_exists)
  1222 
  1223 theorem (in partial_order) complete_lattice_criterion1:
  1224   assumes top_exists: "EX g. greatest L g (carrier L)"
  1225     and inf_exists:
  1226       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
  1227   shows "complete_lattice L"
  1228 proof (rule complete_latticeI)
  1229   from top_exists obtain top where top: "greatest L top (carrier L)" ..
  1230   fix A
  1231   assume L: "A \<subseteq> carrier L"
  1232   let ?B = "Upper L A"
  1233   from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
  1234   then have B_non_empty: "?B ~= {}" by fast
  1235   have B_L: "?B \<subseteq> carrier L" by simp
  1236   from inf_exists [OF B_L B_non_empty]
  1237   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
  1238   have "least L b (Upper L A)"
  1239 apply (rule least_UpperI)
  1240    apply (rule greatest_le [where A = "Lower L ?B"])
  1241     apply (rule b_inf_B)
  1242    apply (rule Lower_memI)
  1243     apply (erule Upper_memD [THEN conjunct1])
  1244      apply assumption
  1245     apply (rule L)
  1246    apply (fast intro: L [THEN subsetD])
  1247   apply (erule greatest_Lower_below [OF b_inf_B])
  1248   apply simp
  1249  apply (rule L)
  1250 apply (rule greatest_closed [OF b_inf_B])
  1251 done
  1252   then show "EX s. least L s (Upper L A)" ..
  1253 next
  1254   fix A
  1255   assume L: "A \<subseteq> carrier L"
  1256   show "EX i. greatest L i (Lower L A)"
  1257   proof (cases "A = {}")
  1258     case True then show ?thesis
  1259       by (simp add: top_exists)
  1260   next
  1261     case False with L show ?thesis
  1262       by (rule inf_exists)
  1263   qed
  1264 qed
  1265 
  1266 (* TODO: prove dual version *)
  1267 
  1268 
  1269 subsection {* Examples *}
  1270 
  1271 subsubsection {* The Powerset of a Set is a Complete Lattice *}
  1272 
  1273 theorem powerset_is_complete_lattice:
  1274   "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
  1275   (is "complete_lattice ?L")
  1276 proof (rule partial_order.complete_latticeI)
  1277   show "partial_order ?L"
  1278     proof qed auto
  1279 next
  1280   fix B
  1281   assume B: "B \<subseteq> carrier ?L"
  1282   show "EX s. least ?L s (Upper ?L B)"
  1283   proof
  1284     from B show "least ?L (\<Union> B) (Upper ?L B)"
  1285       by (fastsimp intro!: least_UpperI simp: Upper_def)
  1286   qed
  1287 next
  1288   fix B
  1289   assume B: "B \<subseteq> carrier ?L"
  1290   show "EX i. greatest ?L i (Lower ?L B)"
  1291   proof
  1292     from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
  1293       txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
  1294 	@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
  1295       by (fastsimp intro!: greatest_LowerI simp: Lower_def)
  1296   qed
  1297 qed
  1298 
  1299 text {* An other example, that of the lattice of subgroups of a group,
  1300   can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
  1301 
  1302 end