src/HOL/Lattices.thy
author haftmann
Thu Mar 11 14:38:20 2010 +0100 (2010-03-11)
changeset 35724 178ad68f93ed
parent 35301 90e42f9ba4d1
child 36008 23dfa8678c7c
permissions -rw-r--r--
fixed typo
     1 (*  Title:      HOL/Lattices.thy
     2     Author:     Tobias Nipkow
     3 *)
     4 
     5 header {* Abstract lattices *}
     6 
     7 theory Lattices
     8 imports Orderings Groups
     9 begin
    10 
    11 subsection {* Abstract semilattice *}
    12 
    13 text {*
    14   This 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 *}
    18 
    19 locale semilattice = abel_semigroup +
    20   assumes idem [simp]: "f a a = a"
    21 begin
    22 
    23 lemma left_idem [simp]:
    24   "f a (f a b) = f a b"
    25   by (simp add: assoc [symmetric])
    26 
    27 end
    28 
    29 
    30 subsection {* Idempotent semigroup *}
    31 
    32 class ab_semigroup_idem_mult = ab_semigroup_mult +
    33   assumes mult_idem: "x * x = x"
    34 
    35 sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    36 qed (fact mult_idem)
    37 
    38 context ab_semigroup_idem_mult
    39 begin
    40 
    41 lemmas mult_left_idem = times.left_idem
    42 
    43 end
    44 
    45 
    46 subsection {* Concrete lattices *}
    47 
    48 notation
    49   less_eq  (infix "\<sqsubseteq>" 50) and
    50   less  (infix "\<sqsubset>" 50) and
    51   top ("\<top>") and
    52   bot ("\<bottom>")
    53 
    54 class semilattice_inf = order +
    55   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    56   assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    57   and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    58   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    59 
    60 class semilattice_sup = order +
    61   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    62   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    63   and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    64   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    65 begin
    66 
    67 text {* Dual lattice *}
    68 
    69 lemma dual_semilattice:
    70   "semilattice_inf (op \<ge>) (op >) sup"
    71 by (rule semilattice_inf.intro, rule dual_order)
    72   (unfold_locales, simp_all add: sup_least)
    73 
    74 end
    75 
    76 class lattice = semilattice_inf + semilattice_sup
    77 
    78 
    79 subsubsection {* Intro and elim rules*}
    80 
    81 context semilattice_inf
    82 begin
    83 
    84 lemma le_infI1:
    85   "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    86   by (rule order_trans) auto
    87 
    88 lemma le_infI2:
    89   "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    90   by (rule order_trans) auto
    91 
    92 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    93   by (blast intro: inf_greatest)
    94 
    95 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    96   by (blast intro: order_trans le_infI1 le_infI2)
    97 
    98 lemma le_inf_iff [simp]:
    99   "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   100   by (blast intro: le_infI elim: le_infE)
   101 
   102 lemma le_iff_inf:
   103   "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   104   by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
   105 
   106 lemma mono_inf:
   107   fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
   108   shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
   109   by (auto simp add: mono_def intro: Lattices.inf_greatest)
   110 
   111 end
   112 
   113 context semilattice_sup
   114 begin
   115 
   116 lemma le_supI1:
   117   "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   118   by (rule order_trans) auto
   119 
   120 lemma le_supI2:
   121   "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   122   by (rule order_trans) auto 
   123 
   124 lemma le_supI:
   125   "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   126   by (blast intro: sup_least)
   127 
   128 lemma le_supE:
   129   "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   130   by (blast intro: le_supI1 le_supI2 order_trans)
   131 
   132 lemma le_sup_iff [simp]:
   133   "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   134   by (blast intro: le_supI elim: le_supE)
   135 
   136 lemma le_iff_sup:
   137   "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   138   by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
   139 
   140 lemma mono_sup:
   141   fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
   142   shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
   143   by (auto simp add: mono_def intro: Lattices.sup_least)
   144 
   145 end
   146 
   147 
   148 subsubsection {* Equational laws *}
   149 
   150 sublocale semilattice_inf < inf!: semilattice inf
   151 proof
   152   fix a b c
   153   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
   154     by (rule antisym) (auto intro: le_infI1 le_infI2)
   155   show "a \<sqinter> b = b \<sqinter> a"
   156     by (rule antisym) auto
   157   show "a \<sqinter> a = a"
   158     by (rule antisym) auto
   159 qed
   160 
   161 context semilattice_inf
   162 begin
   163 
   164 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   165   by (fact inf.assoc)
   166 
   167 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   168   by (fact inf.commute)
   169 
   170 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   171   by (fact inf.left_commute)
   172 
   173 lemma inf_idem: "x \<sqinter> x = x"
   174   by (fact inf.idem)
   175 
   176 lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   177   by (fact inf.left_idem)
   178 
   179 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   180   by (rule antisym) auto
   181 
   182 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   183   by (rule antisym) auto
   184  
   185 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   186 
   187 end
   188 
   189 sublocale semilattice_sup < sup!: semilattice sup
   190 proof
   191   fix a b c
   192   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   193     by (rule antisym) (auto intro: le_supI1 le_supI2)
   194   show "a \<squnion> b = b \<squnion> a"
   195     by (rule antisym) auto
   196   show "a \<squnion> a = a"
   197     by (rule antisym) auto
   198 qed
   199 
   200 context semilattice_sup
   201 begin
   202 
   203 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   204   by (fact sup.assoc)
   205 
   206 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   207   by (fact sup.commute)
   208 
   209 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   210   by (fact sup.left_commute)
   211 
   212 lemma sup_idem: "x \<squnion> x = x"
   213   by (fact sup.idem)
   214 
   215 lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   216   by (fact sup.left_idem)
   217 
   218 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   219   by (rule antisym) auto
   220 
   221 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   222   by (rule antisym) auto
   223 
   224 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   225 
   226 end
   227 
   228 context lattice
   229 begin
   230 
   231 lemma dual_lattice:
   232   "lattice (op \<ge>) (op >) sup inf"
   233   by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
   234     (unfold_locales, auto)
   235 
   236 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
   237   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
   238 
   239 lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   240   by (blast intro: antisym sup_ge1 sup_least inf_le1)
   241 
   242 lemmas inf_sup_aci = inf_aci sup_aci
   243 
   244 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
   245 
   246 text{* Towards distributivity *}
   247 
   248 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   249   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   250 
   251 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   252   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   253 
   254 text{* If you have one of them, you have them all. *}
   255 
   256 lemma distrib_imp1:
   257 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   258 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   259 proof-
   260   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
   261   also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
   262   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
   263     by(simp add:inf_sup_absorb inf_commute)
   264   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
   265   finally show ?thesis .
   266 qed
   267 
   268 lemma distrib_imp2:
   269 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   270 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   271 proof-
   272   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
   273   also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
   274   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   275     by(simp add:sup_inf_absorb sup_commute)
   276   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   277   finally show ?thesis .
   278 qed
   279 
   280 end
   281 
   282 subsubsection {* Strict order *}
   283 
   284 context semilattice_inf
   285 begin
   286 
   287 lemma less_infI1:
   288   "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   289   by (auto simp add: less_le inf_absorb1 intro: le_infI1)
   290 
   291 lemma less_infI2:
   292   "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   293   by (auto simp add: less_le inf_absorb2 intro: le_infI2)
   294 
   295 end
   296 
   297 context semilattice_sup
   298 begin
   299 
   300 lemma less_supI1:
   301   "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   302 proof -
   303   interpret dual: semilattice_inf "op \<ge>" "op >" sup
   304     by (fact dual_semilattice)
   305   assume "x \<sqsubset> a"
   306   then show "x \<sqsubset> a \<squnion> b"
   307     by (fact dual.less_infI1)
   308 qed
   309 
   310 lemma less_supI2:
   311   "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   312 proof -
   313   interpret dual: semilattice_inf "op \<ge>" "op >" sup
   314     by (fact dual_semilattice)
   315   assume "x \<sqsubset> b"
   316   then show "x \<sqsubset> a \<squnion> b"
   317     by (fact dual.less_infI2)
   318 qed
   319 
   320 end
   321 
   322 
   323 subsection {* Distributive lattices *}
   324 
   325 class distrib_lattice = lattice +
   326   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   327 
   328 context distrib_lattice
   329 begin
   330 
   331 lemma sup_inf_distrib2:
   332  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   333 by(simp add: inf_sup_aci sup_inf_distrib1)
   334 
   335 lemma inf_sup_distrib1:
   336  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   337 by(rule distrib_imp2[OF sup_inf_distrib1])
   338 
   339 lemma inf_sup_distrib2:
   340  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   341 by(simp add: inf_sup_aci inf_sup_distrib1)
   342 
   343 lemma dual_distrib_lattice:
   344   "distrib_lattice (op \<ge>) (op >) sup inf"
   345   by (rule distrib_lattice.intro, rule dual_lattice)
   346     (unfold_locales, fact inf_sup_distrib1)
   347 
   348 lemmas distrib =
   349   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   350 
   351 end
   352 
   353 
   354 subsection {* Bounded lattices and boolean algebras *}
   355 
   356 class bounded_lattice = lattice + top + bot
   357 begin
   358 
   359 lemma dual_bounded_lattice:
   360   "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   361   by (rule bounded_lattice.intro, rule dual_lattice)
   362     (unfold_locales, auto simp add: less_le_not_le)
   363 
   364 lemma inf_bot_left [simp]:
   365   "\<bottom> \<sqinter> x = \<bottom>"
   366   by (rule inf_absorb1) simp
   367 
   368 lemma inf_bot_right [simp]:
   369   "x \<sqinter> \<bottom> = \<bottom>"
   370   by (rule inf_absorb2) simp
   371 
   372 lemma sup_top_left [simp]:
   373   "\<top> \<squnion> x = \<top>"
   374   by (rule sup_absorb1) simp
   375 
   376 lemma sup_top_right [simp]:
   377   "x \<squnion> \<top> = \<top>"
   378   by (rule sup_absorb2) simp
   379 
   380 lemma inf_top_left [simp]:
   381   "\<top> \<sqinter> x = x"
   382   by (rule inf_absorb2) simp
   383 
   384 lemma inf_top_right [simp]:
   385   "x \<sqinter> \<top> = x"
   386   by (rule inf_absorb1) simp
   387 
   388 lemma sup_bot_left [simp]:
   389   "\<bottom> \<squnion> x = x"
   390   by (rule sup_absorb2) simp
   391 
   392 lemma sup_bot_right [simp]:
   393   "x \<squnion> \<bottom> = x"
   394   by (rule sup_absorb1) simp
   395 
   396 lemma inf_eq_top_eq1:
   397   assumes "A \<sqinter> B = \<top>"
   398   shows "A = \<top>"
   399 proof (cases "B = \<top>")
   400   case True with assms show ?thesis by simp
   401 next
   402   case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans)
   403   then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2)
   404   with assms show ?thesis by simp
   405 qed
   406 
   407 lemma inf_eq_top_eq2:
   408   assumes "A \<sqinter> B = \<top>"
   409   shows "B = \<top>"
   410   by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
   411 
   412 lemma sup_eq_bot_eq1:
   413   assumes "A \<squnion> B = \<bottom>"
   414   shows "A = \<bottom>"
   415 proof -
   416   interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   417     by (rule dual_bounded_lattice)
   418   from dual.inf_eq_top_eq1 assms show ?thesis .
   419 qed
   420 
   421 lemma sup_eq_bot_eq2:
   422   assumes "A \<squnion> B = \<bottom>"
   423   shows "B = \<bottom>"
   424 proof -
   425   interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   426     by (rule dual_bounded_lattice)
   427   from dual.inf_eq_top_eq2 assms show ?thesis .
   428 qed
   429 
   430 end
   431 
   432 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
   433   assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
   434     and sup_compl_top: "x \<squnion> - x = \<top>"
   435   assumes diff_eq: "x - y = x \<sqinter> - y"
   436 begin
   437 
   438 lemma dual_boolean_algebra:
   439   "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   440   by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
   441     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
   442 
   443 lemma compl_inf_bot:
   444   "- x \<sqinter> x = \<bottom>"
   445   by (simp add: inf_commute inf_compl_bot)
   446 
   447 lemma compl_sup_top:
   448   "- x \<squnion> x = \<top>"
   449   by (simp add: sup_commute sup_compl_top)
   450 
   451 lemma compl_unique:
   452   assumes "x \<sqinter> y = \<bottom>"
   453     and "x \<squnion> y = \<top>"
   454   shows "- x = y"
   455 proof -
   456   have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
   457     using inf_compl_bot assms(1) by simp
   458   then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
   459     by (simp add: inf_commute)
   460   then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
   461     by (simp add: inf_sup_distrib1)
   462   then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
   463     using sup_compl_top assms(2) by simp
   464   then show "- x = y" by simp
   465 qed
   466 
   467 lemma double_compl [simp]:
   468   "- (- x) = x"
   469   using compl_inf_bot compl_sup_top by (rule compl_unique)
   470 
   471 lemma compl_eq_compl_iff [simp]:
   472   "- x = - y \<longleftrightarrow> x = y"
   473 proof
   474   assume "- x = - y"
   475   then have "- x \<sqinter> y = \<bottom>"
   476     and "- x \<squnion> y = \<top>"
   477     by (simp_all add: compl_inf_bot compl_sup_top)
   478   then have "- (- x) = y" by (rule compl_unique)
   479   then show "x = y" by simp
   480 next
   481   assume "x = y"
   482   then show "- x = - y" by simp
   483 qed
   484 
   485 lemma compl_bot_eq [simp]:
   486   "- \<bottom> = \<top>"
   487 proof -
   488   from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   489   then show ?thesis by simp
   490 qed
   491 
   492 lemma compl_top_eq [simp]:
   493   "- \<top> = \<bottom>"
   494 proof -
   495   from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   496   then show ?thesis by simp
   497 qed
   498 
   499 lemma compl_inf [simp]:
   500   "- (x \<sqinter> y) = - x \<squnion> - y"
   501 proof (rule compl_unique)
   502   have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
   503     by (rule inf_sup_distrib1)
   504   also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   505     by (simp only: inf_commute inf_assoc inf_left_commute)
   506   finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
   507     by (simp add: inf_compl_bot)
   508 next
   509   have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
   510     by (rule sup_inf_distrib2)
   511   also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   512     by (simp only: sup_commute sup_assoc sup_left_commute)
   513   finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
   514     by (simp add: sup_compl_top)
   515 qed
   516 
   517 lemma compl_sup [simp]:
   518   "- (x \<squnion> y) = - x \<sqinter> - y"
   519 proof -
   520   interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   521     by (rule dual_boolean_algebra)
   522   then show ?thesis by simp
   523 qed
   524 
   525 end
   526 
   527 
   528 subsection {* Uniqueness of inf and sup *}
   529 
   530 lemma (in semilattice_inf) inf_unique:
   531   fixes f (infixl "\<triangle>" 70)
   532   assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   533   and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   534   shows "x \<sqinter> y = x \<triangle> y"
   535 proof (rule antisym)
   536   show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   537 next
   538   have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
   539   show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   540 qed
   541 
   542 lemma (in semilattice_sup) sup_unique:
   543   fixes f (infixl "\<nabla>" 70)
   544   assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   545   and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   546   shows "x \<squnion> y = x \<nabla> y"
   547 proof (rule antisym)
   548   show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   549 next
   550   have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   551   show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   552 qed
   553   
   554 
   555 subsection {* @{const min}/@{const max} on linear orders as
   556   special case of @{const inf}/@{const sup} *}
   557 
   558 sublocale linorder < min_max!: distrib_lattice less_eq less min max
   559 proof
   560   fix x y z
   561   show "max x (min y z) = min (max x y) (max x z)"
   562     by (auto simp add: min_def max_def)
   563 qed (auto simp add: min_def max_def not_le less_imp_le)
   564 
   565 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   566   by (rule ext)+ (auto intro: antisym)
   567 
   568 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   569   by (rule ext)+ (auto intro: antisym)
   570 
   571 lemmas le_maxI1 = min_max.sup_ge1
   572 lemmas le_maxI2 = min_max.sup_ge2
   573  
   574 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   575   min_max.inf.left_commute
   576 
   577 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   578   min_max.sup.left_commute
   579 
   580 
   581 
   582 subsection {* Bool as lattice *}
   583 
   584 instantiation bool :: boolean_algebra
   585 begin
   586 
   587 definition
   588   bool_Compl_def: "uminus = Not"
   589 
   590 definition
   591   bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
   592 
   593 definition
   594   inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   595 
   596 definition
   597   sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   598 
   599 instance proof
   600 qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def
   601   bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto)
   602 
   603 end
   604 
   605 lemma sup_boolI1:
   606   "P \<Longrightarrow> P \<squnion> Q"
   607   by (simp add: sup_bool_eq)
   608 
   609 lemma sup_boolI2:
   610   "Q \<Longrightarrow> P \<squnion> Q"
   611   by (simp add: sup_bool_eq)
   612 
   613 lemma sup_boolE:
   614   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   615   by (auto simp add: sup_bool_eq)
   616 
   617 
   618 subsection {* Fun as lattice *}
   619 
   620 instantiation "fun" :: (type, lattice) lattice
   621 begin
   622 
   623 definition
   624   inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   625 
   626 definition
   627   sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   628 
   629 instance proof
   630 qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
   631 
   632 end
   633 
   634 instance "fun" :: (type, distrib_lattice) distrib_lattice
   635 proof
   636 qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   637 
   638 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
   639 
   640 instantiation "fun" :: (type, uminus) uminus
   641 begin
   642 
   643 definition
   644   fun_Compl_def: "- A = (\<lambda>x. - A x)"
   645 
   646 instance ..
   647 
   648 end
   649 
   650 instantiation "fun" :: (type, minus) minus
   651 begin
   652 
   653 definition
   654   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   655 
   656 instance ..
   657 
   658 end
   659 
   660 instance "fun" :: (type, boolean_algebra) boolean_algebra
   661 proof
   662 qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def
   663   inf_compl_bot sup_compl_top diff_eq)
   664 
   665 
   666 no_notation
   667   less_eq  (infix "\<sqsubseteq>" 50) and
   668   less (infix "\<sqsubset>" 50) and
   669   inf  (infixl "\<sqinter>" 70) and
   670   sup  (infixl "\<squnion>" 65) and
   671   top ("\<top>") and
   672   bot ("\<bottom>")
   673 
   674 end