--- 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)
--- 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]
--- 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]:
--- 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