src/HOL/Algebra/Lattice.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 30363 9b8d9b6ef803 child 32960 69916a850301 permissions -rw-r--r--
simplified method setup;
     1 (*

     2   Title:     HOL/Algebra/Lattice.thy

     3   Author:    Clemens Ballarin, started 7 November 2003

     4   Copyright: Clemens Ballarin

     5

     6 Most congruence rules by Stephan Hohe.

     7 *)

     8

     9 theory Lattice imports Congruence begin

    10

    11 section {* Orders and Lattices *}

    12

    13 subsection {* Partial Orders *}

    14

    15 record 'a gorder = "'a eq_object" +

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

    17

    18 locale weak_partial_order = equivalence L for L (structure) +

    19   assumes le_refl [intro, simp]:

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

    21     and weak_le_anti_sym [intro]:

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

    23     and le_trans [trans]:

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

    25     and le_cong:

    26       "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"

    27

    28 constdefs (structure L)

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

    30   "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"

    31

    32

    33 subsubsection {* The order relation *}

    34

    35 context weak_partial_order begin

    36

    37 lemma le_cong_l [intro, trans]:

    38   "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"

    39   by (auto intro: le_cong [THEN iffD2])

    40

    41 lemma le_cong_r [intro, trans]:

    42   "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"

    43   by (auto intro: le_cong [THEN iffD1])

    44

    45 lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"

    46   by (simp add: le_cong_l)

    47

    48 end

    49

    50 lemma weak_llessI:

    51   fixes R (structure)

    52   assumes "x \<sqsubseteq> y" and "~(x .= y)"

    53   shows "x \<sqsubset> y"

    54   using assms unfolding lless_def by simp

    55

    56 lemma lless_imp_le:

    57   fixes R (structure)

    58   assumes "x \<sqsubset> y"

    59   shows "x \<sqsubseteq> y"

    60   using assms unfolding lless_def by simp

    61

    62 lemma weak_lless_imp_not_eq:

    63   fixes R (structure)

    64   assumes "x \<sqsubset> y"

    65   shows "\<not> (x .= y)"

    66   using assms unfolding lless_def by simp

    67

    68 lemma weak_llessE:

    69   fixes R (structure)

    70   assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"

    71   shows "P"

    72   using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)

    73

    74 lemma (in weak_partial_order) lless_cong_l [trans]:

    75   assumes xx': "x .= x'"

    76     and xy: "x' \<sqsubset> y"

    77     and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"

    78   shows "x \<sqsubset> y"

    79   using assms unfolding lless_def by (auto intro: trans sym)

    80

    81 lemma (in weak_partial_order) lless_cong_r [trans]:

    82   assumes xy: "x \<sqsubset> y"

    83     and  yy': "y .= y'"

    84     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"

    85   shows "x \<sqsubset> y'"

    86   using assms unfolding lless_def by (auto intro: trans sym)

    87

    88

    89 lemma (in weak_partial_order) lless_antisym:

    90   assumes "a \<in> carrier L" "b \<in> carrier L"

    91     and "a \<sqsubset> b" "b \<sqsubset> a"

    92   shows "P"

    93   using assms

    94   by (elim weak_llessE) auto

    95

    96 lemma (in weak_partial_order) lless_trans [trans]:

    97   assumes "a \<sqsubset> b" "b \<sqsubset> c"

    98     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"

    99   shows "a \<sqsubset> c"

   100   using assms unfolding lless_def by (blast dest: le_trans intro: sym)

   101

   102

   103 subsubsection {* Upper and lower bounds of a set *}

   104

   105 constdefs (structure L)

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

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

   108

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

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

   111

   112 lemma Upper_closed [intro!, simp]:

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

   114   by (unfold Upper_def) clarify

   115

   116 lemma Upper_memD [dest]:

   117   fixes L (structure)

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

   119   by (unfold Upper_def) blast

   120

   121 lemma (in weak_partial_order) Upper_elemD [dest]:

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

   123   unfolding Upper_def elem_def

   124   by (blast dest: sym)

   125

   126 lemma Upper_memI:

   127   fixes L (structure)

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

   129   by (unfold Upper_def) blast

   130

   131 lemma (in weak_partial_order) Upper_elemI:

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

   133   unfolding Upper_def by blast

   134

   135 lemma Upper_antimono:

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

   137   by (unfold Upper_def) blast

   138

   139 lemma (in weak_partial_order) Upper_is_closed [simp]:

   140   "A \<subseteq> carrier L ==> is_closed (Upper L A)"

   141   by (rule is_closedI) (blast intro: Upper_memI)+

   142

   143 lemma (in weak_partial_order) Upper_mem_cong:

   144   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"

   145     and aa': "a .= a'"

   146     and aelem: "a \<in> Upper L A"

   147   shows "a' \<in> Upper L A"

   148 proof (rule Upper_memI[OF _ a'carr])

   149   fix y

   150   assume yA: "y \<in> A"

   151   hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)

   152   also note aa'

   153   finally

   154       show "y \<sqsubseteq> a'"

   155       by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])

   156 qed

   157

   158 lemma (in weak_partial_order) Upper_cong:

   159   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"

   160     and AA': "A {.=} A'"

   161   shows "Upper L A = Upper L A'"

   162 unfolding Upper_def

   163 apply rule

   164  apply (rule, clarsimp) defer 1

   165  apply (rule, clarsimp) defer 1

   166 proof -

   167   fix x a'

   168   assume carr: "x \<in> carrier L" "a' \<in> carrier L"

   169     and a'A': "a' \<in> A'"

   170   assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"

   171

   172   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)

   173   from this obtain a

   174       where aA: "a \<in> A"

   175       and a'a: "a' .= a"

   176       by auto

   177   note [simp] = subsetD[OF Acarr aA] carr

   178

   179   note a'a

   180   also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)

   181   finally show "a' \<sqsubseteq> x" by simp

   182 next

   183   fix x a

   184   assume carr: "x \<in> carrier L" "a \<in> carrier L"

   185     and aA: "a \<in> A"

   186   assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"

   187

   188   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)

   189   from this obtain a'

   190       where a'A': "a' \<in> A'"

   191       and aa': "a .= a'"

   192       by auto

   193   note [simp] = subsetD[OF A'carr a'A'] carr

   194

   195   note aa'

   196   also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')

   197   finally show "a \<sqsubseteq> x" by simp

   198 qed

   199

   200 lemma Lower_closed [intro!, simp]:

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

   202   by (unfold Lower_def) clarify

   203

   204 lemma Lower_memD [dest]:

   205   fixes L (structure)

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

   207   by (unfold Lower_def) blast

   208

   209 lemma Lower_memI:

   210   fixes L (structure)

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

   212   by (unfold Lower_def) blast

   213

   214 lemma Lower_antimono:

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

   216   by (unfold Lower_def) blast

   217

   218 lemma (in weak_partial_order) Lower_is_closed [simp]:

   219   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"

   220   by (rule is_closedI) (blast intro: Lower_memI dest: sym)+

   221

   222 lemma (in weak_partial_order) Lower_mem_cong:

   223   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"

   224     and aa': "a .= a'"

   225     and aelem: "a \<in> Lower L A"

   226   shows "a' \<in> Lower L A"

   227 using assms Lower_closed[of L A]

   228 by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])

   229

   230 lemma (in weak_partial_order) Lower_cong:

   231   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"

   232     and AA': "A {.=} A'"

   233   shows "Lower L A = Lower L A'"

   234 using Lower_memD[of y]

   235 unfolding Lower_def

   236 apply safe

   237  apply clarsimp defer 1

   238  apply clarsimp defer 1

   239 proof -

   240   fix x a'

   241   assume carr: "x \<in> carrier L" "a' \<in> carrier L"

   242     and a'A': "a' \<in> A'"

   243   assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"

   244   hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast

   245

   246   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)

   247   from this obtain a

   248       where aA: "a \<in> A"

   249       and a'a: "a' .= a"

   250       by auto

   251

   252   from aA and subsetD[OF Acarr aA]

   253       have "x \<sqsubseteq> a" by (rule aLxCond)

   254   also note a'a[symmetric]

   255   finally

   256       show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])

   257 next

   258   fix x a

   259   assume carr: "x \<in> carrier L" "a \<in> carrier L"

   260     and aA: "a \<in> A"

   261   assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"

   262   hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+

   263

   264   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)

   265   from this obtain a'

   266       where a'A': "a' \<in> A'"

   267       and aa': "a .= a'"

   268       by auto

   269   from a'A' and subsetD[OF A'carr a'A']

   270       have "x \<sqsubseteq> a'" by (rule a'LxCond)

   271   also note aa'[symmetric]

   272   finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])

   273 qed

   274

   275

   276 subsubsection {* Least and greatest, as predicate *}

   277

   278 constdefs (structure L)

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

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

   281

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

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

   284

   285 text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l

   286   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}

   287

   288 lemma least_closed [intro, simp]:

   289   "least L l A ==> l \<in> carrier L"

   290   by (unfold least_def) fast

   291

   292 lemma least_mem:

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

   294   by (unfold least_def) fast

   295

   296 lemma (in weak_partial_order) weak_least_unique:

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

   298   by (unfold least_def) blast

   299

   300 lemma least_le:

   301   fixes L (structure)

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

   303   by (unfold least_def) fast

   304

   305 lemma (in weak_partial_order) least_cong:

   306   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"

   307   by (unfold least_def) (auto dest: sym)

   308

   309 text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for

   310   @{term "A {.=} A'"} *}

   311

   312 lemma (in weak_partial_order) least_Upper_cong_l:

   313   assumes "x .= x'"

   314     and "x \<in> carrier L" "x' \<in> carrier L"

   315     and "A \<subseteq> carrier L"

   316   shows "least L x (Upper L A) = least L x' (Upper L A)"

   317   apply (rule least_cong) using assms by auto

   318

   319 lemma (in weak_partial_order) least_Upper_cong_r:

   320   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)

   321     and AA': "A {.=} A'"

   322   shows "least L x (Upper L A) = least L x (Upper L A')"

   323 apply (subgoal_tac "Upper L A = Upper L A'", simp)

   324 by (rule Upper_cong) fact+

   325

   326 lemma least_UpperI:

   327   fixes L (structure)

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

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

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

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

   332 proof -

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

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

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

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

   337 qed

   338

   339 lemma least_Upper_above:

   340   fixes L (structure)

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

   342   by (unfold least_def) blast

   343

   344 lemma greatest_closed [intro, simp]:

   345   "greatest L l A ==> l \<in> carrier L"

   346   by (unfold greatest_def) fast

   347

   348 lemma greatest_mem:

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

   350   by (unfold greatest_def) fast

   351

   352 lemma (in weak_partial_order) weak_greatest_unique:

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

   354   by (unfold greatest_def) blast

   355

   356 lemma greatest_le:

   357   fixes L (structure)

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

   359   by (unfold greatest_def) fast

   360

   361 lemma (in weak_partial_order) greatest_cong:

   362   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>

   363   greatest L x A = greatest L x' A"

   364   by (unfold greatest_def) (auto dest: sym)

   365

   366 text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for

   367   @{term "A {.=} A'"} *}

   368

   369 lemma (in weak_partial_order) greatest_Lower_cong_l:

   370   assumes "x .= x'"

   371     and "x \<in> carrier L" "x' \<in> carrier L"

   372     and "A \<subseteq> carrier L" (* unneccessary with current Lower *)

   373   shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"

   374   apply (rule greatest_cong) using assms by auto

   375

   376 lemma (in weak_partial_order) greatest_Lower_cong_r:

   377   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"

   378     and AA': "A {.=} A'"

   379   shows "greatest L x (Lower L A) = greatest L x (Lower L A')"

   380 apply (subgoal_tac "Lower L A = Lower L A'", simp)

   381 by (rule Lower_cong) fact+

   382

   383 lemma greatest_LowerI:

   384   fixes L (structure)

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

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

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

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

   389 proof -

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

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

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

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

   394 qed

   395

   396 lemma greatest_Lower_below:

   397   fixes L (structure)

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

   399   by (unfold greatest_def) blast

   400

   401 text {* Supremum and infimum *}

   402

   403 constdefs (structure L)

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

   405   "\<Squnion>A == SOME x. least L x (Upper L A)"

   406

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

   408   "\<Sqinter>A == SOME x. greatest L x (Lower L A)"

   409

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

   411   "x \<squnion> y == \<Squnion> {x, y}"

   412

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

   414   "x \<sqinter> y == \<Sqinter> {x, y}"

   415

   416

   417 subsection {* Lattices *}

   418

   419 locale weak_upper_semilattice = weak_partial_order +

   420   assumes sup_of_two_exists:

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

   422

   423 locale weak_lower_semilattice = weak_partial_order +

   424   assumes inf_of_two_exists:

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

   426

   427 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice

   428

   429

   430 subsubsection {* Supremum *}

   431

   432 lemma (in weak_upper_semilattice) joinI:

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

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

   435 proof (unfold join_def sup_def)

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

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

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

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

   440     by (fast intro: someI2 P)

   441 qed

   442

   443 lemma (in weak_upper_semilattice) join_closed [simp]:

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

   445   by (rule joinI) (rule least_closed)

   446

   447 lemma (in weak_upper_semilattice) join_cong_l:

   448   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"

   449     and xx': "x .= x'"

   450   shows "x \<squnion> y .= x' \<squnion> y"

   451 proof (rule joinI, rule joinI)

   452   fix a b

   453   from xx' carr

   454       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)

   455

   456   assume leasta: "least L a (Upper L {x, y})"

   457   assume "least L b (Upper L {x', y})"

   458   with carr

   459       have leastb: "least L b (Upper L {x, y})"

   460       by (simp add: least_Upper_cong_r[OF _ _ seq])

   461

   462   from leasta leastb

   463       show "a .= b" by (rule weak_least_unique)

   464 qed (rule carr)+

   465

   466 lemma (in weak_upper_semilattice) join_cong_r:

   467   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"

   468     and yy': "y .= y'"

   469   shows "x \<squnion> y .= x \<squnion> y'"

   470 proof (rule joinI, rule joinI)

   471   fix a b

   472   have "{x, y} = {y, x}" by fast

   473   also from carr yy'

   474       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)

   475   also have "{y', x} = {x, y'}" by fast

   476   finally

   477       have seq: "{x, y} {.=} {x, y'}" .

   478

   479   assume leasta: "least L a (Upper L {x, y})"

   480   assume "least L b (Upper L {x, y'})"

   481   with carr

   482       have leastb: "least L b (Upper L {x, y})"

   483       by (simp add: least_Upper_cong_r[OF _ _ seq])

   484

   485   from leasta leastb

   486       show "a .= b" by (rule weak_least_unique)

   487 qed (rule carr)+

   488

   489 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)

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

   491   by (rule least_UpperI) auto

   492

   493 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:

   494   "x \<in> carrier L ==> \<Squnion>{x} .= x"

   495   unfolding sup_def

   496   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)

   497

   498 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:

   499   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"

   500   unfolding sup_def

   501   by (rule someI2) (auto intro: sup_of_singletonI)

   502

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

   504

   505 lemma (in weak_upper_semilattice) sup_insertI:

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

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

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

   509 proof (unfold sup_def)

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

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

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

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

   514   from L sup_of_two_exists least_a

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

   516   show "P (SOME l. least L l (Upper L (insert x A)))"

   517   proof (rule someI2)

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

   519     proof (rule least_UpperI)

   520       fix z

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

   522       then show "z \<sqsubseteq> s"

   523       proof

   524         assume "z = x" then show ?thesis

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

   526       next

   527         assume "z \<in> A"

   528         with L least_s least_a show ?thesis

   529           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)

   530       qed

   531     next

   532       fix y

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

   534       show "s \<sqsubseteq> y"

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

   536 	fix z

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

   538 	then show "z \<sqsubseteq> y"

   539 	proof

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

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

   542              apply (rule Upper_antimono)

   543 	     apply blast

   544 	    apply (rule y)

   545             done

   546           assume "z = a"

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

   548 	next

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

   550           with y L show ?thesis by blast

   551 	qed

   552       qed (rule Upper_closed [THEN subsetD, OF y])

   553     next

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

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

   556     qed

   557   qed (rule P)

   558 qed

   559

   560 lemma (in weak_upper_semilattice) finite_sup_least:

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

   562 proof (induct set: finite)

   563   case empty

   564   then show ?case by simp

   565 next

   566   case (insert x A)

   567   show ?case

   568   proof (cases "A = {}")

   569     case True

   570     with insert show ?thesis

   571       by simp (simp add: least_cong [OF weak_sup_of_singleton]

   572 	sup_of_singleton_closed sup_of_singletonI)

   573 	(* The above step is hairy; least_cong can make simp loop.

   574 	Would want special version of simp to apply least_cong. *)

   575   next

   576     case False

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

   578     with _ show ?thesis

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

   580   qed

   581 qed

   582

   583 lemma (in weak_upper_semilattice) finite_sup_insertI:

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

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

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

   587 proof (cases "A = {}")

   588   case True with P and xA show ?thesis

   589     by (simp add: finite_sup_least)

   590 next

   591   case False with P and xA show ?thesis

   592     by (simp add: sup_insertI finite_sup_least)

   593 qed

   594

   595 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:

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

   597 proof (induct set: finite)

   598   case empty then show ?case by simp

   599 next

   600   case insert then show ?case

   601     by - (rule finite_sup_insertI, simp_all)

   602 qed

   603

   604 lemma (in weak_upper_semilattice) join_left:

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

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

   607

   608 lemma (in weak_upper_semilattice) join_right:

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

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

   611

   612 lemma (in weak_upper_semilattice) sup_of_two_least:

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

   614 proof (unfold sup_def)

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

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

   617   with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"

   618   by (fast intro: someI2 weak_least_unique)  (* blast fails *)

   619 qed

   620

   621 lemma (in weak_upper_semilattice) join_le:

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

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

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

   625 proof (rule joinI [OF _ x y])

   626   fix s

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

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

   629 qed

   630

   631 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:

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

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

   634 proof (rule finite_sup_insertI)

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

   636   fix s

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

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

   639   proof (rule weak_le_anti_sym)

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

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

   642   next

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

   644     by (erule_tac least_le)

   645       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)

   646   qed (simp_all add: L least_closed [OF sup])

   647 qed (simp_all add: L)

   648

   649 text {* Commutativity holds for @{text "="}. *}

   650

   651 lemma join_comm:

   652   fixes L (structure)

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

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

   655

   656 lemma (in weak_upper_semilattice) weak_join_assoc:

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

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

   659 proof -

   660   (* FIXME: could be simplified by improved simp: uniform use of .=,

   661      omit [symmetric] in last step. *)

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

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

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

   665   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])

   666   finally show ?thesis by (simp add: L)

   667 qed

   668

   669

   670 subsubsection {* Infimum *}

   671

   672 lemma (in weak_lower_semilattice) meetI:

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

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

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

   676 proof (unfold meet_def inf_def)

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

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

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

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

   681   by (fast intro: someI2 weak_greatest_unique P)

   682 qed

   683

   684 lemma (in weak_lower_semilattice) meet_closed [simp]:

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

   686   by (rule meetI) (rule greatest_closed)

   687

   688 lemma (in weak_lower_semilattice) meet_cong_l:

   689   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"

   690     and xx': "x .= x'"

   691   shows "x \<sqinter> y .= x' \<sqinter> y"

   692 proof (rule meetI, rule meetI)

   693   fix a b

   694   from xx' carr

   695       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)

   696

   697   assume greatesta: "greatest L a (Lower L {x, y})"

   698   assume "greatest L b (Lower L {x', y})"

   699   with carr

   700       have greatestb: "greatest L b (Lower L {x, y})"

   701       by (simp add: greatest_Lower_cong_r[OF _ _ seq])

   702

   703   from greatesta greatestb

   704       show "a .= b" by (rule weak_greatest_unique)

   705 qed (rule carr)+

   706

   707 lemma (in weak_lower_semilattice) meet_cong_r:

   708   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"

   709     and yy': "y .= y'"

   710   shows "x \<sqinter> y .= x \<sqinter> y'"

   711 proof (rule meetI, rule meetI)

   712   fix a b

   713   have "{x, y} = {y, x}" by fast

   714   also from carr yy'

   715       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)

   716   also have "{y', x} = {x, y'}" by fast

   717   finally

   718       have seq: "{x, y} {.=} {x, y'}" .

   719

   720   assume greatesta: "greatest L a (Lower L {x, y})"

   721   assume "greatest L b (Lower L {x, y'})"

   722   with carr

   723       have greatestb: "greatest L b (Lower L {x, y})"

   724       by (simp add: greatest_Lower_cong_r[OF _ _ seq])

   725

   726   from greatesta greatestb

   727       show "a .= b" by (rule weak_greatest_unique)

   728 qed (rule carr)+

   729

   730 lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)

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

   732   by (rule greatest_LowerI) auto

   733

   734 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:

   735   "x \<in> carrier L ==> \<Sqinter>{x} .= x"

   736   unfolding inf_def

   737   by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)

   738

   739 lemma (in weak_partial_order) inf_of_singleton_closed:

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

   741   unfolding inf_def

   742   by (rule someI2) (auto intro: inf_of_singletonI)

   743

   744 text {* Condition on @{text A}: infimum exists. *}

   745

   746 lemma (in weak_lower_semilattice) inf_insertI:

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

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

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

   750 proof (unfold inf_def)

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

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

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

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

   755   from L inf_of_two_exists greatest_a

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

   757   show "P (SOME g. greatest L g (Lower L (insert x A)))"

   758   proof (rule someI2)

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

   760     proof (rule greatest_LowerI)

   761       fix z

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

   763       then show "i \<sqsubseteq> z"

   764       proof

   765         assume "z = x" then show ?thesis

   766           by (simp add: greatest_Lower_below [OF greatest_i] L La)

   767       next

   768         assume "z \<in> A"

   769         with L greatest_i greatest_a show ?thesis

   770           by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)

   771       qed

   772     next

   773       fix y

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

   775       show "y \<sqsubseteq> i"

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

   777 	fix z

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

   779 	then show "y \<sqsubseteq> z"

   780 	proof

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

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

   783             apply (rule Lower_antimono)

   784 	     apply blast

   785 	    apply (rule y)

   786             done

   787           assume "z = a"

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

   789 	next

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

   791           with y L show ?thesis by blast

   792 	qed

   793       qed (rule Lower_closed [THEN subsetD, OF y])

   794     next

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

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

   797     qed

   798   qed (rule P)

   799 qed

   800

   801 lemma (in weak_lower_semilattice) finite_inf_greatest:

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

   803 proof (induct set: finite)

   804   case empty then show ?case by simp

   805 next

   806   case (insert x A)

   807   show ?case

   808   proof (cases "A = {}")

   809     case True

   810     with insert show ?thesis

   811       by simp (simp add: greatest_cong [OF weak_inf_of_singleton]

   812 	inf_of_singleton_closed inf_of_singletonI)

   813   next

   814     case False

   815     from insert show ?thesis

   816     proof (rule_tac inf_insertI)

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

   818     qed simp_all

   819   qed

   820 qed

   821

   822 lemma (in weak_lower_semilattice) finite_inf_insertI:

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

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

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

   826 proof (cases "A = {}")

   827   case True with P and xA show ?thesis

   828     by (simp add: finite_inf_greatest)

   829 next

   830   case False with P and xA show ?thesis

   831     by (simp add: inf_insertI finite_inf_greatest)

   832 qed

   833

   834 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:

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

   836 proof (induct set: finite)

   837   case empty then show ?case by simp

   838 next

   839   case insert then show ?case

   840     by (rule_tac finite_inf_insertI) (simp_all)

   841 qed

   842

   843 lemma (in weak_lower_semilattice) meet_left:

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

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

   846

   847 lemma (in weak_lower_semilattice) meet_right:

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

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

   850

   851 lemma (in weak_lower_semilattice) inf_of_two_greatest:

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

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

   854 proof (unfold inf_def)

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

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

   857   with L

   858   show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"

   859   by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)

   860 qed

   861

   862 lemma (in weak_lower_semilattice) meet_le:

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

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

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

   866 proof (rule meetI [OF _ x y])

   867   fix i

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

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

   870 qed

   871

   872 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:

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

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

   875 proof (rule finite_inf_insertI)

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

   877   fix i

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

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

   880   proof (rule weak_le_anti_sym)

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

   882       by (fastsimp intro!: meet_le elim: greatest_Lower_below)

   883   next

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

   885     by (erule_tac greatest_le)

   886       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)

   887   qed (simp_all add: L greatest_closed [OF inf])

   888 qed (simp_all add: L)

   889

   890 lemma meet_comm:

   891   fixes L (structure)

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

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

   894

   895 lemma (in weak_lower_semilattice) weak_meet_assoc:

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

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

   898 proof -

   899   (* FIXME: improved simp, see weak_join_assoc above *)

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

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

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

   903   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])

   904   finally show ?thesis by (simp add: L)

   905 qed

   906

   907

   908 subsection {* Total Orders *}

   909

   910 locale weak_total_order = weak_partial_order +

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

   912

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

   914

   915 lemma (in weak_partial_order) weak_total_orderI:

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

   917   shows "weak_total_order L"

   918   proof qed (rule total)

   919

   920 text {* Total orders are lattices. *}

   921

   922 sublocale weak_total_order < weak: weak_lattice

   923 proof

   924   fix x y

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

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

   927   proof -

   928     note total L

   929     moreover

   930     {

   931       assume "x \<sqsubseteq> y"

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

   933         by (rule_tac least_UpperI) auto

   934     }

   935     moreover

   936     {

   937       assume "y \<sqsubseteq> x"

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

   939         by (rule_tac least_UpperI) auto

   940     }

   941     ultimately show ?thesis by blast

   942   qed

   943 next

   944   fix x y

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

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

   947   proof -

   948     note total L

   949     moreover

   950     {

   951       assume "y \<sqsubseteq> x"

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

   953         by (rule_tac greatest_LowerI) auto

   954     }

   955     moreover

   956     {

   957       assume "x \<sqsubseteq> y"

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

   959         by (rule_tac greatest_LowerI) auto

   960     }

   961     ultimately show ?thesis by blast

   962   qed

   963 qed

   964

   965

   966 subsection {* Complete Lattices *}

   967

   968 locale weak_complete_lattice = weak_lattice +

   969   assumes sup_exists:

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

   971     and inf_exists:

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

   973

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

   975

   976 lemma (in weak_partial_order) weak_complete_latticeI:

   977   assumes sup_exists:

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

   979     and inf_exists:

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

   981   shows "weak_complete_lattice L"

   982   proof qed (auto intro: sup_exists inf_exists)

   983

   984 constdefs (structure L)

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

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

   987

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

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

   990

   991

   992 lemma (in weak_complete_lattice) supI:

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

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

   995 proof (unfold sup_def)

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

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

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

   999   with L show "P (SOME l. least L l (Upper L A))"

  1000   by (fast intro: someI2 weak_least_unique P)

  1001 qed

  1002

  1003 lemma (in weak_complete_lattice) sup_closed [simp]:

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

  1005   by (rule supI) simp_all

  1006

  1007 lemma (in weak_complete_lattice) top_closed [simp, intro]:

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

  1009   by (unfold top_def) simp

  1010

  1011 lemma (in weak_complete_lattice) infI:

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

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

  1014 proof (unfold inf_def)

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

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

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

  1018   with L show "P (SOME l. greatest L l (Lower L A))"

  1019   by (fast intro: someI2 weak_greatest_unique P)

  1020 qed

  1021

  1022 lemma (in weak_complete_lattice) inf_closed [simp]:

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

  1024   by (rule infI) simp_all

  1025

  1026 lemma (in weak_complete_lattice) bottom_closed [simp, intro]:

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

  1028   by (unfold bottom_def) simp

  1029

  1030 text {* Jacobson: Theorem 8.1 *}

  1031

  1032 lemma Lower_empty [simp]:

  1033   "Lower L {} = carrier L"

  1034   by (unfold Lower_def) simp

  1035

  1036 lemma Upper_empty [simp]:

  1037   "Upper L {} = carrier L"

  1038   by (unfold Upper_def) simp

  1039

  1040 theorem (in weak_partial_order) weak_complete_lattice_criterion1:

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

  1042     and inf_exists:

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

  1044   shows "weak_complete_lattice L"

  1045 proof (rule weak_complete_latticeI)

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

  1047   fix A

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

  1049   let ?B = "Upper L A"

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

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

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

  1053   from inf_exists [OF B_L B_non_empty]

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

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

  1056 apply (rule least_UpperI)

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

  1058     apply (rule b_inf_B)

  1059    apply (rule Lower_memI)

  1060     apply (erule Upper_memD [THEN conjunct1])

  1061      apply assumption

  1062     apply (rule L)

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

  1064   apply (erule greatest_Lower_below [OF b_inf_B])

  1065   apply simp

  1066  apply (rule L)

  1067 apply (rule greatest_closed [OF b_inf_B])

  1068 done

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

  1070 next

  1071   fix A

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

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

  1074   proof (cases "A = {}")

  1075     case True then show ?thesis

  1076       by (simp add: top_exists)

  1077   next

  1078     case False with L show ?thesis

  1079       by (rule inf_exists)

  1080   qed

  1081 qed

  1082

  1083 (* TODO: prove dual version *)

  1084

  1085

  1086 subsection {* Orders and Lattices where @{text eq} is the Equality *}

  1087

  1088 locale partial_order = weak_partial_order +

  1089   assumes eq_is_equal: "op .= = op ="

  1090 begin

  1091

  1092 declare weak_le_anti_sym [rule del]

  1093

  1094 lemma le_anti_sym [intro]:

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

  1096   using weak_le_anti_sym unfolding eq_is_equal .

  1097

  1098 lemma lless_eq:

  1099   "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"

  1100   unfolding lless_def by (simp add: eq_is_equal)

  1101

  1102 lemma lless_asym:

  1103   assumes "a \<in> carrier L" "b \<in> carrier L"

  1104     and "a \<sqsubset> b" "b \<sqsubset> a"

  1105   shows "P"

  1106   using assms unfolding lless_eq by auto

  1107

  1108 end

  1109

  1110

  1111 text {* Least and greatest, as predicate *}

  1112

  1113 lemma (in partial_order) least_unique:

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

  1115   using weak_least_unique unfolding eq_is_equal .

  1116

  1117 lemma (in partial_order) greatest_unique:

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

  1119   using weak_greatest_unique unfolding eq_is_equal .

  1120

  1121

  1122 text {* Lattices *}

  1123

  1124 locale upper_semilattice = partial_order +

  1125   assumes sup_of_two_exists:

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

  1127

  1128 sublocale upper_semilattice < weak: weak_upper_semilattice

  1129   proof qed (rule sup_of_two_exists)

  1130

  1131 locale lower_semilattice = partial_order +

  1132   assumes inf_of_two_exists:

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

  1134

  1135 sublocale lower_semilattice < weak: weak_lower_semilattice

  1136   proof qed (rule inf_of_two_exists)

  1137

  1138 locale lattice = upper_semilattice + lower_semilattice

  1139

  1140

  1141 text {* Supremum *}

  1142

  1143 declare (in partial_order) weak_sup_of_singleton [simp del]

  1144

  1145 lemma (in partial_order) sup_of_singleton [simp]:

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

  1147   using weak_sup_of_singleton unfolding eq_is_equal .

  1148

  1149 lemma (in upper_semilattice) join_assoc_lemma:

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

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

  1152   using weak_join_assoc_lemma L unfolding eq_is_equal .

  1153

  1154 lemma (in upper_semilattice) join_assoc:

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

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

  1157   using weak_join_assoc L unfolding eq_is_equal .

  1158

  1159

  1160 text {* Infimum *}

  1161

  1162 declare (in partial_order) weak_inf_of_singleton [simp del]

  1163

  1164 lemma (in partial_order) inf_of_singleton [simp]:

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

  1166   using weak_inf_of_singleton unfolding eq_is_equal .

  1167

  1168 text {* Condition on @{text A}: infimum exists. *}

  1169

  1170 lemma (in lower_semilattice) meet_assoc_lemma:

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

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

  1173   using weak_meet_assoc_lemma L unfolding eq_is_equal .

  1174

  1175 lemma (in lower_semilattice) meet_assoc:

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

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

  1178   using weak_meet_assoc L unfolding eq_is_equal .

  1179

  1180

  1181 text {* Total Orders *}

  1182

  1183 locale total_order = partial_order +

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

  1185

  1186 sublocale total_order < weak: weak_total_order

  1187   proof qed (rule total_order_total)

  1188

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

  1190

  1191 lemma (in partial_order) total_orderI:

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

  1193   shows "total_order L"

  1194   proof qed (rule total)

  1195

  1196 text {* Total orders are lattices. *}

  1197

  1198 sublocale total_order < weak: lattice

  1199   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)

  1200

  1201

  1202 text {* Complete lattices *}

  1203

  1204 locale complete_lattice = lattice +

  1205   assumes sup_exists:

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

  1207     and inf_exists:

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

  1209

  1210 sublocale complete_lattice < weak: weak_complete_lattice

  1211   proof qed (auto intro: sup_exists inf_exists)

  1212

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

  1214

  1215 lemma (in partial_order) complete_latticeI:

  1216   assumes sup_exists:

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

  1218     and inf_exists:

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

  1220   shows "complete_lattice L"

  1221   proof qed (auto intro: sup_exists inf_exists)

  1222

  1223 theorem (in partial_order) complete_lattice_criterion1:

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

  1225     and inf_exists:

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

  1227   shows "complete_lattice L"

  1228 proof (rule complete_latticeI)

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

  1230   fix A

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

  1232   let ?B = "Upper L A"

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

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

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

  1236   from inf_exists [OF B_L B_non_empty]

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

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

  1239 apply (rule least_UpperI)

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

  1241     apply (rule b_inf_B)

  1242    apply (rule Lower_memI)

  1243     apply (erule Upper_memD [THEN conjunct1])

  1244      apply assumption

  1245     apply (rule L)

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

  1247   apply (erule greatest_Lower_below [OF b_inf_B])

  1248   apply simp

  1249  apply (rule L)

  1250 apply (rule greatest_closed [OF b_inf_B])

  1251 done

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

  1253 next

  1254   fix A

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

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

  1257   proof (cases "A = {}")

  1258     case True then show ?thesis

  1259       by (simp add: top_exists)

  1260   next

  1261     case False with L show ?thesis

  1262       by (rule inf_exists)

  1263   qed

  1264 qed

  1265

  1266 (* TODO: prove dual version *)

  1267

  1268

  1269 subsection {* Examples *}

  1270

  1271 subsubsection {* The Powerset of a Set is a Complete Lattice *}

  1272

  1273 theorem powerset_is_complete_lattice:

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

  1275   (is "complete_lattice ?L")

  1276 proof (rule partial_order.complete_latticeI)

  1277   show "partial_order ?L"

  1278     proof qed auto

  1279 next

  1280   fix B

  1281   assume B: "B \<subseteq> carrier ?L"

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

  1283   proof

  1284     from B show "least ?L (\<Union> B) (Upper ?L B)"

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

  1286   qed

  1287 next

  1288   fix B

  1289   assume B: "B \<subseteq> carrier ?L"

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

  1291   proof

  1292     from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"

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

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

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

  1296   qed

  1297 qed

  1298

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

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

  1301

  1302 end