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