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