instance inat :: semiring_char_0

--- a/src/HOL/Library/Nat_Infinity.thy	Mon Dec 08 21:33:50 2008 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Tue Dec 09 11:49:12 2008 -0800
@@ -216,6 +216,15 @@
 lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   unfolding iSuc_plus_1 by (simp add: ring_simps)
 
+lemma of_nat_eq_Fin: "of_nat n = Fin n"
+  apply (induct n)
+  apply (simp add: Fin_0)
+  apply (simp add: plus_1_iSuc iSuc_Fin)
+  done
+
+instance inat :: semiring_char_0
+  by default (simp add: of_nat_eq_Fin)
+
 
 subsection {* Ordering *}