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