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