1.1 --- a/src/HOL/Integ/IntDef.thy Tue May 11 14:00:02 2004 +0200
1.2 +++ b/src/HOL/Integ/IntDef.thy Tue May 11 20:11:08 2004 +0200
1.3 @@ -153,7 +153,7 @@
1.4
1.5 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
1.6
1.7 -lemmas zmult_ac = Ring_and_Field.mult_ac
1.8 +lemmas zmult_ac = OrderedGroup.mult_ac
1.9
1.10 lemma zadd_int: "(int m) + (int n) = int (m + n)"
1.11 by (simp add: int_def add)
1.12 @@ -164,7 +164,7 @@
1.13 lemma int_Suc: "int (Suc m) = 1 + (int m)"
1.14 by (simp add: One_int_def zadd_int)
1.15
1.16 -(*also for the instance declaration int :: plus_ac0*)
1.17 +(*also for the instance declaration int :: comm_monoid_add*)
1.18 lemma zadd_0: "(0::int) + z = z"
1.19 apply (simp add: Zero_int_def int_def)
1.20 apply (cases z, simp add: add)
1.21 @@ -235,8 +235,8 @@
1.22 by (rule trans [OF zmult_commute zmult_1])
1.23
1.24
1.25 -text{*The Integers Form A Ring*}
1.26 -instance int :: ring
1.27 +text{*The Integers Form A comm_ring_1*}
1.28 +instance int :: comm_ring_1
1.29 proof
1.30 fix i j k :: int
1.31 show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
1.32 @@ -368,8 +368,8 @@
1.33 zabs_def: "abs(i::int) == if i < 0 then -i else i"
1.34
1.35
1.36 -text{*The Integers Form an Ordered Ring*}
1.37 -instance int :: ordered_ring
1.38 +text{*The Integers Form an Ordered comm_ring_1*}
1.39 +instance int :: ordered_idom
1.40 proof
1.41 fix i j k :: int
1.42 show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
1.43 @@ -510,7 +510,7 @@
1.44 in theory @{text Ring_and_Field}.
1.45 But is it really better than just rewriting with @{text abs_if}?*}
1.46 lemma abs_split [arith_split]:
1.47 - "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
1.48 + "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
1.49 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
1.50
1.51
1.52 @@ -519,11 +519,11 @@
1.53
1.54 constdefs
1.55
1.56 - neg :: "'a::ordered_ring => bool"
1.57 + neg :: "'a::ordered_idom => bool"
1.58 "neg(Z) == Z < 0"
1.59
1.60 (*For simplifying equalities*)
1.61 - iszero :: "'a::semiring => bool"
1.62 + iszero :: "'a::comm_semiring_1_cancel => bool"
1.63 "iszero z == z = (0)"
1.64
1.65
1.66 @@ -560,9 +560,9 @@
1.67 by (simp add: linorder_not_less neg_def)
1.68
1.69
1.70 -subsection{*Embedding of the Naturals into any Semiring: @{term of_nat}*}
1.71 +subsection{*Embedding of the Naturals into any comm_semiring_1_cancel: @{term of_nat}*}
1.72
1.73 -consts of_nat :: "nat => 'a::semiring"
1.74 +consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
1.75
1.76 primrec
1.77 of_nat_0: "of_nat 0 = 0"
1.78 @@ -581,27 +581,27 @@
1.79 apply (simp_all add: mult_ac add_ac right_distrib)
1.80 done
1.81
1.82 -lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semiring)"
1.83 +lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
1.84 apply (induct m, simp_all)
1.85 apply (erule order_trans)
1.86 apply (rule less_add_one [THEN order_less_imp_le])
1.87 done
1.88
1.89 lemma less_imp_of_nat_less:
1.90 - "m < n ==> of_nat m < (of_nat n::'a::ordered_semiring)"
1.91 + "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
1.92 apply (induct m n rule: diff_induct, simp_all)
1.93 apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
1.94 done
1.95
1.96 lemma of_nat_less_imp_less:
1.97 - "of_nat m < (of_nat n::'a::ordered_semiring) ==> m < n"
1.98 + "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
1.99 apply (induct m n rule: diff_induct, simp_all)
1.100 apply (insert zero_le_imp_of_nat)
1.101 apply (force simp add: linorder_not_less [symmetric])
1.102 done
1.103
1.104 lemma of_nat_less_iff [simp]:
1.105 - "(of_nat m < (of_nat n::'a::ordered_semiring)) = (m<n)"
1.106 + "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
1.107 by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
1.108
1.109 text{*Special cases where either operand is zero*}
1.110 @@ -609,17 +609,17 @@
1.111 declare of_nat_less_iff [of _ 0, simplified, simp]
1.112
1.113 lemma of_nat_le_iff [simp]:
1.114 - "(of_nat m \<le> (of_nat n::'a::ordered_semiring)) = (m \<le> n)"
1.115 + "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
1.116 by (simp add: linorder_not_less [symmetric])
1.117
1.118 text{*Special cases where either operand is zero*}
1.119 declare of_nat_le_iff [of 0, simplified, simp]
1.120 declare of_nat_le_iff [of _ 0, simplified, simp]
1.121
1.122 -text{*The ordering on the semiring is necessary to exclude the possibility of
1.123 +text{*The ordering on the comm_semiring_1_cancel is necessary to exclude the possibility of
1.124 a finite field, which indeed wraps back to zero.*}
1.125 lemma of_nat_eq_iff [simp]:
1.126 - "(of_nat m = (of_nat n::'a::ordered_semiring)) = (m = n)"
1.127 + "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
1.128 by (simp add: order_eq_iff)
1.129
1.130 text{*Special cases where either operand is zero*}
1.131 @@ -627,7 +627,7 @@
1.132 declare of_nat_eq_iff [of _ 0, simplified, simp]
1.133
1.134 lemma of_nat_diff [simp]:
1.135 - "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring)"
1.136 + "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
1.137 by (simp del: of_nat_add
1.138 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
1.139
1.140 @@ -635,7 +635,7 @@
1.141 subsection{*The Set of Natural Numbers*}
1.142
1.143 constdefs
1.144 - Nats :: "'a::semiring set"
1.145 + Nats :: "'a::comm_semiring_1_cancel set"
1.146 "Nats == range of_nat"
1.147
1.148 syntax (xsymbols) Nats :: "'a set" ("\<nat>")
1.149 @@ -681,10 +681,10 @@
1.150 qed
1.151
1.152
1.153 -subsection{*Embedding of the Integers into any Ring: @{term of_int}*}
1.154 +subsection{*Embedding of the Integers into any comm_ring_1: @{term of_int}*}
1.155
1.156 constdefs
1.157 - of_int :: "int => 'a::ring"
1.158 + of_int :: "int => 'a::comm_ring_1"
1.159 "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
1.160
1.161
1.162 @@ -719,7 +719,7 @@
1.163 done
1.164
1.165 lemma of_int_le_iff [simp]:
1.166 - "(of_int w \<le> (of_int z::'a::ordered_ring)) = (w \<le> z)"
1.167 + "(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
1.168 apply (cases w)
1.169 apply (cases z)
1.170 apply (simp add: compare_rls of_int le diff_int_def add minus
1.171 @@ -731,16 +731,16 @@
1.172 declare of_int_le_iff [of _ 0, simplified, simp]
1.173
1.174 lemma of_int_less_iff [simp]:
1.175 - "(of_int w < (of_int z::'a::ordered_ring)) = (w < z)"
1.176 + "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
1.177 by (simp add: linorder_not_le [symmetric])
1.178
1.179 text{*Special cases where either operand is zero*}
1.180 declare of_int_less_iff [of 0, simplified, simp]
1.181 declare of_int_less_iff [of _ 0, simplified, simp]
1.182
1.183 -text{*The ordering on the ring is necessary. See @{text of_nat_eq_iff} above.*}
1.184 +text{*The ordering on the comm_ring_1 is necessary. See @{text of_nat_eq_iff} above.*}
1.185 lemma of_int_eq_iff [simp]:
1.186 - "(of_int w = (of_int z::'a::ordered_ring)) = (w = z)"
1.187 + "(of_int w = (of_int z::'a::ordered_idom)) = (w = z)"
1.188 by (simp add: order_eq_iff)
1.189
1.190 text{*Special cases where either operand is zero*}
1.191 @@ -759,7 +759,7 @@
1.192 subsection{*The Set of Integers*}
1.193
1.194 constdefs
1.195 - Ints :: "'a::ring set"
1.196 + Ints :: "'a::comm_ring_1 set"
1.197 "Ints == range of_int"
1.198
1.199