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