# HG changeset patch
# User haftmann
# Date 1277983934 -7200
# Node ID 41acc0fa6b6c6dd739d8b58904e3fbfa0377a8be
# Parent  f2c98b8c0c5c9428065b23295d83f7929319aeb0
avoid bitstrings in generated code

diff -r f2c98b8c0c5c -r 41acc0fa6b6c src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/Word/Bit_Int.thy	Thu Jul 01 13:32:14 2010 +0200
@@ -12,6 +12,54 @@
 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, simp add: bin_rec_Bit1)
+
+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"
@@ -20,19 +68,19 @@
 begin
 
 definition
-  int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls 
+  int_not_def: "bitNOT = bin_rec (- 1) 0
     (\<lambda>w b s. s BIT (NOT b))"
 
 definition
-  int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
+  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))"
 
 definition
-  int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
+  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))"
 
 definition
-  int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
+  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))"
 
 instance ..
@@ -45,21 +93,19 @@
   "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
   "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
   "NOT (w BIT b) = (NOT w) BIT (NOT b)"
-  unfolding int_not_def by (simp_all add: bin_rec_simps)
+  unfolding int_not_def Pls_def [symmetric] Min_def [symmetric] by (simp_all add: bin_rec_simps)
 
-declare int_not_simps(1-4) [code]
-
-lemma int_xor_Pls [simp, code]: 
+lemma int_xor_Pls [simp]: 
   "Int.Pls XOR x = x"
-  unfolding int_xor_def by (simp add: bin_rec_PM)
+  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
 
-lemma int_xor_Min [simp, code]: 
+lemma int_xor_Min [simp]: 
   "Int.Min XOR x = NOT x"
-  unfolding int_xor_def by (simp add: bin_rec_PM)
+  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)
+  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
@@ -68,7 +114,7 @@
   apply (simp add: int_not_simps [symmetric])
   done
 
-lemma int_xor_Bits2 [simp, code]: 
+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)"
@@ -84,24 +130,24 @@
    apply clarsimp+
   done
 
-lemma int_xor_extra_simps [simp, code]:
+lemma int_xor_extra_simps [simp]:
   "w XOR Int.Pls = w"
   "w XOR Int.Min = NOT w"
   using int_xor_x_simps' by simp_all
 
-lemma int_or_Pls [simp, code]: 
+lemma int_or_Pls [simp]: 
   "Int.Pls OR x = x"
   by (unfold int_or_def) (simp add: bin_rec_PM)
   
-lemma int_or_Min [simp, code]:
+lemma int_or_Min [simp]:
   "Int.Min OR x = Int.Min"
-  by (unfold int_or_def) (simp add: bin_rec_PM)
+  by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM)
 
 lemma int_or_Bits [simp]: 
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
-  unfolding int_or_def by (simp add: bin_rec_simps)
+  unfolding int_or_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
 
-lemma int_or_Bits2 [simp, code]: 
+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)"
@@ -117,24 +163,24 @@
    apply clarsimp+
   done
 
-lemma int_or_extra_simps [simp, code]:
+lemma int_or_extra_simps [simp]:
   "w OR Int.Pls = w"
   "w OR Int.Min = Int.Min"
   using int_or_x_simps' by simp_all
 
-lemma int_and_Pls [simp, code]:
+lemma int_and_Pls [simp]:
   "Int.Pls AND x = Int.Pls"
   unfolding int_and_def by (simp add: bin_rec_PM)
 
-lemma int_and_Min [simp, code]:
+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 by (simp add: bin_rec_simps)
+  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
 
-lemma int_and_Bits2 [simp, code]: 
+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)"
@@ -150,7 +196,7 @@
    apply clarsimp+
   done
 
-lemma int_and_extra_simps [simp, code]:
+lemma int_and_extra_simps [simp]:
   "w AND Int.Pls = Int.Pls"
   "w AND Int.Min = w"
   using int_and_x_simps' by simp_all
@@ -296,12 +342,12 @@
   apply (unfold Bit_def)
   apply clarsimp
   apply (erule_tac x = "x" in allE)
-  apply (simp split: bit.split)
+  apply (simp add: bitval_def split: bit.split)
   done
 
 lemma le_int_or:
