# HG changeset patch
# User huffman
# Date 1325085049 -3600
# Node ID c5a1002161c367f77ec85058e8d9df907b8d7d92
# Parent  c42e43287b5fdb4295112692c44e8e97e8d7e08f
simplify definition of OR for type int;
reorder some lemmas

diff -r c42e43287b5f -r c5a1002161c3 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Wed Dec 28 16:04:58 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Dec 28 16:10:49 2011 +0100
@@ -75,8 +75,7 @@
     (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
 
 definition
-  int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. - 1) 
-    (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
+  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 
@@ -99,6 +98,29 @@
   "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
   unfolding int_not_def Pls_def Min_def Bit0_def Bit1_def by simp_all
 
+lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
+  unfolding int_not_def by simp
+
+lemma int_and_Pls [simp]:
+  "Int.Pls AND x = Int.Pls"
+  unfolding int_and_def Pls_def [symmetric] by (simp add: bin_rec_PM)
+
+lemma int_and_Min [simp]:
+  "Int.Min AND x = x"
+  unfolding int_and_def by (simp add: bin_rec_PM)
+
+lemma int_and_Bits [simp]: 
+  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
+  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric]
+  by (simp add: bin_rec_simps BIT_simps)
+
+lemma int_and_Bits2 [simp]: 
+  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
+  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+  "(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)
@@ -125,45 +147,25 @@
   "(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"
-  by (unfold int_or_def) (simp add: bin_rec_PM)
+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"
-  by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM)
+lemma int_or_Min [simp]: "Int.Min OR x = Int.Min"
+  unfolding int_or_def by simp
+
+lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
+  by (induct b, simp_all) (* TODO: move *)
 
 lemma int_or_Bits [simp]: 
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
-  unfolding int_or_def Pls_def [symmetric] Min_def [symmetric]
-  by (simp add: bin_rec_simps BIT_simps)
+  unfolding int_or_def bit_or_def by simp
 
 lemma int_or_Bits2 [simp]: 
   "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
   "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
   "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
-  unfolding BIT_simps [symmetric] int_or_Bits by simp_all
-
-lemma int_and_Pls [simp]:
-  "Int.Pls AND x = Int.Pls"
-  unfolding int_and_def Pls_def [symmetric] by (simp add: bin_rec_PM)
-
-lemma int_and_Min [simp]:
-  "Int.Min AND x = x"
-  unfolding int_and_def by (simp add: bin_rec_PM)
-
-lemma int_and_Bits [simp]: 
-  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
-  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric]
-  by (simp add: bin_rec_simps BIT_simps)
-
-lemma int_and_Bits2 [simp]: 
-  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
-  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
-  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
-  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
-  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
+  unfolding int_or_def by simp_all
 
 subsubsection {* Binary destructors *}
 
@@ -235,9 +237,6 @@
   "(x::int) XOR x = Int.Pls"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
-lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
-  by (auto simp add: bin_eq_iff bin_nth_ops)
-
 lemmas bin_log_esimps = 
   int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
   int_and_Pls int_and_Min  int_or_Pls int_or_Min  int_xor_Pls int_xor_Min
@@ -631,4 +630,3 @@
   by auto
 
 end
-