11 theory RatArith = Rational |
11 theory RatArith = Rational |
12 files ("rat_arith.ML"): |
12 files ("rat_arith.ML"): |
13 |
13 |
14 instance rat :: number .. |
14 instance rat :: number .. |
15 |
15 |
16 defs |
16 defs (overloaded) |
17 rat_number_of_def: |
17 rat_number_of_def: |
18 "number_of v == Fract (number_of v) 1" |
18 "(number_of v :: rat) == of_int (number_of v)" |
19 (*::bin=>rat ::bin=>int*) |
19 (*::bin=>rat ::bin=>int*) |
20 |
20 |
21 theorem number_of_rat: "number_of b = rat (number_of b)" |
|
22 by (simp add: rat_number_of_def rat_def) |
|
23 |
|
24 declare number_of_rat [symmetric, simp] |
|
25 |
21 |
26 lemma rat_numeral_0_eq_0: "Numeral0 = (0::rat)" |
22 lemma rat_numeral_0_eq_0: "Numeral0 = (0::rat)" |
27 by (simp add: rat_number_of_def zero_rat [symmetric]) |
23 by (simp add: rat_number_of_def zero_rat [symmetric]) |
28 |
24 |
29 lemma rat_numeral_1_eq_1: "Numeral1 = (1::rat)" |
25 lemma rat_numeral_1_eq_1: "Numeral1 = (1::rat)" |
31 |
27 |
32 |
28 |
33 subsection{*Arithmetic Operations On Numerals*} |
29 subsection{*Arithmetic Operations On Numerals*} |
34 |
30 |
35 lemma add_rat_number_of [simp]: |
31 lemma add_rat_number_of [simp]: |
36 "(number_of v :: rat) + number_of v' = number_of (bin_add v v')" |
32 "(number_of v :: rat) + number_of v' = number_of (bin_add v v')" |
37 by (simp add: rat_number_of_def add_rat) |
33 by (simp only: rat_number_of_def of_int_add number_of_add) |
38 |
34 |
39 lemma minus_rat_number_of [simp]: |
35 lemma minus_rat_number_of [simp]: |
40 "- (number_of w :: rat) = number_of (bin_minus w)" |
36 "- (number_of w :: rat) = number_of (bin_minus w)" |
41 by (simp add: rat_number_of_def minus_rat) |
37 by (simp only: rat_number_of_def of_int_minus number_of_minus) |
42 |
38 |
43 lemma diff_rat_number_of [simp]: |
39 lemma diff_rat_number_of [simp]: |
44 "(number_of v :: rat) - number_of w = number_of (bin_add v (bin_minus w))" |
40 "(number_of v :: rat) - number_of w = number_of (bin_add v (bin_minus w))" |
45 by (simp add: rat_number_of_def diff_rat) |
41 by (simp only: add_rat_number_of minus_rat_number_of diff_minus) |
46 |
42 |
47 lemma mult_rat_number_of [simp]: |
43 lemma mult_rat_number_of [simp]: |
48 "(number_of v :: rat) * number_of v' = number_of (bin_mult v v')" |
44 "(number_of v :: rat) * number_of v' = number_of (bin_mult v v')" |
49 by (simp add: rat_number_of_def mult_rat) |
45 by (simp only: rat_number_of_def of_int_mult number_of_mult) |
50 |
46 |
51 text{*Lemmas for specialist use, NOT as default simprules*} |
47 text{*Lemmas for specialist use, NOT as default simprules*} |
52 lemma rat_mult_2: "2 * z = (z+z::rat)" |
48 lemma rat_mult_2: "2 * z = (z+z::rat)" |
53 proof - |
49 proof - |
54 have eq: "(2::rat) = 1 + 1" by (simp add: rat_numeral_1_eq_1 [symmetric]) |
50 have eq: "(2::rat) = 1 + 1" |
|
51 by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric]) |
55 thus ?thesis by (simp add: eq left_distrib) |
52 thus ?thesis by (simp add: eq left_distrib) |
56 qed |
53 qed |
57 |
54 |
58 lemma rat_mult_2_right: "z * 2 = (z+z::rat)" |
55 lemma rat_mult_2_right: "z * 2 = (z+z::rat)" |
59 by (subst mult_commute, rule rat_mult_2) |
56 by (subst mult_commute, rule rat_mult_2) |
61 |
58 |
62 subsection{*Comparisons On Numerals*} |
59 subsection{*Comparisons On Numerals*} |
63 |
60 |
64 lemma eq_rat_number_of [simp]: |
61 lemma eq_rat_number_of [simp]: |
65 "((number_of v :: rat) = number_of v') = |
62 "((number_of v :: rat) = number_of v') = |
66 iszero (number_of (bin_add v (bin_minus v')))" |
63 iszero (number_of (bin_add v (bin_minus v')) :: int)" |
67 by (simp add: rat_number_of_def eq_rat) |
64 by (simp add: rat_number_of_def) |
68 |
65 |
69 text{*@{term neg} is used in rewrite rules for binary comparisons*} |
66 text{*@{term neg} is used in rewrite rules for binary comparisons*} |
70 lemma less_rat_number_of [simp]: |
67 lemma less_rat_number_of [simp]: |
71 "((number_of v :: rat) < number_of v') = |
68 "((number_of v :: rat) < number_of v') = |
72 neg (number_of (bin_add v (bin_minus v')))" |
69 neg (number_of (bin_add v (bin_minus v')) :: int)" |
73 by (simp add: rat_number_of_def less_rat) |
70 by (simp add: rat_number_of_def) |
74 |
71 |
75 |
72 |
76 text{*New versions of existing theorems involving 0, 1*} |
73 text{*New versions of existing theorems involving 0, 1*} |
77 |
74 |
78 lemma rat_minus_1_eq_m1 [simp]: "- 1 = (-1::rat)" |
75 lemma rat_minus_1_eq_m1 [simp]: "- 1 = (-1::rat)" |
79 by (simp add: rat_numeral_1_eq_1 [symmetric]) |
76 by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric]) |
80 |
77 |
81 lemma rat_mult_minus1 [simp]: "-1 * z = -(z::rat)" |
78 lemma rat_mult_minus1 [simp]: "-1 * z = -(z::rat)" |
82 proof - |
79 proof - |
83 have "-1 * z = (- 1) * z" by (simp add: rat_minus_1_eq_m1) |
80 have "-1 * z = (- 1) * z" by (simp add: rat_minus_1_eq_m1) |
84 also have "... = - (1 * z)" by (simp only: minus_mult_left) |
81 also have "... = - (1 * z)" by (simp only: minus_mult_left) |
141 |
138 |
142 subsection{*Absolute Value Function for the Rats*} |
139 subsection{*Absolute Value Function for the Rats*} |
143 |
140 |
144 lemma abs_nat_number_of [simp]: |
141 lemma abs_nat_number_of [simp]: |
145 "abs (number_of v :: rat) = |
142 "abs (number_of v :: rat) = |
146 (if neg (number_of v) then number_of (bin_minus v) |
143 (if neg (number_of v :: int) then number_of (bin_minus v) |
147 else number_of v)" |
144 else number_of v)" |
148 by (simp add: abs_if) |
145 by (simp add: abs_if) |
149 |
146 |
150 lemma abs_minus_one [simp]: "abs (-1) = (1::rat)" |
147 lemma abs_minus_one [simp]: "abs (-1) = (1::rat)" |
151 by (simp add: abs_if) |
148 by (simp add: abs_if) |
|
149 |
|
150 declare rat_number_of_def [simp] |
152 |
151 |
153 |
152 |
154 ML |
153 ML |
155 {* |
154 {* |
156 val rat_divide_minus1 = thm "rat_divide_minus1"; |
155 val rat_divide_minus1 = thm "rat_divide_minus1"; |