# HG changeset patch
# User huffman
# Date 1325085868 -3600
# Node ID 0bb66de5a0bf1a2f2d3ef998ce1d5bd9b1d607dd
# Parent  c5a1002161c367f77ec85058e8d9df907b8d7d92
simplify definition of XOR for type int;
reorder some lemmas

diff -r c5a1002161c3 -r 0bb66de5a0bf src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Wed Dec 28 16:10:49 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Dec 28 16:24:28 2011 +0100
@@ -78,8 +78,7 @@
   int_or_def: "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
 
 definition
-  int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
-    (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
+  int_xor_def: "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
 
 instance ..
 
@@ -121,35 +120,9 @@
   "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
   unfolding BIT_simps [symmetric] int_and_Bits by simp_all
 
-lemma int_xor_Pls [simp]: 
-  "Int.Pls XOR x = x"
-  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
-
-lemma int_xor_Min [simp]: 
-  "Int.Min XOR x = NOT x"
-  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
-
-lemma int_xor_Bits [simp]: 
-  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
-  apply (unfold int_xor_def Pls_def [symmetric] Min_def [symmetric])
-  apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
-    apply (rule ext, simp)
-   prefer 2
-   apply simp
-  apply (rule ext)
-  apply (simp add: int_not_BIT [symmetric])
-  done
-
-lemma int_xor_Bits2 [simp]: 
-  "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
-  "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
-  "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
-  "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
-  unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
-
 lemma int_or_Pls [simp]: "Int.Pls OR x = x"
   unfolding int_or_def by simp
-  
+
 lemma int_or_Min [simp]: "Int.Min OR x = Int.Min"
   unfolding int_or_def by simp
 
@@ -167,6 +140,23 @@
   "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   unfolding int_or_def by simp_all
 
+lemma int_xor_Pls [simp]: "Int.Pls XOR x = x"
+  unfolding int_xor_def by simp
+
+lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
+  by (induct b, simp_all) (* TODO: move *)
+
+lemma int_xor_Bits [simp]: 
+  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
+  unfolding int_xor_def bit_xor_def by simp
+
+lemma int_xor_Bits2 [simp]: 
+  "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
+  "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
+  "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
+  "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
+  unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
+
 subsubsection {* Binary destructors *}
 
 lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
@@ -208,6 +198,9 @@
 
 subsubsection {* Derived properties *}
 
+lemma int_xor_Min [simp]: "Int.Min XOR x = NOT x"
+  by (auto simp add: bin_eq_iff bin_nth_ops)
+
 lemma int_xor_extra_simps [simp]:
   "w XOR Int.Pls = w"
   "w XOR Int.Min = NOT w"