# HG changeset patch
# User huffman
# Date 1325093254 -3600
# Node ID 507331bd8a0883e3fae25d93f63915bce7ccc4db
# Parent  0bb66de5a0bf1a2f2d3ef998ce1d5bd9b1d607dd
remove recursion combinator bin_rec;
define AND for type int directly with function package

diff -r 0bb66de5a0bf -r 507331bd8a08 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Wed Dec 28 16:24:28 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Dec 28 18:27:34 2011 +0100
@@ -12,54 +12,6 @@
 imports Bit_Representation Bit_Operations
 begin
 
-subsection {* Recursion combinators for bitstrings *}
-
-function bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a" where 
-  "bin_rec f1 f2 f3 bin = (if bin = 0 then f1 
-    else if bin = - 1 then f2
-    else f3 (bin_rest bin) (bin_last bin) (bin_rec f1 f2 f3 (bin_rest bin)))"
-  by pat_completeness auto
-
-termination by (relation "measure (nat o abs o snd o snd o snd)")
-  (simp_all add: bin_last_def bin_rest_def)
-
-declare bin_rec.simps [simp del]
-
-lemma bin_rec_PM:
-  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
-  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
-  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
-  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Bit0:
-  "f3 Int.Pls (0::bit) f1 = f1 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)"
-  by (unfold Pls_def Min_def Bit0_def Bit1_def) (simp add: bin_rec.simps bin_last_def bin_rest_def)
-
-lemma bin_rec_Bit1:
-  "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)"
-  apply (cases "w = Int.Min")
-  apply (simp add: bin_rec_Min)
-  apply (cases "w = Int.Pls")
-  apply (simp add: bin_rec_Pls number_of_is_id Pls_def [symmetric] bin_rec.simps)
-  apply (subst bin_rec.simps)
-  apply auto unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id apply auto
-  done
-  
-lemma bin_rec_Bit:
-  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls (0::bit) f1 = f1 ==> 
-    f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
-  by (cases b, simp add: bin_rec_Bit0 BIT_simps, simp add: bin_rec_Bit1 BIT_simps)
-
-lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
-  bin_rec_Bit0 bin_rec_Bit1
-
-
 subsection {* Logical operations *}
 
 text "bit-wise logical operations on the int type"
@@ -67,18 +19,25 @@
 instantiation int :: bit
 begin
 
-definition
-  int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)"
+definition int_not_def:
+  "bitNOT = (\<lambda>x::int. - x - 1)"
+
+function bitAND_int where
+  "bitAND_int x y =
+    (if x = 0 then 0 else if x = -1 then y else
+      (bin_rest x AND bin_rest y) BIT (bin_last x AND bin_last y))"
+  by pat_completeness simp
 
-definition
-  int_and_def: "bitAND = bin_rec (\<lambda>x. 0) (\<lambda>y. y) 
-    (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
+termination
+  by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
+
+declare bitAND_int.simps [simp del]
 
-definition
-  int_or_def: "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
+definition int_or_def:
+  "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
 
-definition
-  int_xor_def: "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
+definition int_xor_def:
+  "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
 
 instance ..
 
@@ -100,18 +59,27 @@
 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_0 [simp]: "(0::int) AND x = 0"
+  by (simp add: bitAND_int.simps)
+
+lemma int_and_m1 [simp]: "(-1::int) AND x = x"
+  by (simp add: bitAND_int.simps)
+
+lemma int_and_Pls [simp]: "Int.Pls AND x = Int.Pls"
+  unfolding Pls_def by simp
 
-lemma int_and_Min [simp]:
-  "Int.Min AND x = x"
-  unfolding int_and_def by (simp add: bin_rec_PM)
+lemma int_and_Min [simp]: "Int.Min AND x = x"
+  unfolding Min_def by simp
+
+lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
+  by (subst BIT_eq_iff [symmetric], simp)
+
+lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
+  by (subst BIT_eq_iff [symmetric], simp)
 
 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)
+  by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
 
 lemma int_and_Bits2 [simp]: 
   "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"