1 (* Title: HOL/RatArith.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2004 University of Cambridge |
|
5 |
|
6 Binary arithmetic and simplification for the rats |
|
7 |
|
8 This case is reduced to that for the integers |
|
9 *) |
|
10 |
|
11 theory RatArith = Rational |
|
12 files ("rat_arith.ML"): |
|
13 |
|
14 instance rat :: number .. |
|
15 |
|
16 defs (overloaded) |
|
17 rat_number_of_def: |
|
18 "(number_of v :: rat) == of_int (number_of v)" |
|
19 (*::bin=>rat ::bin=>int*) |
|
20 |
|
21 |
|
22 lemma rat_numeral_0_eq_0: "Numeral0 = (0::rat)" |
|
23 by (simp add: rat_number_of_def zero_rat [symmetric]) |
|
24 |
|
25 lemma rat_numeral_1_eq_1: "Numeral1 = (1::rat)" |
|
26 by (simp add: rat_number_of_def one_rat [symmetric]) |
|
27 |
|
28 |
|
29 subsection{*Arithmetic Operations On Numerals*} |
|
30 |
|
31 lemma add_rat_number_of [simp]: |
|
32 "(number_of v :: rat) + number_of v' = number_of (bin_add v v')" |
|
33 by (simp only: rat_number_of_def of_int_add number_of_add) |
|
34 |
|
35 lemma minus_rat_number_of [simp]: |
|
36 "- (number_of w :: rat) = number_of (bin_minus w)" |
|
37 by (simp only: rat_number_of_def of_int_minus number_of_minus) |
|
38 |
|
39 lemma diff_rat_number_of [simp]: |
|
40 "(number_of v :: rat) - number_of w = number_of (bin_add v (bin_minus w))" |
|
41 by (simp only: add_rat_number_of minus_rat_number_of diff_minus) |
|
42 |
|
43 lemma mult_rat_number_of [simp]: |
|
44 "(number_of v :: rat) * number_of v' = number_of (bin_mult v v')" |
|
45 by (simp only: rat_number_of_def of_int_mult number_of_mult) |
|
46 |
|
47 text{*Lemmas for specialist use, NOT as default simprules*} |
|
48 lemma rat_mult_2: "2 * z = (z+z::rat)" |
|
49 proof - |
|
50 have eq: "(2::rat) = 1 + 1" |
|
51 by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric]) |
|
52 thus ?thesis by (simp add: eq left_distrib) |
|
53 qed |
|
54 |
|
55 lemma rat_mult_2_right: "z * 2 = (z+z::rat)" |
|
56 by (subst mult_commute, rule rat_mult_2) |
|
57 |
|
58 |
|
59 subsection{*Comparisons On Numerals*} |
|
60 |
|
61 lemma eq_rat_number_of [simp]: |
|
62 "((number_of v :: rat) = number_of v') = |
|
63 iszero (number_of (bin_add v (bin_minus v')) :: int)" |
|
64 by (simp add: rat_number_of_def) |
|
65 |
|
66 text{*@{term neg} is used in rewrite rules for binary comparisons*} |
|
67 lemma less_rat_number_of [simp]: |
|
68 "((number_of v :: rat) < number_of v') = |
|
69 neg (number_of (bin_add v (bin_minus v')) :: int)" |
|
70 by (simp add: rat_number_of_def) |
|
71 |
|
72 |
|
73 text{*New versions of existing theorems involving 0, 1*} |
|
74 |
|
75 lemma rat_minus_1_eq_m1 [simp]: "- 1 = (-1::rat)" |
|
76 by (simp del: rat_number_of_def add: rat_numeral_1_eq_1 [symmetric]) |
|
77 |
|
78 lemma rat_mult_minus1 [simp]: "-1 * z = -(z::rat)" |
|
79 proof - |
|
80 have "-1 * z = (- 1) * z" by (simp add: rat_minus_1_eq_m1) |
|
81 also have "... = - (1 * z)" by (simp only: minus_mult_left) |
|
82 also have "... = -z" by simp |
|
83 finally show ?thesis . |
|
84 qed |
|
85 |
|
86 lemma rat_mult_minus1_right [simp]: "z * -1 = -(z::rat)" |
|
87 by (subst mult_commute, rule rat_mult_minus1) |
|
88 |
|
89 |
|
90 subsection{*Simplification of Arithmetic when Nested to the Right*} |
|
91 |
|
92 lemma rat_add_number_of_left [simp]: |
|
93 "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::rat)" |
|
94 by (simp add: add_assoc [symmetric]) |
|
95 |
|
96 lemma rat_mult_number_of_left [simp]: |
|
97 "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::rat)" |
|
98 apply (simp add: mult_assoc [symmetric]) |
|
99 done |
|
100 |
|
101 lemma rat_add_number_of_diff1 [simp]: |
|
102 "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::rat)" |
|
103 apply (unfold diff_rat_def) |
|
104 apply (rule rat_add_number_of_left) |
|
105 done |
|
106 |
|
107 lemma rat_add_number_of_diff2 [simp]: |
|
108 "number_of v + (c - number_of w) = |
|
109 number_of (bin_add v (bin_minus w)) + (c::rat)" |
|
110 apply (subst diff_rat_number_of [symmetric]) |
|
111 apply (simp only: diff_rat_def add_ac) |
|
112 done |
|
113 |
|
114 |
|
115 declare rat_numeral_0_eq_0 [simp] rat_numeral_1_eq_1 [simp] |
|
116 |
|
117 lemmas rat_add_0_left = add_0 [where ?'a = rat] |
|
118 lemmas rat_add_0_right = add_0_right [where ?'a = rat] |
|
119 lemmas rat_mult_1_left = mult_1 [where ?'a = rat] |
|
120 lemmas rat_mult_1_right = mult_1_right [where ?'a = rat] |
|
121 |
|
122 |
|
123 declare diff_rat_def [symmetric] |
|
124 |
|
125 |
|
126 use "rat_arith.ML" |
|
127 |
|
128 setup rat_arith_setup |
|
129 |
|
130 |
|
131 subsubsection{*Division By @{term "-1"}*} |
|
132 |
|
133 lemma rat_divide_minus1 [simp]: "x/-1 = -(x::rat)" |
|
134 by simp |
|
135 |
|
136 lemma rat_minus1_divide [simp]: "-1/(x::rat) = - (1/x)" |
|
137 by (simp add: divide_rat_def inverse_minus_eq) |
|
138 |
|
139 subsection{*Absolute Value Function for the Rats*} |
|
140 |
|
141 lemma abs_nat_number_of [simp]: |
|
142 "abs (number_of v :: rat) = |
|
143 (if neg (number_of v :: int) then number_of (bin_minus v) |
|
144 else number_of v)" |
|
145 by (simp add: abs_if) |
|
146 |
|
147 lemma abs_minus_one [simp]: "abs (-1) = (1::rat)" |
|
148 by (simp add: abs_if) |
|
149 |
|
150 declare rat_number_of_def [simp] |
|
151 |
|
152 |
|
153 ML |
|
154 {* |
|
155 val rat_divide_minus1 = thm "rat_divide_minus1"; |
|
156 val rat_minus1_divide = thm "rat_minus1_divide"; |
|
157 val abs_nat_number_of = thm "abs_nat_number_of"; |
|
158 val abs_minus_one = thm "abs_minus_one"; |
|
159 *} |
|
160 |
|
161 end |
|