--- 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 \<Rightarrow> int \<Rightarrow> 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 = (\<lambda>n. int_aux n 0)"
- by (simp add: int_aux_def of_nat_aux_def)
-
-definition
nat_aux :: "int \<Rightarrow> nat \<Rightarrow> 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\<Colon>int) = Numeral0"
--- 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\<Colon>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\<Colon>nat) \<le> n \<longleftrightarrow> True"
| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
-declare less_eq_nat.simps [simp del, code del]
+declare less_eq_nat.simps [simp del]
lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps)
lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps)
definition less_nat where
- less_eq_Suc_le [code func del]: "n < m \<longleftrightarrow> Suc n \<le> m"
+ less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> 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 \<Rightarrow> 'a \<Rightarrow> 'a"
-where
- [code func del]: "of_nat_aux n i = of_nat n + i"
+primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> '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 (\<lambda>i. i + 1) n 0"
+proof (induct n)
+ case 0 then show ?case by simp
+next
+ case (Suc n)
+ have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
+ by (induct n) simp_all
+ from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>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.