src/HOL/Lattices.thy
author haftmann
Thu Jul 25 08:57:16 2013 +0200 (2013-07-25)
changeset 52729 412c9e0381a1
parent 52152 b561cdce6c4c
child 54555 e8c5e95d338b
permissions -rw-r--r--
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann@21249
     1
(*  Title:      HOL/Lattices.thy
haftmann@21249
     2
    Author:     Tobias Nipkow
haftmann@21249
     3
*)
haftmann@21249
     4
haftmann@22454
     5
header {* Abstract lattices *}
haftmann@21249
     6
haftmann@21249
     7
theory Lattices
haftmann@35121
     8
imports Orderings Groups
haftmann@21249
     9
begin
haftmann@21249
    10
haftmann@35301
    11
subsection {* Abstract semilattice *}
haftmann@35301
    12
haftmann@35301
    13
text {*
haftmann@51487
    14
  These locales provide a basic structure for interpretation into
haftmann@35301
    15
  bigger structures;  extensions require careful thinking, otherwise
haftmann@35301
    16
  undesired effects may occur due to interpretation.
haftmann@35301
    17
*}
haftmann@35301
    18
haftmann@51487
    19
no_notation times (infixl "*" 70)
haftmann@51487
    20
no_notation Groups.one ("1")
haftmann@51487
    21
haftmann@35301
    22
locale semilattice = abel_semigroup +
haftmann@51487
    23
  assumes idem [simp]: "a * a = a"
haftmann@35301
    24
begin
haftmann@35301
    25
haftmann@51487
    26
lemma left_idem [simp]: "a * (a * b) = a * b"
nipkow@50615
    27
by (simp add: assoc [symmetric])
nipkow@50615
    28
haftmann@51487
    29
lemma right_idem [simp]: "(a * b) * b = a * b"
nipkow@50615
    30
by (simp add: assoc)
haftmann@35301
    31
haftmann@35301
    32
end
haftmann@35301
    33
haftmann@51487
    34
locale semilattice_neutr = semilattice + comm_monoid
haftmann@35301
    35
haftmann@51487
    36
locale semilattice_order = semilattice +
haftmann@51487
    37
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
haftmann@51487
    38
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
haftmann@51487
    39
  assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
haftmann@51487
    40
    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
haftmann@51487
    41
begin
haftmann@51487
    42
haftmann@51487
    43
lemma orderI:
haftmann@51487
    44
  "a = a * b \<Longrightarrow> a \<preceq> b"
haftmann@51487
    45
  by (simp add: order_iff)
haftmann@51487
    46
haftmann@51487
    47
lemma orderE:
haftmann@51487
    48
  assumes "a \<preceq> b"
haftmann@51487
    49
  obtains "a = a * b"
haftmann@51487
    50
  using assms by (unfold order_iff)
haftmann@51487
    51
haftmann@52152
    52
sublocale ordering less_eq less
haftmann@51487
    53
proof
haftmann@51487
    54
  fix a b
haftmann@51487
    55
  show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
haftmann@51487
    56
    by (fact semilattice_strict_iff_order)
haftmann@51487
    57
next
haftmann@51487
    58
  fix a
haftmann@51487
    59
  show "a \<preceq> a"
haftmann@51487
    60
    by (simp add: order_iff)
haftmann@51487
    61
next
haftmann@51487
    62
  fix a b
haftmann@51487
    63
  assume "a \<preceq> b" "b \<preceq> a"
haftmann@51487
    64
  then have "a = a * b" "a * b = b"
haftmann@51487
    65
    by (simp_all add: order_iff commute)
haftmann@51487
    66
  then show "a = b" by simp
haftmann@51487
    67
next
haftmann@51487
    68
  fix a b c
haftmann@51487
    69
  assume "a \<preceq> b" "b \<preceq> c"
haftmann@51487
    70
  then have "a = a * b" "b = b * c"
haftmann@51487
    71
    by (simp_all add: order_iff commute)
haftmann@51487
    72
  then have "a = a * (b * c)"
haftmann@51487
    73
    by simp
haftmann@51487
    74
  then have "a = (a * b) * c"
haftmann@51487
    75
    by (simp add: assoc)
haftmann@51487
    76
  with `a = a * b` [symmetric] have "a = a * c" by simp
haftmann@51487
    77
  then show "a \<preceq> c" by (rule orderI)
haftmann@51487
    78
qed
haftmann@35301
    79
haftmann@51487
    80
lemma cobounded1 [simp]:
haftmann@51487
    81
  "a * b \<preceq> a"
haftmann@51487
    82
  by (simp add: order_iff commute)  
haftmann@51487
    83
haftmann@51487
    84
lemma cobounded2 [simp]:
haftmann@51487
    85
  "a * b \<preceq> b"
haftmann@51487
    86
  by (simp add: order_iff)
haftmann@51487
    87
haftmann@51487
    88
lemma boundedI:
haftmann@51487
    89
  assumes "a \<preceq> b" and "a \<preceq> c"
haftmann@51487
    90
  shows "a \<preceq> b * c"
haftmann@51487
    91
proof (rule orderI)
haftmann@51487
    92
  from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
haftmann@51487
    93
  then show "a = a * (b * c)" by (simp add: assoc [symmetric])
haftmann@51487
    94
qed
haftmann@51487
    95
haftmann@51487
    96
lemma boundedE:
haftmann@51487
    97
  assumes "a \<preceq> b * c"
haftmann@51487
    98
  obtains "a \<preceq> b" and "a \<preceq> c"
