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