# HG changeset patch
# User huffman
# Date 1181155744 -7200
# Node ID dfc459989d24575d33cae7e61472166aa6dabbd0
# Parent  e26ec695c9b3375dc4357d1ff489afc2f8f172f9
add axclass semiring_char_0 for types where of_nat is injective

diff -r e26ec695c9b3 -r dfc459989d24 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Wed Jun 06 19:12:59 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Wed Jun 06 20:49:04 2007 +0200
@@ -460,8 +460,10 @@
 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
 by transfer (rule refl)
 
-instance star :: (ring_char_0) ring_char_0
-by (intro_classes, simp only: star_of_int_def star_of_eq of_int_eq_iff)
+instance star :: (semiring_char_0) semiring_char_0
+by (intro_classes, simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
+
+instance star :: (ring_char_0) ring_char_0 ..
 
 instance star :: (number_ring) number_ring
 by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
diff -r e26ec695c9b3 -r dfc459989d24 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Jun 06 19:12:59 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Jun 06 20:49:04 2007 +0200
@@ -669,16 +669,17 @@
 
 text{*Class for unital rings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
-axclass ring_char_0 < ring_1
-  of_int_inject: "of_int w = of_int z ==> w = z"
+axclass ring_char_0 < ring_1, semiring_char_0
 
 lemma of_int_eq_iff [simp]:
      "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
-by (safe elim!: of_int_inject)
+apply (cases w, cases z, simp add: of_int)
+apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
+apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
+done
 
 text{*Every @{text ordered_idom} has characteristic zero.*}
-instance ordered_idom < ring_char_0
-by intro_classes (simp add: order_eq_iff)
+instance ordered_idom < ring_char_0 ..
 
 text{*Special cases where either operand is zero*}
 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
diff -r e26ec695c9b3 -r dfc459989d24 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jun 06 19:12:59 2007 +0200
+++ b/src/HOL/Nat.thy	Wed Jun 06 20:49:04 2007 +0200
@@ -1353,17 +1353,19 @@
 lemma of_nat_le_0_iff [simp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
   by (rule of_nat_le_iff [of _ 0, simplified])
 
-text{*The ordering on the @{text semiring_1} is necessary
-to exclude the possibility of a finite field, which indeed wraps back to
-zero.*}
-lemma of_nat_eq_iff [simp]:
-    "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
-  by (simp add: order_eq_iff)
+text{*Class for unital semirings with characteristic zero.
+ Includes non-ordered rings like the complex numbers.*}
+axclass semiring_char_0 < semiring_1
+  of_nat_eq_iff [simp]: "(of_nat m = of_nat n) = (m = n)"
+
+text{*Every @{text ordered_semidom} has characteristic zero.*}
+instance ordered_semidom < semiring_char_0
+by intro_classes (simp add: order_eq_iff)
 
 text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp]: "((0::'a::ordered_semidom) = of_nat n) = (0 = n)"
+lemma of_nat_0_eq_iff [simp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
   by (rule of_nat_eq_iff [of 0, simplified])
-lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::ordered_semidom)) = (m = 0)"
+lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   by (rule of_nat_eq_iff [of _ 0, simplified])
 
 lemma of_nat_diff [simp]:
diff -r e26ec695c9b3 -r dfc459989d24 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Wed Jun 06 19:12:59 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Wed Jun 06 20:49:04 2007 +0200
@@ -248,12 +248,11 @@
 text{*Every real algebra has characteristic zero*}
 instance real_algebra_1 < ring_char_0
 proof
-  fix w z :: int
-  assume "of_int w = (of_int z::'a)"
-  hence "of_real (of_int w) = (of_real (of_int z)::'a)"
-    by (simp only: of_real_of_int_eq)
-  thus "w = z"
-    by (simp only: of_real_eq_iff of_int_eq_iff)
+  fix m n :: nat
+  have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
+    by (simp only: of_real_eq_iff of_nat_eq_iff)
+  thus "(of_nat m = (of_nat n::'a)) = (m = n)"
+    by (simp only: of_real_of_nat_eq)
 qed