new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas

--- a/src/HOL/Hyperreal/StarClasses.thy	Thu May 10 00:39:56 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Thu May 10 02:51:53 2007 +0200
@@ -458,6 +458,9 @@
 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 :: (number_ring) number_ring
 by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
 

--- a/src/HOL/Integ/IntDef.thy	Thu May 10 00:39:56 2007 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu May 10 02:51:53 2007 +0200
@@ -667,12 +667,18 @@
 lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified]
 lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified]
 
+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"
 
-text{*The ordering on the @{text ring_1} is necessary.
- See @{text of_nat_eq_iff} above.*}
 lemma of_int_eq_iff [simp]:
-     "(of_int w = (of_int z::'a::ordered_idom)) = (w = z)"
-by (simp add: order_eq_iff)
+     "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
+by (safe elim!: of_int_inject)
+
+text{*Every @{text ordered_idom} has characteristic zero.*}
+instance ordered_idom < ring_char_0
+by intro_classes (simp add: order_eq_iff)
 
 text{*Special cases where either operand is zero*}
 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
@@ -881,4 +887,4 @@
 val abs_split = @{thm abs_split};
 *}
 
-end
\ No newline at end of file
+end

--- a/src/HOL/Integ/Numeral.thy	Thu May 10 00:39:56 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy	Thu May 10 02:51:53 2007 +0200
@@ -368,9 +368,28 @@
 
 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
 
+lemma Ints_double_eq_0_iff:
+  assumes in_Ints: "a \<in> Ints"
+  shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
+proof -
+  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
+  then obtain z where a: "a = of_int z" ..
+  show ?thesis
+  proof
+    assume "a = 0"
+    thus "a + a = 0" by simp
+  next
+    assume eq: "a + a = 0"
+    hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
+    hence "z + z = 0" by (simp only: of_int_eq_iff)
+    hence "z = 0" by (simp only: double_eq_0_iff)
+    thus "a = 0" by (simp add: a)
+  qed
+qed
+
 lemma Ints_odd_nonzero:
   assumes in_Ints: "a \<in> Ints"
-  shows "1 + a + a \<noteq> (0::'a::ordered_idom)"
+  shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
@@ -389,17 +408,17 @@
 
 lemma iszero_number_of_BIT:
   "iszero (number_of (w BIT x)::'a) = 
-   (x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))"
-  by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff 
+   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
+  by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff 
     Ints_odd_nonzero Ints_def split: bit.split)
 
 lemma iszero_number_of_0:
-  "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
+  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 
   iszero (number_of w :: 'a)"
   by (simp only: iszero_number_of_BIT simp_thms)
 
 lemma iszero_number_of_1:
-  "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
+  "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
   by (simp add: iszero_number_of_BIT)