-  "!!x.  bin_sign y = Int.Pls ==> x <= x OR y"
-  apply (induct y rule: bin_induct)
+  "bin_sign (y::int) = Int.Pls ==> x <= x OR y"
+  apply (induct y arbitrary: x rule: bin_induct)
     apply clarsimp
    apply clarsimp
   apply (case_tac x rule: bin_exhaust)
@@ -424,7 +470,7 @@
    apply (case_tac [!] w rule: bin_exhaust)
    apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
-   apply (simp_all split: bit.split)
+   apply (simp_all add: bitval_def split: bit.split)
   done
 
 lemma bin_set_ge:
@@ -433,7 +479,7 @@
    apply (case_tac [!] w rule: bin_exhaust)
    apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
-   apply (simp_all split: bit.split)
+   apply (simp_all add: bitval_def split: bit.split)
   done
 
 lemma bintr_bin_clr_le:
@@ -444,7 +490,7 @@
   apply (case_tac m)
    apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
-   apply (simp_all split: bit.split)
+   apply (simp_all add: bitval_def split: bit.split)
   done
 
 lemma bintr_bin_set_ge:
@@ -455,7 +501,7 @@
   apply (case_tac m)
    apply (auto simp del: BIT_simps)
    apply (unfold Bit_def)
-   apply (simp_all split: bit.split)
+   apply (simp_all add: bitval_def split: bit.split)
   done
 
 lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
@@ -482,6 +528,10 @@
 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
   "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
 
+lemma [code]:
+  "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
+  by (simp add: bin_rcat_def Pls_def)
+
 fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   "bin_rsplit_aux n m c bs =
     (if m = 0 | n = 0 then bs else
@@ -610,7 +660,7 @@
   apply (simp add: bin_rest_div zdiv_zmult2_eq)
   apply (case_tac b rule: bin_exhaust)
   apply simp
-  apply (simp add: Bit_def mod_mult_mult1 p1mod22k
+  apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def
               split: bit.split 
               cong: number_of_False_cong)
   done 
diff -r f2c98b8c0c5c -r 41acc0fa6b6c src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Jul 01 13:32:14 2010 +0200
@@ -2,8 +2,7 @@
   Author: Jeremy Dawson, NICTA
 
   contains basic definition to do with integers
-  expressed using Pls, Min, BIT and important resulting theorems, 
-  in particular, bin_rec and related work
+  expressed using Pls, Min, BIT
 *) 
 
 header {* Basic Definitions for Binary Integers *}
@@ -14,8 +13,16 @@
 
 subsection {* Further properties of numerals *}
 
+definition bitval :: "bit \<Rightarrow> 'a\<Colon>zero_neq_one" where
+  "bitval = bit_case 0 1"
+
+lemma bitval_simps [simp]:
+  "bitval 0 = 0"
+  "bitval 1 = 1"
+  by (simp_all add: bitval_def)
+
 definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
-  "k BIT b = bit_case 0 1 b + k + k"
+  "k BIT b = bitval b + k + k"
 
 lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
   unfolding Bit_def Bit0_def by simp
@@ -43,10 +50,9 @@
 (** ways in which type Bin resembles a datatype **)
 
 lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
-  apply (unfold Bit_def)
-  apply (simp (no_asm_use) split: bit.split_asm)
-     apply simp_all
-   apply (drule_tac f=even in arg_cong, clarsimp)+
+  apply (cases b) apply (simp_all)
+  apply (cases c) apply (simp_all)
+  apply (cases c) apply (simp_all)
   done
      
 lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
@@ -59,11 +65,11 @@
 
 lemma less_Bits: 
   "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
-  unfolding Bit_def by (auto split: bit.split)
+  unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
 
 lemma le_Bits: 
   "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" 
-  unfolding Bit_def by (auto split: bit.split)
+  unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
 
 lemma no_no [simp]: "number_of (number_of i) = i"
   unfolding number_of_eq by simp
@@ -107,7 +113,7 @@
   apply (unfold Bit_def)
   apply (cases "even bin")
    apply (clarsimp simp: even_equiv_def)
