tuned of_nat code generation
authorhaftmann
Tue Oct 07 16:07:18 2008 +0200 (2008-10-07)
changeset 28514da83a614c454
parent 28513 b0b30fd6c264
child 28515 b26ba1b1dbda
tuned of_nat code generation
src/HOL/Int.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Int.thy	Tue Oct 07 16:07:16 2008 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Oct 07 16:07:18 2008 +0200
     1.3 @@ -1922,16 +1922,6 @@
     1.4        auto simp only: Bit0_def Bit1_def)
     1.5  
     1.6  definition
     1.7 -  int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
     1.8 -  [code func del]: "int_aux = of_nat_aux"
     1.9 -
    1.10 -lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
    1.11 -
    1.12 -lemma [code, code unfold, code inline del]:
    1.13 -  "of_nat = (\<lambda>n. int_aux n 0)"
    1.14 -  by (simp add: int_aux_def of_nat_aux_def)
    1.15 -
    1.16 -definition
    1.17    nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
    1.18    "nat_aux i n = nat i + n"
    1.19  
    1.20 @@ -1943,7 +1933,7 @@
    1.21  lemma [code]: "nat i = nat_aux i 0"
    1.22    by (simp add: nat_aux_def)
    1.23  
    1.24 -hide (open) const int_aux nat_aux
    1.25 +hide (open) const nat_aux
    1.26  
    1.27  lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
    1.28    "(0\<Colon>int) = Numeral0" 
     2.1 --- a/src/HOL/Nat.thy	Tue Oct 07 16:07:16 2008 +0200
     2.2 +++ b/src/HOL/Nat.thy	Tue Oct 07 16:07:18 2008 +0200
     2.3 @@ -147,6 +147,8 @@
     2.4  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
     2.5    by (induct m) simp_all
     2.6  
     2.7 +declare add_0 [code]
     2.8 +
     2.9  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
    2.10    by simp
    2.11  
    2.12 @@ -155,7 +157,8 @@
    2.13    diff_0:     "m - 0 = (m\<Colon>nat)"
    2.14    | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    2.15  
    2.16 -declare diff_Suc [simp del, code del]
    2.17 +declare diff_Suc [simp del]
    2.18 +declare diff_0 [code]
    2.19  
    2.20  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
    2.21    by (induct n) (simp_all add: diff_Suc)
    2.22 @@ -347,12 +350,12 @@
    2.23    "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
    2.24    | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    2.25  
    2.26 -declare less_eq_nat.simps [simp del, code del]
    2.27 +declare less_eq_nat.simps [simp del]
    2.28  lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
    2.29  lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps)
    2.30  
    2.31  definition less_nat where
    2.32 -  less_eq_Suc_le [code func del]: "n < m \<longleftrightarrow> Suc n \<le> m"
    2.33 +  less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
    2.34  
    2.35  lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m"
    2.36    by (simp add: less_eq_nat.simps(2))
    2.37 @@ -1161,20 +1164,23 @@
    2.38  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    2.39    by (induct m) (simp_all add: add_ac left_distrib)
    2.40  
    2.41 -definition
    2.42 -  of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    2.43 -where
    2.44 -  [code func del]: "of_nat_aux n i = of_nat n + i"
    2.45 +primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    2.46 +  "of_nat_aux inc 0 i = i"
    2.47 +  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    2.48  
    2.49 -lemma of_nat_aux_code [code]:
    2.50 -  "of_nat_aux 0 i = i"
    2.51 -  "of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *}
    2.52 -  by (simp_all add: of_nat_aux_def add_ac)
    2.53 -
    2.54 -lemma of_nat_code [code]:
    2.55 -  "of_nat n = of_nat_aux n 0"
    2.56 -  by (simp add: of_nat_aux_def)
    2.57 -
    2.58 +lemma of_nat_code [code, code unfold, code inline del]:
    2.59 +  "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
    2.60 +proof (induct n)
    2.61 +  case 0 then show ?case by simp
    2.62 +next
    2.63 +  case (Suc n)
    2.64 +  have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
    2.65 +    by (induct n) simp_all
    2.66 +  from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1"
    2.67 +    by simp
    2.68 +  with Suc show ?case by (simp add: add_commute)
    2.69 +qed
    2.70 +    
    2.71  end
    2.72  
    2.73  text{*Class for unital semirings with characteristic zero.