src/HOL/Lattices.thy
author haftmann
Sat Mar 23 17:11:06 2013 +0100 (2013-03-23)
changeset 51487 f4bfdee99304
parent 51387 dbc4a77488b2
child 51489 f738e6dbd844
permissions -rw-r--r--
locales for abstract orders
     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   These locales provide a basic structure for interpretation into
    15   bigger structures;  extensions require careful thinking, otherwise
    16   undesired effects may occur due to interpretation.
    17 *}
    18 
    19 no_notation times (infixl "*" 70)
    20 no_notation Groups.one ("1")
    21 
    22 locale semilattice = abel_semigroup +
    23   assumes idem [simp]: "a * a = a"
    24 begin
    25 
    26 lemma left_idem [simp]: "a * (a * b) = a * b"
    27 by (simp add: assoc [symmetric])
    28 
    29 lemma right_idem [simp]: "(a * b) * b = a * b"
    30 by (simp add: assoc)
    31 
    32 end
    33 
    34 locale semilattice_neutr = semilattice + comm_monoid
    35 
    36 locale semilattice_order = semilattice +
    37   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
    38     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
    39   assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
    40     and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    41 begin
    42 
    43 lemma orderI:
    44   "a = a * b \<Longrightarrow> a \<preceq> b"
    45   by (simp add: order_iff)
    46 
    47 lemma orderE:
    48   assumes "a \<preceq> b"
    49   obtains "a = a * b"
    50   using assms by (unfold order_iff)
    51 
    52 end
    53 
    54 sublocale semilattice_order < ordering less_eq less
    55 proof
    56   fix a b
    57   show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    58     by (fact semilattice_strict_iff_order)
    59 next
    60   fix a
    61   show "a \<preceq> a"
    62     by (simp add: order_iff)
    63 next
    64   fix a b
    65   assume "a \<preceq> b" "b \<preceq> a"
    66   then have "a = a * b" "a * b = b"
    67     by (simp_all add: order_iff commute)
    68   then show "a = b" by simp
    69 next
    70   fix a b c
    71   assume "a \<preceq> b" "b \<preceq> c"
    72   then have "a = a * b" "b = b * c"
    73     by (simp_all add: order_iff commute)
    74   then have "a = a * (b * c)"
    75     by simp
    76   then have "a = (a * b) * c"
    77     by (simp add: assoc)
    78   with `a = a * b` [symmetric] have "a = a * c" by simp
    79   then show "a \<preceq> c" by (rule orderI)
    80 qed
    81 
    82 context semilattice_order
    83 begin
    84 
    85 lemma cobounded1 [simp]:
    86   "a * b \<preceq> a"
    87   by (simp add: order_iff commute)  
    88 
    89 lemma cobounded2 [simp]:
    90   "a * b \<preceq> b"
    91   by (simp add: order_iff)
    92 
    93 lemma boundedI:
    94   assumes "a \<preceq> b" and "a \<preceq> c"
    95   shows "a \<preceq> b * c"
    96 proof (rule orderI)
    97   from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
    98   then show "a = a * (b * c)" by (simp add: assoc [symmetric])
    99 qed
   100 
   101 lemma boundedE:
   102   assumes "a \<preceq> b * c"
   103   obtains "a \<preceq> b" and "a \<preceq> c"
   104   using assms by (blast intro: trans cobounded1 cobounded2)
   105 
   106 lemma bounded_iff:
   107   "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
   108   by (blast intro: boundedI elim: boundedE)
   109 
   110 lemma strict_boundedE:
   111   assumes "a \<prec> b * c"
   112   obtains "a \<prec> b" and "a \<prec> c"
   113   using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
   114 
   115 lemma coboundedI1:
   116   "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   117   by (rule trans) auto
   118 
   119 lemma coboundedI2:
   120   "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   121   by (rule trans) auto
   122 
   123 lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
   124   by (blast intro: boundedI coboundedI1 coboundedI2)
   125 
   126 lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
   127   by (rule antisym) (auto simp add: refl bounded_iff)
   128 
   129 lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
   130   by (rule antisym) (auto simp add: refl bounded_iff)
   131 
   132 end
   133 
   134 locale semilattice_neutr_order = semilattice_neutr + semilattice_order
   135 
   136 sublocale semilattice_neutr_order < ordering_top less_eq less 1
   137   by default (simp add: order_iff)
   138 
   139 notation times (infixl "*" 70)
   140 notation Groups.one ("1")
   141 
   142 
   143 subsection {* Syntactic infimum and supremum operations *}
   144 
   145 class inf =
   146   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
   147 
   148 class sup = 
   149   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
   150 
   151 
   152 subsection {* Concrete lattices *}
   153 
   154 notation
   155   less_eq  (infix "\<sqsubseteq>" 50) and
   156   less  (infix "\<sqsubset>" 50)
   157 
   158 class semilattice_inf =  order + inf +
   159   assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
   160   and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
   161   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
   162 
   163 class semilattice_sup = order + sup +
   164   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
   165   and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
   166   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
   167 begin
   168 
   169 text {* Dual lattice *}
   170 
   171 lemma dual_semilattice:
   172   "class.semilattice_inf sup greater_eq greater"
   173 by (rule class.semilattice_inf.intro, rule dual_order)
   174   (unfold_locales, simp_all add: sup_least)
   175 
   176 end
   177 
   178 class lattice = semilattice_inf + semilattice_sup
   179 
   180 
   181 subsubsection {* Intro and elim rules*}
   182 
   183 context semilattice_inf
   184 begin
   185 
   186 lemma le_infI1:
   187   "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   188   by (rule order_trans) auto
   189 
   190 lemma le_infI2:
   191   "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   192   by (rule order_trans) auto
   193 
   194 lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
   195   by (rule inf_greatest) (* FIXME: duplicate lemma *)
   196 
   197 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
   198   by (blast intro: order_trans inf_le1 inf_le2)
   199 
   200 lemma le_inf_iff [simp]:
   201   "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   202   by (blast intro: le_infI elim: le_infE)
   203 
   204 lemma le_iff_inf:
   205   "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   206   by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
   207 
   208 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
   209   by (fast intro: inf_greatest le_infI1 le_infI2)
   210 
   211 lemma mono_inf:
   212   fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
   213   shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
   214   by (auto simp add: mono_def intro: Lattices.inf_greatest)
   215 
   216 end
   217 
   218 context semilattice_sup
   219 begin
   220 
   221 lemma le_supI1:
   222   "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   223   by (rule order_trans) auto
   224 
   225 lemma le_supI2:
   226   "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   227   by (rule order_trans) auto 
   228 
   229 lemma le_supI:
   230   "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   231   by (rule sup_least) (* FIXME: duplicate lemma *)
   232 
   233 lemma le_supE:
   234   "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   235   by (blast intro: order_trans sup_ge1 sup_ge2)
   236 
   237 lemma le_sup_iff [simp]:
   238   "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   239   by (blast intro: le_supI elim: le_supE)
   240 
   241 lemma le_iff_sup:
   242   "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   243   by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
   244 
   245 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
   246   by (fast intro: sup_least le_supI1 le_supI2)
   247 
   248 lemma mono_sup:
   249   fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
   250   shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
   251   by (auto simp add: mono_def intro: Lattices.sup_least)
   252 
   253 end
   254 
   255 
   256 subsubsection {* Equational laws *}
   257 
   258 sublocale semilattice_inf < inf!: semilattice inf
   259 proof
   260   fix a b c
   261   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
   262     by (rule antisym) (auto intro: le_infI1 le_infI2)
   263   show "a \<sqinter> b = b \<sqinter> a"
   264     by (rule antisym) auto
   265   show "a \<sqinter> a = a"
   266     by (rule antisym) auto
   267 qed
   268 
   269 sublocale semilattice_sup < sup!: semilattice sup
   270 proof
   271   fix a b c
   272   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   273     by (rule antisym) (auto intro: le_supI1 le_supI2)
   274   show "a \<squnion> b = b \<squnion> a"
   275     by (rule antisym) auto
   276   show "a \<squnion> a = a"
   277     by (rule antisym) auto
   278 qed
   279 
   280 sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
   281   by default (auto simp add: le_iff_inf less_le)
   282 
   283 sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
   284   by default (auto simp add: le_iff_sup sup.commute less_le)
   285 
   286 context semilattice_inf
   287 begin
   288 
   289 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   290   by (fact inf.assoc)
   291 
   292 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   293   by (fact inf.commute)
   294 
   295 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   296   by (fact inf.left_commute)
   297 
   298 lemma inf_idem: "x \<sqinter> x = x"
   299   by (fact inf.idem) (* already simp *)
   300 
   301 lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   302   by (fact inf.left_idem) (* already simp *)
   303 
   304 lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
   305   by (fact inf.right_idem) (* already simp *)
   306 
   307 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   308   by (rule antisym) auto
   309 
   310 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   311   by (rule antisym) auto
   312  
   313 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   314 
   315 end
   316 
   317 context semilattice_sup
   318 begin
   319 
   320 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   321   by (fact sup.assoc)
   322 
   323 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   324   by (fact sup.commute)
   325 
   326 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   327   by (fact sup.left_commute)
   328 
   329 lemma sup_idem: "x \<squnion> x = x"
   330   by (fact sup.idem) (* already simp *)
   331 
   332 lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   333   by (fact sup.left_idem)
   334 
   335 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   336   by (rule antisym) auto
   337 
   338 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   339   by (rule antisym) auto
   340 
   341 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   342 
   343 end
   344 
   345 context lattice
   346 begin
   347 
   348 lemma dual_lattice:
   349   "class.lattice sup (op \<ge>) (op >) inf"
   350   by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
   351     (unfold_locales, auto)
   352 
   353 lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
   354   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
   355 
   356 lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"
   357   by (blast intro: antisym sup_ge1 sup_least inf_le1)
   358 
   359 lemmas inf_sup_aci = inf_aci sup_aci
   360 
   361 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
   362 
   363 text{* Towards distributivity *}
   364 
   365 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   366   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   367 
   368 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   369   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   370 
   371 text{* If you have one of them, you have them all. *}
   372 
   373 lemma distrib_imp1:
   374 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   375 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   376 proof-
   377   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp
   378   also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
   379     by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
   380   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
   381     by(simp add: inf_commute)
   382   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
   383   finally show ?thesis .
   384 qed
   385 
   386 lemma distrib_imp2:
   387 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   388 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   389 proof-
   390   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp
   391   also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
   392     by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
   393   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   394     by(simp add: sup_commute)
   395   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   396   finally show ?thesis .
   397 qed
   398 
   399 end
   400 
   401 subsubsection {* Strict order *}
   402 
   403 context semilattice_inf
   404 begin
   405 
   406 lemma less_infI1:
   407   "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   408   by (auto simp add: less_le inf_absorb1 intro: le_infI1)
   409 
   410 lemma less_infI2:
   411   "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   412   by (auto simp add: less_le inf_absorb2 intro: le_infI2)
   413 
   414 end
   415 
   416 context semilattice_sup
   417 begin
   418 
   419 lemma less_supI1:
   420   "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   421   using dual_semilattice
   422   by (rule semilattice_inf.less_infI1)
   423 
   424 lemma less_supI2:
   425   "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   426   using dual_semilattice
   427   by (rule semilattice_inf.less_infI2)
   428 
   429 end
   430 
   431 
   432 subsection {* Distributive lattices *}
   433 
   434 class distrib_lattice = lattice +
   435   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   436 
   437 context distrib_lattice
   438 begin
   439 
   440 lemma sup_inf_distrib2:
   441   "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   442   by (simp add: sup_commute sup_inf_distrib1)
   443 
   444 lemma inf_sup_distrib1:
   445   "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   446   by (rule distrib_imp2 [OF sup_inf_distrib1])
   447 
   448 lemma inf_sup_distrib2:
   449   "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   450   by (simp add: inf_commute inf_sup_distrib1)
   451 
   452 lemma dual_distrib_lattice:
   453   "class.distrib_lattice sup (op \<ge>) (op >) inf"
   454   by (rule class.distrib_lattice.intro, rule dual_lattice)
   455     (unfold_locales, fact inf_sup_distrib1)
   456 
   457 lemmas sup_inf_distrib =
   458   sup_inf_distrib1 sup_inf_distrib2
   459 
   460 lemmas inf_sup_distrib =
   461   inf_sup_distrib1 inf_sup_distrib2
   462 
   463 lemmas distrib =
   464   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   465 
   466 end
   467 
   468 
   469 subsection {* Bounded lattices and boolean algebras *}
   470 
   471 class bounded_semilattice_inf_top = semilattice_inf + top
   472 
   473 sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
   474 proof
   475   fix x
   476   show "x \<sqinter> \<top> = x"
   477     by (rule inf_absorb1) simp
   478 qed
   479 
   480 sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
   481 
   482 class bounded_semilattice_sup_bot = semilattice_sup + bot
   483 
   484 sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
   485 proof
   486   fix x
   487   show "x \<squnion> \<bottom> = x"
   488     by (rule sup_absorb1) simp
   489 qed
   490 
   491 sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
   492 
   493 class bounded_lattice_bot = lattice + bot
   494 begin
   495 
   496 subclass bounded_semilattice_sup_bot ..
   497 
   498 lemma inf_bot_left [simp]:
   499   "\<bottom> \<sqinter> x = \<bottom>"
   500   by (rule inf_absorb1) simp
   501 
   502 lemma inf_bot_right [simp]:
   503   "x \<sqinter> \<bottom> = \<bottom>"
   504   by (rule inf_absorb2) simp
   505 
   506 lemma sup_bot_left:
   507   "\<bottom> \<squnion> x = x"
   508   by (fact sup_bot.left_neutral)
   509 
   510 lemma sup_bot_right:
   511   "x \<squnion> \<bottom> = x"
   512   by (fact sup_bot.right_neutral)
   513 
   514 lemma sup_eq_bot_iff [simp]:
   515   "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   516   by (simp add: eq_iff)
   517 
   518 end
   519 
   520 class bounded_lattice_top = lattice + top
   521 begin
   522 
   523 subclass bounded_semilattice_inf_top ..
   524 
   525 lemma sup_top_left [simp]:
   526   "\<top> \<squnion> x = \<top>"
   527   by (rule sup_absorb1) simp
   528 
   529 lemma sup_top_right [simp]:
   530   "x \<squnion> \<top> = \<top>"
   531   by (rule sup_absorb2) simp
   532 
   533 lemma inf_top_left:
   534   "\<top> \<sqinter> x = x"
   535   by (fact inf_top.left_neutral)
   536 
   537 lemma inf_top_right:
   538   "x \<sqinter> \<top> = x"
   539   by (fact inf_top.right_neutral)
   540 
   541 lemma inf_eq_top_iff [simp]:
   542   "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   543   by (simp add: eq_iff)
   544 
   545 end
   546 
   547 class bounded_lattice = lattice + bot + top
   548 begin
   549 
   550 subclass bounded_lattice_bot ..
   551 subclass bounded_lattice_top ..
   552 
   553 lemma dual_bounded_lattice:
   554   "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   555   by unfold_locales (auto simp add: less_le_not_le)
   556 
   557 end
   558 
   559 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
   560   assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
   561     and sup_compl_top: "x \<squnion> - x = \<top>"
   562   assumes diff_eq: "x - y = x \<sqinter> - y"
   563 begin
   564 
   565 lemma dual_boolean_algebra:
   566   "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
   567   by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
   568     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
   569 
   570 lemma compl_inf_bot [simp]:
   571   "- x \<sqinter> x = \<bottom>"
   572   by (simp add: inf_commute inf_compl_bot)
   573 
   574 lemma compl_sup_top [simp]:
   575   "- x \<squnion> x = \<top>"
   576   by (simp add: sup_commute sup_compl_top)
   577 
   578 lemma compl_unique:
   579   assumes "x \<sqinter> y = \<bottom>"
   580     and "x \<squnion> y = \<top>"
   581   shows "- x = y"
   582 proof -
   583   have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
   584     using inf_compl_bot assms(1) by simp
   585   then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
   586     by (simp add: inf_commute)
   587   then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
   588     by (simp add: inf_sup_distrib1)
   589   then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
   590     using sup_compl_top assms(2) by simp
   591   then show "- x = y" by simp
   592 qed
   593 
   594 lemma double_compl [simp]:
   595   "- (- x) = x"
   596   using compl_inf_bot compl_sup_top by (rule compl_unique)
   597 
   598 lemma compl_eq_compl_iff [simp]:
   599   "- x = - y \<longleftrightarrow> x = y"
   600 proof
   601   assume "- x = - y"
   602   then have "- (- x) = - (- y)" by (rule arg_cong)
   603   then show "x = y" by simp
   604 next
   605   assume "x = y"
   606   then show "- x = - y" by simp
   607 qed
   608 
   609 lemma compl_bot_eq [simp]:
   610   "- \<bottom> = \<top>"
   611 proof -
   612   from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   613   then show ?thesis by simp
   614 qed
   615 
   616 lemma compl_top_eq [simp]:
   617   "- \<top> = \<bottom>"
   618 proof -
   619   from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   620   then show ?thesis by simp
   621 qed
   622 
   623 lemma compl_inf [simp]:
   624   "- (x \<sqinter> y) = - x \<squnion> - y"
   625 proof (rule compl_unique)
   626   have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   627     by (simp only: inf_sup_distrib inf_aci)
   628   then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
   629     by (simp add: inf_compl_bot)
   630 next
   631   have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   632     by (simp only: sup_inf_distrib sup_aci)
   633   then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
   634     by (simp add: sup_compl_top)
   635 qed
   636 
   637 lemma compl_sup [simp]:
   638   "- (x \<squnion> y) = - x \<sqinter> - y"
   639   using dual_boolean_algebra
   640   by (rule boolean_algebra.compl_inf)
   641 
   642 lemma compl_mono:
   643   "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
   644 proof -
   645   assume "x \<sqsubseteq> y"
   646   then have "x \<squnion> y = y" by (simp only: le_iff_sup)
   647   then have "- (x \<squnion> y) = - y" by simp
   648   then have "- x \<sqinter> - y = - y" by simp
   649   then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
   650   then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
   651 qed
   652 
   653 lemma compl_le_compl_iff [simp]:
   654   "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   655   by (auto dest: compl_mono)
   656 
   657 lemma compl_le_swap1:
   658   assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
   659 proof -
   660   from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
   661   then show ?thesis by simp
   662 qed
   663 
   664 lemma compl_le_swap2:
   665   assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
   666 proof -
   667   from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
   668   then show ?thesis by simp
   669 qed
   670 
   671 lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
   672   "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
   673   by (auto simp add: less_le)
   674 
   675 lemma compl_less_swap1:
   676   assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
   677 proof -
   678   from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
   679   then show ?thesis by simp
   680 qed
   681 
   682 lemma compl_less_swap2:
   683   assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
   684 proof -
   685   from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
   686   then show ?thesis by simp
   687 qed
   688 
   689 end
   690 
   691 
   692 subsection {* Uniqueness of inf and sup *}
   693 
   694 lemma (in semilattice_inf) inf_unique:
   695   fixes f (infixl "\<triangle>" 70)
   696   assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   697   and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   698   shows "x \<sqinter> y = x \<triangle> y"
   699 proof (rule antisym)
   700   show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   701 next
   702   have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
   703   show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   704 qed
   705 
   706 lemma (in semilattice_sup) sup_unique:
   707   fixes f (infixl "\<nabla>" 70)
   708   assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   709   and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   710   shows "x \<squnion> y = x \<nabla> y"
   711 proof (rule antisym)
   712   show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   713 next
   714   have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   715   show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   716 qed
   717 
   718 
   719 subsection {* @{const min}/@{const max} on linear orders as
   720   special case of @{const inf}/@{const sup} *}
   721 
   722 sublocale linorder < min_max!: distrib_lattice min less_eq less max
   723 proof
   724   fix x y z
   725   show "max x (min y z) = min (max x y) (max x z)"
   726     by (auto simp add: min_def max_def)
   727 qed (auto simp add: min_def max_def not_le less_imp_le)
   728 
   729 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   730   by (rule ext)+ (auto intro: antisym)
   731 
   732 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   733   by (rule ext)+ (auto intro: antisym)
   734 
   735 lemmas le_maxI1 = min_max.sup_ge1
   736 lemmas le_maxI2 = min_max.sup_ge2
   737  
   738 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   739   min_max.inf.left_commute
   740 
   741 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   742   min_max.sup.left_commute
   743 
   744 
   745 subsection {* Lattice on @{typ bool} *}
   746 
   747 instantiation bool :: boolean_algebra
   748 begin
   749 
   750 definition
   751   bool_Compl_def [simp]: "uminus = Not"
   752 
   753 definition
   754   bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
   755 
   756 definition
   757   [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   758 
   759 definition
   760   [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   761 
   762 instance proof
   763 qed auto
   764 
   765 end
   766 
   767 lemma sup_boolI1:
   768   "P \<Longrightarrow> P \<squnion> Q"
   769   by simp
   770 
   771 lemma sup_boolI2:
   772   "Q \<Longrightarrow> P \<squnion> Q"
   773   by simp
   774 
   775 lemma sup_boolE:
   776   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   777   by auto
   778 
   779 
   780 subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
   781 
   782 instantiation "fun" :: (type, semilattice_sup) semilattice_sup
   783 begin
   784 
   785 definition
   786   "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   787 
   788 lemma sup_apply [simp, code]:
   789   "(f \<squnion> g) x = f x \<squnion> g x"
   790   by (simp add: sup_fun_def)
   791 
   792 instance proof
   793 qed (simp_all add: le_fun_def)
   794 
   795 end
   796 
   797 instantiation "fun" :: (type, semilattice_inf) semilattice_inf
   798 begin
   799 
   800 definition
   801   "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   802 
   803 lemma inf_apply [simp, code]:
   804   "(f \<sqinter> g) x = f x \<sqinter> g x"
   805   by (simp add: inf_fun_def)
   806 
   807 instance proof
   808 qed (simp_all add: le_fun_def)
   809 
   810 end
   811 
   812 instance "fun" :: (type, lattice) lattice ..
   813 
   814 instance "fun" :: (type, distrib_lattice) distrib_lattice proof
   815 qed (rule ext, simp add: sup_inf_distrib1)
   816 
   817 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
   818 
   819 instantiation "fun" :: (type, uminus) uminus
   820 begin
   821 
   822 definition
   823   fun_Compl_def: "- A = (\<lambda>x. - A x)"
   824 
   825 lemma uminus_apply [simp, code]:
   826   "(- A) x = - (A x)"
   827   by (simp add: fun_Compl_def)
   828 
   829 instance ..
   830 
   831 end
   832 
   833 instantiation "fun" :: (type, minus) minus
   834 begin
   835 
   836 definition
   837   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   838 
   839 lemma minus_apply [simp, code]:
   840   "(A - B) x = A x - B x"
   841   by (simp add: fun_diff_def)
   842 
   843 instance ..
   844 
   845 end
   846 
   847 instance "fun" :: (type, boolean_algebra) boolean_algebra proof
   848 qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
   849 
   850 
   851 subsection {* Lattice on unary and binary predicates *}
   852 
   853 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   854   by (simp add: inf_fun_def)
   855 
   856 lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
   857   by (simp add: inf_fun_def)
   858 
   859 lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
   860   by (simp add: inf_fun_def)
   861 
   862 lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
   863   by (simp add: inf_fun_def)
   864 
   865 lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
   866   by (simp add: inf_fun_def)
   867 
   868 lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
   869   by (simp add: inf_fun_def)
   870 
   871 lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   872   by (simp add: inf_fun_def)
   873 
   874 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   875   by (simp add: inf_fun_def)
   876 
   877 lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
   878   by (simp add: sup_fun_def)
   879 
   880 lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   881   by (simp add: sup_fun_def)
   882 
   883 lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
   884   by (simp add: sup_fun_def)
   885 
   886 lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   887   by (simp add: sup_fun_def)
   888 
   889 lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   890   by (simp add: sup_fun_def) iprover
   891 
   892 lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   893   by (simp add: sup_fun_def) iprover
   894 
   895 text {*
   896   \medskip Classical introduction rule: no commitment to @{text A} vs
   897   @{text B}.
   898 *}
   899 
   900 lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   901   by (auto simp add: sup_fun_def)
   902 
   903 lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   904   by (auto simp add: sup_fun_def)
   905 
   906 
   907 no_notation
   908   less_eq (infix "\<sqsubseteq>" 50) and
   909   less (infix "\<sqsubset>" 50)
   910 
   911 end
   912