--- a/src/HOL/Library/Boolean_Algebra.thy Sat Apr 20 13:44:16 2019 +0000
+++ b/src/HOL/Library/Boolean_Algebra.thy Sat Apr 20 18:02:20 2019 +0000
@@ -8,7 +8,7 @@
imports Main
begin
-locale boolean =
+locale boolean_algebra =
fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<sqinter>" 70)
and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<squnion>" 65)
and compl :: "'a \<Rightarrow> 'a" ("\<sim> _" [81] 80)
@@ -38,8 +38,8 @@
lemmas conj_ac = conj.assoc conj.commute conj.left_commute
lemmas disj_ac = disj.assoc disj.commute disj.left_commute
-lemma dual: "boolean disj conj compl one zero"
- apply (rule boolean.intro)
+lemma dual: "boolean_algebra disj conj compl one zero"
+ apply (rule boolean_algebra.intro)
apply (rule disj_assoc)
apply (rule conj_assoc)
apply (rule disj_commute)
@@ -143,28 +143,28 @@
subsection \<open>Disjunction\<close>
lemma disj_absorb [simp]: "x \<squnion> x = x"
- by (rule boolean.conj_absorb [OF dual])
+ by (rule boolean_algebra.conj_absorb [OF dual])
lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>"
- by (rule boolean.conj_zero_right [OF dual])
+ by (rule boolean_algebra.conj_zero_right [OF dual])
lemma compl_zero [simp]: "\<sim> \<zero> = \<one>"
- by (rule boolean.compl_one [OF dual])
+ by (rule boolean_algebra.compl_one [OF dual])
lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x"
- by (rule boolean.conj_one_left [OF dual])
+ by (rule boolean_algebra.conj_one_left [OF dual])
lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>"
- by (rule boolean.conj_zero_left [OF dual])
+ by (rule boolean_algebra.conj_zero_left [OF dual])
lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>"
- by (rule boolean.conj_cancel_left [OF dual])
+ by (rule boolean_algebra.conj_cancel_left [OF dual])
lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
- by (rule boolean.conj_left_absorb [OF dual])
+ by (rule boolean_algebra.conj_left_absorb [OF dual])
lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
- by (rule boolean.conj_disj_distrib2 [OF dual])
+ by (rule boolean_algebra.conj_disj_distrib2 [OF dual])
lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2
@@ -189,14 +189,14 @@
qed
lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
- by (rule boolean.de_Morgan_conj [OF dual])
+ by (rule boolean_algebra.de_Morgan_conj [OF dual])
end
subsection \<open>Symmetric Difference\<close>
-locale boolean_xor = boolean +
+locale boolean_algebra_xor = boolean_algebra +
fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<oplus>" 65)
assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
begin
--- a/src/HOL/Word/Word.thy Sat Apr 20 13:44:16 2019 +0000
+++ b/src/HOL/Word/Word.thy Sat Apr 20 18:02:20 2019 +0000
@@ -4202,8 +4202,8 @@
lemma word_or_not [simp]: "x OR NOT x = max_word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-lemma word_boolean: "boolean (AND) (OR) bitNOT 0 max_word"
- apply (rule boolean.intro)
+lemma word_boolean_algebra: "boolean_algebra (AND) (OR) bitNOT 0 max_word"
+ apply (rule boolean_algebra.intro)
apply (rule word_bw_assocs)
apply (rule word_bw_assocs)
apply (rule word_bw_comms)
@@ -4216,17 +4216,17 @@
apply (rule word_or_not)
done
-interpretation word_bool_alg: boolean "(AND)" "(OR)" bitNOT 0 max_word
- by (rule word_boolean)
+interpretation word_bool_alg: boolean_algebra "(AND)" "(OR)" bitNOT 0 max_word
+ by (rule word_boolean_algebra)
lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
for x y :: "'a::len0 word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-interpretation word_bool_alg: boolean_xor "(AND)" "(OR)" bitNOT 0 max_word "(XOR)"
- apply (rule boolean_xor.intro)
- apply (rule word_boolean)
- apply (rule boolean_xor_axioms.intro)
+interpretation word_bool_alg: boolean_algebra_xor "(AND)" "(OR)" bitNOT 0 max_word "(XOR)"
+ apply (rule boolean_algebra_xor.intro)
+ apply (rule word_boolean_algebra)
+ apply (rule boolean_algebra_xor_axioms.intro)
apply (rule word_xor_and_or)
done