1465
|
1 |
(* Title: HOL/Hoare/Arith2.ML
|
1335
|
2 |
ID: $Id$
|
1465
|
3 |
Author: Norbert Galm
|
1335
|
4 |
Copyright 1995 TUM
|
|
5 |
|
|
6 |
More arithmetic lemmas.
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Arith2;
|
|
10 |
|
|
11 |
|
|
12 |
(*** HOL lemmas ***)
|
|
13 |
|
|
14 |
|
|
15 |
val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P";
|
|
16 |
by (cut_facts_tac [prem1 COMP impI,prem2] 1);
|
|
17 |
by (fast_tac HOL_cs 1);
|
|
18 |
val not_imp_swap=result();
|
|
19 |
|
|
20 |
|
|
21 |
(*** analogue of diff_induct, for simultaneous induction over 3 vars ***)
|
|
22 |
|
|
23 |
val prems = goal Nat.thy
|
|
24 |
"[| !!x. P x 0 0; \
|
|
25 |
\ !!y. P 0 (Suc y) 0; \
|
|
26 |
\ !!z. P 0 0 (Suc z); \
|
|
27 |
\ !!x y. [| P x y 0 |] ==> P (Suc x) (Suc y) 0; \
|
|
28 |
\ !!x z. [| P x 0 z |] ==> P (Suc x) 0 (Suc z); \
|
|
29 |
\ !!y z. [| P 0 y z |] ==> P 0 (Suc y) (Suc z); \
|
|
30 |
\ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \
|
|
31 |
\ |] ==> P m n k";
|
|
32 |
by (res_inst_tac [("x","m")] spec 1);
|
1476
|
33 |
br diff_induct 1;
|
|
34 |
br allI 1;
|
|
35 |
br allI 2;
|
1335
|
36 |
by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
|
|
37 |
by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
|
1476
|
38 |
br allI 7;
|
1335
|
39 |
by (nat_ind_tac "xa" 7);
|
|
40 |
by (ALLGOALS (resolve_tac prems));
|
1476
|
41 |
ba 1;
|
|
42 |
ba 1;
|
1335
|
43 |
by (fast_tac HOL_cs 1);
|
|
44 |
by (fast_tac HOL_cs 1);
|
|
45 |
qed "diff_induct3";
|
|
46 |
|
|
47 |
(*** interaction of + and - ***)
|
|
48 |
|
|
49 |
val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
|
|
50 |
by (cut_facts_tac prems 1);
|
1476
|
51 |
br mp 1;
|
|
52 |
ba 2;
|
1335
|
53 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
54 |
by (ALLGOALS Asm_simp_tac);
|
|
55 |
qed "diff_not_assoc";
|
|
56 |
|
|
57 |
val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
|
|
58 |
by (cut_facts_tac prems 1);
|
1476
|
59 |
bd conjI 1;
|
|
60 |
ba 1;
|
1335
|
61 |
by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
|
1476
|
62 |
ba 2;
|
1335
|
63 |
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
|
|
64 |
by (ALLGOALS Asm_simp_tac);
|
1476
|
65 |
br impI 1;
|
1335
|
66 |
by (dres_inst_tac [("P","~x<y")] conjE 1);
|
1476
|
67 |
ba 2;
|
|
68 |
br (Suc_diff_n RS sym) 1;
|
|
69 |
br le_less_trans 1;
|
|
70 |
be (not_less_eq RS subst) 2;
|
|
71 |
br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
|
1335
|
72 |
qed "diff_add_not_assoc";
|
|
73 |
|
|
74 |
val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
|
|
75 |
by (cut_facts_tac prems 1);
|
1476
|
76 |
br mp 1;
|
|
77 |
ba 2;
|
1335
|
78 |
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
|
|
79 |
by (ALLGOALS Asm_simp_tac);
|
|
80 |
qed "add_diff_assoc";
|
|
81 |
|
|
82 |
(*** more ***)
|
|
83 |
|
|
84 |
val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
|
1476
|
85 |
br iffI 1;
|
1335
|
86 |
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
|
|
87 |
by (Asm_full_simp_tac 1);
|
1476
|
88 |
be disjE 1;
|
|
89 |
be (less_not_refl2 RS not_sym) 1;
|
|
90 |
be less_not_refl2 1;
|
1335
|
91 |
qed "not_eq_eq_less_or_gr";
|
|
92 |
|
|
93 |
val [prem] = goal Arith.thy "m<n ==> n-m~=0";
|
|
94 |
by (rtac (prem RS rev_mp) 1);
|
|
95 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
96 |
by (ALLGOALS Asm_simp_tac);
|
|
97 |
qed "less_imp_diff_not_0";
|
|
98 |
|
|
99 |
(*******************************************************************)
|
|
100 |
|
|
101 |
val prems = goal Arith.thy "(i::nat)<j ==> k+i<k+j";
|
|
102 |
by (cut_facts_tac prems 1);
|
|
103 |
by (nat_ind_tac "k" 1);
|
|
104 |
by (ALLGOALS Asm_simp_tac);
|
|
105 |
qed "add_less_mono_l";
|
|
106 |
|
|
107 |
val prems = goal Arith.thy "~(i::nat)<j ==> ~k+i<k+j";
|
|
108 |
by (cut_facts_tac prems 1);
|
|
109 |
by (nat_ind_tac "k" 1);
|
|
110 |
by (ALLGOALS Asm_simp_tac);
|
|
111 |
qed "add_not_less_mono_l";
|
|
112 |
|
|
113 |
val prems = goal Arith.thy "[|0<k; m<(n::nat)|] ==> m*k<n*k";
|
|
114 |
by (cut_facts_tac prems 1);
|
|
115 |
by (res_inst_tac [("n","k")] natE 1);
|
|
116 |
by (ALLGOALS Asm_full_simp_tac);
|
|
117 |
by (nat_ind_tac "x" 1);
|
1476
|
118 |
be add_less_mono 2;
|
1335
|
119 |
by (ALLGOALS Asm_full_simp_tac);
|
|
120 |
qed "mult_less_mono_r";
|
|
121 |
|
|
122 |
val prems = goal Arith.thy "~m<(n::nat) ==> ~m*k<n*k";
|
|
123 |
by (cut_facts_tac prems 1);
|
|
124 |
by (nat_ind_tac "k" 1);
|
|
125 |
by (ALLGOALS Simp_tac);
|
|
126 |
by (fold_goals_tac [le_def]);
|
1476
|
127 |
be add_le_mono 1;
|
|
128 |
ba 1;
|
1335
|
129 |
qed "mult_not_less_mono_r";
|
|
130 |
|
|
131 |
val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
|
|
132 |
by (cut_facts_tac prems 1);
|
|
133 |
by (nat_ind_tac "k" 1);
|
|
134 |
by (ALLGOALS Asm_simp_tac);
|
|
135 |
qed "mult_eq_mono_r";
|
|
136 |
|
|
137 |
val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
|
|
138 |
by (cut_facts_tac prems 1);
|
|
139 |
by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
|
1476
|
140 |
br (less_not_refl2 RS not_sym) 2;
|
|
141 |
be mult_less_mono_r 2;
|
|
142 |
br less_not_refl2 3;
|
|
143 |
be mult_less_mono_r 3;
|
1335
|
144 |
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
|
|
145 |
qed "mult_not_eq_mono_r";
|
|
146 |
|
|
147 |
(******************************************************************)
|
|
148 |
|
|
149 |
val prems = goal Arith.thy "(m - n)*k = (m*k) - ((n*k)::nat)";
|
|
150 |
by (res_inst_tac [("P","m*k<n*k")] case_split_thm 1);
|
|
151 |
by (forward_tac [mult_not_less_mono_r COMP not_imp_swap] 1);
|
1476
|
152 |
bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
|
|
153 |
bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
|
|
154 |
br mp 2;
|
|
155 |
ba 3;
|
1335
|
156 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 2);
|
|
157 |
by (ALLGOALS Asm_simp_tac);
|
1476
|
158 |
br impI 1;
|
|
159 |
bd (refl RS iffD1) 1;
|
1335
|
160 |
by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
|
1476
|
161 |
bd (refl RS iffD1) 1;
|
|
162 |
bd (refl RS iffD1) 1;
|
|
163 |
bd diff_not_assoc 1;
|
1335
|
164 |
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_add_inverse]) 1);
|
|
165 |
qed "diff_mult_distrib_r";
|
|
166 |
|
|
167 |
|
|
168 |
(*** mod ***)
|
|
169 |
|
1476
|
170 |
goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
|
|
171 |
\ (%f j. if j<n then j else f (j-n))";
|
|
172 |
by (simp_tac (HOL_ss addsimps [mod_def]) 1);
|
|
173 |
val mod_def = result() RS eq_reflection;
|
|
174 |
|
1335
|
175 |
(* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *)
|
|
176 |
(*
|
|
177 |
val prems = goal thy "0<n ==> n mod n = 0";
|
|
178 |
by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1);
|
|
179 |
by (cut_facts_tac prems 1);
|
|
180 |
by (Asm_full_simp_tac 1);
|
|
181 |
by (fast_tac HOL_cs 1);
|
|
182 |
*)
|
|
183 |
|
|
184 |
val prems=goal thy "0<n ==> n mod n = 0";
|
|
185 |
by (cut_facts_tac prems 1);
|
1476
|
186 |
br (mod_def RS wf_less_trans) 1;
|
1335
|
187 |
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
|
1476
|
188 |
be mod_less 1;
|
1335
|
189 |
qed "mod_nn_is_0";
|
|
190 |
|
|
191 |
val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
|
|
192 |
by (cut_facts_tac prems 1);
|
|
193 |
by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
|
1476
|
194 |
br add_commute 1;
|
1335
|
195 |
by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
|
1476
|
196 |
br diff_add_inverse 1;
|
|
197 |
br sym 1;
|
|
198 |
be mod_geq 1;
|
1335
|
199 |
by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
|
|
200 |
by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
|
1476
|
201 |
br le_add1 1;
|
1335
|
202 |
qed "mod_eq_add";
|
|
203 |
|
|
204 |
val prems=goal thy "0<n ==> m*n mod n = 0";
|
|
205 |
by (cut_facts_tac prems 1);
|
|
206 |
by (nat_ind_tac "m" 1);
|
|
207 |
by (Simp_tac 1);
|
1476
|
208 |
be mod_less 1;
|
1335
|
209 |
by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
|
|
210 |
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
|
|
211 |
qed "mod_prod_nn_is_0";
|
|
212 |
|
|
213 |
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
|
|
214 |
by (cut_facts_tac prems 1);
|
|
215 |
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
|
1476
|
216 |
be mod_div_equality 1;
|
1335
|
217 |
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
|
1476
|
218 |
be mod_div_equality 1;
|
1335
|
219 |
by (Asm_simp_tac 1);
|
|
220 |
by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
|
1476
|
221 |
br add_mult_distrib 1;
|
|
222 |
be mod_prod_nn_is_0 1;
|
1335
|
223 |
qed "mod0_sum";
|
|
224 |
|
|
225 |
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
|
|
226 |
by (cut_facts_tac prems 1);
|
|
227 |
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
|
1476
|
228 |
be mod_div_equality 1;
|
1335
|
229 |
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
|
1476
|
230 |
be mod_div_equality 1;
|
1335
|
231 |
by (Asm_simp_tac 1);
|
|
232 |
by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
|
1476
|
233 |
br diff_mult_distrib_r 1;
|
|
234 |
be mod_prod_nn_is_0 1;
|
1335
|
235 |
qed "mod0_diff";
|
|
236 |
|
|
237 |
|
|
238 |
(*** div ***)
|
|
239 |
|
1476
|
240 |
|
1335
|
241 |
val prems = goal thy "0<n ==> m*n div n = m";
|
|
242 |
by (cut_facts_tac prems 1);
|
1476
|
243 |
br (mult_not_eq_mono_r RS not_imp_swap) 1;
|
|
244 |
ba 1;
|
|
245 |
ba 1;
|
1335
|
246 |
by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
|
1476
|
247 |
ba 1;
|
1335
|
248 |
by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
|
|
249 |
by (Asm_simp_tac 1);
|
|
250 |
qed "div_prod_nn_is_m";
|
|
251 |
|
|
252 |
|
|
253 |
(*** divides ***)
|
|
254 |
|
|
255 |
val prems=goalw thy [divides_def] "0<n ==> n divides n";
|
|
256 |
by (cut_facts_tac prems 1);
|
|
257 |
by (forward_tac [mod_nn_is_0] 1);
|
|
258 |
by (Asm_simp_tac 1);
|
|
259 |
qed "divides_nn";
|
|
260 |
|
|
261 |
val prems=goalw thy [divides_def] "x divides n ==> x<=n";
|
|
262 |
by (cut_facts_tac prems 1);
|
1476
|
263 |
br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
|
1335
|
264 |
by (Asm_simp_tac 1);
|
1476
|
265 |
br (less_not_refl2 RS not_sym) 1;
|
1335
|
266 |
by (Asm_simp_tac 1);
|
|
267 |
qed "divides_le";
|
|
268 |
|
|
269 |
val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
|
|
270 |
by (cut_facts_tac prems 1);
|
|
271 |
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
|
1476
|
272 |
br conjI 1;
|
1335
|
273 |
by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
|
1476
|
274 |
ba 1;
|
|
275 |
be conjI 1;
|
|
276 |
br mod0_sum 1;
|
1335
|
277 |
by (ALLGOALS atac);
|
|
278 |
qed "divides_sum";
|
|
279 |
|
|
280 |
val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
|
|
281 |
by (cut_facts_tac prems 1);
|
|
282 |
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
|
1476
|
283 |
br conjI 1;
|
|
284 |
be less_imp_diff_positive 1;
|
|
285 |
be conjI 1;
|
|
286 |
br mod0_diff 1;
|
1335
|
287 |
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
|
1476
|
288 |
be less_not_sym 1;
|
1335
|
289 |
qed "divides_diff";
|
|
290 |
|
|
291 |
|
|
292 |
(*** cd ***)
|
|
293 |
|
|
294 |
|
|
295 |
val prems=goalw thy [cd_def] "0<n ==> cd n n n";
|
|
296 |
by (cut_facts_tac prems 1);
|
1476
|
297 |
bd divides_nn 1;
|
1335
|
298 |
by (Asm_simp_tac 1);
|
|
299 |
qed "cd_nnn";
|
|
300 |
|
|
301 |
val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
|
|
302 |
by (cut_facts_tac prems 1);
|
1476
|
303 |
bd conjE 1;
|
|
304 |
ba 2;
|
|
305 |
bd divides_le 1;
|
|
306 |
bd divides_le 1;
|
1335
|
307 |
by (Asm_simp_tac 1);
|
|
308 |
qed "cd_le";
|
|
309 |
|
|
310 |
val prems=goalw thy [cd_def] "cd x m n = cd x n m";
|
|
311 |
by (fast_tac HOL_cs 1);
|
|
312 |
qed "cd_swap";
|
|
313 |
|
|
314 |
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
|
|
315 |
by (cut_facts_tac prems 1);
|
1476
|
316 |
br iffI 1;
|
|
317 |
bd conjE 1;
|
|
318 |
ba 2;
|
|
319 |
br conjI 1;
|
|
320 |
br divides_diff 1;
|
|
321 |
bd conjE 5;
|
|
322 |
ba 6;
|
|
323 |
br conjI 5;
|
|
324 |
bd less_not_sym 5;
|
|
325 |
bd add_diff_inverse 5;
|
1335
|
326 |
by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
|
|
327 |
by (ALLGOALS Asm_full_simp_tac);
|
|
328 |
qed "cd_diff_l";
|
|
329 |
|
|
330 |
val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
|
|
331 |
by (cut_facts_tac prems 1);
|
1476
|
332 |
br iffI 1;
|
|
333 |
bd conjE 1;
|
|
334 |
ba 2;
|
|
335 |
br conjI 1;
|
|
336 |
br divides_diff 2;
|
|
337 |
bd conjE 5;
|
|
338 |
ba 6;
|
|
339 |
br conjI 5;
|
|
340 |
bd less_not_sym 6;
|
|
341 |
bd add_diff_inverse 6;
|
1335
|
342 |
by (dres_inst_tac [("n","n-m")] divides_sum 6);
|
|
343 |
by (ALLGOALS Asm_full_simp_tac);
|
|
344 |
qed "cd_diff_r";
|
|
345 |
|
|
346 |
|
|
347 |
(*** gcd ***)
|
|
348 |
|
|
349 |
val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
|
|
350 |
by (cut_facts_tac prems 1);
|
1476
|
351 |
bd cd_nnn 1;
|
|
352 |
br (select_equality RS sym) 1;
|
|
353 |
be conjI 1;
|
|
354 |
br allI 1;
|
|
355 |
br impI 1;
|
|
356 |
bd cd_le 1;
|
|
357 |
bd conjE 2;
|
|
358 |
ba 3;
|
|
359 |
br le_anti_sym 2;
|
1335
|
360 |
by (dres_inst_tac [("x","x")] cd_le 2);
|
|
361 |
by (dres_inst_tac [("x","n")] spec 3);
|
|
362 |
by (ALLGOALS Asm_full_simp_tac);
|
|
363 |
qed "gcd_nnn";
|
|
364 |
|
|
365 |
val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
|
|
366 |
by (simp_tac ((simpset_of "Arith") addsimps [cd_swap]) 1);
|
|
367 |
qed "gcd_swap";
|
|
368 |
|
|
369 |
val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (m-n) n";
|
|
370 |
by (cut_facts_tac prems 1);
|
|
371 |
by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
|
|
372 |
by (Asm_simp_tac 1);
|
1476
|
373 |
br allI 1;
|
|
374 |
be cd_diff_l 1;
|
1335
|
375 |
qed "gcd_diff_l";
|
|
376 |
|
|
377 |
val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
|
|
378 |
by (cut_facts_tac prems 1);
|
|
379 |
by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
|
|
380 |
by (Asm_simp_tac 1);
|
1476
|
381 |
br allI 1;
|
|
382 |
be cd_diff_r 1;
|
1335
|
383 |
qed "gcd_diff_r";
|
|
384 |
|
|
385 |
|
|
386 |
(*** pow ***)
|
|
387 |
|
|
388 |
val [pow_0,pow_Suc] = nat_recs pow_def;
|
|
389 |
store_thm("pow_0",pow_0);
|
|
390 |
store_thm("pow_Suc",pow_Suc);
|
|
391 |
|
|
392 |
goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k";
|
|
393 |
by (nat_ind_tac "k" 1);
|
|
394 |
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [mult_left_commute])));
|
|
395 |
qed "pow_add_reduce";
|
|
396 |
|
|
397 |
goalw thy [pow_def] "m pow n pow k = m pow (n*k)";
|
|
398 |
by (nat_ind_tac "k" 1);
|
|
399 |
by (ALLGOALS Asm_simp_tac);
|
|
400 |
by (fold_goals_tac [pow_def]);
|
1476
|
401 |
br (pow_add_reduce RS sym) 1;
|
1335
|
402 |
qed "pow_pow_reduce";
|
|
403 |
|
|
404 |
(*** fac ***)
|
|
405 |
|
|
406 |
Addsimps(nat_recs fac_def);
|