src/HOL/Lattices.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (21 months ago)
changeset 66983 df83b66f1d94
parent 63820 9f004fbf9d5c
child 67399 eab6ce8368fa
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     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