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);
|
1875
|
17 |
by (Fast_tac 1);
|
1335
|
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);
|
2031
|
33 |
by (rtac diff_induct 1);
|
|
34 |
by (rtac allI 1);
|
|
35 |
by (rtac 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);
|
2031
|
38 |
by (rtac allI 7);
|
1335
|
39 |
by (nat_ind_tac "xa" 7);
|
|
40 |
by (ALLGOALS (resolve_tac prems));
|
2031
|
41 |
by (assume_tac 1);
|
|
42 |
by (assume_tac 1);
|
1875
|
43 |
by (Fast_tac 1);
|
|
44 |
by (Fast_tac 1);
|
1335
|
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);
|
2031
|
51 |
by (rtac mp 1);
|
|
52 |
by (assume_tac 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);
|
2031
|
59 |
by (dtac conjI 1);
|
|
60 |
by (assume_tac 1);
|
1335
|
61 |
by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
|
2031
|
62 |
by (assume_tac 2);
|
1335
|
63 |
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
|
|
64 |
by (ALLGOALS Asm_simp_tac);
|
2031
|
65 |
by (rtac impI 1);
|
1335
|
66 |
by (dres_inst_tac [("P","~x<y")] conjE 1);
|
2031
|
67 |
by (assume_tac 2);
|
|
68 |
by (rtac (Suc_diff_n RS sym) 1);
|
|
69 |
by (rtac le_less_trans 1);
|
|
70 |
by (etac (not_less_eq RS subst) 2);
|
|
71 |
by (rtac (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);
|
2031
|
76 |
by (rtac mp 1);
|
|
77 |
by (assume_tac 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)";
|
2031
|
85 |
by (rtac iffI 1);
|
1335
|
86 |
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
|
|
87 |
by (Asm_full_simp_tac 1);
|
2031
|
88 |
by (etac disjE 1);
|
|
89 |
by (etac (less_not_refl2 RS not_sym) 1);
|
|
90 |
by (etac 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 |
(******************************************************************)
|
|
114 |
|
|
115 |
(*** mod ***)
|
|
116 |
|
|
117 |
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
|
|
118 |
by (cut_facts_tac prems 1);
|
|
119 |
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
|
2031
|
120 |
by (etac mod_div_equality 1);
|
1335
|
121 |
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
|
2031
|
122 |
by (etac mod_div_equality 1);
|
1335
|
123 |
by (Asm_simp_tac 1);
|
|
124 |
by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
|
2031
|
125 |
by (rtac add_mult_distrib 1);
|
|
126 |
by (etac mod_prod_nn_is_0 1);
|
1335
|
127 |
qed "mod0_sum";
|
|
128 |
|
|
129 |
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
|
|
130 |
by (cut_facts_tac prems 1);
|
|
131 |
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
|
2031
|
132 |
by (etac mod_div_equality 1);
|
1335
|
133 |
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
|
2031
|
134 |
by (etac mod_div_equality 1);
|
1335
|
135 |
by (Asm_simp_tac 1);
|
|
136 |
by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
|
2031
|
137 |
by (rtac diff_mult_distrib 1);
|
|
138 |
by (etac mod_prod_nn_is_0 1);
|
1335
|
139 |
qed "mod0_diff";
|
|
140 |
|
|
141 |
|
|
142 |
(*** divides ***)
|
|
143 |
|
|
144 |
val prems=goalw thy [divides_def] "0<n ==> n divides n";
|
|
145 |
by (cut_facts_tac prems 1);
|
|
146 |
by (forward_tac [mod_nn_is_0] 1);
|
|
147 |
by (Asm_simp_tac 1);
|
|
148 |
qed "divides_nn";
|
|
149 |
|
|
150 |
val prems=goalw thy [divides_def] "x divides n ==> x<=n";
|
|
151 |
by (cut_facts_tac prems 1);
|
2031
|
152 |
by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1);
|
1335
|
153 |
by (Asm_simp_tac 1);
|
2031
|
154 |
by (rtac (less_not_refl2 RS not_sym) 1);
|
1335
|
155 |
by (Asm_simp_tac 1);
|
|
156 |
qed "divides_le";
|
|
157 |
|
|
158 |
val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
|
|
159 |
by (cut_facts_tac prems 1);
|
|
160 |
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
|
2031
|
161 |
by (rtac conjI 1);
|
1335
|
162 |
by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
|
2031
|
163 |
by (assume_tac 1);
|
|
164 |
by (etac conjI 1);
|
|
165 |
by (rtac mod0_sum 1);
|
1335
|
166 |
by (ALLGOALS atac);
|
|
167 |
qed "divides_sum";
|
|
168 |
|
|
169 |
val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
|
|
170 |
by (cut_facts_tac prems 1);
|
|
171 |
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
|
2031
|
172 |
by (rtac conjI 1);
|
|
173 |
by (etac less_imp_diff_positive 1);
|
|
174 |
by (etac conjI 1);
|
|
175 |
by (rtac mod0_diff 1);
|
3238
|
176 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [le_def])));
|
2031
|
177 |
by (etac less_not_sym 1);
|
1335
|
178 |
qed "divides_diff";
|
|
179 |
|
|
180 |
|
|
181 |
(*** cd ***)
|
|
182 |
|
|
183 |
|
|
184 |
val prems=goalw thy [cd_def] "0<n ==> cd n n n";
|
|
185 |
by (cut_facts_tac prems 1);
|
2031
|
186 |
by (dtac divides_nn 1);
|
1335
|
187 |
by (Asm_simp_tac 1);
|
|
188 |
qed "cd_nnn";
|
|
189 |
|
|
190 |
val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
|
|
191 |
by (cut_facts_tac prems 1);
|
2031
|
192 |
by (dtac conjE 1);
|
|
193 |
by (assume_tac 2);
|
|
194 |
by (dtac divides_le 1);
|
|
195 |
by (dtac divides_le 1);
|
1335
|
196 |
by (Asm_simp_tac 1);
|
|
197 |
qed "cd_le";
|
|
198 |
|
|
199 |
val prems=goalw thy [cd_def] "cd x m n = cd x n m";
|
1875
|
200 |
by (Fast_tac 1);
|
1335
|
201 |
qed "cd_swap";
|
|
202 |
|
|
203 |
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
|
|
204 |
by (cut_facts_tac prems 1);
|
2031
|
205 |
by (rtac iffI 1);
|
|
206 |
by (dtac conjE 1);
|
|
207 |
by (assume_tac 2);
|
|
208 |
by (rtac conjI 1);
|
|
209 |
by (rtac divides_diff 1);
|
|
210 |
by (dtac conjE 5);
|
|
211 |
by (assume_tac 6);
|
|
212 |
by (rtac conjI 5);
|
|
213 |
by (dtac less_not_sym 5);
|
|
214 |
by (dtac add_diff_inverse 5);
|
1335
|
215 |
by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
|
|
216 |
by (ALLGOALS Asm_full_simp_tac);
|
|
217 |
qed "cd_diff_l";
|
|
218 |
|
|
219 |
val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
|
|
220 |
by (cut_facts_tac prems 1);
|
2031
|
221 |
by (rtac iffI 1);
|
|
222 |
by (dtac conjE 1);
|
|
223 |
by (assume_tac 2);
|
|
224 |
by (rtac conjI 1);
|
|
225 |
by (rtac divides_diff 2);
|
|
226 |
by (dtac conjE 5);
|
|
227 |
by (assume_tac 6);
|
|
228 |
by (rtac conjI 5);
|
|
229 |
by (dtac less_not_sym 6);
|
|
230 |
by (dtac add_diff_inverse 6);
|
1335
|
231 |
by (dres_inst_tac [("n","n-m")] divides_sum 6);
|
|
232 |
by (ALLGOALS Asm_full_simp_tac);
|
|
233 |
qed "cd_diff_r";
|
|
234 |
|
|
235 |
|
|
236 |
(*** gcd ***)
|
|
237 |
|
|
238 |
val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
|
|
239 |
by (cut_facts_tac prems 1);
|
2031
|
240 |
by (dtac cd_nnn 1);
|
|
241 |
by (rtac (select_equality RS sym) 1);
|
|
242 |
by (etac conjI 1);
|
|
243 |
by (rtac allI 1);
|
|
244 |
by (rtac impI 1);
|
|
245 |
by (dtac cd_le 1);
|
|
246 |
by (dtac conjE 2);
|
|
247 |
by (assume_tac 3);
|
|
248 |
by (rtac le_anti_sym 2);
|
1335
|
249 |
by (dres_inst_tac [("x","x")] cd_le 2);
|
|
250 |
by (dres_inst_tac [("x","n")] spec 3);
|
|
251 |
by (ALLGOALS Asm_full_simp_tac);
|
|
252 |
qed "gcd_nnn";
|
|
253 |
|
|
254 |
val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
|
3238
|
255 |
by (simp_tac (!simpset addsimps [cd_swap]) 1);
|
1335
|
256 |
qed "gcd_swap";
|
|
257 |
|
|
258 |
val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (m-n) n";
|
|
259 |
by (cut_facts_tac prems 1);
|
|
260 |
by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
|
|
261 |
by (Asm_simp_tac 1);
|
2031
|
262 |
by (rtac allI 1);
|
|
263 |
by (etac cd_diff_l 1);
|
1335
|
264 |
qed "gcd_diff_l";
|
|
265 |
|
|
266 |
val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
|
|
267 |
by (cut_facts_tac prems 1);
|
|
268 |
by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
|
|
269 |
by (Asm_simp_tac 1);
|
2031
|
270 |
by (rtac allI 1);
|
|
271 |
by (etac cd_diff_r 1);
|
1335
|
272 |
qed "gcd_diff_r";
|
|
273 |
|
|
274 |
|
|
275 |
(*** pow ***)
|
|
276 |
|
|
277 |
val [pow_0,pow_Suc] = nat_recs pow_def;
|
|
278 |
store_thm("pow_0",pow_0);
|
|
279 |
store_thm("pow_Suc",pow_Suc);
|
|
280 |
|
|
281 |
goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k";
|
|
282 |
by (nat_ind_tac "k" 1);
|
3238
|
283 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_left_commute])));
|
1335
|
284 |
qed "pow_add_reduce";
|
|
285 |
|
|
286 |
goalw thy [pow_def] "m pow n pow k = m pow (n*k)";
|
|
287 |
by (nat_ind_tac "k" 1);
|
|
288 |
by (ALLGOALS Asm_simp_tac);
|
|
289 |
by (fold_goals_tac [pow_def]);
|
2031
|
290 |
by (rtac (pow_add_reduce RS sym) 1);
|
1335
|
291 |
qed "pow_pow_reduce";
|
|
292 |
|
|
293 |
(*** fac ***)
|
|
294 |
|
|
295 |
Addsimps(nat_recs fac_def);
|