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