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