src/HOL/Algebra/Lattice.thy
author nipkow
Mon Sep 12 07:55:43 2011 +0200 (2011-09-12)
changeset 44890 22f665a2e91c
parent 44655 fe0365331566
child 46008 c296c75f4cf4
permissions -rw-r--r--
new fastforce replacing fastsimp - less confusing name
     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>
    28       x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
    29 
    30 definition
    31   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    32   where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
    33 
    34 
    35 subsubsection {* The order relation *}
    36 
    37 context weak_partial_order
    38 begin
    39 
    40 lemma le_cong_l [intro, trans]:
    41   "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    42   by (auto intro: le_cong [THEN iffD2])
    43 
    44 lemma le_cong_r [intro, trans]:
    45   "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    46   by (auto intro: le_cong [THEN iffD1])
    47 
    48 lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
    49   by (simp add: le_cong_l)
    50 
    51 end
    52 
    53 lemma weak_llessI:
    54   fixes R (structure)
    55   assumes "x \<sqsubseteq> y" and "~(x .= y)"
    56   shows "x \<sqsubset> y"
    57   using assms unfolding lless_def by simp
    58 
    59 lemma lless_imp_le:
    60   fixes R (structure)
    61   assumes "x \<sqsubset> y"
    62   shows "x \<sqsubseteq> y"
    63   using assms unfolding lless_def by simp
    64 
    65 lemma weak_lless_imp_not_eq:
    66   fixes R (structure)
    67   assumes "x \<sqsubset> y"
    68   shows "\<not> (x .= y)"
    69   using assms unfolding lless_def by simp
    70 
    71 lemma weak_llessE:
    72   fixes R (structure)
    73   assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
    74   shows "P"
    75   using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
    76 
    77 lemma (in weak_partial_order) lless_cong_l [trans]:
    78   assumes xx': "x .= x'"
    79     and xy: "x' \<sqsubset> y"
    80     and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
    81   shows "x \<sqsubset> y"
    82   using assms unfolding lless_def by (auto intro: trans sym)
    83 
    84 lemma (in weak_partial_order) lless_cong_r [trans]:
    85   assumes xy: "x \<sqsubset> y"
    86     and  yy': "y .= y'"
    87     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
    88   shows "x \<sqsubset> y'"
    89   using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
    90 
    91 
    92 lemma (in weak_partial_order) lless_antisym:
    93   assumes "a \<in> carrier L" "b \<in> carrier L"
    94     and "a \<sqsubset> b" "b \<sqsubset> a"
    95   shows "P"
    96   using assms
    97   by (elim weak_llessE) auto
    98 
    99 lemma (in weak_partial_order) lless_trans [trans]:
   100   assumes "a \<sqsubset> b" "b \<sqsubset> c"
   101     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
   102   shows "a \<sqsubset> c"
   103   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
   104 
   105 
   106 subsubsection {* Upper and lower bounds of a set *}
   107 
   108 definition
   109   Upper :: "[_, 'a set] => 'a set"
   110   where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
   111 
   112 definition
   113   Lower :: "[_, 'a set] => 'a set"
   114   where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
   115 
   116 lemma Upper_closed [intro!, simp]:
   117   "Upper L A \<subseteq> carrier L"
   118   by (unfold Upper_def) clarify
   119 
   120 lemma Upper_memD [dest]:
   121   fixes L (structure)
   122   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   123   by (unfold Upper_def) blast
   124 
   125 lemma (in weak_partial_order) Upper_elemD [dest]:
   126   "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   127   unfolding Upper_def elem_def
   128   by (blast dest: sym)
   129 
   130 lemma Upper_memI:
   131   fixes L (structure)
   132   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   133   by (unfold Upper_def) blast
   134 
   135 lemma (in weak_partial_order) Upper_elemI:
   136   "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
   137   unfolding Upper_def by blast
   138 
   139 lemma Upper_antimono:
   140   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   141   by (unfold Upper_def) blast
   142 
   143 lemma (in weak_partial_order) Upper_is_closed [simp]:
   144   "A \<subseteq> carrier L ==> is_closed (Upper L A)"
   145   by (rule is_closedI) (blast intro: Upper_memI)+
   146 
   147 lemma (in weak_partial_order) Upper_mem_cong:
   148   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   149     and aa': "a .= a'"
   150     and aelem: "a \<in> Upper L A"
   151   shows "a' \<in> Upper L A"
   152 proof (rule Upper_memI[OF _ a'carr])
   153   fix y
   154   assume yA: "y \<in> A"
   155   hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
   156   also note aa'
   157   finally
   158       show "y \<sqsubseteq> a'"
   159       by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
   160 qed
   161 
   162 lemma (in weak_partial_order) Upper_cong:
   163   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   164     and AA': "A {.=} A'"
   165   shows "Upper L A = Upper L A'"
   166 unfolding Upper_def
   167 apply rule
   168  apply (rule, clarsimp) defer 1
   169  apply (rule, clarsimp) defer 1
   170 proof -
   171   fix x a'
   172   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   173     and a'A': "a' \<in> A'"
   174   assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
   175 
   176   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   177   from this obtain a
   178       where aA: "a \<in> A"
   179       and a'a: "a' .= a"
   180       by auto
   181   note [simp] = subsetD[OF Acarr aA] carr
   182 
   183   note a'a
   184   also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
   185   finally show "a' \<sqsubseteq> x" by simp
   186 next
   187   fix x a
   188   assume carr: "x \<in> carrier L" "a \<in> carrier L"
   189     and aA: "a \<in> A"
   190   assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
   191 
   192   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   193   from this obtain a'
   194       where a'A': "a' \<in> A'"
   195       and aa': "a .= a'"
   196       by auto
   197   note [simp] = subsetD[OF A'carr a'A'] carr
   198 
   199   note aa'
   200   also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
   201   finally show "a \<sqsubseteq> x" by simp
   202 qed
   203 
   204 lemma Lower_closed [intro!, simp]:
   205   "Lower L A \<subseteq> carrier L"
   206   by (unfold Lower_def) clarify
   207 
   208 lemma Lower_memD [dest]:
   209   fixes L (structure)
   210   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   211   by (unfold Lower_def) blast
   212 
   213 lemma Lower_memI:
   214   fixes L (structure)
   215   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   216   by (unfold Lower_def) blast
   217 
   218 lemma Lower_antimono:
   219   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   220   by (unfold Lower_def) blast
   221 
   222 lemma (in weak_partial_order) Lower_is_closed [simp]:
   223   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
   224   by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
   225 
   226 lemma (in weak_partial_order) Lower_mem_cong:
   227   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   228     and aa': "a .= a'"
   229     and aelem: "a \<in> Lower L A"
   230   shows "a' \<in> Lower L A"
   231 using assms Lower_closed[of L A]
   232 by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
   233 
   234 lemma (in weak_partial_order) Lower_cong:
   235   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   236     and AA': "A {.=} A'"
   237   shows "Lower L A = Lower L A'"
   238 unfolding Lower_def
   239 apply rule
   240  apply clarsimp defer 1
   241  apply clarsimp defer 1
   242 proof -
   243   fix x a'
   244   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   245     and a'A': "a' \<in> A'"
   246   assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
   247   hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
   248 
   249   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   250   from this obtain a
   251       where aA: "a \<in> A"
   252       and a'a: "a' .= a"
   253       by auto
   254 
   255   from aA and subsetD[OF Acarr aA]
   256       have "x \<sqsubseteq> a" by (rule aLxCond)
   257   also note a'a[symmetric]
   258   finally
   259       show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
   260 next
   261   fix x a
   262   assume carr: "x \<in> carrier L" "a \<in> carrier L"
   263     and aA: "a \<in> A"
   264   assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
   265   hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
   266 
   267   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   268   from this obtain a'
   269       where a'A': "a' \<in> A'"
   270       and aa': "a .= a'"
   271       by auto
   272   from a'A' and subsetD[OF A'carr a'A']
   273       have "x \<sqsubseteq> a'" by (rule a'LxCond)
   274   also note aa'[symmetric]
   275   finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
   276 qed
   277 
   278 
   279 subsubsection {* Least and greatest, as predicate *}
   280 
   281 definition
   282   least :: "[_, 'a, 'a set] => bool"
   283   where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
   284 
   285 definition
   286   greatest :: "[_, 'a, 'a set] => bool"
   287   where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
   288 
   289 text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
   290   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
   291 
   292 lemma least_closed [intro, simp]:
   293   "least L l A ==> l \<in> carrier L"
   294   by (unfold least_def) fast
   295 
   296 lemma least_mem:
   297   "least L l A ==> l \<in> A"
   298   by (unfold least_def) fast
   299 
   300 lemma (in weak_partial_order) weak_least_unique:
   301   "[| least L x A; least L y A |] ==> x .= y"
   302   by (unfold least_def) blast
   303 
   304 lemma least_le:
   305   fixes L (structure)
   306   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   307   by (unfold least_def) fast
   308 
   309 lemma (in weak_partial_order) least_cong:
   310   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   311   by (unfold least_def) (auto dest: sym)
   312 
   313 text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
   314   @{term "A {.=} A'"} *}
   315 
   316 lemma (in weak_partial_order) least_Upper_cong_l:
   317   assumes "x .= x'"
   318     and "x \<in> carrier L" "x' \<in> carrier L"
   319     and "A \<subseteq> carrier L"
   320   shows "least L x (Upper L A) = least L x' (Upper L A)"
   321   apply (rule least_cong) using assms by auto
   322 
   323 lemma (in weak_partial_order) least_Upper_cong_r:
   324   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
   325     and AA': "A {.=} A'"
   326   shows "least L x (Upper L A) = least L x (Upper L A')"
   327 apply (subgoal_tac "Upper L A = Upper L A'", simp)
   328 by (rule Upper_cong) fact+
   329 
   330 lemma least_UpperI:
   331   fixes L (structure)
   332   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   333     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   334     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   335   shows "least L s (Upper L A)"
   336 proof -
   337   have "Upper L A \<subseteq> carrier L" by simp
   338   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   339   moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   340   ultimately show ?thesis by (simp add: least_def)
   341 qed
   342 
   343 lemma least_Upper_above:
   344   fixes L (structure)
   345   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   346   by (unfold least_def) blast
   347 
   348 lemma greatest_closed [intro, simp]:
   349   "greatest L l A ==> l \<in> carrier L"
   350   by (unfold greatest_def) fast
   351 
   352 lemma greatest_mem:
   353   "greatest L l A ==> l \<in> A"
   354   by (unfold greatest_def) fast
   355 
   356 lemma (in weak_partial_order) weak_greatest_unique:
   357   "[| greatest L x A; greatest L y A |] ==> x .= y"
   358   by (unfold greatest_def) blast
   359 
   360 lemma greatest_le:
   361   fixes L (structure)
   362   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   363   by (unfold greatest_def) fast
   364 
   365 lemma (in weak_partial_order) greatest_cong:
   366   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   367   greatest L x A = greatest L x' A"
   368   by (unfold greatest_def) (auto dest: sym)
   369 
   370 text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
   371   @{term "A {.=} A'"} *}
   372 
   373 lemma (in weak_partial_order) greatest_Lower_cong_l:
   374   assumes "x .= x'"
   375     and "x \<in> carrier L" "x' \<in> carrier L"
   376     and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
   377   shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
   378   apply (rule greatest_cong) using assms by auto
   379 
   380 lemma (in weak_partial_order) greatest_Lower_cong_r:
   381   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
   382     and AA': "A {.=} A'"
   383   shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
   384 apply (subgoal_tac "Lower L A = Lower L A'", simp)
   385 by (rule Lower_cong) fact+
   386 
   387 lemma greatest_LowerI:
   388   fixes L (structure)
   389   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   390     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   391     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   392   shows "greatest L i (Lower L A)"
   393 proof -
   394   have "Lower L A \<subseteq> carrier L" by simp
   395   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   396   moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   397   ultimately show ?thesis by (simp add: greatest_def)
   398 qed
   399 
   400 lemma greatest_Lower_below:
   401   fixes L (structure)
   402   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   403   by (unfold greatest_def) blast
   404 
   405 text {* Supremum and infimum *}
   406 
   407 definition
   408   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   409   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
   410 
   411 definition
   412   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   413   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
   414 
   415 definition
   416   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   417   where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
   418 
   419 definition
   420   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   421   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
   422 
   423 
   424 subsection {* Lattices *}
   425 
   426 locale weak_upper_semilattice = weak_partial_order +
   427   assumes sup_of_two_exists:
   428     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   429 
   430 locale weak_lower_semilattice = weak_partial_order +
   431   assumes inf_of_two_exists:
   432     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   433 
   434 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
   435 
   436 
   437 subsubsection {* Supremum *}
   438 
   439 lemma (in weak_upper_semilattice) joinI:
   440   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   441   ==> P (x \<squnion> y)"
   442 proof (unfold join_def sup_def)
   443   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   444     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   445   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   446   with L show "P (SOME l. least L l (Upper L {x, y}))"
   447     by (fast intro: someI2 P)
   448 qed
   449 
   450 lemma (in weak_upper_semilattice) join_closed [simp]:
   451   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   452   by (rule joinI) (rule least_closed)
   453 
   454 lemma (in weak_upper_semilattice) join_cong_l:
   455   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   456     and xx': "x .= x'"
   457   shows "x \<squnion> y .= x' \<squnion> y"
   458 proof (rule joinI, rule joinI)
   459   fix a b
   460   from xx' carr
   461       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   462 
   463   assume leasta: "least L a (Upper L {x, y})"
   464   assume "least L b (Upper L {x', y})"
   465   with carr
   466       have leastb: "least L b (Upper L {x, y})"
   467       by (simp add: least_Upper_cong_r[OF _ _ seq])
   468 
   469   from leasta leastb
   470       show "a .= b" by (rule weak_least_unique)
   471 qed (rule carr)+
   472 
   473 lemma (in weak_upper_semilattice) join_cong_r:
   474   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   475     and yy': "y .= y'"
   476   shows "x \<squnion> y .= x \<squnion> y'"
   477 proof (rule joinI, rule joinI)
   478   fix a b
   479   have "{x, y} = {y, x}" by fast
   480   also from carr yy'
   481       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   482   also have "{y', x} = {x, y'}" by fast
   483   finally
   484       have seq: "{x, y} {.=} {x, y'}" .
   485 
   486   assume leasta: "least L a (Upper L {x, y})"
   487   assume "least L b (Upper L {x, y'})"
   488   with carr
   489       have leastb: "least L b (Upper L {x, y})"
   490       by (simp add: least_Upper_cong_r[OF _ _ seq])
   491 
   492   from leasta leastb
   493       show "a .= b" by (rule weak_least_unique)
   494 qed (rule carr)+
   495 
   496 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   497   "x \<in> carrier L ==> least L x (Upper L {x})"
   498   by (rule least_UpperI) auto
   499 
   500 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
   501   "x \<in> carrier L ==> \<Squnion>{x} .= x"
   502   unfolding sup_def
   503   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
   504 
   505 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
   506   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
   507   unfolding sup_def
   508   by (rule someI2) (auto intro: sup_of_singletonI)
   509 
   510 text {* Condition on @{text A}: supremum exists. *}
   511 
   512 lemma (in weak_upper_semilattice) sup_insertI:
   513   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   514   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   515   ==> P (\<Squnion>(insert x A))"
   516 proof (unfold sup_def)
   517   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   518     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   519     and least_a: "least L a (Upper L A)"
   520   from L least_a have La: "a \<in> carrier L" by simp
   521   from L sup_of_two_exists least_a
   522   obtain s where least_s: "least L s (Upper L {a, x})" by blast
   523   show "P (SOME l. least L l (Upper L (insert x A)))"
   524   proof (rule someI2)
   525     show "least L s (Upper L (insert x A))"
   526     proof (rule least_UpperI)
   527       fix z
   528       assume "z \<in> insert x A"
   529       then show "z \<sqsubseteq> s"
   530       proof
   531         assume "z = x" then show ?thesis
   532           by (simp add: least_Upper_above [OF least_s] L La)
   533       next
   534         assume "z \<in> A"
   535         with L least_s least_a show ?thesis
   536           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
   537       qed
   538     next
   539       fix y
   540       assume y: "y \<in> Upper L (insert x A)"
   541       show "s \<sqsubseteq> y"
   542       proof (rule least_le [OF least_s], rule Upper_memI)
   543         fix z
   544         assume z: "z \<in> {a, x}"
   545         then show "z \<sqsubseteq> y"
   546         proof
   547           have y': "y \<in> Upper L A"
   548             apply (rule subsetD [where A = "Upper L (insert x A)"])
   549              apply (rule Upper_antimono)
   550              apply blast
   551             apply (rule y)
   552             done
   553           assume "z = a"
   554           with y' least_a show ?thesis by (fast dest: least_le)
   555         next
   556           assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
   557           with y L show ?thesis by blast
   558         qed
   559       qed (rule Upper_closed [THEN subsetD, OF y])
   560     next
   561       from L show "insert x A \<subseteq> carrier L" by simp
   562       from least_s show "s \<in> carrier L" by simp
   563     qed
   564   qed (rule P)
   565 qed
   566 
   567 lemma (in weak_upper_semilattice) finite_sup_least:
   568   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   569 proof (induct set: finite)
   570   case empty
   571   then show ?case by simp
   572 next
   573   case (insert x A)
   574   show ?case
   575   proof (cases "A = {}")
   576     case True
   577     with insert show ?thesis
   578       by simp (simp add: least_cong [OF weak_sup_of_singleton] 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 (fastforce 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 (fastforce 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   by default (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   by default (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   by default (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   by default (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   by default (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   by default (rule total)
  1202 
  1203 text {* Total orders are lattices. *}
  1204 
  1205 sublocale total_order < weak: lattice
  1206   by default (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   by default (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   by default (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     by default 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 (fastforce 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 (fastforce 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