haftmann@51487
    99
  using assms by (blast intro: trans cobounded1 cobounded2)
haftmann@51487
   100
haftmann@51487
   101
lemma bounded_iff:
haftmann@51487
   102
  "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
haftmann@51487
   103
  by (blast intro: boundedI elim: boundedE)
haftmann@51487
   104
haftmann@51487
   105
lemma strict_boundedE:
haftmann@51487
   106
  assumes "a \<prec> b * c"
haftmann@51487
   107
  obtains "a \<prec> b" and "a \<prec> c"
haftmann@51487
   108
  using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
haftmann@51487
   109
haftmann@51487
   110
lemma coboundedI1:
haftmann@51487
   111
  "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
haftmann@51487
   112
  by (rule trans) auto
haftmann@51487
   113
haftmann@51487
   114
lemma coboundedI2:
haftmann@51487
   115
  "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
haftmann@51487
   116
  by (rule trans) auto
haftmann@51487
   117
haftmann@51487
   118
lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
haftmann@51487
   119
  by (blast intro: boundedI coboundedI1 coboundedI2)
haftmann@51487
   120
haftmann@51487
   121
lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
haftmann@51487
   122
  by (rule antisym) (auto simp add: refl bounded_iff)
haftmann@51487
   123
haftmann@51487
   124
lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
haftmann@51487
   125
  by (rule antisym) (auto simp add: refl bounded_iff)
haftmann@35301
   126
haftmann@35301
   127
end
haftmann@35301
   128
haftmann@51487
   129
locale semilattice_neutr_order = semilattice_neutr + semilattice_order
haftmann@52152
   130
begin
haftmann@51487
   131
haftmann@52152
   132
sublocale ordering_top less_eq less 1
haftmann@51487
   133
  by default (simp add: order_iff)
haftmann@51487
   134
haftmann@52152
   135
end
haftmann@52152
   136
haftmann@51487
   137
notation times (infixl "*" 70)
haftmann@51487
   138
notation Groups.one ("1")
haftmann@51487
   139
haftmann@35301
   140
haftmann@46691
   141
subsection {* Syntactic infimum and supremum operations *}
haftmann@41082
   142
krauss@44845
   143
class inf =
krauss@44845
   144
  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
haftmann@25206
   145
krauss@44845
   146
class sup = 
krauss@44845
   147
  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
krauss@44845
   148
haftmann@46691
   149
haftmann@46691
   150
subsection {* Concrete lattices *}
haftmann@46691
   151
haftmann@46691
   152
notation
haftmann@46691
   153
  less_eq  (infix "\<sqsubseteq>" 50) and
haftmann@46691
   154
  less  (infix "\<sqsubset>" 50)
haftmann@46691
   155
krauss@44845
   156
class semilattice_inf =  order + inf +
haftmann@22737
   157
  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
haftmann@22737
   158
  and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
nipkow@21733
   159
  and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
haftmann@21249
   160
krauss@44845
   161
class semilattice_sup = order + sup +
haftmann@22737
   162
  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
haftmann@22737
   163
  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
nipkow@21733
   164
  and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
haftmann@26014
   165
begin
haftmann@26014
   166
haftmann@26014
   167
text {* Dual lattice *}
haftmann@26014
   168
haftmann@31991
   169
lemma dual_semilattice:
krauss@44845
   170
  "class.semilattice_inf sup greater_eq greater"
haftmann@36635
   171
by (rule class.semilattice_inf.intro, rule dual_order)
haftmann@27682
   172
  (unfold_locales, simp_all add: sup_least)
haftmann@26014
   173
haftmann@26014
   174
end
haftmann@21249
   175
haftmann@35028
   176
class lattice = semilattice_inf + semilattice_sup
haftmann@21249
   177
wenzelm@25382
   178
haftmann@28562
   179
subsubsection {* Intro and elim rules*}
nipkow@21733
   180
haftmann@35028
   181
context semilattice_inf
nipkow@21733
   182
begin
haftmann@21249
   183
haftmann@32064
   184
lemma le_infI1:
haftmann@32064
   185
  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
haftmann@32064
   186
  by (rule order_trans) auto
haftmann@21249
   187
haftmann@32064
   188
lemma le_infI2:
haftmann@32064
   189
  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
haftmann@32064
   190
  by (rule order_trans) auto
nipkow@21733
   191
haftmann@32064
   192
lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
huffman@36008
   193
  by (rule inf_greatest) (* FIXME: duplicate lemma *)
haftmann@21249
   194
haftmann@32064
   195
lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
huffman@36008
   196
  by (blast intro: order_trans inf_le1 inf_le2)
haftmann@21249
   197
nipkow@21734
   198
lemma le_inf_iff [simp]:
haftmann@32064
   199
  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
haftmann@32064
   200
  by (blast intro: le_infI elim: le_infE)
nipkow@21733
   201
haftmann@32064
   202
lemma le_iff_inf:
haftmann@32064
   203
  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
haftmann@32064
   204
  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
haftmann@21249
   205
haftmann@43753
   206
lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
huffman@36008
   207
  by (fast intro: inf_greatest le_infI1 le_infI2)
huffman@36008
   208
haftmann@25206
   209
lemma mono_inf:
haftmann@35028
   210
  fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
haftmann@34007
   211
  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
haftmann@25206
   212
  by (auto simp add: mono_def intro: Lattices.inf_greatest)
nipkow@21733
   213
haftmann@25206
   214
end
nipkow@21733
   215
