1 (* Title: HOL/Arith_Tools.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Author: Amine Chaieb, TU Muenchen |
|
5 *) |
|
6 |
|
7 header {* Setup of arithmetic tools *} |
|
8 |
|
9 theory Arith_Tools |
|
10 imports NatBin |
|
11 uses |
|
12 "~~/src/Provers/Arith/cancel_numeral_factor.ML" |
|
13 "~~/src/Provers/Arith/extract_common_term.ML" |
|
14 "Tools/int_factor_simprocs.ML" |
|
15 "Tools/nat_simprocs.ML" |
|
16 "Tools/Qelim/qelim.ML" |
|
17 begin |
|
18 |
|
19 subsection {* Simprocs for the Naturals *} |
|
20 |
|
21 declaration {* K nat_simprocs_setup *} |
|
22 |
|
23 subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
|
24 |
|
25 text{*Where K above is a literal*} |
|
26 |
|
27 lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)" |
|
28 by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) |
|
29 |
|
30 text {*Now just instantiating @{text n} to @{text "number_of v"} does |
|
31 the right simplification, but with some redundant inequality |
|
32 tests.*} |
|
33 lemma neg_number_of_pred_iff_0: |
|
34 "neg (number_of (Int.pred v)::int) = (number_of v = (0::nat))" |
|
35 apply (subgoal_tac "neg (number_of (Int.pred v)) = (number_of v < Suc 0) ") |
|
36 apply (simp only: less_Suc_eq_le le_0_eq) |
|
37 apply (subst less_number_of_Suc, simp) |
|
38 done |
|
39 |
|
40 text{*No longer required as a simprule because of the @{text inverse_fold} |
|
41 simproc*} |
|
42 lemma Suc_diff_number_of: |
|
43 "Int.Pls < v ==> |
|
44 Suc m - (number_of v) = m - (number_of (Int.pred v))" |
|
45 apply (subst Suc_diff_eq_diff_pred) |
|
46 apply simp |
|
47 apply (simp del: nat_numeral_1_eq_1) |
|
48 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |
|
49 neg_number_of_pred_iff_0) |
|
50 done |
|
51 |
|
52 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
|
53 by (simp add: numerals split add: nat_diff_split) |
|
54 |
|
55 |
|
56 subsubsection{*For @{term nat_case} and @{term nat_rec}*} |
|
57 |
|
58 lemma nat_case_number_of [simp]: |
|
59 "nat_case a f (number_of v) = |
|
60 (let pv = number_of (Int.pred v) in |
|
61 if neg pv then a else f (nat pv))" |
|
62 by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) |
|
63 |
|
64 lemma nat_case_add_eq_if [simp]: |
|
65 "nat_case a f ((number_of v) + n) = |
|
66 (let pv = number_of (Int.pred v) in |
|
67 if neg pv then nat_case a f n else f (nat pv + n))" |
|
68 apply (subst add_eq_if) |
|
69 apply (simp split add: nat.split |
|
70 del: nat_numeral_1_eq_1 |
|
71 add: nat_numeral_1_eq_1 [symmetric] |
|
72 numeral_1_eq_Suc_0 [symmetric] |
|
73 neg_number_of_pred_iff_0) |
|
74 done |
|
75 |
|
76 lemma nat_rec_number_of [simp]: |
|
77 "nat_rec a f (number_of v) = |
|
78 (let pv = number_of (Int.pred v) in |
|
79 if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" |
|
80 apply (case_tac " (number_of v) ::nat") |
|
81 apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) |
|
82 apply (simp split add: split_if_asm) |
|
83 done |
|
84 |
|
85 lemma nat_rec_add_eq_if [simp]: |
|
86 "nat_rec a f (number_of v + n) = |
|
87 (let pv = number_of (Int.pred v) in |
|
88 if neg pv then nat_rec a f n |
|
89 else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
|
90 apply (subst add_eq_if) |
|
91 apply (simp split add: nat.split |
|
92 del: nat_numeral_1_eq_1 |
|
93 add: nat_numeral_1_eq_1 [symmetric] |
|
94 numeral_1_eq_Suc_0 [symmetric] |
|
95 neg_number_of_pred_iff_0) |
|
96 done |
|
97 |
|
98 |
|
99 subsubsection{*Various Other Lemmas*} |
|
100 |
|
101 text {*Evens and Odds, for Mutilated Chess Board*} |
|
102 |
|
103 text{*Lemmas for specialist use, NOT as default simprules*} |
|
104 lemma nat_mult_2: "2 * z = (z+z::nat)" |
|
105 proof - |
|
106 have "2*z = (1 + 1)*z" by simp |
|
107 also have "... = z+z" by (simp add: left_distrib) |
|
108 finally show ?thesis . |
|
109 qed |
|
110 |
|
111 lemma nat_mult_2_right: "z * 2 = (z+z::nat)" |
|
112 by (subst mult_commute, rule nat_mult_2) |
|
113 |
|
114 text{*Case analysis on @{term "n<2"}*} |
|
115 lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" |
|
116 by arith |
|
117 |
|
118 lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)" |
|
119 by arith |
|
120 |
|
121 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" |
|
122 by (simp add: nat_mult_2 [symmetric]) |
|
123 |
|
124 lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" |
|
125 apply (subgoal_tac "m mod 2 < 2") |
|
126 apply (erule less_2_cases [THEN disjE]) |
|
127 apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) |
|
128 done |
|
129 |
|
130 lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)" |
|
131 apply (subgoal_tac "m mod 2 < 2") |
|
132 apply (force simp del: mod_less_divisor, simp) |
|
133 done |
|
134 |
|
135 text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} |
|
136 |
|
137 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
|
138 by simp |
|
139 |
|
140 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
|
141 by simp |
|
142 |
|
143 text{*Can be used to eliminate long strings of Sucs, but not by default*} |
|
144 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
|
145 by simp |
|
146 |
|
147 |
|
148 text{*These lemmas collapse some needless occurrences of Suc: |
|
149 at least three Sucs, since two and fewer are rewritten back to Suc again! |
|
150 We already have some rules to simplify operands smaller than 3.*} |
|
151 |
|
152 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" |
|
153 by (simp add: Suc3_eq_add_3) |
|
154 |
|
155 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" |
|
156 by (simp add: Suc3_eq_add_3) |
|
157 |
|
158 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" |
|
159 by (simp add: Suc3_eq_add_3) |
|
160 |
|
161 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" |
|
162 by (simp add: Suc3_eq_add_3) |
|
163 |
|
164 lemmas Suc_div_eq_add3_div_number_of = |
|
165 Suc_div_eq_add3_div [of _ "number_of v", standard] |
|
166 declare Suc_div_eq_add3_div_number_of [simp] |
|
167 |
|
168 lemmas Suc_mod_eq_add3_mod_number_of = |
|
169 Suc_mod_eq_add3_mod [of _ "number_of v", standard] |
|
170 declare Suc_mod_eq_add3_mod_number_of [simp] |
|
171 |
|
172 |
|
173 subsubsection{*Special Simplification for Constants*} |
|
174 |
|
175 text{*These belong here, late in the development of HOL, to prevent their |
|
176 interfering with proofs of abstract properties of instances of the function |
|
177 @{term number_of}*} |
|
178 |
|
179 text{*These distributive laws move literals inside sums and differences.*} |
|
180 lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard] |
|
181 declare left_distrib_number_of [simp] |
|
182 |
|
183 lemmas right_distrib_number_of = right_distrib [of "number_of v", standard] |
|
184 declare right_distrib_number_of [simp] |
|
185 |
|
186 |
|
187 lemmas left_diff_distrib_number_of = |
|
188 left_diff_distrib [of _ _ "number_of v", standard] |
|
189 declare left_diff_distrib_number_of [simp] |
|
190 |
|
191 lemmas right_diff_distrib_number_of = |
|
192 right_diff_distrib [of "number_of v", standard] |
|
193 declare right_diff_distrib_number_of [simp] |
|
194 |
|
195 |
|
196 text{*These are actually for fields, like real: but where else to put them?*} |
|
197 lemmas zero_less_divide_iff_number_of = |
|
198 zero_less_divide_iff [of "number_of w", standard] |
|
199 declare zero_less_divide_iff_number_of [simp,noatp] |
|
200 |
|
201 lemmas divide_less_0_iff_number_of = |
|
202 divide_less_0_iff [of "number_of w", standard] |
|
203 declare divide_less_0_iff_number_of [simp,noatp] |
|
204 |
|
205 lemmas zero_le_divide_iff_number_of = |
|
206 zero_le_divide_iff [of "number_of w", standard] |
|
207 declare zero_le_divide_iff_number_of [simp,noatp] |
|
208 |
|
209 lemmas divide_le_0_iff_number_of = |
|
210 divide_le_0_iff [of "number_of w", standard] |
|
211 declare divide_le_0_iff_number_of [simp,noatp] |
|
212 |
|
213 |
|
214 (**** |
|
215 IF times_divide_eq_right and times_divide_eq_left are removed as simprules, |
|
216 then these special-case declarations may be useful. |
|
217 |
|
218 text{*These simprules move numerals into numerators and denominators.*} |
|
219 lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)" |
|
220 by (simp add: times_divide_eq) |
|
221 |
|
222 lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)" |
|
223 by (simp add: times_divide_eq) |
|
224 |
|
225 lemmas times_divide_eq_right_number_of = |
|
226 times_divide_eq_right [of "number_of w", standard] |
|
227 declare times_divide_eq_right_number_of [simp] |
|
228 |
|
229 lemmas times_divide_eq_right_number_of = |
|
230 times_divide_eq_right [of _ _ "number_of w", standard] |
|
231 declare times_divide_eq_right_number_of [simp] |
|
232 |
|
233 lemmas times_divide_eq_left_number_of = |
|
234 times_divide_eq_left [of _ "number_of w", standard] |
|
235 declare times_divide_eq_left_number_of [simp] |
|
236 |
|
237 lemmas times_divide_eq_left_number_of = |
|
238 times_divide_eq_left [of _ _ "number_of w", standard] |
|
239 declare times_divide_eq_left_number_of [simp] |
|
240 |
|
241 ****) |
|
242 |
|
243 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks |
|
244 strange, but then other simprocs simplify the quotient.*} |
|
245 |
|
246 lemmas inverse_eq_divide_number_of = |
|
247 inverse_eq_divide [of "number_of w", standard] |
|
248 declare inverse_eq_divide_number_of [simp] |
|
249 |
|
250 |
|
251 text {*These laws simplify inequalities, moving unary minus from a term |
|
252 into the literal.*} |
|
253 lemmas less_minus_iff_number_of = |
|
254 less_minus_iff [of "number_of v", standard] |
|
255 declare less_minus_iff_number_of [simp,noatp] |
|
256 |
|
257 lemmas le_minus_iff_number_of = |
|
258 le_minus_iff [of "number_of v", standard] |
|
259 declare le_minus_iff_number_of [simp,noatp] |
|
260 |
|
261 lemmas equation_minus_iff_number_of = |
|
262 equation_minus_iff [of "number_of v", standard] |
|
263 declare equation_minus_iff_number_of [simp,noatp] |
|
264 |
|
265 |
|
266 lemmas minus_less_iff_number_of = |
|
267 minus_less_iff [of _ "number_of v", standard] |
|
268 declare minus_less_iff_number_of [simp,noatp] |
|
269 |
|
270 lemmas minus_le_iff_number_of = |
|
271 minus_le_iff [of _ "number_of v", standard] |
|
272 declare minus_le_iff_number_of [simp,noatp] |
|
273 |
|
274 lemmas minus_equation_iff_number_of = |
|
275 minus_equation_iff [of _ "number_of v", standard] |
|
276 declare minus_equation_iff_number_of [simp,noatp] |
|
277 |
|
278 |
|
279 text{*To Simplify Inequalities Where One Side is the Constant 1*} |
|
280 |
|
281 lemma less_minus_iff_1 [simp,noatp]: |
|
282 fixes b::"'b::{ordered_idom,number_ring}" |
|
283 shows "(1 < - b) = (b < -1)" |
|
284 by auto |
|
285 |
|
286 lemma le_minus_iff_1 [simp,noatp]: |
|
287 fixes b::"'b::{ordered_idom,number_ring}" |
|
288 shows "(1 \<le> - b) = (b \<le> -1)" |
|
289 by auto |
|
290 |
|
291 lemma equation_minus_iff_1 [simp,noatp]: |
|
292 fixes b::"'b::number_ring" |
|
293 shows "(1 = - b) = (b = -1)" |
|
294 by (subst equation_minus_iff, auto) |
|
295 |
|
296 lemma minus_less_iff_1 [simp,noatp]: |
|
297 fixes a::"'b::{ordered_idom,number_ring}" |
|
298 shows "(- a < 1) = (-1 < a)" |
|
299 by auto |
|
300 |
|
301 lemma minus_le_iff_1 [simp,noatp]: |
|
302 fixes a::"'b::{ordered_idom,number_ring}" |
|
303 shows "(- a \<le> 1) = (-1 \<le> a)" |
|
304 by auto |
|
305 |
|
306 lemma minus_equation_iff_1 [simp,noatp]: |
|
307 fixes a::"'b::number_ring" |
|
308 shows "(- a = 1) = (a = -1)" |
|
309 by (subst minus_equation_iff, auto) |
|
310 |
|
311 |
|
312 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} |
|
313 |
|
314 lemmas mult_less_cancel_left_number_of = |
|
315 mult_less_cancel_left [of "number_of v", standard] |
|
316 declare mult_less_cancel_left_number_of [simp,noatp] |
|
317 |
|
318 lemmas mult_less_cancel_right_number_of = |
|
319 mult_less_cancel_right [of _ "number_of v", standard] |
|
320 declare mult_less_cancel_right_number_of [simp,noatp] |
|
321 |
|
322 lemmas mult_le_cancel_left_number_of = |
|
323 mult_le_cancel_left [of "number_of v", standard] |
|
324 declare mult_le_cancel_left_number_of [simp,noatp] |
|
325 |
|
326 lemmas mult_le_cancel_right_number_of = |
|
327 mult_le_cancel_right [of _ "number_of v", standard] |
|
328 declare mult_le_cancel_right_number_of [simp,noatp] |
|
329 |
|
330 |
|
331 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} |
|
332 |
|
333 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard] |
|
334 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard] |
|
335 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard] |
|
336 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard] |
|
337 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard] |
|
338 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard] |
|
339 |
|
340 |
|
341 subsubsection{*Optional Simplification Rules Involving Constants*} |
|
342 |
|
343 text{*Simplify quotients that are compared with a literal constant.*} |
|
344 |
|
345 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] |
|
346 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] |
|
347 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] |
|
348 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] |
|
349 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] |
|
350 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] |
|
351 |
|
352 |
|
353 text{*Not good as automatic simprules because they cause case splits.*} |
|
354 lemmas divide_const_simps = |
|
355 le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of |
|
356 divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of |
|
357 le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 |
|
358 |
|
359 text{*Division By @{text "-1"}*} |
|
360 |
|
361 lemma divide_minus1 [simp]: |
|
362 "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" |
|
363 by simp |
|
364 |
|
365 lemma minus1_divide [simp]: |
|
366 "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" |
|
367 by (simp add: divide_inverse inverse_minus_eq) |
|
368 |
|
369 lemma half_gt_zero_iff: |
|
370 "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" |
|
371 by auto |
|
372 |
|
373 lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard] |
|
374 declare half_gt_zero [simp] |
|
375 |
|
376 (* The following lemma should appear in Divides.thy, but there the proof |
|
377 doesn't work. *) |
|
378 |
|
379 lemma nat_dvd_not_less: |
|
380 "[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)" |
|
381 by (unfold dvd_def) auto |
|
382 |
|
383 ML {* |
|
384 val divide_minus1 = @{thm divide_minus1}; |
|
385 val minus1_divide = @{thm minus1_divide}; |
|
386 *} |
|
387 |
|
388 end |
|