# HG changeset patch
# User huffman
# Date 1315585864 25200
# Node ID 73d5b722c4b4999c162824864131eb050ba79f1e
# Parent  3d44712a5f66375075ffbb3de26bc488f015d14b
generalize lemma of_nat_number_of_eq to class number_semiring

diff -r 3d44712a5f66 -r 73d5b722c4b4 src/HOL/Nat_Numeral.thy
--- 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"}*}