haftmann@35028
   216
context semilattice_sup
nipkow@21733
   217
begin
haftmann@21249
   218
haftmann@32064
   219
lemma le_supI1:
haftmann@32064
   220
  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
haftmann@25062
   221
  by (rule order_trans) auto
haftmann@21249
   222
haftmann@32064
   223
lemma le_supI2:
haftmann@32064
   224
  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
haftmann@25062
   225
  by (rule order_trans) auto 
nipkow@21733
   226
haftmann@32064
   227
lemma le_supI:
haftmann@32064
   228
  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
huffman@36008
   229
  by (rule sup_least) (* FIXME: duplicate lemma *)
haftmann@21249
   230
haftmann@32064
   231
lemma le_supE:
haftmann@32064
   232
  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
huffman@36008
   233
  by (blast intro: order_trans sup_ge1 sup_ge2)
haftmann@22422
   234
haftmann@32064
   235
lemma le_sup_iff [simp]:
haftmann@32064
   236
  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
haftmann@32064
   237
  by (blast intro: le_supI elim: le_supE)
nipkow@21733
   238
haftmann@32064
   239
lemma le_iff_sup:
haftmann@32064
   240
  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
haftmann@32064
   241
  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
nipkow@21734
   242
haftmann@43753
   243
lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
huffman@36008
   244
  by (fast intro: sup_least le_supI1 le_supI2)
huffman@36008
   245
haftmann@25206
   246
lemma mono_sup:
haftmann@35028
   247
  fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
haftmann@34007
   248
  shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
haftmann@25206
   249
  by (auto simp add: mono_def intro: Lattices.sup_least)
nipkow@21733
   250
haftmann@25206
   251
end
haftmann@23878
   252
nipkow@21733
   253
haftmann@32064
   254
subsubsection {* Equational laws *}
haftmann@21249
   255
haftmann@52152
   256
context semilattice_inf
haftmann@52152
   257
begin
haftmann@52152
   258
haftmann@52152
   259
sublocale inf!: semilattice inf
haftmann@34973
   260
proof
haftmann@34973
   261
  fix a b c
haftmann@34973
   262
  show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
haftmann@34973
   263
    by (rule antisym) (auto intro: le_infI1 le_infI2)
haftmann@34973
   264
  show "a \<sqinter> b = b \<sqinter> a"
haftmann@34973
   265
    by (rule antisym) auto
haftmann@34973
   266
  show "a \<sqinter> a = a"
haftmann@34973
   267
    by (rule antisym) auto
haftmann@34973
   268
qed
haftmann@34973
   269
haftmann@52152
   270
sublocale inf!: semilattice_order inf less_eq less
haftmann@51487
   271
  by default (auto simp add: le_iff_inf less_le)
haftmann@51487
   272
haftmann@34973
   273
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
haftmann@34973
   274
  by (fact inf.assoc)
nipkow@21733
   275
haftmann@34973
   276
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
haftmann@34973
   277
  by (fact inf.commute)
nipkow@21733
   278
haftmann@34973
   279
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
haftmann@34973
   280
  by (fact inf.left_commute)
nipkow@21733
   281
huffman@44921
   282
lemma inf_idem: "x \<sqinter> x = x"
huffman@44921
   283
  by (fact inf.idem) (* already simp *)
haftmann@34973
   284
nipkow@50615
   285
lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
nipkow@50615
   286
  by (fact inf.left_idem) (* already simp *)
nipkow@50615
   287
nipkow@50615
   288
lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
nipkow@50615
   289
  by (fact inf.right_idem) (* already simp *)
nipkow@21733
   290
haftmann@32642
   291
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
haftmann@32064
   292
  by (rule antisym) auto
nipkow@21733
   293
haftmann@32642
   294
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
haftmann@32064
   295
  by (rule antisym) auto
haftmann@34973
   296
 
haftmann@32064
   297
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
nipkow@21733
   298
nipkow@21733
   299
end
nipkow@21733
   300
haftmann@35028
   301
context semilattice_sup
nipkow@21733
   302
begin
haftmann@21249
   303
haftmann@52152
   304
sublocale sup!: semilattice sup
haftmann@52152
   305
proof
haftmann@52152
   306
  fix a b c
haftmann@52152
   307
  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
haftmann@52152
   308
    by (rule antisym) (auto intro: le_supI1 le_supI2)
haftmann@52152
   309
  show "a \<squnion> b = b \<squnion> a"
haftmann@52152
   310
    by (rule antisym) auto
haftmann@52152
   311
  show "a \<squnion> a = a"
haftmann@52152
   312
    by (rule antisym) auto
haftmann@52152
   313
qed
haftmann@52152
   314
haftmann@52152
   315
sublocale sup!: semilattice_order sup greater_eq greater
haftmann@52152
   316
  by default (auto simp add: le_iff_sup sup.commute less_le)
haftmann@52152
   317
haftmann@34973
   318
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
haftmann@34973
   319
  by (fact sup.assoc)
nipkow@21733
   320
haftmann@34973
   321
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
haftmann@34973
   322
  by (fact sup.commute)
nipkow@21733
   323
haftmann@34973
   324
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
haftmann@34973
   325
  by (fact sup.left_commute)
nipkow@21733
   326
huffman@44921
   327
lemma sup_idem: "x \<squnion> x = x"
huffman@44921
   328
  by (fact sup.idem) (* already simp *)
haftmann@34973
   329
noschinl@44918
   330
lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
haftmann@34973
   331
  by (fact sup.left_idem)
