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