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