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