tuned towards code generation
authorhaftmann
Wed Apr 02 15:58:36 2008 +0200 (2008-04-02)
changeset 26514eff55c0a6d34
parent 26513 6f306c8c2c54
child 26515 4a2063a8c2d2
tuned towards code generation
src/HOL/Word/BinGeneral.thy
src/HOL/Word/BinOperations.thy
src/HOL/Word/Num_Lemmas.thy
src/HOL/Word/Size.thy
src/HOL/Word/WordArith.thy
src/HOL/Word/WordDefinition.thy
     1.1 --- a/src/HOL/Word/BinGeneral.thy	Wed Apr 02 15:58:32 2008 +0200
     1.2 +++ b/src/HOL/Word/BinGeneral.thy	Wed Apr 02 15:58:36 2008 +0200
     1.3 @@ -19,15 +19,15 @@
     1.4    unfolding Min_def pred_def by arith
     1.5  
     1.6  function
     1.7 -  bin_rec' :: "int * 'a * 'a * (int => bit => 'a => 'a) => 'a"  
     1.8 -  where 
     1.9 -  "bin_rec' (bin, f1, f2, f3) = (if bin = Int.Pls then f1 
    1.10 +  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"  
    1.11 +where 
    1.12 +  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 
    1.13      else if bin = Int.Min then f2
    1.14 -    else case bin_rl bin of (w, b) => f3 w b (bin_rec' (w, f1, f2, f3)))"
    1.15 +    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
    1.16    by pat_completeness auto
    1.17  
    1.18  termination 
    1.19 -  apply (relation "measure (nat o abs o fst)")
    1.20 +  apply (relation "measure (nat o abs o snd o snd o snd)")
    1.21     apply simp
    1.22    apply (simp add: Pls_def brlem)
    1.23    apply (clarsimp simp: bin_rl_char pred_def)
    1.24 @@ -38,41 +38,41 @@
    1.25     apply auto
    1.26    done
    1.27  
    1.28 -constdefs
    1.29 -  bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a"
    1.30 -  "bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"
    1.31 +declare bin_rec.simps [simp del]
    1.32  
    1.33  lemma bin_rec_PM:
    1.34    "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
    1.35 -  apply safe
    1.36 -   apply (unfold bin_rec_def)
    1.37 -   apply (auto intro: bin_rec'.simps [THEN trans])
    1.38 -  done
    1.39 +  by (auto simp add: bin_rec.simps)
    1.40  
    1.41  lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
    1.42 -  unfolding bin_rec_def by simp
    1.43 +  by (simp add: bin_rec.simps)
    1.44  
    1.45  lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
    1.46 -  unfolding bin_rec_def by simp
    1.47 +  by (simp add: bin_rec.simps)
    1.48  
    1.49  lemma bin_rec_Bit0:
    1.50    "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
    1.51      bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
    1.52 -  apply (unfold bin_rec_def)
    1.53 -  apply (rule bin_rec'.simps [THEN trans])
    1.54 -  apply (fold bin_rec_def)
    1.55 -  apply (simp add: eq_Bit0_Pls eq_Bit0_Min bin_rec_Pls)
    1.56 +  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
    1.57 +  unfolding Pls_def Min_def Bit0_def
    1.58 +  apply auto
    1.59 +  apply presburger
    1.60 +  apply (simp add: bin_rec.simps)
    1.61    done
    1.62  
    1.63  lemma bin_rec_Bit1:
    1.64    "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
    1.65      bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
    1.66 -  apply (unfold bin_rec_def)
    1.67 -  apply (rule bin_rec'.simps [THEN trans])
    1.68 -  apply (fold bin_rec_def)
    1.69 -  apply (simp add: eq_Bit1_Pls eq_Bit1_Min bin_rec_Min)
    1.70 +  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
    1.71 +  unfolding Pls_def Min_def Bit1_def
    1.72 +  apply auto
    1.73 +  apply (cases w)
    1.74 +  apply auto
    1.75 +  apply (simp add: bin_rec.simps)
    1.76 +    unfolding Min_def Pls_def number_of_is_id apply auto
    1.77 +  unfolding Bit0_def apply presburger
    1.78    done
    1.79 -
    1.80 +  
    1.81  lemma bin_rec_Bit:
    1.82    "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
    1.83      f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
    1.84 @@ -83,21 +83,18 @@
    1.85  
    1.86  subsection {* Destructors for binary integers *}
    1.87  
    1.88 -consts
    1.89 -  -- "corresponding operations analysing bins"
    1.90 -  bin_last :: "int => bit"
    1.91 -  bin_rest :: "int => int"
    1.92 -  bin_sign :: "int => int"
    1.93 -  bin_nth :: "int => nat => bool"
    1.94 +definition
    1.95 +  bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
    1.96 +
    1.97 +definition
    1.98 +  bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
    1.99  
   1.100 -primrec
   1.101 -  Z : "bin_nth w 0 = (bin_last w = bit.B1)"
   1.102 -  Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
   1.103 +definition
   1.104 +  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
   1.105  
   1.106 -defs  
   1.107 -  bin_rest_def : "bin_rest w == fst (bin_rl w)"
   1.108 -  bin_last_def : "bin_last w == snd (bin_rl w)"
   1.109 -  bin_sign_def : "bin_sign == bin_rec Int.Pls Int.Min (%w b s. s)"
   1.110 +primrec bin_nth where
   1.111 +  "bin_nth.Z" : "bin_nth w 0 = (bin_last w = bit.B1)"
   1.112 +  | "bin_nth.Suc" : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
   1.113  
   1.114  lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
   1.115    unfolding bin_rest_def bin_last_def by auto
   1.116 @@ -107,27 +104,33 @@
   1.117  lemma bin_rest_simps [simp]: 
   1.118    "bin_rest Int.Pls = Int.Pls"
   1.119    "bin_rest Int.Min = Int.Min"
   1.120 -  "bin_rest (w BIT b) = w"
   1.121    "bin_rest (Int.Bit0 w) = w"
   1.122    "bin_rest (Int.Bit1 w) = w"
   1.123 +  "bin_rest (w BIT b) = w"
   1.124    unfolding bin_rest_def by auto
   1.125  
   1.126 +declare bin_rest_simps(1-4) [code func]
   1.127 +
   1.128  lemma bin_last_simps [simp]: 
   1.129    "bin_last Int.Pls = bit.B0"
   1.130    "bin_last Int.Min = bit.B1"
   1.131 -  "bin_last (w BIT b) = b"
   1.132    "bin_last (Int.Bit0 w) = bit.B0"
   1.133    "bin_last (Int.Bit1 w) = bit.B1"
   1.134 +  "bin_last (w BIT b) = b"
   1.135    unfolding bin_last_def by auto
   1.136  
   1.137 +declare bin_last_simps(1-4) [code func]
   1.138 +
   1.139  lemma bin_sign_simps [simp]:
   1.140    "bin_sign Int.Pls = Int.Pls"
   1.141    "bin_sign Int.Min = Int.Min"
   1.142 -  "bin_sign (w BIT b) = bin_sign w"
   1.143    "bin_sign (Int.Bit0 w) = bin_sign w"
   1.144    "bin_sign (Int.Bit1 w) = bin_sign w"
   1.145 +  "bin_sign (w BIT b) = bin_sign w"
   1.146    unfolding bin_sign_def by (auto simp: bin_rec_simps)
   1.147  
   1.148 +declare bin_sign_simps(1-4) [code func]
   1.149 +
   1.150  lemma bin_r_l_extras [simp]:
   1.151    "bin_last 0 = bit.B0"
   1.152    "bin_last (- 1) = bit.B1"
     2.1 --- a/src/HOL/Word/BinOperations.thy	Wed Apr 02 15:58:32 2008 +0200
     2.2 +++ b/src/HOL/Word/BinOperations.thy	Wed Apr 02 15:58:36 2008 +0200
     2.3 @@ -306,7 +306,7 @@
     2.4    apply (case_tac x rule: bin_exhaust)
     2.5    apply (case_tac b)
     2.6     apply (case_tac [!] bit)
     2.7 -     apply (auto simp: less_eq_numeral_code)
     2.8 +     apply (auto simp: less_eq_int_code)
     2.9    done
    2.10  
    2.11  lemmas int_and_le =
     3.1 --- a/src/HOL/Word/Num_Lemmas.thy	Wed Apr 02 15:58:32 2008 +0200
     3.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Wed Apr 02 15:58:36 2008 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  definition
     3.6    Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
     3.7 -  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
     3.8 +  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
     3.9  
    3.10  lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
    3.11    unfolding Bit_def Bit0_def by simp
     4.1 --- a/src/HOL/Word/Size.thy	Wed Apr 02 15:58:32 2008 +0200
     4.2 +++ b/src/HOL/Word/Size.thy	Wed Apr 02 15:58:36 2008 +0200
     4.3 @@ -17,27 +17,42 @@
     4.4    default instantiation for numeral types. This independence requires
     4.5    some duplication with the definitions in Numeral\_Type.
     4.6  *}
     4.7 -axclass len0 < type
     4.8  
     4.9 -consts
    4.10 -  len_of :: "('a :: len0 itself) => nat"
    4.11 +class len0 = type +
    4.12 +  fixes len_of :: "'a itself \<Rightarrow> nat"
    4.13  
    4.14  text {* 
    4.15    Some theorems are only true on words with length greater 0.
    4.16  *}
    4.17 -axclass len < len0
    4.18 -  len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
    4.19 +
    4.20 +class len = len0 +
    4.21 +  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
    4.22 +
    4.23 +instantiation num0 and num1 :: len0
    4.24 +begin
    4.25 +
    4.26 +definition
    4.27 +  len_num0:  "len_of (x::num0 itself) = 0"
    4.28 +
    4.29 +definition
    4.30 +  len_num1: "len_of (x::num1 itself) = 1"
    4.31 +
    4.32 +instance ..
    4.33  
    4.34 -instance num0  :: len0 ..
    4.35 -instance num1 :: len0 ..
    4.36 -instance bit0 :: (len0) len0 ..
    4.37 -instance bit1 :: (len0) len0 ..
    4.38 +end
    4.39 +
    4.40 +instantiation bit0 and bit1 :: (len0) len0
    4.41 +begin
    4.42  
    4.43 -defs (overloaded)
    4.44 -  len_num0:  "len_of (x::num0 itself) == 0"
    4.45 -  len_num1: "len_of (x::num1 itself) == 1"
    4.46 -  len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    4.47 -  len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    4.48 +definition
    4.49 +  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
    4.50 +
    4.51 +definition
    4.52 +  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
    4.53 +
    4.54 +instance ..
    4.55 +
    4.56 +end
    4.57  
    4.58  lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    4.59  
     5.1 --- a/src/HOL/Word/WordArith.thy	Wed Apr 02 15:58:32 2008 +0200
     5.2 +++ b/src/HOL/Word/WordArith.thy	Wed Apr 02 15:58:36 2008 +0200
     5.3 @@ -395,7 +395,8 @@
     5.4  
     5.5  lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
     5.6    unfolding word_arith_wis
     5.7 -  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc eq_Bit0_Bit1)
     5.8 +  apply (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
     5.9 +  unfolding Bit0_def Bit1_def by simp
    5.10  
    5.11  lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
    5.12  
     6.1 --- a/src/HOL/Word/WordDefinition.thy	Wed Apr 02 15:58:32 2008 +0200
     6.2 +++ b/src/HOL/Word/WordDefinition.thy	Wed Apr 02 15:58:36 2008 +0200
     6.3 @@ -28,7 +28,9 @@
     6.4          only difference in these is the type class *}
     6.5    word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
     6.6  where
     6.7 -  "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
     6.8 +  [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
     6.9 +
    6.10 +code_datatype word_of_int
    6.11  
    6.12  
    6.13  subsection "Type conversions and casting"
    6.14 @@ -92,6 +94,13 @@
    6.15  
    6.16  subsection  "Arithmetic operations"
    6.17  
    6.18 +declare uint_def [code func del]
    6.19 +
    6.20 +lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
    6.21 +  unfolding uint_def word_of_int_def
    6.22 +  apply (rule Abs_word_inverse)
    6.23 +  using range_bintrunc by auto
    6.24 +
    6.25  instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
    6.26  begin
    6.27