src/HOL/Lattices.thy
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 51593 d40aec502416
child 52152 b561cdce6c4c
permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
     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   + inf_top!: semilattice_neutr_order inf top less_eq less
   475 proof
   476   fix x
   477   show "x \<sqinter> \<top> = x"
   478     by (rule inf_absorb1) simp
   479 qed
   480 
   481 class bounded_semilattice_sup_bot = semilattice_sup + bot
   482 
   483 sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
   484   + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
   485 proof
   486   fix x
   487   show "x \<squnion> \<bottom> = x"
   488     by (rule sup_absorb1) simp
   489 qed
   490 
   491 class bounded_lattice_bot = lattice + bot
   492 begin
   493 
   494 subclass bounded_semilattice_sup_bot ..
   495 
   496 lemma inf_bot_left [simp]:
   497   "\<bottom> \<sqinter> x = \<bottom>"
   498   by (rule inf_absorb1) simp
   499 
   500 lemma inf_bot_right [simp]:
   501   "x \<sqinter> \<bottom> = \<bottom>"
   502   by (rule inf_absorb2) simp
   503 
   504 lemma sup_bot_left:
   505   "\<bottom> \<squnion> x = x"
   506   by (fact sup_bot.left_neutral)
   507 
   508 lemma sup_bot_right:
   509   "x \<squnion> \<bottom> = x"
   510   by (fact sup_bot.right_neutral)
   511 
   512 lemma sup_eq_bot_iff [simp]:
   513   "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   514   by (simp add: eq_iff)
   515 
   516 lemma bot_eq_sup_iff [simp]:
   517   "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   518   by (simp add: eq_iff)
   519 
   520 end
   521 
   522 class bounded_lattice_top = lattice + top
   523 begin
   524 
   525 subclass bounded_semilattice_inf_top ..
   526 
   527 lemma sup_top_left [simp]:
   528   "\<top> \<squnion> x = \<top>"
   529   by (rule sup_absorb1) simp
   530 
   531 lemma sup_top_right [simp]:
   532   "x \<squnion> \<top> = \<top>"
   533   by (rule sup_absorb2) simp
   534 
   535 lemma inf_top_left:
   536   "\<top> \<sqinter> x = x"
   537   by (fact inf_top.left_neutral)
   538 
   539 lemma inf_top_right:
   540   "x \<sqinter> \<top> = x"
   541   by (fact inf_top.right_neutral)
   542 
   543 lemma inf_eq_top_iff [simp]:
   544   "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   545   by (simp add: eq_iff)
   546 
   547 end
   548 
   549 class bounded_lattice = lattice + bot + top
   550 begin
   551 
   552 subclass bounded_lattice_bot ..
   553 subclass bounded_lattice_top ..
   554 
   555 lemma dual_bounded_lattice:
   556   "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   557   by unfold_locales (auto simp add: less_le_not_le)
   558 
   559 end
   560 
   561 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
   562   assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
   563     and sup_compl_top: "x \<squnion> - x = \<top>"
   564   assumes diff_eq: "x - y = x \<sqinter> - y"
   565 begin
   566 
   567 lemma dual_boolean_algebra:
   568   "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
   569   by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
   570     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
   571 
   572 lemma compl_inf_bot [simp]:
   573   "- x \<sqinter> x = \<bottom>"
   574   by (simp add: inf_commute inf_compl_bot)
   575 
   576 lemma compl_sup_top [simp]:
   577   "- x \<squnion> x = \<top>"
   578   by (simp add: sup_commute sup_compl_top)
   579 
   580 lemma compl_unique:
   581   assumes "x \<sqinter> y = \<bottom>"
   582     and "x \<squnion> y = \<top>"
   583   shows "- x = y"
   584 proof -
   585   have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
   586     using inf_compl_bot assms(1) by simp
   587   then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
   588     by (simp add: inf_commute)
   589   then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
   590     by (simp add: inf_sup_distrib1)
   591   then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
   592     using sup_compl_top assms(2) by simp
   593   then show "- x = y" by simp
   594 qed
   595 
   596 lemma double_compl [simp]:
   597   "- (- x) = x"
   598   using compl_inf_bot compl_sup_top by (rule compl_unique)
   599 
   600 lemma compl_eq_compl_iff [simp]:
   601   "- x = - y \<longleftrightarrow> x = y"
   602 proof
   603   assume "- x = - y"
   604   then have "- (- x) = - (- y)" by (rule arg_cong)
   605   then show "x = y" by simp
   606 next
   607   assume "x = y"
   608   then show "- x = - y" by simp
   609 qed
   610 
   611 lemma compl_bot_eq [simp]:
   612   "- \<bottom> = \<top>"
   613 proof -
   614   from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   615   then show ?thesis by simp
   616 qed
   617 
   618 lemma compl_top_eq [simp]:
   619   "- \<top> = \<bottom>"
   620 proof -
   621   from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   622   then show ?thesis by simp
   623 qed
   624 
   625 lemma compl_inf [simp]:
   626   "- (x \<sqinter> y) = - x \<squnion> - y"
   627 proof (rule compl_unique)
   628   have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   629     by (simp only: inf_sup_distrib inf_aci)
   630   then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
   631     by (simp add: inf_compl_bot)
   632 next
   633   have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   634     by (simp only: sup_inf_distrib sup_aci)
   635   then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
   636     by (simp add: sup_compl_top)
   637 qed
   638 
   639 lemma compl_sup [simp]:
   640   "- (x \<squnion> y) = - x \<sqinter> - y"
   641   using dual_boolean_algebra
   642   by (rule boolean_algebra.compl_inf)
   643 
   644 lemma compl_mono:
   645   "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
   646 proof -
   647   assume "x \<sqsubseteq> y"
   648   then have "x \<squnion> y = y" by (simp only: le_iff_sup)
   649   then have "- (x \<squnion> y) = - y" by simp
   650   then have "- x \<sqinter> - y = - y" by simp
   651   then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
   652   then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
   653 qed
   654 
   655 lemma compl_le_compl_iff [simp]:
   656   "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   657   by (auto dest: compl_mono)
   658 
   659 lemma compl_le_swap1:
   660   assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
   661 proof -
   662   from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
   663   then show ?thesis by simp
   664 qed
   665 
   666 lemma compl_le_swap2:
   667   assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
   668 proof -
   669   from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
   670   then show ?thesis by simp
   671 qed
   672 
   673 lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
   674   "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
   675   by (auto simp add: less_le)
   676 
   677 lemma compl_less_swap1:
   678   assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
   679 proof -
   680   from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
   681   then show ?thesis by simp
   682 qed
   683 
   684 lemma compl_less_swap2:
   685   assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
   686 proof -
   687   from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
   688   then show ?thesis by simp
   689 qed
   690 
   691 end
   692 
   693 
   694 subsection {* @{text "min/max"} as special case of lattice *}
   695 
   696 sublocale linorder < min!: semilattice_order min less_eq less
   697   + max!: semilattice_order max greater_eq greater
   698   by default (auto simp add: min_def max_def)
   699 
   700 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   701   by (auto intro: antisym simp add: min_def fun_eq_iff)
   702 
   703 lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   704   by (auto intro: antisym simp add: max_def fun_eq_iff)
   705 
   706 
   707 subsection {* Uniqueness of inf and sup *}
   708 
   709 lemma (in semilattice_inf) inf_unique:
   710   fixes f (infixl "\<triangle>" 70)
   711   assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   712   and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   713   shows "x \<sqinter> y = x \<triangle> y"
   714 proof (rule antisym)
   715   show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   716 next
   717   have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
   718   show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   719 qed
   720 
   721 lemma (in semilattice_sup) sup_unique:
   722   fixes f (infixl "\<nabla>" 70)
   723   assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   724   and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   725   shows "x \<squnion> y = x \<nabla> y"
   726 proof (rule antisym)
   727   show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   728 next
   729   have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   730   show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   731 qed
   732 
   733 
   734 subsection {* Lattice on @{typ bool} *}
   735 
   736 instantiation bool :: boolean_algebra
   737 begin
   738 
   739 definition
   740   bool_Compl_def [simp]: "uminus = Not"
   741 
   742 definition
   743   bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
   744 
   745 definition
   746   [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   747 
   748 definition
   749   [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   750 
   751 instance proof
   752 qed auto
   753 
   754 end
   755 
   756 lemma sup_boolI1:
   757   "P \<Longrightarrow> P \<squnion> Q"
   758   by simp
   759 
   760 lemma sup_boolI2:
   761   "Q \<Longrightarrow> P \<squnion> Q"
   762   by simp
   763 
   764 lemma sup_boolE:
   765   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   766   by auto
   767 
   768 
   769 subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
   770 
   771 instantiation "fun" :: (type, semilattice_sup) semilattice_sup
   772 begin
   773 
   774 definition
   775   "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   776 
   777 lemma sup_apply [simp, code]:
   778   "(f \<squnion> g) x = f x \<squnion> g x"
   779   by (simp add: sup_fun_def)
   780 
   781 instance proof
   782 qed (simp_all add: le_fun_def)
   783 
   784 end
   785 
   786 instantiation "fun" :: (type, semilattice_inf) semilattice_inf
   787 begin
   788 
   789 definition
   790   "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   791 
   792 lemma inf_apply [simp, code]:
   793   "(f \<sqinter> g) x = f x \<sqinter> g x"
   794   by (simp add: inf_fun_def)
   795 
   796 instance proof
   797 qed (simp_all add: le_fun_def)
   798 
   799 end
   800 
   801 instance "fun" :: (type, lattice) lattice ..
   802 
   803 instance "fun" :: (type, distrib_lattice) distrib_lattice proof
   804 qed (rule ext, simp add: sup_inf_distrib1)
   805 
   806 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
   807 
   808 instantiation "fun" :: (type, uminus) uminus
   809 begin
   810 
   811 definition
   812   fun_Compl_def: "- A = (\<lambda>x. - A x)"
   813 
   814 lemma uminus_apply [simp, code]:
   815   "(- A) x = - (A x)"
   816   by (simp add: fun_Compl_def)
   817 
   818 instance ..
   819 
   820 end
   821 
   822 instantiation "fun" :: (type, minus) minus
   823 begin
   824 
   825 definition
   826   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   827 
   828 lemma minus_apply [simp, code]:
   829   "(A - B) x = A x - B x"
   830   by (simp add: fun_diff_def)
   831 
   832 instance ..
   833 
   834 end
   835 
   836 instance "fun" :: (type, boolean_algebra) boolean_algebra proof
   837 qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
   838 
   839 
   840 subsection {* Lattice on unary and binary predicates *}
   841 
   842 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   843   by (simp add: inf_fun_def)
   844 
   845 lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
   846   by (simp add: inf_fun_def)
   847 
   848 lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
   849   by (simp add: inf_fun_def)
   850 
   851 lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
   852   by (simp add: inf_fun_def)
   853 
   854 lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
   855   by (simp add: inf_fun_def)
   856 
   857 lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
   858   by (simp add: inf_fun_def)
   859 
   860 lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   861   by (simp add: inf_fun_def)
   862 
   863 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   864   by (simp add: inf_fun_def)
   865 
   866 lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
   867   by (simp add: sup_fun_def)
   868 
   869 lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   870   by (simp add: sup_fun_def)
   871 
   872 lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
   873   by (simp add: sup_fun_def)
   874 
   875 lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   876   by (simp add: sup_fun_def)
   877 
   878 lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   879   by (simp add: sup_fun_def) iprover
   880 
   881 lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   882   by (simp add: sup_fun_def) iprover
   883 
   884 text {*
   885   \medskip Classical introduction rule: no commitment to @{text A} vs
   886   @{text B}.
   887 *}
   888 
   889 lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   890   by (auto simp add: sup_fun_def)
   891 
   892 lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   893   by (auto simp add: sup_fun_def)
   894 
   895 
   896 no_notation
   897   less_eq (infix "\<sqsubseteq>" 50) and
   898   less (infix "\<sqsubset>" 50)
   899 
   900 end
   901