# HG changeset patch
# User huffman
# Date 1187643470 -7200
# Node ID 08b11604954756bf611779c20e45e53b213cef58
# Parent  038b164edfef6de87745cfc1cbbd44921635b33b
move bit simps from BinOperations to BitSyntax

diff -r 038b164edfef -r 08b116049547 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Mon Aug 20 22:48:24 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy	Mon Aug 20 22:57:50 2007 +0200
@@ -34,30 +34,6 @@
   "NOT (w BIT b) = (NOT w) BIT (NOT b)"
   by (unfold int_not_def) (auto intro: bin_rec_simps)
 
-lemma bit_extra_simps [simp]: 
-  "x AND bit.B0 = bit.B0"
-  "x AND bit.B1 = x"
-  "x OR bit.B1 = bit.B1"
-  "x OR bit.B0 = x"
-  "x XOR bit.B1 = NOT x"
-  "x XOR bit.B0 = x"
-  by (cases x, auto)+
-
-lemma bit_ops_comm: 
-  "(x::bit) AND y = y AND x"
-  "(x::bit) OR y = y OR x"
-  "(x::bit) XOR y = y XOR x"
-  by (cases y, auto)+
-
-lemma bit_ops_same [simp]: 
-  "(x::bit) AND x = x"
-  "(x::bit) OR x = x"
-  "(x::bit) XOR x = bit.B0"
-  by (cases x, auto)+
-
-lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
-  by (cases x) auto
-
 lemma int_xor_Pls [simp]: 
   "Numeral.Pls XOR x = x"
   unfolding int_xor_def by (simp add: bin_rec_PM)
diff -r 038b164edfef -r 08b116049547 src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Mon Aug 20 22:48:24 2007 +0200
+++ b/src/HOL/Word/BitSyntax.thy	Mon Aug 20 22:57:50 2007 +0200
@@ -70,7 +70,28 @@
   by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def
                     XOR_bit_def split: bit.split)
 
-lemma bit_NOT_NOT: "NOT (NOT (b::bit)) = b"
-  by (induct b) simp_all
+lemma bit_extra_simps [simp]: 
+  "x AND bit.B0 = bit.B0"
+  "x AND bit.B1 = x"
+  "x OR bit.B1 = bit.B1"
+  "x OR bit.B0 = x"
+  "x XOR bit.B1 = NOT x"
+  "x XOR bit.B0 = x"
+  by (cases x, auto)+
+
+lemma bit_ops_comm: 
+  "(x::bit) AND y = y AND x"
+  "(x::bit) OR y = y OR x"
+  "(x::bit) XOR y = y XOR x"
+  by (cases y, auto)+
+
+lemma bit_ops_same [simp]: 
+  "(x::bit) AND x = x"
+  "(x::bit) OR x = x"
+  "(x::bit) XOR x = bit.B0"
+  by (cases x, auto)+
+
+lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
+  by (cases x) auto
 
 end