added number_semiring class, plus a few new lemmas;
no changes to the simpset yet

--- a/src/HOL/Int.thy	Thu Jun 23 16:31:20 2011 +0200
+++ b/src/HOL/Int.thy	Thu Jun 23 09:04:20 2011 -0700
@@ -941,6 +941,15 @@
 class number_ring = number + comm_ring_1 +
   assumes number_of_eq: "number_of k = of_int k"
 
+class number_semiring = number + comm_semiring_1 +
+  assumes number_of_int: "number_of (of_nat n) = of_nat n"
+
+instance number_ring \<subseteq> number_semiring
+proof
+  fix n show "number_of (of_nat n) = (of_nat n :: 'a)"
+    unfolding number_of_eq by (rule of_int_of_nat_eq)
+qed
+
 text {* self-embedding of the integers *}
 
 instantiation int :: number_ring
@@ -995,13 +1004,23 @@
   Converting numerals 0 and 1 to their abstract versions.
 *}
 
+lemma semiring_numeral_0_eq_0:
+  "Numeral0 = (0::'a::number_semiring)"
+  using number_of_int [where 'a='a and n=0]
+  unfolding numeral_simps by simp
+
+lemma semiring_numeral_1_eq_1:
+  "Numeral1 = (1::'a::number_semiring)"
+  using number_of_int [where 'a='a and n=1]
+  unfolding numeral_simps by simp
+
 lemma numeral_0_eq_0 [simp, code_post]:
   "Numeral0 = (0::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  by (rule semiring_numeral_0_eq_0)
 
 lemma numeral_1_eq_1 [simp, code_post]:
   "Numeral1 = (1::'a::number_ring)"
-  unfolding number_of_eq numeral_simps by simp
+  by (rule semiring_numeral_1_eq_1)
 
 text {*
   Special-case simplification for small constants.
@@ -1467,8 +1486,12 @@
 lemmas add_number_of_eq = number_of_add [symmetric]
 
 text{*Allow 1 on either or both sides*}
+lemma semiring_one_add_one_is_two: "1 + 1 = (2::'a::number_semiring)"
+  using number_of_int [where 'a='a and n="Suc (Suc 0)"]
+  by (simp add: numeral_simps)
+
 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
-by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
+by (rule semiring_one_add_one_is_two)
 
 lemmas add_special =
     one_add_one_is_two
@@ -1555,11 +1578,18 @@
 by (simp add: number_of_eq) 
 
 text{*Lemmas for specialist use, NOT as default simprules*}
+(* TODO: see if semiring duplication can be removed without breaking proofs *)
+lemma semiring_mult_2: "2 * z = (z+z::'a::number_semiring)"
+unfolding semiring_one_add_one_is_two [symmetric] left_distrib by simp
+
+lemma semiring_mult_2_right: "z * 2 = (z+z::'a::number_semiring)"
+by (subst mult_commute, rule semiring_mult_2)
+
 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
-unfolding one_add_one_is_two [symmetric] left_distrib by simp
+by (rule semiring_mult_2)
 
 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
-by (subst mult_commute, rule mult_2)
+by (rule semiring_mult_2_right)
 
 
 subsection{*More Inequality Reasoning*}

--- a/src/HOL/Nat_Numeral.thy	Thu Jun 23 16:31:20 2011 +0200
+++ b/src/HOL/Nat_Numeral.thy	Thu Jun 23 09:04:20 2011 -0700
@@ -15,14 +15,17 @@
   Arithmetic for naturals is reduced to that for the non-negative integers.
 *}
 
-instantiation nat :: number
+instantiation nat :: number_semiring
 begin
 
 definition
   nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
 
-instance ..
-
+instance proof
+  fix n show "number_of (int n) = (of_nat n :: nat)"
+    unfolding nat_number_of_def number_of_eq by simp
+qed
+ 
 end
 
 lemma [code_post]:
@@ -250,9 +253,9 @@
 end
 
 lemma power2_sum:
-  fixes x y :: "'a::number_ring"
+  fixes x y :: "'a::number_semiring"
   shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
-  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
+  by (simp add: algebra_simps power2_eq_square semiring_mult_2_right)
 
 lemma power2_diff:
   fixes x y :: "'a::number_ring"
@@ -345,6 +348,9 @@
   unfolding nat_number_of_def number_of_is_id neg_def
   by simp
 
+lemma nonneg_int_cases:
+  fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
+  using assms by (cases k, simp, simp)
 
 subsubsection{*Successor *}
 
@@ -390,7 +396,30 @@
   by (simp add: nat_add_distrib)
 
 lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
-  by (rule int_int_eq [THEN iffD1]) simp
+  by (rule semiring_one_add_one_is_two)
+
+text {* TODO: replace simp rules above with these generic ones: *}
+
+lemma semiring_add_number_of:
+  "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
+    (number_of v :: 'a::number_semiring) + number_of v' = number_of (v + v')"
+  unfolding Int.Pls_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int of_nat_add [symmetric])
+
+lemma semiring_number_of_add_1:
+  "Int.Pls \<le> v \<Longrightarrow>
+    number_of v + (1::'a::number_semiring) = number_of (Int.succ v)"
+  unfolding Int.Pls_def Int.succ_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
+
+lemma semiring_1_add_number_of:
+  "Int.Pls \<le> v \<Longrightarrow>
+    (1::'a::number_semiring) + number_of v = number_of (Int.succ v)"
+  unfolding Int.Pls_def Int.succ_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric])
 
 
 subsubsection{*Subtraction *}
@@ -426,6 +455,14 @@
   unfolding nat_number_of_def number_of_is_id numeral_simps
   by (simp add: nat_mult_distrib)
 
+(* TODO: replace mult_nat_number_of with this next rule *)
+lemma semiring_mult_number_of:
+  "\<lbrakk>Int.Pls \<le> v; Int.Pls \<le> v'\<rbrakk> \<Longrightarrow>
+    (number_of v :: 'a::number_semiring) * number_of v' = number_of (v * v')"
+  unfolding Int.Pls_def
+  by (elim nonneg_int_cases,
+    simp only: number_of_int of_nat_mult [symmetric])
+
 
 subsection{*Comparisons*}
 
@@ -842,10 +879,10 @@
 
 text{*Lemmas for specialist use, NOT as default simprules*}
 lemma nat_mult_2: "2 * z = (z+z::nat)"
-unfolding nat_1_add_1 [symmetric] left_distrib by simp
+by (rule semiring_mult_2)
 
 lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
-by (subst mult_commute, rule nat_mult_2)
+by (rule semiring_mult_2_right)
 
 text{*Case analysis on @{term "n<2"}*}
 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"