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