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.8 +defs (overloaded)
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.24 lemma add_rat_number_of [simp]:
1.25 - "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
1.26 -by (simp add: rat_number_of_def add_rat)
1.27 + "(number_of v :: rat) + number_of v' = number_of (bin_add v v')"
1.28 +by (simp only: rat_number_of_def of_int_add number_of_add)
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.61 +by (simp add: rat_number_of_def)
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.69 +by (simp add: rat_number_of_def)
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)"
1.87 -by (simp add: abs_if)
1.88 +by (simp add: abs_if)
1.89
1.90 lemma abs_minus_one [simp]: "abs (-1) = (1::rat)"
1.91 by (simp add: abs_if)
1.92
1.93 +declare rat_number_of_def [simp]
1.94 +
1.95
1.96 ML
1.97 {*