nipkow@21733
   332
haftmann@32642
   333
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
haftmann@32064
   334
  by (rule antisym) auto
nipkow@21733
   335
haftmann@32642
   336
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
haftmann@32064
   337
  by (rule antisym) auto
haftmann@21249
   338
haftmann@32064
   339
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
nipkow@21733
   340
nipkow@21733
   341
end
haftmann@21249
   342
nipkow@21733
   343
context lattice
nipkow@21733
   344
begin
nipkow@21733
   345
haftmann@31991
   346
lemma dual_lattice:
krauss@44845
   347
  "class.lattice sup (op \<ge>) (op >) inf"
haftmann@36635
   348
  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
haftmann@31991
   349
    (unfold_locales, auto)
haftmann@31991
   350
noschinl@44918
   351
lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
haftmann@25102
   352
  by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
nipkow@21733
   353
noschinl@44918
   354
lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"
haftmann@25102
   355
  by (blast intro: antisym sup_ge1 sup_least inf_le1)
nipkow@21733
   356
haftmann@32064
   357
lemmas inf_sup_aci = inf_aci sup_aci
nipkow@21734
   358
haftmann@22454
   359
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
haftmann@22454
   360
nipkow@21734
   361
text{* Towards distributivity *}
haftmann@21249
   362
nipkow@21734
   363
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@32064
   364
  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
nipkow@21734
   365
nipkow@21734
   366
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
haftmann@32064
   367
  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
nipkow@21734
   368
nipkow@21734
   369
text{* If you have one of them, you have them all. *}
haftmann@21249
   370
nipkow@21733
   371
lemma distrib_imp1:
haftmann@21249
   372
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
haftmann@21249
   373
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@21249
   374
proof-
noschinl@44918
   375
  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp
noschinl@44918
   376
  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
noschinl@44918
   377
    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
haftmann@21249
   378
  also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
noschinl@44919
   379
    by(simp add: inf_commute)
haftmann@21249
   380
  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
haftmann@21249
   381
  finally show ?thesis .
haftmann@21249
   382
qed
haftmann@21249
   383
nipkow@21733
   384
lemma distrib_imp2:
haftmann@21249
   385
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@21249
   386
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
haftmann@21249
   387
proof-
noschinl@44918
   388
  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp
noschinl@44918
   389
  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
noschinl@44918
   390
    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
haftmann@21249
   391
  also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
noschinl@44919
   392
    by(simp add: sup_commute)
haftmann@21249
   393
  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
haftmann@21249
   394
  finally show ?thesis .
haftmann@21249
   395
qed
haftmann@21249
   396
nipkow@21733
   397
end
haftmann@21249
   398
haftmann@32568
   399
subsubsection {* Strict order *}
haftmann@32568
   400
haftmann@35028
   401
context semilattice_inf
haftmann@32568
   402
begin
haftmann@32568
   403
haftmann@32568
   404
lemma less_infI1:
haftmann@32568
   405
  "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
haftmann@32642
   406
  by (auto simp add: less_le inf_absorb1 intro: le_infI1)
haftmann@32568
   407
haftmann@32568
   408
lemma less_infI2:
haftmann@32568
   409
  "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
haftmann@32642
   410
  by (auto simp add: less_le inf_absorb2 intro: le_infI2)
haftmann@32568
   411
haftmann@32568
   412
end
haftmann@32568
   413
haftmann@35028
   414
context semilattice_sup
haftmann@32568
   415
begin
haftmann@32568
   416
haftmann@32568
   417
lemma less_supI1:
haftmann@34007
   418
  "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
huffman@44921
   419
  using dual_semilattice
huffman@44921
   420
  by (rule semilattice_inf.less_infI1)
haftmann@32568
   421
haftmann@32568
   422
lemma less_supI2:
haftmann@34007
   423
  "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
huffman@44921
   424
  using dual_semilattice
huffman@44921
   425
  by (rule semilattice_inf.less_infI2)
haftmann@32568
   426
haftmann@32568
   427
end
haftmann@32568
   428
haftmann@21249
   429
haftmann@24164
   430
subsection {* Distributive lattices *}
haftmann@21249
   431
haftmann@22454
   432
class distrib_lattice = lattice +
haftmann@21249
   433
  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@21249
   434
nipkow@21733
   435
context distrib_lattice
nipkow@21733
   436
begin
nipkow@21733
   437
nipkow@21733
   438
lemma sup_inf_distrib2:
huffman@44921
   439
  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
huffman@44921
   440
  by (simp add: sup_commute sup_inf_distrib1)
haftmann@21249
   441
nipkow@21733
   442
lemma inf_sup_distrib1:
huffman@44921
   443
  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
huffman@44921
   444
  by (rule distrib_imp2 [OF sup_inf_distrib1])
haftmann@21249
   445
nipkow@21733
   446
lemma inf_sup_distrib2:
huffman@44921
   447
  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
huffman@44921
   448
  by (simp add: inf_commute inf_sup_distrib1)
haftmann@21249
   449
haftmann@31991
   450
lemma dual_distrib_lattice:
krauss@44845
   451
  "class.distrib_lattice sup (op \<ge>) (op >) inf"
haftmann@36635
   452
  by (rule class.distrib_lattice.intro, rule dual_lattice)
haftmann@31991
   453
    (unfold_locales, fact inf_sup_distrib1)
haftmann@31991
   454
huffman@36008
   455
lemmas sup_inf_distrib =
huffman@36008
   456
  sup_inf_distrib1 sup_inf_distrib2
