# HG changeset patch
# User haftmann
# Date 1207144716 -7200
# Node ID eff55c0a6d342c5eff725b75e97377af17327e44
# Parent  6f306c8c2c5495adf1e367de9c020e2117dfedf7
tuned towards code generation

diff -r 6f306c8c2c54 -r eff55c0a6d34 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Wed Apr 02 15:58:32 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Wed Apr 02 15:58:36 2008 +0200
@@ -19,15 +19,15 @@
   unfolding Min_def pred_def by arith
 
 function
-  bin_rec' :: "int * 'a * 'a * (int => bit => 'a => 'a) => 'a"  
-  where 
-  "bin_rec' (bin, f1, f2, f3) = (if bin = Int.Pls then f1 
+  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' (w, f1, f2, f3)))"
+    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 fst)")
+  apply (relation "measure (nat o abs o snd o snd o snd)")
    apply simp
   apply (simp add: Pls_def brlem)
   apply (clarsimp simp: bin_rl_char pred_def)
@@ -38,41 +38,41 @@
    apply auto
   done
 
-constdefs
-  bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a"
-  "bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"
+declare bin_rec.simps [simp del]
 
 lemma bin_rec_PM:
   "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
-  apply safe
-   apply (unfold bin_rec_def)
-   apply (auto intro: bin_rec'.simps [THEN trans])
-  done
+  by (auto simp add: bin_rec.simps)
 
 lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
-  unfolding bin_rec_def by simp
+  by (simp add: bin_rec.simps)
 
 lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
-  unfolding bin_rec_def by simp
+  by (simp add: bin_rec.simps)
 
 lemma bin_rec_Bit0:
   "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
     bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
-  apply (unfold bin_rec_def)
-  apply (rule bin_rec'.simps [THEN trans])
-  apply (fold bin_rec_def)
-  apply (simp add: eq_Bit0_Pls eq_Bit0_Min bin_rec_Pls)
+  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
+  unfolding Pls_def Min_def Bit0_def
+  apply auto
+  apply presburger
+  apply (simp add: bin_rec.simps)
   done
 
 lemma bin_rec_Bit1:
   "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
     bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
-  apply (unfold bin_rec_def)
-  apply (rule bin_rec'.simps [THEN trans])
-  apply (fold bin_rec_def)
-  apply (simp add: eq_Bit1_Pls eq_Bit1_Min bin_rec_Min)
+  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
+  unfolding Pls_def Min_def Bit1_def
+  apply auto
+  apply (cases w)
+  apply auto
+  apply (simp add: bin_rec.simps)
+    unfolding Min_def Pls_def number_of_is_id apply auto
+  unfolding Bit0_def apply presburger
   done
-
+  
 lemma bin_rec_Bit:
   "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
     f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
@@ -83,21 +83,18 @@
 
 subsection {* Destructors for binary integers *}
 
-consts
-  -- "corresponding operations analysing bins"
-  bin_last :: "int => bit"
-  bin_rest :: "int => int"
-  bin_sign :: "int => int"
-  bin_nth :: "int => nat => bool"
+definition
+  bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
+
+definition
+  bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
 
-primrec
-  Z : "bin_nth w 0 = (bin_last w = bit.B1)"
-  Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
+definition
+  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
 
-defs  
-  bin_rest_def : "bin_rest w == fst (bin_rl w)"
-  bin_last_def : "bin_last w == snd (bin_rl w)"
-  bin_sign_def : "bin_sign == bin_rec Int.Pls Int.Min (%w b s. s)"
+primrec bin_nth where
+  "bin_nth.Z" : "bin_nth w 0 = (bin_last w = bit.B1)"
+  | "bin_nth.Suc" : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
 
 lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
   unfolding bin_rest_def bin_last_def by auto
@@ -107,27 +104,33 @@
 lemma bin_rest_simps [simp]: 
   "bin_rest Int.Pls = Int.Pls"
   "bin_rest Int.Min = Int.Min"
-  "bin_rest (w BIT b) = w"
   "bin_rest (Int.Bit0 w) = w"
   "bin_rest (Int.Bit1 w) = w"
+  "bin_rest (w BIT b) = w"
   unfolding bin_rest_def by auto
 
+declare bin_rest_simps(1-4) [code func]
+
 lemma bin_last_simps [simp]: 
   "bin_last Int.Pls = bit.B0"
   "bin_last Int.Min = bit.B1"
-  "bin_last (w BIT b) = b"
   "bin_last (Int.Bit0 w) = bit.B0"
   "bin_last (Int.Bit1 w) = bit.B1"
+  "bin_last (w BIT b) = b"
   unfolding bin_last_def by auto
 
+declare bin_last_simps(1-4) [code func]
+
 lemma bin_sign_simps [simp]:
   "bin_sign Int.Pls = Int.Pls"
   "bin_sign Int.Min = Int.Min"
-  "bin_sign (w BIT b) = bin_sign w"
   "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 func]
+
 lemma bin_r_l_extras [simp]:
   "bin_last 0 = bit.B0"
   "bin_last (- 1) = bit.B1"
diff -r 6f306c8c2c54 -r eff55c0a6d34 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Wed Apr 02 15:58:32 2008 +0200
+++ b/src/HOL/Word/BinOperations.thy	Wed Apr 02 15:58:36 2008 +0200
@@ -306,7 +306,7 @@
   apply (case_tac x rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] bit)
-     apply (auto simp: less_eq_numeral_code)
+     apply (auto simp: less_eq_int_code)
   done
 
 lemmas int_and_le =
diff -r 6f306c8c2c54 -r eff55c0a6d34 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Wed Apr 02 15:58:32 2008 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Wed Apr 02 15:58:36 2008 +0200
@@ -13,7 +13,7 @@
 
 definition
   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
-  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
 
 lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
   unfolding Bit_def Bit0_def by simp
diff -r 6f306c8c2c54 -r eff55c0a6d34 src/HOL/Word/Size.thy
--- a/src/HOL/Word/Size.thy	Wed Apr 02 15:58:32 2008 +0200
+++ b/src/HOL/Word/Size.thy	Wed Apr 02 15:58:36 2008 +0200
@@ -17,27 +17,42 @@
   default instantiation for numeral types. This independence requires
   some duplication with the definitions in Numeral\_Type.
 *}
-axclass len0 < type
 
-consts
-  len_of :: "('a :: len0 itself) => nat"
+class len0 = type +
+  fixes len_of :: "'a itself \<Rightarrow> nat"
 
 text {* 
   Some theorems are only true on words with length greater 0.
 *}
-axclass len < len0
-  len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
+
+class len = len0 +
+  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
+
+instantiation num0 and num1 :: len0
+begin
+
+definition
+  len_num0:  "len_of (x::num0 itself) = 0"
+
+definition
+  len_num1: "len_of (x::num1 itself) = 1"
+
+instance ..
 
-instance num0  :: len0 ..
-instance num1 :: len0 ..
-instance bit0 :: (len0) len0 ..
-instance bit1 :: (len0) len0 ..
+end
+
+instantiation bit0 and bit1 :: (len0) len0
+begin
 
-defs (overloaded)
-  len_num0:  "len_of (x::num0 itself) == 0"
-  len_num1: "len_of (x::num1 itself) == 1"
-  len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
-  len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
+definition
+  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
+
+definition
+  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
+
+instance ..
+
+end
 
 lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
 
diff -r 6f306c8c2c54 -r eff55c0a6d34 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Wed Apr 02 15:58:32 2008 +0200
+++ b/src/HOL/Word/WordArith.thy	Wed Apr 02 15:58:36 2008 +0200
@@ -395,7 +395,8 @@
 
 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
   unfolding word_arith_wis
-  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc eq_Bit0_Bit1)
+  apply (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+  unfolding Bit0_def Bit1_def by simp
 
 lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
 
diff -r 6f306c8c2c54 -r eff55c0a6d34 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Wed Apr 02 15:58:32 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Wed Apr 02 15:58:36 2008 +0200
@@ -28,7 +28,9 @@
         only difference in these is the type class *}
   word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
 where
-  "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
+  [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
+
+code_datatype word_of_int
 
 
 subsection "Type conversions and casting"
@@ -92,6 +94,13 @@
 
 subsection  "Arithmetic operations"
 
+declare uint_def [code func del]
+
+lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
+  unfolding uint_def word_of_int_def
+  apply (rule Abs_word_inverse)
+  using range_bintrunc by auto
+
 instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
 begin