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