huffman@36008
   457
huffman@36008
   458
lemmas inf_sup_distrib =
huffman@36008
   459
  inf_sup_distrib1 inf_sup_distrib2
huffman@36008
   460
nipkow@21733
   461
lemmas distrib =
haftmann@21249
   462
  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
haftmann@21249
   463
nipkow@21733
   464
end
nipkow@21733
   465
haftmann@21249
   466
haftmann@34007
   467
subsection {* Bounded lattices and boolean algebras *}
haftmann@31991
   468
haftmann@52729
   469
class bounded_semilattice_inf_top = semilattice_inf + order_top
haftmann@52152
   470
begin
haftmann@51487
   471
haftmann@52152
   472
sublocale inf_top!: semilattice_neutr inf top
haftmann@51546
   473
  + inf_top!: semilattice_neutr_order inf top less_eq less
haftmann@51487
   474
proof
haftmann@51487
   475
  fix x
haftmann@51487
   476
  show "x \<sqinter> \<top> = x"
haftmann@51487
   477
    by (rule inf_absorb1) simp
haftmann@51487
   478
qed
haftmann@51487
   479
haftmann@52152
   480
end
haftmann@51487
   481
haftmann@52729
   482
class bounded_semilattice_sup_bot = semilattice_sup + order_bot
haftmann@52152
   483
begin
haftmann@52152
   484
haftmann@52152
   485
sublocale sup_bot!: semilattice_neutr sup bot
haftmann@51546
   486
  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
haftmann@51487
   487
proof
haftmann@51487
   488
  fix x
haftmann@51487
   489
  show "x \<squnion> \<bottom> = x"
haftmann@51487
   490
    by (rule sup_absorb1) simp
haftmann@51487
   491
qed
haftmann@51487
   492
haftmann@52152
   493
end
haftmann@52152
   494
haftmann@52729
   495
class bounded_lattice_bot = lattice + order_bot
haftmann@31991
   496
begin
haftmann@31991
   497
haftmann@51487
   498
subclass bounded_semilattice_sup_bot ..
haftmann@51487
   499
haftmann@31991
   500
lemma inf_bot_left [simp]:
haftmann@34007
   501
  "\<bottom> \<sqinter> x = \<bottom>"
haftmann@31991
   502
  by (rule inf_absorb1) simp
haftmann@31991
   503
haftmann@31991
   504
lemma inf_bot_right [simp]:
haftmann@34007
   505
  "x \<sqinter> \<bottom> = \<bottom>"
haftmann@31991
   506
  by (rule inf_absorb2) simp
haftmann@31991
   507
haftmann@51487
   508
lemma sup_bot_left:
kaliszyk@36352
   509
  "\<bottom> \<squnion> x = x"
haftmann@51487
   510
  by (fact sup_bot.left_neutral)
kaliszyk@36352
   511
haftmann@51487
   512
lemma sup_bot_right:
kaliszyk@36352
   513
  "x \<squnion> \<bottom> = x"
haftmann@51487
   514
  by (fact sup_bot.right_neutral)
kaliszyk@36352
   515
kaliszyk@36352
   516
lemma sup_eq_bot_iff [simp]:
kaliszyk@36352
   517
  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
kaliszyk@36352
   518
  by (simp add: eq_iff)
kaliszyk@36352
   519
nipkow@51593
   520
lemma bot_eq_sup_iff [simp]:
nipkow@51593
   521
  "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
nipkow@51593
   522
  by (simp add: eq_iff)
nipkow@51593
   523
kaliszyk@36352
   524
end
kaliszyk@36352
   525
haftmann@52729
   526
class bounded_lattice_top = lattice + order_top
kaliszyk@36352
   527
begin
kaliszyk@36352
   528
haftmann@51487
   529
subclass bounded_semilattice_inf_top ..
haftmann@51487
   530
haftmann@31991
   531
lemma sup_top_left [simp]:
haftmann@34007
   532
  "\<top> \<squnion> x = \<top>"
haftmann@31991
   533
  by (rule sup_absorb1) simp
haftmann@31991
   534
haftmann@31991
   535
lemma sup_top_right [simp]:
haftmann@34007
   536
  "x \<squnion> \<top> = \<top>"
haftmann@31991
   537
  by (rule sup_absorb2) simp
haftmann@31991
   538
haftmann@51487
   539
lemma inf_top_left:
haftmann@34007
   540
  "\<top> \<sqinter> x = x"
haftmann@51487
   541
  by (fact inf_top.left_neutral)
haftmann@31991
   542
haftmann@51487
   543
lemma inf_top_right:
haftmann@34007
   544
  "x \<sqinter> \<top> = x"
haftmann@51487
   545
  by (fact inf_top.right_neutral)
haftmann@31991
   546
huffman@36008
   547
lemma inf_eq_top_iff [simp]:
huffman@36008
   548
  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
huffman@36008
   549
  by (simp add: eq_iff)
haftmann@32568
   550
kaliszyk@36352
   551
end
kaliszyk@36352
   552
haftmann@52729
   553
class bounded_lattice = lattice + order_bot + order_top
kaliszyk@36352
   554
begin
kaliszyk@36352
   555
haftmann@51487
   556
subclass bounded_lattice_bot ..
haftmann@51487
   557
subclass bounded_lattice_top ..
haftmann@51487
   558
kaliszyk@36352
   559
lemma dual_bounded_lattice:
krauss@44845
   560
  "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
kaliszyk@36352
   561
  by unfold_locales (auto simp add: less_le_not_le)
