author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63462  c1fe30f2bc32 
child 65343  0a8e30a7b10e 
permissions  rwrr 
29629  1 
(* Title: HOL/Library/Boolean_Algebra.thy 
2 
Author: Brian Huffman 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

3 
*) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

4 

60500  5 
section \<open>Boolean Algebras\<close> 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

6 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

7 
theory Boolean_Algebra 
63462  8 
imports Main 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

9 
begin 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

10 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

11 
locale boolean = 
24357  12 
fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70) 
13 
fixes disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65) 

14 
fixes compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

15 
fixes zero :: "'a" ("\<zero>") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

16 
fixes one :: "'a" ("\<one>") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

17 
assumes conj_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

18 
assumes disj_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

19 
assumes conj_commute: "x \<sqinter> y = y \<sqinter> x" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

20 
assumes disj_commute: "x \<squnion> y = y \<squnion> x" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

21 
assumes conj_disj_distrib: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

22 
assumes disj_conj_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
24357  23 
assumes conj_one_right [simp]: "x \<sqinter> \<one> = x" 
24 
assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x" 

25 
assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>" 

26 
assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>" 

54868  27 
begin 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

28 

61605  29 
sublocale conj: abel_semigroup conj 
60855  30 
by standard (fact conj_assoc conj_commute)+ 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

31 

61605  32 
sublocale disj: abel_semigroup disj 
60855  33 
by standard (fact disj_assoc disj_commute)+ 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

34 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

35 
lemmas conj_left_commute = conj.left_commute 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

36 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

37 
lemmas disj_left_commute = disj.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

38 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

39 
lemmas conj_ac = conj.assoc conj.commute conj.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

40 
lemmas disj_ac = disj.assoc disj.commute disj.left_commute 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

41 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

42 
lemma dual: "boolean disj conj compl one zero" 
63462  43 
apply (rule boolean.intro) 
44 
apply (rule disj_assoc) 

45 
apply (rule conj_assoc) 

46 
apply (rule disj_commute) 

47 
apply (rule conj_commute) 

48 
apply (rule disj_conj_distrib) 

49 
apply (rule conj_disj_distrib) 

50 
apply (rule disj_zero_right) 

51 
apply (rule conj_one_right) 

52 
apply (rule disj_cancel_right) 

53 
apply (rule conj_cancel_right) 

54 
done 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

55 

60855  56 

60500  57 
subsection \<open>Complement\<close> 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

58 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

59 
lemma complement_unique: 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

60 
assumes 1: "a \<sqinter> x = \<zero>" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

61 
assumes 2: "a \<squnion> x = \<one>" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

62 
assumes 3: "a \<sqinter> y = \<zero>" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

63 
assumes 4: "a \<squnion> y = \<one>" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

64 
shows "x = y" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

65 
proof  
63462  66 
have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)" 
67 
using 1 3 by simp 

68 
then have "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)" 

69 
using conj_commute by simp 

70 
then have "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)" 

71 
using conj_disj_distrib by simp 

72 
then have "x \<sqinter> \<one> = y \<sqinter> \<one>" 

73 
using 2 4 by simp 

74 
then show "x = y" 

75 
using conj_one_right by simp 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

76 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

77 

63462  78 
lemma compl_unique: "x \<sqinter> y = \<zero> \<Longrightarrow> x \<squnion> y = \<one> \<Longrightarrow> \<sim> x = y" 
79 
by (rule complement_unique [OF conj_cancel_right disj_cancel_right]) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

80 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

81 
lemma double_compl [simp]: "\<sim> (\<sim> x) = x" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

82 
proof (rule compl_unique) 
63462  83 
from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>" 
84 
by (simp only: conj_commute) 

85 
from disj_cancel_right show "\<sim> x \<squnion> x = \<one>" 

86 
by (simp only: disj_commute) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

87 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

88 

63462  89 
lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y" 
90 
by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

91 

60855  92 

60500  93 
subsection \<open>Conjunction\<close> 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

94 

24393  95 
lemma conj_absorb [simp]: "x \<sqinter> x = x" 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

96 
proof  
63462  97 
have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" 
98 
using disj_zero_right by simp 

