src/HOL/Real/RatArith.thy
 changeset 14378 69c4d5997669 parent 14365 3d4df8c166ae
```     1.1 --- a/src/HOL/Real/RatArith.thy	Thu Feb 05 10:45:28 2004 +0100
1.2 +++ b/src/HOL/Real/RatArith.thy	Tue Feb 10 12:02:11 2004 +0100
1.3 @@ -13,15 +13,11 @@
1.4
1.5  instance rat :: number ..
1.6
1.7 -defs
1.9    rat_number_of_def:
1.10 -    "number_of v == Fract (number_of v) 1"
1.11 +    "(number_of v :: rat) == of_int (number_of v)"
1.12       (*::bin=>rat         ::bin=>int*)
1.13
1.14 -theorem number_of_rat: "number_of b = rat (number_of b)"
1.15 -  by (simp add: rat_number_of_def rat_def)
1.16 -
1.17 -declare number_of_rat [symmetric, simp]
1.18
1.19  lemma rat_numeral_0_eq_0: "Numeral0 = (0::rat)"
1.20  by (simp add: rat_number_of_def zero_rat [symmetric])
1.21 @@ -33,25 +29,26 @@
1.22  subsection{*Arithmetic Operations On Numerals*}
1.23
1.25 -     "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
1.27 +     "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
1.29
1.30  lemma minus_rat_number_of [simp]:
1.31       "- (number_of w :: rat) = number_of (bin_minus w)"
1.32 -by (simp add: rat_number_of_def minus_rat)
1.33 +by (simp only: rat_number_of_def of_int_minus number_of_minus)
1.34
1.35  lemma diff_rat_number_of [simp]:
1.36     "(number_of v :: rat) - number_of w = number_of (bin_add v (bin_minus w))"
1.37 -by (simp add: rat_number_of_def diff_rat)
1.38 +by (simp only: add_rat_number_of minus_rat_number_of diff_minus)
1.39
1.40  lemma mult_rat_number_of [simp]:
1.41       "(number_of v :: rat) * number_of v' = number_of (bin_mult v v')"
1.42 -by (simp add: rat_number_of_def mult_rat)
1.43 +by (simp only: rat_number_of_def of_int_mult number_of_mult)
1.44
1.45  text{*Lemmas for specialist use, NOT as default simprules*}
1.46  lemma rat_mult_2: "2 * z = (z+z::rat)"
1.47  proof -
1.48 -  have eq: "(2::rat) = 1 + 1" by (simp add: rat_numeral_1_eq_1 [symmetric])
1.49 +  have eq: "(2::rat) = 1 + 1"
1.50 +    by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric])
1.51    thus ?thesis by (simp add: eq left_distrib)
1.52  qed
1.53
1.54 @@ -63,20 +60,20 @@
1.55
1.56  lemma eq_rat_number_of [simp]:
1.57       "((number_of v :: rat) = number_of v') =
1.58 -      iszero (number_of (bin_add v (bin_minus v')))"
1.59 -by (simp add: rat_number_of_def eq_rat)
1.60 +      iszero (number_of (bin_add v (bin_minus v')) :: int)"
1.62
1.63  text{*@{term neg} is used in rewrite rules for binary comparisons*}
1.64  lemma less_rat_number_of [simp]:
1.65       "((number_of v :: rat) < number_of v') =
1.66 -      neg (number_of (bin_add v (bin_minus v')))"
1.67 -by (simp add: rat_number_of_def less_rat)
1.68 +      neg (number_of (bin_add v (bin_minus v')) :: int)"
1.70
1.71
1.72  text{*New versions of existing theorems involving 0, 1*}
1.73
1.74  lemma rat_minus_1_eq_m1 [simp]: "- 1 = (-1::rat)"
1.75 -by (simp add: rat_numeral_1_eq_1 [symmetric])
1.76 +by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric])
1.77
1.78  lemma rat_mult_minus1 [simp]: "-1 * z = -(z::rat)"
1.79  proof -
1.80 @@ -143,13 +140,15 @@
1.81
1.82  lemma abs_nat_number_of [simp]:
1.83       "abs (number_of v :: rat) =
1.84 -        (if neg (number_of v) then number_of (bin_minus v)
1.85 +        (if neg (number_of v :: int)  then number_of (bin_minus v)
1.86           else number_of v)"