generalize lemma of_nat_number_of_eq to class number_semiring

--- a/src/HOL/Nat_Numeral.thy	Fri Sep 09 15:14:59 2011 +0200
+++ b/src/HOL/Nat_Numeral.thy	Fri Sep 09 09:31:04 2011 -0700
@@ -791,15 +791,16 @@
 lemma of_nat_number_of_lemma:
      "of_nat (number_of v :: nat) =  
          (if 0 \<le> (number_of v :: int) 
-          then (number_of v :: 'a :: number_ring)
+          then (number_of v :: 'a :: number_semiring)
           else 0)"
-by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat)
+  by (auto simp add: int_number_of_def nat_number_of_def number_of_int
+    elim!: nonneg_int_cases)
 
 lemma of_nat_number_of_eq [simp]:
      "of_nat (number_of v :: nat) =  
          (if neg (number_of v :: int) then 0  
-          else (number_of v :: 'a :: number_ring))"
-by (simp only: of_nat_number_of_lemma neg_def, simp) 
+          else (number_of v :: 'a :: number_semiring))"
+  by (simp only: of_nat_number_of_lemma neg_def, simp)
 
 
 subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}