-   apply (auto simp: odd_equiv_def split: bit.split)
+   apply (auto simp: odd_equiv_def bitval_def split: bit.split)
   done
 
 lemma bin_exhaust:
@@ -237,7 +243,7 @@
    apply (rule refl)
   apply (drule trans)
    apply (rule Bit_def)
-  apply (simp add: z1pdiv2 split: bit.split)
+  apply (simp add: bitval_def z1pdiv2 split: bit.split)
   done
 
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
@@ -314,61 +320,10 @@
   bin_nth_minus_Bit0 bin_nth_minus_Bit1
 
 
-subsection {* Recursion combinator for binary integers *}
-
-lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
-  unfolding Min_def pred_def by arith
-
-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 = Int.Pls then f1 
-    else if bin = Int.Min then f2
-    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
-  by pat_completeness auto
-
-termination 
-  apply (relation "measure (nat o abs o snd o snd o snd)")
-  apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
-  unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
-  apply auto
-  done
-
-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 (auto simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
-  by (simp add: bin_rec.simps)
-
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
-  by (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 (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
-
-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)"
-  by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"])
-  
-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, simp add: bin_rec_Bit1)
-
-lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
-  bin_rec_Bit0 bin_rec_Bit1
-
-
 subsection {* Truncating binary integers *}
 
 definition
-  bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
+  bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
 
 lemma bin_sign_simps [simp]:
   "bin_sign Int.Pls = Int.Pls"
@@ -376,26 +331,26 @@
   "bin_sign (Int.Bit0 w) = bin_sign w"
   "bin_sign (Int.Bit1 w) = bin_sign w"
   "bin_sign (w BIT b) = bin_sign w"
-  unfolding bin_sign_def by (auto simp: bin_rec_simps)
-
-declare bin_sign_simps(1-4) [code]
+  by (unfold bin_sign_def numeral_simps Bit_def bitval_def) (simp_all split: bit.split)
 
 lemma bin_sign_rest [simp]: 
-  "bin_sign (bin_rest w) = (bin_sign w)"
+  "bin_sign (bin_rest w) = bin_sign w"
   by (cases w rule: bin_exhaust) auto
 
-consts
-  bintrunc :: "nat => int => int"
-primrec 
+primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where
   Z : "bintrunc 0 bin = Int.Pls"
-  Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
+| Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
 
-consts
-  sbintrunc :: "nat => int => int" 
-primrec 
+primrec sbintrunc :: "nat => int => int" where
   Z : "sbintrunc 0 bin = 
     (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)"
-  Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
+| Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
+
+lemma [code]:
+  "sbintrunc 0 bin = 
+    (case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)"
+  "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
+  apply simp_all apply (cases "bin_last bin") apply simp apply (unfold Min_def number_of_is_id) apply simp done
 
 lemma sign_bintr:
   "!!w. bin_sign (bintrunc n w) = Int.Pls"
@@ -862,6 +817,11 @@
   | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
         in (w1, w2 BIT bin_last w))"
 
+lemma [code]:
+  "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))"
+  "bin_split 0 w = (w, 0)"
+  by (simp_all add: Pls_def)
+
 primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
   Z: "bin_cat w 0 v = w"
   | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
diff -r f2c98b8c0c5c -r 41acc0fa6b6c src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Thu Jul 01 13:32:14 2010 +0200
@@ -22,6 +22,10 @@
 definition bl_to_bin :: "bool list \<Rightarrow> int" where
   bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
 
+lemma [code]:
+  "bl_to_bin bs = bl_to_bin_aux bs 0"
+  by (simp add: bl_to_bin_def Pls_def)
+
 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
   Z: "bin_to_bl_aux 0 w bl = bl"
   | Suc: "bin_to_bl_aux (Suc n) w bl =
diff -r f2c98b8c0c5c -r 41acc0fa6b6c src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jul 01 08:13:20 2010 +0200
+++ b/src/HOL/Word/Word.thy	Thu Jul 01 13:32:14 2010 +0200
@@ -240,6 +240,10 @@
 
 end
 
+lemma [code]:
+  "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
+  by (simp only: word_msb_def Min_def)
+
 definition setBit :: "'a :: len0 word => nat => 'a word" where 
   "setBit w n == set_bit w n True"