20 val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS |
20 val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS |
21 def_wfrec RS trans; |
21 def_wfrec RS trans; |
22 |
22 |
23 (*** Remainder ***) |
23 (*** Remainder ***) |
24 |
24 |
25 goal thy "(%m. m mod n) = wfrec (trancl pred_nat) \ |
25 Goal "(%m. m mod n) = wfrec (trancl pred_nat) \ |
26 \ (%f j. if j<n then j else f (j-n))"; |
26 \ (%f j. if j<n then j else f (j-n))"; |
27 by (simp_tac (simpset() addsimps [mod_def]) 1); |
27 by (simp_tac (simpset() addsimps [mod_def]) 1); |
28 qed "mod_eq"; |
28 qed "mod_eq"; |
29 |
29 |
30 goal thy "!!m. m<n ==> m mod n = m"; |
30 Goal "!!m. m<n ==> m mod n = m"; |
31 by (rtac (mod_eq RS wf_less_trans) 1); |
31 by (rtac (mod_eq RS wf_less_trans) 1); |
32 by (Asm_simp_tac 1); |
32 by (Asm_simp_tac 1); |
33 qed "mod_less"; |
33 qed "mod_less"; |
34 |
34 |
35 goal thy "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n"; |
35 Goal "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n"; |
36 by (rtac (mod_eq RS wf_less_trans) 1); |
36 by (rtac (mod_eq RS wf_less_trans) 1); |
37 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); |
37 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); |
38 qed "mod_geq"; |
38 qed "mod_geq"; |
39 |
39 |
40 (*NOT suitable for rewriting: loops*) |
40 (*NOT suitable for rewriting: loops*) |
41 goal thy "!!m. 0<n ==> m mod n = (if m<n then m else (m-n) mod n)"; |
41 Goal "!!m. 0<n ==> m mod n = (if m<n then m else (m-n) mod n)"; |
42 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); |
42 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); |
43 qed "mod_if"; |
43 qed "mod_if"; |
44 |
44 |
45 goal thy "m mod 1 = 0"; |
45 Goal "m mod 1 = 0"; |
46 by (induct_tac "m" 1); |
46 by (induct_tac "m" 1); |
47 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]))); |
47 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]))); |
48 qed "mod_1"; |
48 qed "mod_1"; |
49 Addsimps [mod_1]; |
49 Addsimps [mod_1]; |
50 |
50 |
51 goal thy "!!n. 0<n ==> n mod n = 0"; |
51 Goal "!!n. 0<n ==> n mod n = 0"; |
52 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); |
52 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); |
53 qed "mod_self"; |
53 qed "mod_self"; |
54 |
54 |
55 goal thy "!!n. 0<n ==> (m+n) mod n = m mod n"; |
55 Goal "!!n. 0<n ==> (m+n) mod n = m mod n"; |
56 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1); |
56 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1); |
57 by (stac (mod_geq RS sym) 2); |
57 by (stac (mod_geq RS sym) 2); |
58 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
58 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
59 qed "mod_add_self2"; |
59 qed "mod_add_self2"; |
60 |
60 |
61 goal thy "!!k. 0<n ==> (n+m) mod n = m mod n"; |
61 Goal "!!k. 0<n ==> (n+m) mod n = m mod n"; |
62 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); |
62 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); |
63 qed "mod_add_self1"; |
63 qed "mod_add_self1"; |
64 |
64 |
65 goal thy "!!n. 0<n ==> (m + k*n) mod n = m mod n"; |
65 Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n"; |
66 by (induct_tac "k" 1); |
66 by (induct_tac "k" 1); |
67 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1])))); |
67 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1])))); |
68 qed "mod_mult_self1"; |
68 qed "mod_mult_self1"; |
69 |
69 |
70 goal thy "!!m. 0<n ==> (m + n*k) mod n = m mod n"; |
70 Goal "!!m. 0<n ==> (m + n*k) mod n = m mod n"; |
71 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); |
71 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); |
72 qed "mod_mult_self2"; |
72 qed "mod_mult_self2"; |
73 |
73 |
74 Addsimps [mod_mult_self1, mod_mult_self2]; |
74 Addsimps [mod_mult_self1, mod_mult_self2]; |
75 |
75 |
76 goal thy "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)"; |
76 Goal "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)"; |
77 by (res_inst_tac [("n","m")] less_induct 1); |
77 by (res_inst_tac [("n","m")] less_induct 1); |
78 by (stac mod_if 1); |
78 by (stac mod_if 1); |
79 by (Asm_simp_tac 1); |
79 by (Asm_simp_tac 1); |
80 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, |
80 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, |
81 diff_less, diff_mult_distrib]) 1); |
81 diff_less, diff_mult_distrib]) 1); |
82 qed "mod_mult_distrib"; |
82 qed "mod_mult_distrib"; |
83 |
83 |
84 goal thy "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)"; |
84 Goal "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)"; |
85 by (res_inst_tac [("n","m")] less_induct 1); |
85 by (res_inst_tac [("n","m")] less_induct 1); |
86 by (stac mod_if 1); |
86 by (stac mod_if 1); |
87 by (Asm_simp_tac 1); |
87 by (Asm_simp_tac 1); |
88 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, |
88 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, |
89 diff_less, diff_mult_distrib2]) 1); |
89 diff_less, diff_mult_distrib2]) 1); |
90 qed "mod_mult_distrib2"; |
90 qed "mod_mult_distrib2"; |
91 |
91 |
92 goal thy "!!n. 0<n ==> m*n mod n = 0"; |
92 Goal "!!n. 0<n ==> m*n mod n = 0"; |
93 by (induct_tac "m" 1); |
93 by (induct_tac "m" 1); |
94 by (asm_simp_tac (simpset() addsimps [mod_less]) 1); |
94 by (asm_simp_tac (simpset() addsimps [mod_less]) 1); |
95 by (dres_inst_tac [("m","m*n")] mod_add_self2 1); |
95 by (dres_inst_tac [("m","m*n")] mod_add_self2 1); |
96 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); |
96 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); |
97 qed "mod_mult_self_is_0"; |
97 qed "mod_mult_self_is_0"; |
98 Addsimps [mod_mult_self_is_0]; |
98 Addsimps [mod_mult_self_is_0]; |
99 |
99 |
100 (*** Quotient ***) |
100 (*** Quotient ***) |
101 |
101 |
102 goal thy "(%m. m div n) = wfrec (trancl pred_nat) \ |
102 Goal "(%m. m div n) = wfrec (trancl pred_nat) \ |
103 \ (%f j. if j<n then 0 else Suc (f (j-n)))"; |
103 \ (%f j. if j<n then 0 else Suc (f (j-n)))"; |
104 by (simp_tac (simpset() addsimps [div_def]) 1); |
104 by (simp_tac (simpset() addsimps [div_def]) 1); |
105 qed "div_eq"; |
105 qed "div_eq"; |
106 |
106 |
107 goal thy "!!m. m<n ==> m div n = 0"; |
107 Goal "!!m. m<n ==> m div n = 0"; |
108 by (rtac (div_eq RS wf_less_trans) 1); |
108 by (rtac (div_eq RS wf_less_trans) 1); |
109 by (Asm_simp_tac 1); |
109 by (Asm_simp_tac 1); |
110 qed "div_less"; |
110 qed "div_less"; |
111 |
111 |
112 goal thy "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"; |
112 Goal "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"; |
113 by (rtac (div_eq RS wf_less_trans) 1); |
113 by (rtac (div_eq RS wf_less_trans) 1); |
114 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); |
114 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); |
115 qed "div_geq"; |
115 qed "div_geq"; |
116 |
116 |
117 (*NOT suitable for rewriting: loops*) |
117 (*NOT suitable for rewriting: loops*) |
118 goal thy "!!m. 0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"; |
118 Goal "!!m. 0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"; |
119 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); |
119 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); |
120 qed "div_if"; |
120 qed "div_if"; |
121 |
121 |
122 (*Main Result about quotient and remainder.*) |
122 (*Main Result about quotient and remainder.*) |
123 goal thy "!!m. 0<n ==> (m div n)*n + m mod n = m"; |
123 Goal "!!m. 0<n ==> (m div n)*n + m mod n = m"; |
124 by (res_inst_tac [("n","m")] less_induct 1); |
124 by (res_inst_tac [("n","m")] less_induct 1); |
125 by (stac mod_if 1); |
125 by (stac mod_if 1); |
126 by (ALLGOALS (asm_simp_tac |
126 by (ALLGOALS (asm_simp_tac |
127 (simpset() addsimps ([add_assoc] @ |
127 (simpset() addsimps ([add_assoc] @ |
128 [div_less, div_geq, |
128 [div_less, div_geq, |
129 add_diff_inverse, diff_less])))); |
129 add_diff_inverse, diff_less])))); |
130 qed "mod_div_equality"; |
130 qed "mod_div_equality"; |
131 |
131 |
132 (* a simple rearrangement of mod_div_equality: *) |
132 (* a simple rearrangement of mod_div_equality: *) |
133 goal thy "!!k. 0<k ==> k*(m div k) = m - (m mod k)"; |
133 Goal "!!k. 0<k ==> k*(m div k) = m - (m mod k)"; |
134 by (dres_inst_tac [("m","m")] mod_div_equality 1); |
134 by (dres_inst_tac [("m","m")] mod_div_equality 1); |
135 by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac), |
135 by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac), |
136 K(IF_UNSOLVED no_tac)]); |
136 K(IF_UNSOLVED no_tac)]); |
137 qed "mult_div_cancel"; |
137 qed "mult_div_cancel"; |
138 |
138 |
139 goal thy "m div 1 = m"; |
139 Goal "m div 1 = m"; |
140 by (induct_tac "m" 1); |
140 by (induct_tac "m" 1); |
141 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq]))); |
141 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq]))); |
142 qed "div_1"; |
142 qed "div_1"; |
143 Addsimps [div_1]; |
143 Addsimps [div_1]; |
144 |
144 |
145 goal thy "!!n. 0<n ==> n div n = 1"; |
145 Goal "!!n. 0<n ==> n div n = 1"; |
146 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); |
146 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); |
147 qed "div_self"; |
147 qed "div_self"; |
148 |
148 |
149 |
149 |
150 goal thy "!!n. 0<n ==> (m+n) div n = Suc (m div n)"; |
150 Goal "!!n. 0<n ==> (m+n) div n = Suc (m div n)"; |
151 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1); |
151 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1); |
152 by (stac (div_geq RS sym) 2); |
152 by (stac (div_geq RS sym) 2); |
153 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
153 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
154 qed "div_add_self2"; |
154 qed "div_add_self2"; |
155 |
155 |
156 goal thy "!!k. 0<n ==> (n+m) div n = Suc (m div n)"; |
156 Goal "!!k. 0<n ==> (n+m) div n = Suc (m div n)"; |
157 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1); |
157 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1); |
158 qed "div_add_self1"; |
158 qed "div_add_self1"; |
159 |
159 |
160 goal thy "!!n. 0<n ==> (m + k*n) div n = k + m div n"; |
160 Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n"; |
161 by (induct_tac "k" 1); |
161 by (induct_tac "k" 1); |
162 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1])))); |
162 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1])))); |
163 qed "div_mult_self1"; |
163 qed "div_mult_self1"; |
164 |
164 |
165 goal thy "!!m. 0<n ==> (m + n*k) div n = k + m div n"; |
165 Goal "!!m. 0<n ==> (m + n*k) div n = k + m div n"; |
166 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); |
166 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); |
167 qed "div_mult_self2"; |
167 qed "div_mult_self2"; |
168 |
168 |
169 Addsimps [div_mult_self1, div_mult_self2]; |
169 Addsimps [div_mult_self1, div_mult_self2]; |
170 |
170 |
171 |
171 |
172 (* Monotonicity of div in first argument *) |
172 (* Monotonicity of div in first argument *) |
173 goal thy "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)"; |
173 Goal "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)"; |
174 by (res_inst_tac [("n","n")] less_induct 1); |
174 by (res_inst_tac [("n","n")] less_induct 1); |
175 by (Clarify_tac 1); |
175 by (Clarify_tac 1); |
176 by (case_tac "na<k" 1); |
176 by (case_tac "na<k" 1); |
177 (* 1 case n<k *) |
177 (* 1 case n<k *) |
178 by (subgoal_tac "m<k" 1); |
178 by (subgoal_tac "m<k" 1); |
268 (** Evens and Odds **) |
268 (** Evens and Odds **) |
269 |
269 |
270 (*With less_zeroE, causes case analysis on b<2*) |
270 (*With less_zeroE, causes case analysis on b<2*) |
271 AddSEs [less_SucE]; |
271 AddSEs [less_SucE]; |
272 |
272 |
273 goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"; |
273 Goal "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"; |
274 by (subgoal_tac "k mod 2 < 2" 1); |
274 by (subgoal_tac "k mod 2 < 2" 1); |
275 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
275 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
276 by (Asm_simp_tac 1); |
276 by (Asm_simp_tac 1); |
277 by Safe_tac; |
277 by Safe_tac; |
278 qed "mod2_cases"; |
278 qed "mod2_cases"; |
279 |
279 |
280 goal thy "Suc(Suc(m)) mod 2 = m mod 2"; |
280 Goal "Suc(Suc(m)) mod 2 = m mod 2"; |
281 by (subgoal_tac "m mod 2 < 2" 1); |
281 by (subgoal_tac "m mod 2 < 2" 1); |
282 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
282 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
283 by Safe_tac; |
283 by Safe_tac; |
284 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); |
284 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); |
285 qed "mod2_Suc_Suc"; |
285 qed "mod2_Suc_Suc"; |
286 Addsimps [mod2_Suc_Suc]; |
286 Addsimps [mod2_Suc_Suc]; |
287 |
287 |
288 goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)"; |
288 Goal "(0 < m mod 2) = (m mod 2 = 1)"; |
289 by (subgoal_tac "m mod 2 < 2" 1); |
289 by (subgoal_tac "m mod 2 < 2" 1); |
290 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
290 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
291 by Auto_tac; |
291 by Auto_tac; |
292 qed "mod2_gr_0"; |
292 qed "mod2_gr_0"; |
293 Addsimps [mod2_gr_0]; |
293 Addsimps [mod2_gr_0]; |
294 |
294 |
295 goal thy "(m+m) mod 2 = 0"; |
295 Goal "(m+m) mod 2 = 0"; |
296 by (induct_tac "m" 1); |
296 by (induct_tac "m" 1); |
297 by (simp_tac (simpset() addsimps [mod_less]) 1); |
297 by (simp_tac (simpset() addsimps [mod_less]) 1); |
298 by (Asm_simp_tac 1); |
298 by (Asm_simp_tac 1); |
299 qed "mod2_add_self_eq_0"; |
299 qed "mod2_add_self_eq_0"; |
300 Addsimps [mod2_add_self_eq_0]; |
300 Addsimps [mod2_add_self_eq_0]; |
301 |
301 |
302 goal thy "((m+m)+n) mod 2 = n mod 2"; |
302 Goal "((m+m)+n) mod 2 = n mod 2"; |
303 by (induct_tac "m" 1); |
303 by (induct_tac "m" 1); |
304 by (simp_tac (simpset() addsimps [mod_less]) 1); |
304 by (simp_tac (simpset() addsimps [mod_less]) 1); |
305 by (Asm_simp_tac 1); |
305 by (Asm_simp_tac 1); |
306 qed "mod2_add_self"; |
306 qed "mod2_add_self"; |
307 Addsimps [mod2_add_self]; |
307 Addsimps [mod2_add_self]; |
349 |
349 |
350 (************************************************) |
350 (************************************************) |
351 (** Divides Relation **) |
351 (** Divides Relation **) |
352 (************************************************) |
352 (************************************************) |
353 |
353 |
354 goalw thy [dvd_def] "m dvd 0"; |
354 Goalw [dvd_def] "m dvd 0"; |
355 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); |
355 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); |
356 qed "dvd_0_right"; |
356 qed "dvd_0_right"; |
357 Addsimps [dvd_0_right]; |
357 Addsimps [dvd_0_right]; |
358 |
358 |
359 goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0"; |
359 Goalw [dvd_def] "!!m. 0 dvd m ==> m = 0"; |
360 by (fast_tac (claset() addss simpset()) 1); |
360 by (fast_tac (claset() addss simpset()) 1); |
361 qed "dvd_0_left"; |
361 qed "dvd_0_left"; |
362 |
362 |
363 goalw thy [dvd_def] "1 dvd k"; |
363 Goalw [dvd_def] "1 dvd k"; |
364 by (Simp_tac 1); |
364 by (Simp_tac 1); |
365 qed "dvd_1_left"; |
365 qed "dvd_1_left"; |
366 AddIffs [dvd_1_left]; |
366 AddIffs [dvd_1_left]; |
367 |
367 |
368 goalw thy [dvd_def] "m dvd m"; |
368 Goalw [dvd_def] "m dvd m"; |
369 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); |
369 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); |
370 qed "dvd_refl"; |
370 qed "dvd_refl"; |
371 Addsimps [dvd_refl]; |
371 Addsimps [dvd_refl]; |
372 |
372 |
373 goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p"; |
373 Goalw [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p"; |
374 by (blast_tac (claset() addIs [mult_assoc] ) 1); |
374 by (blast_tac (claset() addIs [mult_assoc] ) 1); |
375 qed "dvd_trans"; |
375 qed "dvd_trans"; |
376 |
376 |
377 goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n"; |
377 Goalw [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n"; |
378 by (fast_tac (claset() addDs [mult_eq_self_implies_10] |
378 by (fast_tac (claset() addDs [mult_eq_self_implies_10] |
379 addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1); |
379 addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1); |
380 qed "dvd_anti_sym"; |
380 qed "dvd_anti_sym"; |
381 |
381 |
382 goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)"; |
382 Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)"; |
383 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); |
383 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); |
384 qed "dvd_add"; |
384 qed "dvd_add"; |
385 |
385 |
386 goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)"; |
386 Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)"; |
387 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); |
387 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); |
388 qed "dvd_diff"; |
388 qed "dvd_diff"; |
389 |
389 |
390 goal thy "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m"; |
390 Goal "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m"; |
391 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
391 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
392 by (blast_tac (claset() addIs [dvd_add]) 1); |
392 by (blast_tac (claset() addIs [dvd_add]) 1); |
393 qed "dvd_diffD"; |
393 qed "dvd_diffD"; |
394 |
394 |
395 goalw thy [dvd_def] "!!k. k dvd n ==> k dvd (m*n)"; |
395 Goalw [dvd_def] "!!k. k dvd n ==> k dvd (m*n)"; |
396 by (blast_tac (claset() addIs [mult_left_commute]) 1); |
396 by (blast_tac (claset() addIs [mult_left_commute]) 1); |
397 qed "dvd_mult"; |
397 qed "dvd_mult"; |
398 |
398 |
399 goal thy "!!k. k dvd m ==> k dvd (m*n)"; |
399 Goal "!!k. k dvd m ==> k dvd (m*n)"; |
400 by (stac mult_commute 1); |
400 by (stac mult_commute 1); |
401 by (etac dvd_mult 1); |
401 by (etac dvd_mult 1); |
402 qed "dvd_mult2"; |
402 qed "dvd_mult2"; |
403 |
403 |
404 (* k dvd (m*k) *) |
404 (* k dvd (m*k) *) |
405 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; |
405 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; |
406 |
406 |
407 goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)"; |
407 Goalw [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)"; |
408 by (Clarify_tac 1); |
408 by (Clarify_tac 1); |
409 by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); |
409 by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); |
410 by (res_inst_tac |
410 by (res_inst_tac |
411 [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] |
411 [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] |
412 exI 1); |
412 exI 1); |
413 by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, |
413 by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, |
414 mult_mod_distrib, add_mult_distrib2]) 1); |
414 mult_mod_distrib, add_mult_distrib2]) 1); |
415 qed "dvd_mod"; |
415 qed "dvd_mod"; |
416 |
416 |
417 goal thy "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m"; |
417 Goal "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m"; |
418 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1); |
418 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1); |
419 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); |
419 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); |
420 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); |
420 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); |
421 qed "dvd_mod_imp_dvd"; |
421 qed "dvd_mod_imp_dvd"; |
422 |
422 |
423 goalw thy [dvd_def] "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n"; |
423 Goalw [dvd_def] "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n"; |
424 by (etac exE 1); |
424 by (etac exE 1); |
425 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); |
425 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); |
426 by (Blast_tac 1); |
426 by (Blast_tac 1); |
427 qed "dvd_mult_cancel"; |
427 qed "dvd_mult_cancel"; |
428 |
428 |
429 goalw thy [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)"; |
429 Goalw [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)"; |
430 by (Clarify_tac 1); |
430 by (Clarify_tac 1); |
431 by (res_inst_tac [("x","k*ka")] exI 1); |
431 by (res_inst_tac [("x","k*ka")] exI 1); |
432 by (asm_simp_tac (simpset() addsimps mult_ac) 1); |
432 by (asm_simp_tac (simpset() addsimps mult_ac) 1); |
433 qed "mult_dvd_mono"; |
433 qed "mult_dvd_mono"; |
434 |
434 |
435 goalw thy [dvd_def] "!!c. (i*j) dvd k ==> i dvd k"; |
435 Goalw [dvd_def] "!!c. (i*j) dvd k ==> i dvd k"; |
436 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); |
436 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); |
437 by (Blast_tac 1); |
437 by (Blast_tac 1); |
438 qed "dvd_mult_left"; |
438 qed "dvd_mult_left"; |
439 |
439 |
440 goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n"; |
440 Goalw [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n"; |
441 by (Clarify_tac 1); |
441 by (Clarify_tac 1); |
442 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
442 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
443 by (etac conjE 1); |
443 by (etac conjE 1); |
444 by (rtac le_trans 1); |
444 by (rtac le_trans 1); |
445 by (rtac (le_refl RS mult_le_mono) 2); |
445 by (rtac (le_refl RS mult_le_mono) 2); |
446 by (etac Suc_leI 2); |
446 by (etac Suc_leI 2); |
447 by (Simp_tac 1); |
447 by (Simp_tac 1); |
448 qed "dvd_imp_le"; |
448 qed "dvd_imp_le"; |
449 |
449 |
450 goalw thy [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)"; |
450 Goalw [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)"; |
451 by Safe_tac; |
451 by Safe_tac; |
452 by (stac mult_commute 1); |
452 by (stac mult_commute 1); |
453 by (Asm_simp_tac 1); |
453 by (Asm_simp_tac 1); |
454 by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1); |
454 by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1); |
455 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); |
455 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); |