add axclass semiring_char_0 for types where of_nat is injective
authorhuffman
Wed Jun 06 20:49:04 2007 +0200 (2007-06-06)
changeset 23282dfc459989d24
parent 23281 e26ec695c9b3
child 23283 c7ab7051aba0
add axclass semiring_char_0 for types where of_nat is injective
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IntDef.thy
src/HOL/Nat.thy
src/HOL/Real/RealVector.thy
     1.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Wed Jun 06 19:12:59 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Wed Jun 06 20:49:04 2007 +0200
     1.3 @@ -460,8 +460,10 @@
     1.4  lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
     1.5  by transfer (rule refl)
     1.6  
     1.7 -instance star :: (ring_char_0) ring_char_0
     1.8 -by (intro_classes, simp only: star_of_int_def star_of_eq of_int_eq_iff)
     1.9 +instance star :: (semiring_char_0) semiring_char_0
    1.10 +by (intro_classes, simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
    1.11 +
    1.12 +instance star :: (ring_char_0) ring_char_0 ..
    1.13  
    1.14  instance star :: (number_ring) number_ring
    1.15  by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
     2.1 --- a/src/HOL/IntDef.thy	Wed Jun 06 19:12:59 2007 +0200
     2.2 +++ b/src/HOL/IntDef.thy	Wed Jun 06 20:49:04 2007 +0200
     2.3 @@ -669,16 +669,17 @@
     2.4  
     2.5  text{*Class for unital rings with characteristic zero.
     2.6   Includes non-ordered rings like the complex numbers.*}
     2.7 -axclass ring_char_0 < ring_1
     2.8 -  of_int_inject: "of_int w = of_int z ==> w = z"
     2.9 +axclass ring_char_0 < ring_1, semiring_char_0
    2.10  
    2.11  lemma of_int_eq_iff [simp]:
    2.12       "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"
    2.13 -by (safe elim!: of_int_inject)
    2.14 +apply (cases w, cases z, simp add: of_int)
    2.15 +apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
    2.16 +apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
    2.17 +done
    2.18  
    2.19  text{*Every @{text ordered_idom} has characteristic zero.*}
    2.20 -instance ordered_idom < ring_char_0
    2.21 -by intro_classes (simp add: order_eq_iff)
    2.22 +instance ordered_idom < ring_char_0 ..
    2.23  
    2.24  text{*Special cases where either operand is zero*}
    2.25  lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified]
     3.1 --- a/src/HOL/Nat.thy	Wed Jun 06 19:12:59 2007 +0200
     3.2 +++ b/src/HOL/Nat.thy	Wed Jun 06 20:49:04 2007 +0200
     3.3 @@ -1353,17 +1353,19 @@
     3.4  lemma of_nat_le_0_iff [simp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
     3.5    by (rule of_nat_le_iff [of _ 0, simplified])
     3.6  
     3.7 -text{*The ordering on the @{text semiring_1} is necessary
     3.8 -to exclude the possibility of a finite field, which indeed wraps back to
     3.9 -zero.*}
    3.10 -lemma of_nat_eq_iff [simp]:
    3.11 -    "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
    3.12 -  by (simp add: order_eq_iff)
    3.13 +text{*Class for unital semirings with characteristic zero.
    3.14 + Includes non-ordered rings like the complex numbers.*}
    3.15 +axclass semiring_char_0 < semiring_1
    3.16 +  of_nat_eq_iff [simp]: "(of_nat m = of_nat n) = (m = n)"
    3.17 +
    3.18 +text{*Every @{text ordered_semidom} has characteristic zero.*}
    3.19 +instance ordered_semidom < semiring_char_0
    3.20 +by intro_classes (simp add: order_eq_iff)
    3.21  
    3.22  text{*Special cases where either operand is zero*}
    3.23 -lemma of_nat_0_eq_iff [simp]: "((0::'a::ordered_semidom) = of_nat n) = (0 = n)"
    3.24 +lemma of_nat_0_eq_iff [simp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
    3.25    by (rule of_nat_eq_iff [of 0, simplified])
    3.26 -lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::ordered_semidom)) = (m = 0)"
    3.27 +lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
    3.28    by (rule of_nat_eq_iff [of _ 0, simplified])
    3.29  
    3.30  lemma of_nat_diff [simp]:
     4.1 --- a/src/HOL/Real/RealVector.thy	Wed Jun 06 19:12:59 2007 +0200
     4.2 +++ b/src/HOL/Real/RealVector.thy	Wed Jun 06 20:49:04 2007 +0200
     4.3 @@ -248,12 +248,11 @@
     4.4  text{*Every real algebra has characteristic zero*}
     4.5  instance real_algebra_1 < ring_char_0
     4.6  proof
     4.7 -  fix w z :: int
     4.8 -  assume "of_int w = (of_int z::'a)"
     4.9 -  hence "of_real (of_int w) = (of_real (of_int z)::'a)"
    4.10 -    by (simp only: of_real_of_int_eq)
    4.11 -  thus "w = z"
    4.12 -    by (simp only: of_real_eq_iff of_int_eq_iff)
    4.13 +  fix m n :: nat
    4.14 +  have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
    4.15 +    by (simp only: of_real_eq_iff of_nat_eq_iff)
    4.16 +  thus "(of_nat m = (of_nat n::'a)) = (m = n)"
    4.17 +    by (simp only: of_real_of_nat_eq)
    4.18  qed
    4.19  
    4.20