wneuper/isa: comparison src/HOL/Integ/IntDef.thy

equal deleted inserted replaced

-:77ea79aed99d
+:83f1a514dcb4
 apply (rule zadd_commute)
 done
 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
-lemmas zmult_ac = Ring_and_Field.mult_ac
+lemmas zmult_ac = OrderedGroup.mult_ac
 lemma zadd_int: "(int m) + (int n) = int (m + n)"
 by (simp add: int_def add)
 lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
 by (simp add: zadd_int zadd_assoc [symmetric])
 lemma int_Suc: "int (Suc m) = 1 + (int m)"
 by (simp add: One_int_def zadd_int)
-(*also for the instance declaration int :: plus_ac0*)
+(*also for the instance declaration int :: comm_monoid_add*)
 lemma zadd_0: "(0::int) + z = z"
 apply (simp add: Zero_int_def int_def)
 apply (cases z, simp add: add)
 done
 lemma zmult_1_right: "z * (1::int) = z"
 by (rule trans [OF zmult_commute zmult_1])
-text{*The Integers Form A Ring*}
+text{*The Integers Form A comm_ring_1*}
-instance int :: ring
+instance int :: comm_ring_1
 proof
 fix i j k :: int
 show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
 show "i + j = j + i" by (simp add: zadd_commute)
 show "0 + i = i" by (rule zadd_0)
 defs (overloaded)
 zabs_def:  "abs(i::int) == if i < 0 then -i else i"
-text{*The Integers Form an Ordered Ring*}
+text{*The Integers Form an Ordered comm_ring_1*}
-instance int :: ordered_ring
+instance int :: ordered_idom
 proof
 fix i j k :: int
 show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
 show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
 show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
 text{*This version is proved for all ordered rings, not just integers!
 It is proved here because attribute @{text arith_split} is not available
 in theory @{text Ring_and_Field}.
 But is it really better than just rewriting with @{text abs_if}?*}
 lemma abs_split [arith_split]:
-"P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+"P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 subsection{*The Constants @{term neg} and @{term iszero}*}
 constdefs
-neg   :: "'a::ordered_ring => bool"
+neg   :: "'a::ordered_idom => bool"
 "neg(Z) == Z < 0"
 (*For simplifying equalities*)
-iszero :: "'a::semiring => bool"
+iszero :: "'a::comm_semiring_1_cancel => bool"
 "iszero z == z = (0)"
 lemma not_neg_int [simp]: "~ neg(int n)"
 by (simp add: neg_def)
 lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
 by (simp add: linorder_not_less neg_def)
-subsection{*Embedding of the Naturals into any Semiring: @{term of_nat}*}
+subsection{*Embedding of the Naturals into any comm_semiring_1_cancel: @{term of_nat}*}
-consts of_nat :: "nat => 'a::semiring"
+consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
 primrec
 of_nat_0:   "of_nat 0 = 0"
 of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
 lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
 apply (induct m)
 apply (simp_all add: mult_ac add_ac right_distrib)
 done
-lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semiring)"
+lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
 apply (induct m, simp_all)
 apply (erule order_trans)
 apply (rule less_add_one [THEN order_less_imp_le])
 done
 lemma less_imp_of_nat_less:
-"m < n ==> of_nat m < (of_nat n::'a::ordered_semiring)"
+"m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
 apply (induct m n rule: diff_induct, simp_all)
 apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
 done
 lemma of_nat_less_imp_less:
-"of_nat m < (of_nat n::'a::ordered_semiring) ==> m < n"
+"of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
 apply (induct m n rule: diff_induct, simp_all)
 apply (insert zero_le_imp_of_nat)
 apply (force simp add: linorder_not_less [symmetric])
 done
 lemma of_nat_less_iff [simp]:
-"(of_nat m < (of_nat n::'a::ordered_semiring)) = (m<n)"
+"(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
 by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
 text{*Special cases where either operand is zero*}
 declare of_nat_less_iff [of 0, simplified, simp]
 declare of_nat_less_iff [of _ 0, simplified, simp]
 lemma of_nat_le_iff [simp]:
-"(of_nat m \<le> (of_nat n::'a::ordered_semiring)) = (m \<le> n)"
+"(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
 by (simp add: linorder_not_less [symmetric])
 text{*Special cases where either operand is zero*}
 declare of_nat_le_iff [of 0, simplified, simp]
 declare of_nat_le_iff [of _ 0, simplified, simp]
-text{*The ordering on the semiring is necessary to exclude the possibility of
+text{*The ordering on the comm_semiring_1_cancel 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_semiring)) = (m = n)"
+"(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
 by (simp add: order_eq_iff)
 text{*Special cases where either operand is zero*}
 declare of_nat_eq_iff [of 0, simplified, simp]
 declare of_nat_eq_iff [of _ 0, simplified, simp]
 lemma of_nat_diff [simp]:
-"n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring)"
+"n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
 by (simp del: of_nat_add
 	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
 subsection{*The Set of Natural Numbers*}
 constdefs
-Nats  :: "'a::semiring set"
+Nats  :: "'a::comm_semiring_1_cancel set"
 "Nats == range of_nat"
 syntax (xsymbols)    Nats :: "'a set"   ("\<nat>")
 lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
 fix n
 show "of_nat n = id n"  by (induct n, simp_all)
 qed
-subsection{*Embedding of the Integers into any Ring: @{term of_int}*}
+subsection{*Embedding of the Integers into any comm_ring_1: @{term of_int}*}
 constdefs
-of_int :: "int => 'a::ring"
+of_int :: "int => 'a::comm_ring_1"
 "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
 apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib
 mult add_ac)
 done
 lemma of_int_le_iff [simp]:
-"(of_int w \<le> (of_int z::'a::ordered_ring)) = (w \<le> z)"
+"(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)"
 apply (cases w)
 apply (cases z)
 apply (simp add: compare_rls of_int le diff_int_def add minus
 of_nat_add [symmetric]   del: of_nat_add)
 done
 text{*Special cases where either operand is zero*}
 declare of_int_le_iff [of 0, simplified, simp]
 declare of_int_le_iff [of _ 0, simplified, simp]
 lemma of_int_less_iff [simp]:
-"(of_int w < (of_int z::'a::ordered_ring)) = (w < z)"
+"(of_int w < (of_int z::'a::ordered_idom)) = (w < z)"
 by (simp add: linorder_not_le [symmetric])
 text{*Special cases where either operand is zero*}
 declare of_int_less_iff [of 0, simplified, simp]
 declare of_int_less_iff [of _ 0, simplified, simp]
-text{*The ordering on the ring is necessary. See @{text of_nat_eq_iff} above.*}
+text{*The ordering on the comm_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_ring)) = (w = z)"
+"(of_int w = (of_int z::'a::ordered_idom)) = (w = z)"
 by (simp add: order_eq_iff)
 text{*Special cases where either operand is zero*}
 declare of_int_eq_iff [of 0, simplified, simp]
 declare of_int_eq_iff [of _ 0, simplified, simp]
 subsection{*The Set of Integers*}
 constdefs
-Ints  :: "'a::ring set"
+Ints  :: "'a::comm_ring_1 set"
 "Ints == range of_int"
 syntax (xsymbols)
 Ints      :: "'a set"                   ("\<int>")

changeset 14738	83f1a514dcb4
parent 14691	e1eedc8cad37
child 14740	c8e1937110c2