haftmann@32568
   562
haftmann@34007
   563
end
haftmann@34007
   564
haftmann@34007
   565
class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
haftmann@34007
   566
  assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
haftmann@34007
   567
    and sup_compl_top: "x \<squnion> - x = \<top>"
haftmann@34007
   568
  assumes diff_eq: "x - y = x \<sqinter> - y"
haftmann@34007
   569
begin
haftmann@34007
   570
haftmann@34007
   571
lemma dual_boolean_algebra:
krauss@44845
   572
  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
haftmann@36635
   573
  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
haftmann@34007
   574
    (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
haftmann@34007
   575
noschinl@44918
   576
lemma compl_inf_bot [simp]:
haftmann@34007
   577
  "- x \<sqinter> x = \<bottom>"
haftmann@34007
   578
  by (simp add: inf_commute inf_compl_bot)
haftmann@34007
   579
noschinl@44918
   580
lemma compl_sup_top [simp]:
haftmann@34007
   581
  "- x \<squnion> x = \<top>"
haftmann@34007
   582
  by (simp add: sup_commute sup_compl_top)
haftmann@34007
   583
haftmann@31991
   584
lemma compl_unique:
haftmann@34007
   585
  assumes "x \<sqinter> y = \<bottom>"
haftmann@34007
   586
    and "x \<squnion> y = \<top>"
haftmann@31991
   587
  shows "- x = y"
haftmann@31991
   588
proof -
haftmann@31991
   589
  have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
haftmann@31991
   590
    using inf_compl_bot assms(1) by simp
haftmann@31991
   591
  then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
haftmann@31991
   592
    by (simp add: inf_commute)
haftmann@31991
   593
  then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
haftmann@31991
   594
    by (simp add: inf_sup_distrib1)
haftmann@34007
   595
  then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
haftmann@31991
   596
    using sup_compl_top assms(2) by simp
krauss@34209
   597
  then show "- x = y" by simp
haftmann@31991
   598
qed
haftmann@31991
   599
haftmann@31991
   600
lemma double_compl [simp]:
haftmann@31991
   601
  "- (- x) = x"
haftmann@31991
   602
  using compl_inf_bot compl_sup_top by (rule compl_unique)
haftmann@31991
   603
haftmann@31991
   604
lemma compl_eq_compl_iff [simp]:
haftmann@31991
   605
  "- x = - y \<longleftrightarrow> x = y"
haftmann@31991
   606
proof
haftmann@31991
   607
  assume "- x = - y"
huffman@36008
   608
  then have "- (- x) = - (- y)" by (rule arg_cong)
haftmann@31991
   609
  then show "x = y" by simp
haftmann@31991
   610
next
haftmann@31991
   611
  assume "x = y"
haftmann@31991
   612
  then show "- x = - y" by simp
haftmann@31991
   613
qed
haftmann@31991
   614
haftmann@31991
   615
lemma compl_bot_eq [simp]:
haftmann@34007
   616
  "- \<bottom> = \<top>"
haftmann@31991
   617
proof -
haftmann@34007
   618
  from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
haftmann@31991
   619
  then show ?thesis by simp
haftmann@31991
   620
qed
haftmann@31991
   621
haftmann@31991
   622
lemma compl_top_eq [simp]:
haftmann@34007
   623
  "- \<top> = \<bottom>"
haftmann@31991
   624
proof -
haftmann@34007
   625
  from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
haftmann@31991
   626
  then show ?thesis by simp
haftmann@31991
   627
qed
haftmann@31991
   628
haftmann@31991
   629
lemma compl_inf [simp]:
haftmann@31991
   630
  "- (x \<sqinter> y) = - x \<squnion> - y"
haftmann@31991
   631
proof (rule compl_unique)
huffman@36008
   632
  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
huffman@36008
   633
    by (simp only: inf_sup_distrib inf_aci)
huffman@36008
   634
  then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
haftmann@31991
   635
    by (simp add: inf_compl_bot)
haftmann@31991
   636
next
huffman@36008
   637
  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
huffman@36008
   638
    by (simp only: sup_inf_distrib sup_aci)
huffman@36008
   639
  then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
haftmann@31991
   640
    by (simp add: sup_compl_top)
haftmann@31991
   641
qed
haftmann@31991
   642
haftmann@31991
   643
lemma compl_sup [simp]:
haftmann@31991
   644
  "- (x \<squnion> y) = - x \<sqinter> - y"
huffman@44921
   645
  using dual_boolean_algebra
huffman@44921
   646
  by (rule boolean_algebra.compl_inf)
haftmann@31991
   647
huffman@36008
   648
lemma compl_mono:
huffman@36008
   649
  "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
huffman@36008
   650
proof -
huffman@36008
   651
  assume "x \<sqsubseteq> y"
huffman@36008
   652
  then have "x \<squnion> y = y" by (simp only: le_iff_sup)
huffman@36008
   653
  then have "- (x \<squnion> y) = - y" by simp
huffman@36008
   654
  then have "- x \<sqinter> - y = - y" by simp
huffman@36008
   655
  then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
huffman@36008
   656
  then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
huffman@36008
   657
qed
huffman@36008
   658
noschinl@44918
   659
lemma compl_le_compl_iff [simp]:
haftmann@43753
   660
  "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
haftmann@43873
   661
  by (auto dest: compl_mono)
haftmann@43873
   662
haftmann@43873
   663
lemma compl_le_swap1:
haftmann@43873
   664
  assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
haftmann@43873
   665
proof -
haftmann@43873
   666
  from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
haftmann@43873
   667
  then show ?thesis by simp
haftmann@43873
   668
qed
haftmann@43873
   669
haftmann@43873
   670
lemma compl_le_swap2:
haftmann@43873
   671
  assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
haftmann@43873
   672
proof -
haftmann@43873
   673
  from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
haftmann@43873
   674
  then show ?thesis by simp
haftmann@43873
   675
qed
haftmann@43873
   676
haftmann@43873
   677
lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
haftmann@43873
   678
  "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
noschinl@44919
   679
  by (auto simp add: less_le)
haftmann@43873
   680
haftmann@43873
   681
lemma compl_less_swap1:
haftmann@43873
   682
  assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
haftmann@43873
   683
proof -
haftmann@43873
   684
  from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
haftmann@43873
   685
  then show ?thesis by simp
haftmann@43873
   686
qed
haftmann@43873
   687
haftmann@43873
   688
lemma compl_less_swap2:
haftmann@43873
   689
  assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
haftmann@43873
   690
proof -
haftmann@43873
   691
  from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
haftmann@43873
   692
  then show ?thesis by simp
haftmann@43873
   693
qed
huffman@36008
   694
haftmann@31991
   695
end
haftmann@31991
   696
haftmann@31991
   697
haftmann@51540
   698
subsection {* @{text "min/max"} as special case of lattice *}
haftmann@51540
   699
haftmann@51540
   700
sublocale linorder < min!: semilattice_order min less_eq less
haftmann@51540
   701
  + max!: semilattice_order max greater_eq greater
haftmann@51540
   702
  by default (auto simp add: min_def max_def)
haftmann@51540
   703
haftmann@51540
   704
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
haftmann@51540
   705
  by (auto intro: antisym simp add: min_def fun_eq_iff)
haftmann@51540
   706
haftmann@51540
   707
lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
haftmann@51540
   708
  by (auto intro: antisym simp add: max_def fun_eq_iff)
haftmann@51540
   709
haftmann@51540
   710
haftmann@22454
   711
subsection {* Uniqueness of inf and sup *}
haftmann@22454
   712
haftmann@35028
   713
lemma (in semilattice_inf) inf_unique:
haftmann@22454
   714
  fixes f (infixl "\<triangle>" 70)
haftmann@34007
   715
  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
haftmann@34007
   716
  and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
haftmann@22737
   717
  shows "x \<sqinter> y = x \<triangle> y"
haftmann@22454
   718
proof (rule antisym)
haftmann@34007
   719
  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
haftmann@22454
   720
next
haftmann@34007
   721
  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
haftmann@34007
   722
  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
haftmann@22454
   723
qed
haftmann@22454
   724
haftmann@35028
   725
lemma (in semilattice_sup) sup_unique:
haftmann@22454
   726
  fixes f (infixl "\<nabla>" 70)
haftmann@34007
   727
  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
haftmann@34007
   728
  and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
haftmann@22737
   729
  shows "x \<squnion> y = x \<nabla> y"
haftmann@22454
   730
proof (rule antisym)
haftmann@34007
   731
  show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
haftmann@22454
   732
next
haftmann@34007
   733
  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
haftmann@34007
   734
  show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
haftmann@22454
   735
qed
huffman@36008
   736
haftmann@22454
   737
haftmann@46631
   738
subsection {* Lattice on @{typ bool} *}
haftmann@22454
   739
haftmann@31991
   740
instantiation bool :: boolean_algebra
haftmann@25510
   741
begin
haftmann@25510
   742
haftmann@25510
   743
definition
haftmann@41080
   744
  bool_Compl_def [simp]: "uminus = Not"
haftmann@31991
   745
haftmann@31991
   746
definition
haftmann@41080
   747
  bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
haftmann@31991
   748
haftmann@31991
   749
definition
haftmann@41080
   750
  [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
haftmann@25510
   751
haftmann@25510
   752
definition
haftmann@41080
   753
  [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
haftmann@25510
   754
haftmann@31991
   755
instance proof
haftmann@41080
   756
qed auto
haftmann@22454
   757
haftmann@25510
   758
end
haftmann@25510
   759
haftmann@32781
   760
lemma sup_boolI1:
haftmann@32781
   761
  "P \<Longrightarrow> P \<squnion> Q"
haftmann@41080
   762
  by simp
haftmann@32781
   763
haftmann@32781
   764
lemma sup_boolI2:
haftmann@32781
   765
  "Q \<Longrightarrow> P \<squnion> Q"
haftmann@41080
   766
  by simp
haftmann@32781
   767
haftmann@32781
   768
lemma sup_boolE:
haftmann@32781
   769
  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
haftmann@41080
   770
  by auto
haftmann@32781
   771
haftmann@23878
   772
haftmann@46631
   773
subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
haftmann@23878
   774
nipkow@51387
   775
instantiation "fun" :: (type, semilattice_sup) semilattice_sup
haftmann@25510
   776
begin
haftmann@25510
   777
haftmann@25510
   778
definition
haftmann@41080
   779
  "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
haftmann@41080
   780
haftmann@49769
   781
lemma sup_apply [simp, code]:
haftmann@41080
   782
  "(f \<squnion> g) x = f x \<squnion> g x"
haftmann@41080
   783
  by (simp add: sup_fun_def)
haftmann@25510
   784
haftmann@32780
   785
instance proof
noschinl@46884
   786
qed (simp_all add: le_fun_def)
haftmann@23878
   787
haftmann@25510
   788
end
haftmann@23878
   789
nipkow@51387
   790
instantiation "fun" :: (type, semilattice_inf) semilattice_inf
nipkow@51387
   791
begin
nipkow@51387
   792
nipkow@51387
   793
definition
nipkow@51387
   794
  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
nipkow@51387
   795
nipkow@51387
   796
lemma inf_apply [simp, code]:
nipkow@51387
   797
  "(f \<sqinter> g) x = f x \<sqinter> g x"
nipkow@51387
   798
  by (simp add: inf_fun_def)
nipkow@51387
   799
nipkow@51387
   800
instance proof
nipkow@51387
   801
qed (simp_all add: le_fun_def)
nipkow@51387
   802
nipkow@51387
   803
end
nipkow@51387
   804
nipkow@51387
   805
instance "fun" :: (type, lattice) lattice ..
nipkow@51387
   806
haftmann@41080
   807
instance "fun" :: (type, distrib_lattice) distrib_lattice proof
noschinl@46884
   808
qed (rule ext, simp add: sup_inf_distrib1)
haftmann@31991
   809
haftmann@34007
   810
instance "fun" :: (type, bounded_lattice) bounded_lattice ..
haftmann@34007
   811
haftmann@31991
   812
instantiation "fun" :: (type, uminus) uminus
haftmann@31991
   813
begin
haftmann@31991
   814
haftmann@31991
   815
definition
haftmann@31991
   816
  fun_Compl_def: "- A = (\<lambda>x. - A x)"
haftmann@31991
   817
haftmann@49769
   818
lemma uminus_apply [simp, code]:
haftmann@41080
   819
  "(- A) x = - (A x)"
haftmann@41080
   820
  by (simp add: fun_Compl_def)
haftmann@41080
   821
haftmann@31991
   822
instance ..
haftmann@31991
   823
haftmann@31991
   824
end
haftmann@31991
   825
haftmann@31991
   826
instantiation "fun" :: (type, minus) minus
haftmann@31991
   827
begin
haftmann@31991
   828
haftmann@31991
   829
definition
haftmann@31991
   830
  fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
haftmann@31991
   831
haftmann@49769
   832
lemma minus_apply [simp, code]:
haftmann@41080
   833
  "(A - B) x = A x - B x"
haftmann@41080
   834
  by (simp add: fun_diff_def)
haftmann@41080
   835
haftmann@31991
   836
instance ..
haftmann@31991
   837
haftmann@31991
   838
end
haftmann@31991
   839
haftmann@41080
   840
instance "fun" :: (type, boolean_algebra) boolean_algebra proof
noschinl@46884
   841
qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
berghofe@26794
   842
haftmann@46631
   843
haftmann@46631
   844
subsection {* Lattice on unary and binary predicates *}
haftmann@46631
   845
haftmann@46631
   846
lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
haftmann@46631
   847
  by (simp add: inf_fun_def)
haftmann@46631
   848
haftmann@46631
   849
lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
haftmann@46631
   850
  by (simp add: inf_fun_def)
haftmann@46631
   851
haftmann@46631
   852
lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
haftmann@46631
   853
  by (simp add: inf_fun_def)
haftmann@46631
   854
haftmann@46631
   855
lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
haftmann@46631
   856
  by (simp add: inf_fun_def)
haftmann@46631
   857
haftmann@46631
   858
lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
haftmann@46631
   859
  by (simp add: inf_fun_def)
haftmann@46631
   860
haftmann@46631
   861
lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
haftmann@46631
   862
  by (simp add: inf_fun_def)
haftmann@46631
   863
haftmann@46631
   864
lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
haftmann@46631
   865
  by (simp add: inf_fun_def)
haftmann@46631
   866
haftmann@46631
   867
lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
haftmann@46631
   868
  by (simp add: inf_fun_def)
haftmann@46631
   869
haftmann@46631
   870
lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
haftmann@46631
   871
  by (simp add: sup_fun_def)
haftmann@46631
   872
haftmann@46631
   873
lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
haftmann@46631
   874
  by (simp add: sup_fun_def)
haftmann@46631
   875
haftmann@46631
   876
lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
haftmann@46631
   877
  by (simp add: sup_fun_def)
haftmann@46631
   878
haftmann@46631
   879
lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
haftmann@46631
   880
  by (simp add: sup_fun_def)
haftmann@46631
   881
haftmann@46631
   882
lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
haftmann@46631
   883
  by (simp add: sup_fun_def) iprover
haftmann@46631
   884
haftmann@46631
   885
lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
haftmann@46631
   886
  by (simp add: sup_fun_def) iprover
haftmann@46631
   887
haftmann@46631
   888
text {*
haftmann@46631
   889
  \medskip Classical introduction rule: no commitment to @{text A} vs
haftmann@46631
   890
  @{text B}.
haftmann@46631
   891
*}
haftmann@46631
   892
haftmann@46631
   893
lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
haftmann@46631
   894
  by (auto simp add: sup_fun_def)
haftmann@46631
   895
haftmann@46631
   896
lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
haftmann@46631
   897
  by (auto simp add: sup_fun_def)
haftmann@46631
   898
haftmann@46631
   899
haftmann@25062
   900
no_notation
haftmann@46691
   901
  less_eq (infix "\<sqsubseteq>" 50) and
haftmann@46691
   902
  less (infix "\<sqsubset>" 50)
haftmann@25062
   903
haftmann@21249
   904
end
haftmann@46631
   905