(* Title: HOL/Boolean_Algebras.thy
Author: Brian Huffman
Author: Florian Haftmann
*)
section ‹Boolean Algebras
›
theory Boolean_Algebras
imports Lattices
begin
subsection ‹Abstract boolean algebra
›
locale abstract_boolean_algebra = conj: abel_semigroup
‹(
🚫⊓)
› + disj: abel_semigroup
‹(
??⊔)
›
for conj ::
‹'a \ 'a
==> 'a\ (infixr \\<^bold>\\ 70)
and disj ::
‹'a \ 'a
==> 'a\ (infixr \\<^bold>\\ 65) +
fixes compl ::
‹'a \ 'a
› (
‹(
‹open_block
notation=
‹prefix
🚫-
››🚫- _)
› [81] 80)
and zero ::
‹'a\ (\\<^bold>0\)
and one ::
‹'a\ (\\<^bold>1\)
assumes conj_disj_distrib:
‹x
🚫⊓ (y
🚫⊔ z) = (x
🚫⊓ y)
🚫⊔ (x
🚫⊓ z)
›
and disj_conj_distrib:
‹x
🚫⊔ (y
🚫⊓ z) = (x
🚫⊔ y)
🚫⊓ (x
🚫⊔ z)
›
and conj_one_right:
‹x
🚫⊓ 🚫1 = x
›
and disj_zero_right:
‹x
🚫⊔ 🚫0 = x
›
and conj_cancel_right [simp]:
‹x
🚫⊓ 🚫- x =
🚫0
›
and disj_cancel_right [simp]:
‹x
🚫⊔ 🚫- x =
🚫1
›
begin
sublocale conj: semilattice_neutr
‹(
🚫⊓)
› ‹🚫1
›
proof
show "x \<^bold>\ \<^bold>1 = x" for x
by (fact conj_one_right)
show "x \<^bold>\ x = x" for x
proof -
have "x \<^bold>\ x = (x \<^bold>\ x) \<^bold>\ \<^bold>0"
by (simp add: disj_zero_right)
also have "\ = (x \<^bold>\ x) \<^bold>\ (x \<^bold>\ \<^bold>- x)"
by simp
also have "\ = x \<^bold>\ (x \<^bold>\ \<^bold>- x)"
by (simp only: conj_disj_distrib)
also have "\ = x \<^bold>\ \<^bold>1"
by simp
also have "\ = x"
by (simp add: conj_one_right)
finally show ?thesis .
qed
qed
sublocale disj: semilattice_neutr
‹(
🚫⊔)
› ‹🚫0
›
proof
show "x \<^bold>\ \<^bold>0 = x" for x
by (fact disj_zero_right)
show "x \<^bold>\ x = x" for x
proof -
have "x \<^bold>\ x = (x \<^bold>\ x) \<^bold>\ \<^bold>1"
by simp
also have "\ = (x \<^bold>\ x) \<^bold>\ (x \<^bold>\ \<^bold>- x)"
by simp
also have "\ = x \<^bold>\ (x \<^bold>\ \<^bold>- x)"
by (simp only: disj_conj_distrib)
also have "\ = x \<^bold>\ \<^bold>0"
by simp
also have "\ = x"
by (simp add: disj_zero_right)
finally show ?thesis .
qed
qed
subsubsection
‹Complement
›
lemma complement_unique:
assumes 1:
"a \<^bold>\ x = \<^bold>0"
assumes 2:
"a \<^bold>\ x = \<^bold>1"
assumes 3:
"a \<^bold>\ y = \<^bold>0"
assumes 4:
"a \<^bold>\ y = \<^bold>1"
shows "x = y"
proof -
from 1 3
have "(a \<^bold>\ x) \<^bold>\ (x \<^bold>\ y) = (a \<^bold>\ y) \<^bold>\ (x \<^bold>\ y)"
by simp
then have "(x \<^bold>\ a) \<^bold>\ (x \<^bold>\ y) = (y \<^bold>\ a) \<^bold>\ (y \<^bold>\ x)"
by (simp add: ac_simps)
then have "x \<^bold>\ (a \<^bold>\ y) = y \<^bold>\ (a \<^bold>\ x)"
by (simp add: conj_disj_distrib)
with 2 4
have "x \<^bold>\ \<^bold>1 = y \<^bold>\ \<^bold>1"
by simp
then show "x = y"
by simp
qed
lemma compl_unique:
"x \<^bold>\ y = \<^bold>0 \ x \<^bold>\ y = \<^bold>1 \ \<^bold>- x = y"
by (rule complement_unique [OF conj_cancel_right disj_cancel_right])
lemma double_compl [simp]:
"\<^bold>- (\<^bold>- x) = x"
proof (rule compl_unique)
show "\<^bold>- x \<^bold>\ x = \<^bold>0"
by (simp only: conj_cancel_right conj.commute)
show "\<^bold>- x \<^bold>\ x = \<^bold>1"
by (simp only: disj_cancel_right disj.commute)
qed
lemma compl_eq_compl_iff [simp]:
‹🚫- x =
🚫- y
⟷ x = y
› (
is ‹?P
⟷ ?Q
›)
proof
assume ‹?Q
›
then show ?P
by simp
next
assume ‹?P
›
then have ‹🚫- (
🚫- x) =
🚫- (
🚫- y)
›
by simp
then show ?Q
by simp
qed
subsubsection
‹Conjunction
›
lemma conj_zero_right [simp]:
"x \<^bold>\ \<^bold>0 = \<^bold>0"
using conj.left_idem conj_cancel_right
by fastforce
lemma compl_one [simp]:
"\<^bold>- \<^bold>1 = \<^bold>0"
by (rule compl_unique [OF conj_zero_right disj_zero_right])
lemma conj_zero_left [simp]:
"\<^bold>0 \<^bold>\ x = \<^bold>0"
by (subst conj.commute) (rule conj_zero_right)
lemma conj_cancel_left [simp]:
"\<^bold>- x \<^bold>\ x = \<^bold>0"
by (subst conj.commute) (rule conj_cancel_right)
lemma conj_disj_distrib2:
"(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)"
by (simp only: conj.commute conj_disj_distrib)
lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2
subsubsection
‹Disjunction
›
context
begin
interpretation dual: abstract_boolean_algebra
‹(
🚫⊔)
› ‹(
🚫⊓)
› compl
‹🚫1
› ‹🚫0
›
apply standard
apply (rule disj_conj_distrib)
apply (rule conj_disj_distrib)
apply simp_all
done
lemma disj_one_right [simp]:
"x \<^bold>\ \<^bold>1 = \<^bold>1"
by (fact dual.conj_zero_right)
lemma compl_zero [simp]:
"\<^bold>- \<^bold>0 = \<^bold>1"
by (fact dual.compl_one)
lemma disj_one_left [simp]:
"\<^bold>1 \<^bold>\ x = \<^bold>1"
by (fact dual.conj_zero_left)
lemma disj_cancel_left [simp]:
"\<^bold>- x \<^bold>\ x = \<^bold>1"
by (fact dual.conj_cancel_left)
lemma disj_conj_distrib2:
"(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)"
by (fact dual.conj_disj_distrib2)
lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2
end
subsubsection
‹De Morgan
's Laws\
lemma de_Morgan_conj [simp]:
"\<^bold>- (x \<^bold>\ y) = \<^bold>- x \<^bold>\ \<^bold>- y"
proof (rule compl_unique)
have "(x \<^bold>\ y) \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y) = ((x \<^bold>\ y) \<^bold>\ \<^bold>- x) \<^bold>\ ((x \<^bold>\ y) \<^bold>\ \<^bold>- y)"
by (rule conj_disj_distrib)
also have "\ = (y \<^bold>\ (x \<^bold>\ \<^bold>- x)) \<^bold>\ (x \<^bold>\ (y \<^bold>\ \<^bold>- y))"
by (simp only: ac_simps)
finally show "(x \<^bold>\ y) \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y) = \<^bold>0"
by (simp only: conj_cancel_right conj_zero_right disj_zero_right)
next
have "(x \<^bold>\ y) \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y) = (x \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y)) \<^bold>\ (y \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y))"
by (rule disj_conj_distrib2)
also have "\ = (\<^bold>- y \<^bold>\ (x \<^bold>\ \<^bold>- x)) \<^bold>\ (\<^bold>- x \<^bold>\ (y \<^bold>\ \<^bold>- y))"
by (simp only: ac_simps)
finally show "(x \<^bold>\ y) \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y) = \<^bold>1"
by (simp only: disj_cancel_right disj_one_right conj_one_right)
qed
context
begin
interpretation dual: abstract_boolean_algebra
‹(
🚫⊔)
› ‹(
🚫⊓)
› compl
‹🚫1
› ‹🚫0
›
apply standard
apply (rule disj_conj_distrib)
apply (rule conj_disj_distrib)
apply simp_all
done
lemma de_Morgan_disj [simp]:
"\<^bold>- (x \<^bold>\ y) = \<^bold>- x \<^bold>\ \<^bold>- y"
by (fact dual.de_Morgan_conj)
end
end
subsection ‹Symmetric Difference
›
locale abstract_boolean_algebra_sym_diff = abstract_boolean_algebra +
fixes xor ::
‹'a \ 'a
==> 'a\ (infixr \\<^bold>\\ 65)
assumes xor_def :
‹x
🚫⊖ y = (x
🚫⊓ 🚫- y)
🚫⊔ (
🚫- x
🚫⊓ y)
›
begin
sublocale xor: comm_monoid xor
‹🚫0
›
proof
fix x y z ::
'a
let ?t =
"(x \<^bold>\ y \<^bold>\ z) \<^bold>\ (x \<^bold>\ \<^bold>- y \<^bold>\ \<^bold>- z) \<^bold>\ (\<^bold>- x \<^bold>\ y \<^bold>\ \<^bold>- z) \<^bold>\ (\<^bold>- x \<^bold>\ \<^bold>- y \<^bold>\ z)"
have "?t \<^bold>\ (z \<^bold>\ x \<^bold>\ \<^bold>- x) \<^bold>\ (z \<^bold>\ y \<^bold>\ \<^bold>- y) = ?t \<^bold>\ (x \<^bold>\ y \<^bold>\ \<^bold>- y) \<^bold>\ (x \<^bold>\ z \<^bold>\ \<^bold>- z)"
by (simp only: conj_cancel_right conj_zero_right)
then show "(x \<^bold>\ y) \<^bold>\ z = x \<^bold>\ (y \<^bold>\ z)"
by (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
(simp only: conj_disj_distribs conj_ac ac_simps)
show "x \<^bold>\ y = y \<^bold>\ x"
by (simp only: xor_def ac_simps)
show "x \<^bold>\ \<^bold>0 = x"
by (simp add: xor_def)
qed
lemma xor_def2:
‹x
🚫⊖ y = (x
🚫⊔ y)
🚫⊓ (
🚫- x
🚫⊔ 🚫- y)
›
proof -
note xor_def [of x y]
also have ‹x
🚫⊓ 🚫- y
🚫⊔ 🚫- x
🚫⊓ y = ((x
🚫⊔ 🚫- x)
🚫⊓ (
🚫- y
🚫⊔ 🚫- x))
🚫⊓ (x
🚫⊔ y)
🚫⊓ (
🚫- y
🚫⊔ y)
›
by (simp add: ac_simps disj_conj_distribs)
also have ‹… = (x
🚫⊔ y)
🚫⊓ (
🚫- x
🚫⊔ 🚫- y)
›
by (simp add: ac_simps)
finally show ?thesis .
qed
lemma xor_one_right [simp]:
"x \<^bold>\ \<^bold>1 = \<^bold>- x"
by (simp only: xor_def compl_one conj_zero_right conj_one_right disj.left_neutral)
lemma xor_one_left [simp]:
"\<^bold>1 \<^bold>\ x = \<^bold>- x"
using xor_one_right [of x]
by (simp add: ac_simps)
lemma xor_self [simp]:
"x \<^bold>\ x = \<^bold>0"
by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
lemma xor_left_self [simp]:
"x \<^bold>\ (x \<^bold>\ y) = y"
by (simp only: xor.assoc [symmetric] xor_self xor.left_neutral)
lemma xor_compl_left [simp]:
"\<^bold>- x \<^bold>\ y = \<^bold>- (x \<^bold>\ y)"
by (simp add: ac_simps flip: xor_one_left)
lemma xor_compl_right [simp]:
"x \<^bold>\ \<^bold>- y = \<^bold>- (x \<^bold>\ y)"
using xor.commute xor_compl_left
by auto
lemma xor_cancel_right [simp]:
"x \<^bold>\ \<^bold>- x = \<^bold>1"
by (simp only: xor_compl_right xor_self compl_zero)
lemma xor_cancel_left [simp]:
"\<^bold>- x \<^bold>\ x = \<^bold>1"
by (simp only: xor_compl_left xor_self compl_zero)
lemma conj_xor_distrib:
"x \<^bold>\ (y \<^bold>\ z) = (x \<^bold>\ y) \<^bold>\ (x \<^bold>\ z)"
proof -
have *:
"(x \<^bold>\ y \<^bold>\ \<^bold>- z) \<^bold>\ (x \<^bold>\ \<^bold>- y \<^bold>\ z) =
(y
🚫⊓ x
🚫⊓ 🚫- x)
🚫⊔ (z
🚫⊓ x
🚫⊓ 🚫- x)
🚫⊔ (x
🚫⊓ y
🚫⊓ 🚫- z)
🚫⊔ (x
🚫⊓ 🚫- y
🚫⊓ z)
"
by (simp only: conj_cancel_right conj_zero_right disj.left_neutral)
then show "x \<^bold>\ (y \<^bold>\ z) = (x \<^bold>\ y) \<^bold>\ (x \<^bold>\ z)"
by (simp (no_asm_use) only:
xor_def de_Morgan_disj de_Morgan_conj double_compl
conj_disj_distribs ac_simps)
qed
lemma conj_xor_distrib2:
"(y \<^bold>\ z) \<^bold>\ x = (y \<^bold>\ x) \<^bold>\ (z \<^bold>\ x)"
by (simp add: conj.commute conj_xor_distrib)
lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2
end
subsection ‹Type
classes›
class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
assumes inf_compl_bot:
‹x
⊓ - x =
⊥›
and sup_compl_top:
‹x
⊔ - x =
⊤›
assumes diff_eq:
‹x - y = x
⊓ - y
›
begin
sublocale boolean_algebra: abstract_boolean_algebra
‹(
⊓)
› ‹(
⊔)
› uminus
⊥ ⊤
apply standard
apply (rule inf_sup_distrib1)
apply (rule sup_inf_distrib1)
apply (simp_all add: ac_simps inf_compl_bot sup_compl_top)
done
lemma compl_inf_bot:
"- x \ x = \"
by (fact boolean_algebra.conj_cancel_left)
lemma compl_sup_top:
"- x \ x = \"
by (fact boolean_algebra.disj_cancel_left)
lemma compl_unique:
assumes "x \ y = \"
and "x \ y = \"
shows "- x = y"
using assms
by (rule boolean_algebra.compl_unique)
lemma double_compl:
"- (- x) = x"
by (fact boolean_algebra.double_compl)
lemma compl_eq_compl_iff:
"- x = - y \ x = y"
by (fact boolean_algebra.compl_eq_compl_iff)
lemma compl_bot_eq:
"- \ = \"
by (fact boolean_algebra.compl_zero)
lemma compl_top_eq:
"- \ = \"
by (fact boolean_algebra.compl_one)
lemma compl_inf:
"- (x \ y) = - x \ - y"
by (fact boolean_algebra.de_Morgan_conj)
lemma compl_sup:
"- (x \ y) = - x \ - y"
by (fact boolean_algebra.de_Morgan_disj)
lemma compl_mono:
assumes "x \ y"
shows "- y \ - x"
proof -
from assms
have "x \ y = y" by (simp only: le_iff_sup)
then have "- (x \ y) = - y" by simp
then have "- x \ - y = - y" by simp
then have "- y \ - x = - y" by (simp only: inf_commute)
then show ?thesis
by (simp only: le_iff_inf)
qed
lemma compl_le_compl_iff [simp]:
"- x \ - y \ y \ x"
by (auto dest: compl_mono)
lemma compl_le_swap1:
assumes "y \ - x"
shows "x \ -y"
proof -
from assms
have "- (- x) \ - y" by (simp only: compl_le_compl_iff)
then show ?thesis
by simp
qed
lemma compl_le_swap2:
assumes "- y \ x"
shows "- x \ y"
proof -
from assms
have "- x \ - (- y)" by (simp only: compl_le_compl_iff)
then show ?thesis
by simp
qed
lemma compl_less_compl_iff [simp]:
"- x < - y \ y < x"
by (auto simp add: less_le)
lemma compl_less_swap1:
assumes "y < - x"
shows "x < - y"
proof -
from assms
have "- (- x) < - y" by (simp only: compl_less_compl_iff)
then show ?thesis
by simp
qed
lemma compl_less_swap2:
assumes "- y < x"
shows "- x < y"
proof -
from assms
have "- x < - (- y)"
by (simp only: compl_less_compl_iff)
then show ?thesis
by simp
qed
lemma sup_cancel_left1:
‹x
⊔ a
⊔ (- x
⊔ b) =
⊤›
by (simp add: ac_simps)
lemma sup_cancel_left2:
‹- x
⊔ a
⊔ (x
⊔ b) =
⊤›
by (simp add: ac_simps)
lemma inf_cancel_left1:
‹x
⊓ a
⊓ (- x
⊓ b) =
⊥›
by (simp add: ac_simps)
lemma inf_cancel_left2:
‹- x
⊓ a
⊓ (x
⊓ b) =
⊥›
by (simp add: ac_simps)
lemma sup_compl_top_left1 [simp]:
‹- x
⊔ (x
⊔ y) =
⊤›
by (simp add: sup_assoc [symmetric])
lemma sup_compl_top_left2 [simp]:
‹x
⊔ (- x
⊔ y) =
⊤›
using sup_compl_top_left1 [of
"- x" y]
by simp
lemma inf_compl_bot_left1 [simp]:
‹- x
⊓ (x
⊓ y) =
⊥›
by (simp add: inf_assoc [symmetric])
lemma inf_compl_bot_left2 [simp]:
‹x
⊓ (- x
⊓ y) =
⊥›
using inf_compl_bot_left1 [of
"- x" y]
by simp
lemma inf_compl_bot_right [simp]:
‹x
⊓ (y
⊓ - x) =
⊥›
by (subst inf_left_commute) simp
end
subsection ‹Lattice on
🍋‹bool
››
instantiation bool :: boolean_algebra
begin
definition bool_Compl_def [simp]:
"uminus = Not"
definition bool_diff_def [simp]:
"A - B \ A \ \ B"
definition [simp]:
"P \ Q \ P \ Q"
definition [simp]:
"P \ Q \ P \ Q"
instance by standard auto
end
lemma sup_boolI1:
"P \ P \ Q"
by simp
lemma sup_boolI2:
"Q \ P \ Q"
by simp
lemma sup_boolE:
"P \ Q \ (P \ R) \ (Q \ R) \ R"
by auto
instance "fun" :: (type, boolean_algebra) boolean_algebra
by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
subsection ‹Lattice on unary
and binary predicates
›
lemma inf1I:
"A x \ B x \ (A \ B) x"
by (simp add: inf_fun_def)
lemma inf2I:
"A x y \ B x y \ (A \ B) x y"
by (simp add: inf_fun_def)
lemma inf1E:
"(A \ B) x \ (A x \ B x \ P) \ P"
by (simp add: inf_fun_def)
lemma inf2E:
"(A \ B) x y \ (A x y \ B x y \ P) \ P"
by (simp add: inf_fun_def)
lemma inf1D1:
"(A \ B) x \ A x"
by (rule inf1E)
lemma inf2D1:
"(A \ B) x y \ A x y"
by (rule inf2E)
lemma inf1D2:
"(A \ B) x \ B x"
by (rule inf1E)
lemma inf2D2:
"(A \ B) x y \ B x y"
by (rule inf2E)
lemma sup1I1:
"A x \ (A \ B) x"
by (simp add: sup_fun_def)
lemma sup2I1:
"A x y \ (A \ B) x y"
by (simp add: sup_fun_def)
lemma sup1I2:
"B x \ (A \ B) x"
by (simp add: sup_fun_def)
lemma sup2I2:
"B x y \ (A \ B) x y"
by (simp add: sup_fun_def)
lemma sup1E:
"(A \ B) x \ (A x \ P) \ (B x \ P) \ P"
by (simp add: sup_fun_def) iprover
lemma sup2E:
"(A \ B) x y \ (A x y \ P) \ (B x y \ P) \ P"
by (simp add: sup_fun_def) iprover
text ‹ 🚫 Classical introduction rule: no commitment
to ‹A
› vs
‹B
›.
›
lemma sup1CI:
"(\ B x \ A x) \ (A \ B) x"
by (auto simp add: sup_fun_def)
lemma sup2CI:
"(\ B x y \ A x y) \ (A \ B) x y"
by (auto simp add: sup_fun_def)
subsection ‹Simproc
setup›
locale boolean_algebra_cancel
begin
lemma sup1:
"(A::'a::semilattice_sup) \ sup k a \ sup A b \ sup k (sup a b)"
by (simp only: ac_simps)
lemma sup2:
"(B::'a::semilattice_sup) \ sup k b \ sup a B \ sup k (sup a b)"
by (simp only: ac_simps)
lemma sup0:
"(a::'a::bounded_semilattice_sup_bot) \ sup a bot"
by simp
lemma inf1:
"(A::'a::semilattice_inf) \ inf k a \ inf A b \ inf k (inf a b)"
by (simp only: ac_simps)
lemma inf2:
"(B::'a::semilattice_inf) \ inf k b \ inf a B \ inf k (inf a b)"
by (simp only: ac_simps)
lemma inf0:
"(a::'a::bounded_semilattice_inf_top) \ inf a top"
by simp
end
ML_file
‹Tools/boolean_algebra_cancel.ML
›
simproc_setup boolean_algebra_cancel_sup (
"sup a b::'a::boolean_algebra") =
‹K (K (try Boolean_Algebra_Cancel.cancel_sup_conv))
›
simproc_setup boolean_algebra_cancel_inf (
"inf a b::'a::boolean_algebra") =
‹K (K (try Boolean_Algebra_Cancel.cancel_inf_conv))
›
context boolean_algebra
begin
lemma shunt1:
"(x \ y \ z) \ (x \ -y \ z)"
proof
assume "x \ y \ z"
hence "-y \ (x \ y) \ -y \ z"
using sup.mono
by blast
hence "-y \ x \ -y \ z"
by (simp add: sup_inf_distrib1)
thus "x \ -y \ z"
by simp
next
assume "x \ -y \ z"
hence "x \ y \ (-y \ z) \ y"
using inf_mono
by auto
thus "x \ y \ z"
using inf.boundedE inf_sup_distrib2
by auto
qed
lemma shunt2:
"(x \ -y \ z) \ (x \ y \ z)"
by (simp add: shunt1)
lemma inf_shunt:
"(x \ y = \) \ (x \ - y)"
by (simp add: order.eq_iff shunt1)
lemma sup_shunt:
"(x \ y = \) \ (- x \ y)"
using inf_shunt [of
‹- x
› ‹- y
›, symmetric]
by (simp flip: compl_sup compl_top_eq)
lemma diff_shunt_var[simp]:
"(x - y = \) \ (x \ y)"
by (simp add: diff_eq inf_shunt)
lemma diff_shunt[simp]:
"(\ = x - y) \ (x \ y)"
by (auto simp flip: diff_shunt_var)
lemma sup_neg_inf:
‹p
≤ q
⊔ r
⟷ p
⊓ -q
≤ r
› (
is ‹?P
⟷ ?Q
›)
proof
assume ?P
then have ‹p
⊓ - q
≤ (q
⊔ r)
⊓ - q
›
by (rule inf_mono) simp
then show ?Q
by (simp add: inf_sup_distrib2)
next
assume ?Q
then have ‹p
⊓ - q
⊔ q
≤ r
⊔ q
›
by (rule sup_mono) simp
then show ?P
by (simp add: sup_inf_distrib ac_simps)
qed
end
end
