src/HOL/Nat.thy
changeset 28514 da83a614c454
parent 27823 52971512d1a2
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Nat.thy	Tue Oct 07 16:07:16 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Oct 07 16:07:18 2008 +0200
     1.3 @@ -147,6 +147,8 @@
     1.4  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
     1.5    by (induct m) simp_all
     1.6  
     1.7 +declare add_0 [code]
     1.8 +
     1.9  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
    1.10    by simp
    1.11  
    1.12 @@ -155,7 +157,8 @@
    1.13    diff_0:     "m - 0 = (m\<Colon>nat)"
    1.14    | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.15  
    1.16 -declare diff_Suc [simp del, code del]
    1.17 +declare diff_Suc [simp del]
    1.18 +declare diff_0 [code]
    1.19  
    1.20  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
    1.21    by (induct n) (simp_all add: diff_Suc)
    1.22 @@ -347,12 +350,12 @@
    1.23    "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
    1.24    | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    1.25  
    1.26 -declare less_eq_nat.simps [simp del, code del]
    1.27 +declare less_eq_nat.simps [simp del]
    1.28  lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
    1.29  lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps)
    1.30  
    1.31  definition less_nat where
    1.32 -  less_eq_Suc_le [code func del]: "n < m \<longleftrightarrow> Suc n \<le> m"
    1.33 +  less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
    1.34  
    1.35  lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m"
    1.36    by (simp add: less_eq_nat.simps(2))
    1.37 @@ -1161,20 +1164,23 @@
    1.38  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    1.39    by (induct m) (simp_all add: add_ac left_distrib)
    1.40  
    1.41 -definition
    1.42 -  of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.43 -where
    1.44 -  [code func del]: "of_nat_aux n i = of_nat n + i"
    1.45 +primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.46 +  "of_nat_aux inc 0 i = i"
    1.47 +  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    1.48  
    1.49 -lemma of_nat_aux_code [code]:
    1.50 -  "of_nat_aux 0 i = i"
    1.51 -  "of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *}
    1.52 -  by (simp_all add: of_nat_aux_def add_ac)
    1.53 -
    1.54 -lemma of_nat_code [code]:
    1.55 -  "of_nat n = of_nat_aux n 0"
    1.56 -  by (simp add: of_nat_aux_def)
    1.57 -
    1.58 +lemma of_nat_code [code, code unfold, code inline del]:
    1.59 +  "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
    1.60 +proof (induct n)
    1.61 +  case 0 then show ?case by simp
    1.62 +next
    1.63 +  case (Suc n)
    1.64 +  have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
    1.65 +    by (induct n) simp_all
    1.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"
    1.67 +    by simp
    1.68 +  with Suc show ?case by (simp add: add_commute)
    1.69 +qed
    1.70 +    
    1.71  end
    1.72  
    1.73  text{*Class for unital semirings with characteristic zero.