99 
also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" 

100 
using conj_cancel_right by simp 

101 
also have "... = x \<sqinter> (x \<squnion> \<sim> x)" 

102 
using conj_disj_distrib by (simp only:) 

103 
also have "... = x \<sqinter> \<one>" 

104 
using disj_cancel_right by simp 

105 
also have "... = x" 

106 
using conj_one_right by simp 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

107 
finally show ?thesis . 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

108 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

109 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

110 
lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

111 
proof  
63462  112 
have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" 
113 
using conj_cancel_right by simp 

114 
also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" 

115 
using conj_assoc by (simp only:) 

116 
also have "... = x \<sqinter> \<sim> x" 

117 
using conj_absorb by simp 

118 
also have "... = \<zero>" 

119 
using conj_cancel_right by simp 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

120 
finally show ?thesis . 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

121 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

122 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

123 
lemma compl_one [simp]: "\<sim> \<one> = \<zero>" 
63462  124 
by (rule compl_unique [OF conj_zero_right disj_zero_right]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

125 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

126 
lemma conj_zero_left [simp]: "\<zero> \<sqinter> x = \<zero>" 
63462  127 
by (subst conj_commute) (rule conj_zero_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

128 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

129 
lemma conj_one_left [simp]: "\<one> \<sqinter> x = x" 
63462  130 
by (subst conj_commute) (rule conj_one_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

131 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

132 
lemma conj_cancel_left [simp]: "\<sim> x \<sqinter> x = \<zero>" 
63462  133 
by (subst conj_commute) (rule conj_cancel_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

134 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

135 
lemma conj_left_absorb [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" 
63462  136 
by (simp only: conj_assoc [symmetric] conj_absorb) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

137 

63462  138 
lemma conj_disj_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
139 
by (simp only: conj_commute conj_disj_distrib) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

140 

63462  141 
lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

142 

60855  143 

60500  144 
subsection \<open>Disjunction\<close> 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

145 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

146 
lemma disj_absorb [simp]: "x \<squnion> x = x" 
63462  147 
by (rule boolean.conj_absorb [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

148 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

149 
lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>" 
63462  150 
by (rule boolean.conj_zero_right [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

151 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

152 
lemma compl_zero [simp]: "\<sim> \<zero> = \<one>" 
63462  153 
by (rule boolean.compl_one [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

154 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

155 
lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x" 
63462  156 
by (rule boolean.conj_one_left [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

157 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

158 
lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>" 
63462  159 
by (rule boolean.conj_zero_left [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

160 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

161 
lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>" 
63462  162 
by (rule boolean.conj_cancel_left [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

163 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

164 
lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" 
63462  165 
by (rule boolean.conj_left_absorb [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

166 

63462  167 
lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" 
168 
by (rule boolean.conj_disj_distrib2 [OF dual]) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

169 

63462  170 
lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

171 

60855  172 

60500  173 
subsection \<open>De Morgan's Laws\<close> 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

174 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

175 
lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

176 
proof (rule compl_unique) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

177 
have "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = ((x \<sqinter> y) \<sqinter> \<sim> x) \<squnion> ((x \<sqinter> y) \<sqinter> \<sim> y)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

178 
by (rule conj_disj_distrib) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

179 
also have "... = (y \<sqinter> (x \<sqinter> \<sim> x)) \<squnion> (x \<sqinter> (y \<sqinter> \<sim> y))" 
24357  180 
by (simp only: conj_ac) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

181 
finally show "(x \<sqinter> y) \<sqinter> (\<sim> x \<squnion> \<sim> y) = \<zero>" 
24357  182 
by (simp only: conj_cancel_right conj_zero_right disj_zero_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

183 
next 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

184 
have "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = (x \<squnion> (\<sim> x \<squnion> \<sim> y)) \<sqinter> (y \<squnion> (\<sim> x \<squnion> \<sim> y))" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

185 
by (rule disj_conj_distrib2) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

186 
also have "... = (\<sim> y \<squnion> (x \<squnion> \<sim> x)) \<sqinter> (\<sim> x \<squnion> (y \<squnion> \<sim> y))" 
24357  187 
by (simp only: disj_ac) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

188 
finally show "(x \<sqinter> y) \<squnion> (\<sim> x \<squnion> \<sim> y) = \<one>" 
24357  189 
by (simp only: disj_cancel_right disj_one_right conj_one_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

190 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

191 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

192 
lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y" 
63462  193 
by (rule boolean.de_Morgan_conj [OF dual]) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

194 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

195 
end 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

196 

60855  197 

60500  198 
subsection \<open>Symmetric Difference\<close> 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

199 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

200 
locale boolean_xor = boolean + 
60855  201 
fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<oplus>" 65) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

202 
assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)" 
54868  203 
begin 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

204 

61605  205 
sublocale xor: abel_semigroup xor 
60855  206 
proof 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

207 
fix x y z :: 'a 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

208 
let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion> 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

209 
(\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

210 
have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) = 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

211 
?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)" 
24357  212 
by (simp only: conj_cancel_right conj_zero_right) 
63462  213 
then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" 
24357  214 
apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) 
215 
apply (simp only: conj_disj_distribs conj_ac disj_ac) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

216 
done 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

217 
show "x \<oplus> y = y \<oplus> x" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

218 
by (simp only: xor_def conj_commute disj_commute) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

219 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

220 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

221 
lemmas xor_assoc = xor.assoc 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

222 
lemmas xor_commute = xor.commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

223 
lemmas xor_left_commute = xor.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

224 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

225 
lemmas xor_ac = xor.assoc xor.commute xor.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
30663
diff
changeset

226 

63462  227 
lemma xor_def2: "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)" 
228 
by (simp only: xor_def conj_disj_distribs disj_ac conj_ac conj_cancel_right disj_zero_left) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

229 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

230 
lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x" 
63462  231 
by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

232 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

233 
lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x" 
63462  234 
by (subst xor_commute) (rule xor_zero_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

235 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

236 
lemma xor_one_right [simp]: "x \<oplus> \<one> = \<sim> x" 
63462  237 
by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

238 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

239 
lemma xor_one_left [simp]: "\<one> \<oplus> x = \<sim> x" 
63462  240 
by (subst xor_commute) (rule xor_one_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

241 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

242 
lemma xor_self [simp]: "x \<oplus> x = \<zero>" 
63462  243 
by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

244 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

245 
lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y" 
63462  246 
by (simp only: xor_assoc [symmetric] xor_self xor_zero_left) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

247 

29996  248 
lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)" 
63462  249 
apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) 
250 
apply (simp only: conj_disj_distribs) 

251 
apply (simp only: conj_cancel_right conj_cancel_left) 

252 
apply (simp only: disj_zero_left disj_zero_right) 

253 
apply (simp only: disj_ac conj_ac) 

254 
done 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

255 

29996  256 
lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)" 
63462  257 
apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl) 
258 
apply (simp only: conj_disj_distribs) 

259 
apply (simp only: conj_cancel_right conj_cancel_left) 

260 
apply (simp only: disj_zero_left disj_zero_right) 

261 
apply (simp only: disj_ac conj_ac) 

262 
done 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

263 

29996  264 
lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>" 
63462  265 
by (simp only: xor_compl_right xor_self compl_zero) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

266 

29996  267 
lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>" 
63462  268 
by (simp only: xor_compl_left xor_self compl_zero) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

269 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

270 
lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

271 
proof  
63462  272 
have *: "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) = 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

273 
(y \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z)" 
24357  274 
by (simp only: conj_cancel_right conj_zero_right disj_zero_left) 
63462  275 
then show "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)" 
24357  276 
by (simp (no_asm_use) only: 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

277 
xor_def de_Morgan_disj de_Morgan_conj double_compl 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

278 
conj_disj_distribs conj_ac disj_ac) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

279 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

280 

60855  281 
lemma conj_xor_distrib2: "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)" 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

282 
proof  
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

283 
have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

284 
by (rule conj_xor_distrib) 
63462  285 
then show "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)" 
24357  286 
by (simp only: conj_commute) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

287 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

288 

60855  289 
lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

290 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

291 
end 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

292 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

293 
end 