# HG changeset patch # User haftmann # Date 1223388438 -7200 # Node ID da83a614c454cfec29e434f12e7726a6270d982f # Parent b0b30fd6c264d9a2c65117ab5170cd408fe61258 tuned of_nat code generation diff -r b0b30fd6c264 -r da83a614c454 src/HOL/Int.thy --- a/src/HOL/Int.thy Tue Oct 07 16:07:16 2008 +0200 +++ b/src/HOL/Int.thy Tue Oct 07 16:07:18 2008 +0200 @@ -1922,16 +1922,6 @@ auto simp only: Bit0_def Bit1_def) definition - int_aux :: "nat \ int \ int" where - [code func del]: "int_aux = of_nat_aux" - -lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code] - -lemma [code, code unfold, code inline del]: - "of_nat = (\n. int_aux n 0)" - by (simp add: int_aux_def of_nat_aux_def) - -definition nat_aux :: "int \ nat \ nat" where "nat_aux i n = nat i + n" @@ -1943,7 +1933,7 @@ lemma [code]: "nat i = nat_aux i 0" by (simp add: nat_aux_def) -hide (open) const int_aux nat_aux +hide (open) const nat_aux lemma zero_is_num_zero [code func, code inline, symmetric, code post]: "(0\int) = Numeral0" diff -r b0b30fd6c264 -r da83a614c454 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Oct 07 16:07:16 2008 +0200 +++ b/src/HOL/Nat.thy Tue Oct 07 16:07:18 2008 +0200 @@ -147,6 +147,8 @@ lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)" by (induct m) simp_all +declare add_0 [code] + lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" by simp @@ -155,7 +157,8 @@ diff_0: "m - 0 = (m\nat)" | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" -declare diff_Suc [simp del, code del] +declare diff_Suc [simp del] +declare diff_0 [code] lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)" by (induct n) (simp_all add: diff_Suc) @@ -347,12 +350,12 @@ "(0\nat) \ n \ True" | "Suc m \ n \ (case n of 0 \ False | Suc n \ m \ n)" -declare less_eq_nat.simps [simp del, code del] +declare less_eq_nat.simps [simp del] lemma [code]: "(0\nat) \ n \ True" by (simp add: less_eq_nat.simps) lemma le0 [iff]: "0 \ (n\nat)" by (simp add: less_eq_nat.simps) definition less_nat where - less_eq_Suc_le [code func del]: "n < m \ Suc n \ m" + less_eq_Suc_le: "n < m \ Suc n \ m" lemma Suc_le_mono [iff]: "Suc n \ Suc m \ n \ m" by (simp add: less_eq_nat.simps(2)) @@ -1161,20 +1164,23 @@ lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n" by (induct m) (simp_all add: add_ac left_distrib) -definition - of_nat_aux :: "nat \ 'a \ 'a" -where - [code func del]: "of_nat_aux n i = of_nat n + i" +primrec of_nat_aux :: "('a \ 'a) \ nat \ 'a \ 'a" where + "of_nat_aux inc 0 i = i" + | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *} -lemma of_nat_aux_code [code]: - "of_nat_aux 0 i = i" - "of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *} - by (simp_all add: of_nat_aux_def add_ac) - -lemma of_nat_code [code]: - "of_nat n = of_nat_aux n 0" - by (simp add: of_nat_aux_def) - +lemma of_nat_code [code, code unfold, code inline del]: + "of_nat n = of_nat_aux (\i. i + 1) n 0" +proof (induct n) + case 0 then show ?case by simp +next + case (Suc n) + have "\i. of_nat_aux (\i. i + 1) n (i + 1) = of_nat_aux (\i. i + 1) n i + 1" + by (induct n) simp_all + from this [of 0] have "of_nat_aux (\i. i + 1) n 1 = of_nat_aux (\i. i + 1) n 0 + 1" + by simp + with Suc show ?case by (simp add: add_commute) +qed + end text{*Class for unital semirings with characteristic zero.