generalize of_nat and related constants to class semiring_1
authorhuffman
Wed Jun 06 17:00:09 2007 +0200 (2007-06-06)
changeset 23276a70934b63910
parent 23275 339cdc29b0bc
child 23277 aa158e145ea3
generalize of_nat and related constants to class semiring_1
src/HOL/IntDef.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/IntDef.thy	Wed Jun 06 16:42:39 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Wed Jun 06 17:00:09 2007 +0200
     1.3 @@ -521,7 +521,7 @@
     1.4    [code inline]: "neg Z \<longleftrightarrow> Z < 0"
     1.5  
     1.6  definition (*for simplifying equalities*)
     1.7 -  iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
     1.8 +  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
     1.9  where
    1.10    "iszero z \<longleftrightarrow> z = 0"
    1.11  
    1.12 @@ -561,7 +561,7 @@
    1.13  subsection{*The Set of Natural Numbers*}
    1.14  
    1.15  constdefs
    1.16 -  Nats  :: "'a::semiring_1_cancel set"
    1.17 +  Nats  :: "'a::semiring_1 set"
    1.18    "Nats == range of_nat"
    1.19  
    1.20  notation (xsymbols)
     2.1 --- a/src/HOL/Nat.thy	Wed Jun 06 16:42:39 2007 +0200
     2.2 +++ b/src/HOL/Nat.thy	Wed Jun 06 17:00:09 2007 +0200
     2.3 @@ -1292,9 +1292,9 @@
     2.4  
     2.5  
     2.6  subsection{*Embedding of the Naturals into any
     2.7 -  @{text semiring_1_cancel}: @{term of_nat}*}
     2.8 +  @{text semiring_1}: @{term of_nat}*}
     2.9  
    2.10 -consts of_nat :: "nat => 'a::semiring_1_cancel"
    2.11 +consts of_nat :: "nat => 'a::semiring_1"
    2.12  
    2.13  primrec
    2.14    of_nat_0:   "of_nat 0 = 0"
    2.15 @@ -1353,7 +1353,7 @@
    2.16  lemma of_nat_le_0_iff [simp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
    2.17    by (rule of_nat_le_iff [of _ 0, simplified])
    2.18  
    2.19 -text{*The ordering on the @{text semiring_1_cancel} is necessary
    2.20 +text{*The ordering on the @{text semiring_1} is necessary
    2.21  to exclude the possibility of a finite field, which indeed wraps back to
    2.22  zero.*}
    2.23  lemma of_nat_eq_iff [simp]: