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