9548
|
1 |
(* Title: ZF/ArithSimp.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2000 University of Cambridge
|
|
5 |
|
|
6 |
Arithmetic with simplification
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
Addsimprocs ArithData.nat_cancel;
|
|
11 |
|
|
12 |
|
|
13 |
(*** Difference ***)
|
|
14 |
|
|
15 |
Goal "m #- m = 0";
|
|
16 |
by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
|
|
17 |
by (rtac (natify_in_nat RS nat_induct) 2);
|
|
18 |
by Auto_tac;
|
|
19 |
qed "diff_self_eq_0";
|
|
20 |
|
|
21 |
(**Addition is the inverse of subtraction**)
|
|
22 |
|
|
23 |
(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
|
|
24 |
n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
|
|
25 |
Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m";
|
|
26 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
27 |
by (etac rev_mp 1);
|
|
28 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
29 |
by Auto_tac;
|
|
30 |
qed "add_diff_inverse";
|
|
31 |
|
|
32 |
Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m";
|
|
33 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
34 |
by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
|
|
35 |
qed "add_diff_inverse2";
|
|
36 |
|
|
37 |
(*Proof is IDENTICAL to that of add_diff_inverse*)
|
|
38 |
Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
|
|
39 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
40 |
by (etac rev_mp 1);
|
|
41 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
42 |
by (ALLGOALS Asm_simp_tac);
|
|
43 |
qed "diff_succ";
|
|
44 |
|
|
45 |
Goal "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m<n";
|
|
46 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
47 |
by (ALLGOALS Asm_simp_tac);
|
|
48 |
qed "zero_less_diff";
|
|
49 |
Addsimps [zero_less_diff];
|
|
50 |
|
|
51 |
|
|
52 |
(** Difference distributes over multiplication **)
|
|
53 |
|
|
54 |
Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
|
|
55 |
by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
|
|
56 |
\ (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
|
|
57 |
by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
|
|
58 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
|
|
59 |
qed "diff_mult_distrib" ;
|
|
60 |
|
|
61 |
Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
|
|
62 |
by (simp_tac
|
|
63 |
(simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
|
|
64 |
qed "diff_mult_distrib2";
|
|
65 |
|
|
66 |
|
|
67 |
(*** Remainder ***)
|
|
68 |
|
|
69 |
(*We need m:nat even with natify*)
|
|
70 |
Goal "[| 0<n; n le m; m:nat |] ==> m #- n < m";
|
|
71 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
72 |
by (etac rev_mp 1);
|
|
73 |
by (etac rev_mp 1);
|
|
74 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
|
|
75 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
|
|
76 |
qed "div_termination";
|
|
77 |
|
|
78 |
val div_rls = (*for mod and div*)
|
|
79 |
nat_typechecks @
|
|
80 |
[Ord_transrec_type, apply_funtype, div_termination RS ltD,
|
|
81 |
nat_into_Ord, not_lt_iff_le RS iffD1];
|
|
82 |
|
|
83 |
val div_ss = simpset() addsimps [div_termination RS ltD,
|
|
84 |
not_lt_iff_le RS iffD2];
|
|
85 |
|
|
86 |
Goalw [raw_mod_def] "[| m:nat; n:nat |] ==> raw_mod (m, n) : nat";
|
|
87 |
by (rtac Ord_transrec_type 1);
|
|
88 |
by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
|
|
89 |
by (REPEAT (ares_tac div_rls 1));
|
|
90 |
qed "raw_mod_type";
|
|
91 |
|
|
92 |
Goalw [mod_def] "m mod n : nat";
|
|
93 |
by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1);
|
|
94 |
qed "mod_type";
|
|
95 |
AddTCs [mod_type];
|
|
96 |
AddIffs [mod_type];
|
|
97 |
|
|
98 |
|
|
99 |
(** Aribtrary definitions for division by zero. Useful to simplify
|
|
100 |
certain equations **)
|
|
101 |
|
|
102 |
Goalw [div_def] "a div 0 = 0";
|
|
103 |
by (rtac (raw_div_def RS def_transrec RS trans) 1);
|
|
104 |
by (Asm_simp_tac 1);
|
|
105 |
qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*)
|
|
106 |
|
|
107 |
Goalw [mod_def] "a mod 0 = natify(a)";
|
|
108 |
by (rtac (raw_mod_def RS def_transrec RS trans) 1);
|
|
109 |
by (Asm_simp_tac 1);
|
|
110 |
qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*)
|
|
111 |
|
|
112 |
fun div_undefined_case_tac s i =
|
|
113 |
case_tac s i THEN
|
|
114 |
asm_full_simp_tac
|
|
115 |
(simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN
|
|
116 |
asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV,
|
|
117 |
DIVISION_BY_ZERO_MOD]) i;
|
|
118 |
|
|
119 |
Goal "m<n ==> raw_mod (m,n) = m";
|
|
120 |
by (rtac (raw_mod_def RS def_transrec RS trans) 1);
|
|
121 |
by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
|
|
122 |
qed "raw_mod_less";
|
|
123 |
|
|
124 |
Goal "[| m<n; n : nat |] ==> m mod n = m";
|
|
125 |
by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
|
|
126 |
by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1);
|
|
127 |
qed "mod_less";
|
|
128 |
|
|
129 |
Goal "[| 0<n; n le m; m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)";
|
|
130 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
131 |
by (rtac (raw_mod_def RS def_transrec RS trans) 1);
|
|
132 |
by (asm_simp_tac div_ss 1);
|
|
133 |
by (Blast_tac 1);
|
|
134 |
qed "raw_mod_geq";
|
|
135 |
|
|
136 |
Goal "[| n le m; m:nat |] ==> m mod n = (m#-n) mod n";
|
|
137 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
138 |
by (div_undefined_case_tac "n=0" 1);
|
|
139 |
by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1);
|
|
140 |
qed "mod_geq";
|
|
141 |
|
|
142 |
Addsimps [mod_less];
|
|
143 |
|
|
144 |
|
|
145 |
(*** Division ***)
|
|
146 |
|
|
147 |
Goalw [raw_div_def] "[| m:nat; n:nat |] ==> raw_div (m, n) : nat";
|
|
148 |
by (rtac Ord_transrec_type 1);
|
|
149 |
by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
|
|
150 |
by (REPEAT (ares_tac div_rls 1));
|
|
151 |
qed "raw_div_type";
|
|
152 |
|
|
153 |
Goalw [div_def] "m div n : nat";
|
|
154 |
by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1);
|
|
155 |
qed "div_type";
|
|
156 |
AddTCs [div_type];
|
|
157 |
AddIffs [div_type];
|
|
158 |
|
|
159 |
Goal "m<n ==> raw_div (m,n) = 0";
|
|
160 |
by (rtac (raw_div_def RS def_transrec RS trans) 1);
|
|
161 |
by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
|
|
162 |
qed "raw_div_less";
|
|
163 |
|
|
164 |
Goal "[| m<n; n : nat |] ==> m div n = 0";
|
|
165 |
by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
|
|
166 |
by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1);
|
|
167 |
qed "div_less";
|
|
168 |
|
|
169 |
Goal "[| 0<n; n le m; m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))";
|
|
170 |
by (subgoal_tac "n ~= 0" 1);
|
|
171 |
by (Blast_tac 2);
|
|
172 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
173 |
by (rtac (raw_div_def RS def_transrec RS trans) 1);
|
|
174 |
by (asm_simp_tac div_ss 1);
|
|
175 |
qed "raw_div_geq";
|
|
176 |
|
|
177 |
Goal "[| 0<n; n le m; m:nat |] ==> m div n = succ ((m#-n) div n)";
|
|
178 |
by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
|
|
179 |
by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1);
|
|
180 |
qed "div_geq";
|
|
181 |
|
|
182 |
Addsimps [div_less, div_geq];
|
|
183 |
|
|
184 |
|
|
185 |
(*A key result*)
|
|
186 |
Goal "[| m: nat; n: nat |] ==> (m div n)#*n #+ m mod n = m";
|
|
187 |
by (div_undefined_case_tac "n=0" 1);
|
|
188 |
by (etac complete_induct 1);
|
|
189 |
by (case_tac "x<n" 1);
|
|
190 |
(*case n le x*)
|
|
191 |
by (asm_full_simp_tac
|
|
192 |
(simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
|
|
193 |
div_termination RS ltD, add_diff_inverse]) 2);
|
|
194 |
(*case x<n*)
|
|
195 |
by (Asm_simp_tac 1);
|
|
196 |
val lemma = result();
|
|
197 |
|
|
198 |
Goal "(m div n)#*n #+ m mod n = natify(m)";
|
|
199 |
by (subgoal_tac
|
|
200 |
"(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
|
|
201 |
\ natify(m)" 1);
|
|
202 |
by (stac lemma 2);
|
|
203 |
by Auto_tac;
|
|
204 |
qed "mod_div_equality_natify";
|
|
205 |
|
|
206 |
Goal "m: nat ==> (m div n)#*n #+ m mod n = m";
|
|
207 |
by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1);
|
|
208 |
qed "mod_div_equality";
|
|
209 |
|
|
210 |
|
|
211 |
(*** Further facts about mod (mainly for mutilated chess board) ***)
|
|
212 |
|
|
213 |
Goal "[| 0<n; m:nat; n:nat |] \
|
|
214 |
\ ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
|
|
215 |
by (etac complete_induct 1);
|
|
216 |
by (excluded_middle_tac "succ(x)<n" 1);
|
|
217 |
(* case succ(x) < n *)
|
|
218 |
by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans,
|
|
219 |
succ_neq_self]) 2);
|
|
220 |
by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
|
|
221 |
(* case n le succ(x) *)
|
|
222 |
by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
|
|
223 |
by (etac leE 1);
|
|
224 |
(*equality case*)
|
|
225 |
by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
|
|
226 |
by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD,
|
|
227 |
diff_succ]) 1);
|
|
228 |
val lemma = result();
|
|
229 |
|
|
230 |
Goal "n:nat ==> \
|
|
231 |
\ succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
|
|
232 |
by (case_tac "n=0" 1);
|
|
233 |
by (asm_simp_tac (simpset() addsimps [natify_succ, DIVISION_BY_ZERO_MOD]) 1);
|
|
234 |
by (subgoal_tac
|
|
235 |
"natify(succ(m)) mod n = \
|
|
236 |
\ (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1);
|
|
237 |
by (stac natify_succ 2);
|
|
238 |
by (rtac lemma 2);
|
|
239 |
by (auto_tac(claset(),
|
|
240 |
simpset() delsimps [natify_succ]
|
|
241 |
addsimps [nat_into_Ord RS Ord_0_lt_iff]));
|
|
242 |
qed "mod_succ";
|
|
243 |
|
|
244 |
Goal "[| 0<n; n:nat |] ==> m mod n < n";
|
|
245 |
by (subgoal_tac "natify(m) mod n < n" 1);
|
|
246 |
by (res_inst_tac [("i","natify(m)")] complete_induct 2);
|
|
247 |
by (case_tac "x<n" 3);
|
|
248 |
(*case x<n*)
|
|
249 |
by (Asm_simp_tac 3);
|
|
250 |
(*case n le x*)
|
|
251 |
by (asm_full_simp_tac
|
|
252 |
(simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
|
|
253 |
by Auto_tac;
|
|
254 |
qed "mod_less_divisor";
|
|
255 |
|
|
256 |
Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
|
|
257 |
by (subgoal_tac "k mod 2: 2" 1);
|
|
258 |
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
|
|
259 |
by (dtac ltD 1);
|
|
260 |
by Auto_tac;
|
|
261 |
qed "mod2_cases";
|
|
262 |
|
|
263 |
Goal "succ(succ(m)) mod 2 = m mod 2";
|
|
264 |
by (subgoal_tac "m mod 2: 2" 1);
|
|
265 |
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
|
|
266 |
by (auto_tac (claset(), simpset() addsimps [mod_succ]));
|
|
267 |
qed "mod2_succ_succ";
|
|
268 |
|
|
269 |
Addsimps [mod2_succ_succ];
|
|
270 |
|
|
271 |
Goal "(m#+m#+n) mod 2 = n mod 2";
|
|
272 |
by (subgoal_tac "(natify(m)#+natify(m)#+n) mod 2 = n mod 2" 1);
|
|
273 |
by (res_inst_tac [("n","natify(m)")] nat_induct 2);
|
|
274 |
by Auto_tac;
|
|
275 |
qed "mod2_add_more";
|
|
276 |
|
|
277 |
Goal "(m#+m) mod 2 = 0";
|
|
278 |
by (cut_inst_tac [("n","0")] mod2_add_more 1);
|
|
279 |
by Auto_tac;
|
|
280 |
qed "mod2_add_self";
|
|
281 |
|
|
282 |
Addsimps [mod2_add_more, mod2_add_self];
|
|
283 |
|
|
284 |
|
|
285 |
(**** Additional theorems about "le" ****)
|
|
286 |
|
|
287 |
Goal "m:nat ==> m le (m #+ n)";
|
|
288 |
by (induct_tac "m" 1);
|
|
289 |
by (ALLGOALS Asm_simp_tac);
|
|
290 |
qed "add_le_self";
|
|
291 |
|
|
292 |
Goal "m:nat ==> m le (n #+ m)";
|
|
293 |
by (stac add_commute 1);
|
|
294 |
by (etac add_le_self 1);
|
|
295 |
qed "add_le_self2";
|
|
296 |
|
|
297 |
(*** Monotonicity of Multiplication ***)
|
|
298 |
|
|
299 |
Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
|
|
300 |
by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
|
|
301 |
by (ftac lt_nat_in_nat 2);
|
|
302 |
by (res_inst_tac [("n","natify(k)")] nat_induct 3);
|
|
303 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
|
|
304 |
qed "mult_le_mono1";
|
|
305 |
|
|
306 |
(* le monotonicity, BOTH arguments*)
|
|
307 |
Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
|
|
308 |
by (rtac (mult_le_mono1 RS le_trans) 1);
|
|
309 |
by (REPEAT (assume_tac 1));
|
|
310 |
by (EVERY [stac mult_commute 1,
|
|
311 |
stac mult_commute 1,
|
|
312 |
rtac mult_le_mono1 1]);
|
|
313 |
by (REPEAT (assume_tac 1));
|
|
314 |
qed "mult_le_mono";
|
|
315 |
|
|
316 |
(*strict, in 1st argument; proof is by induction on k>0.
|
|
317 |
I can't see how to relax the typing conditions.*)
|
|
318 |
Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
|
|
319 |
by (etac zero_lt_natE 1);
|
|
320 |
by (ftac lt_nat_in_nat 2);
|
|
321 |
by (ALLGOALS Asm_simp_tac);
|
|
322 |
by (induct_tac "x" 1);
|
|
323 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
|
|
324 |
qed "mult_lt_mono2";
|
|
325 |
|
|
326 |
Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
|
|
327 |
by (asm_simp_tac (simpset() addsimps [mult_lt_mono2,
|
|
328 |
inst "n" "k" mult_commute]) 1);
|
|
329 |
qed "mult_lt_mono1";
|
|
330 |
|
|
331 |
Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
|
|
332 |
by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
|
|
333 |
by (res_inst_tac [("n","natify(m)")] natE 2);
|
|
334 |
by (res_inst_tac [("n","natify(n)")] natE 4);
|
|
335 |
by Auto_tac;
|
|
336 |
qed "add_eq_0_iff";
|
|
337 |
AddIffs [add_eq_0_iff];
|
|
338 |
|
|
339 |
Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
|
|
340 |
by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
|
|
341 |
\ 0 < natify(m) & 0 < natify(n)" 1);
|
|
342 |
by (res_inst_tac [("n","natify(m)")] natE 2);
|
|
343 |
by (res_inst_tac [("n","natify(n)")] natE 4);
|
|
344 |
by (res_inst_tac [("n","natify(n)")] natE 3);
|
|
345 |
by Auto_tac;
|
|
346 |
qed "zero_lt_mult_iff";
|
|
347 |
|
|
348 |
Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
|
|
349 |
by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
|
|
350 |
by (res_inst_tac [("n","natify(m)")] natE 2);
|
|
351 |
by (res_inst_tac [("n","natify(n)")] natE 4);
|
|
352 |
by Auto_tac;
|
|
353 |
qed "mult_eq_1_iff";
|
|
354 |
AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
|
|
355 |
|
|
356 |
(*Cancellation law for division*)
|
|
357 |
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
|
|
358 |
by (eres_inst_tac [("i","m")] complete_induct 1);
|
|
359 |
by (excluded_middle_tac "x<n" 1);
|
|
360 |
by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff,
|
|
361 |
mult_lt_mono2]) 2);
|
|
362 |
by (asm_full_simp_tac
|
|
363 |
(simpset() addsimps [not_lt_iff_le,
|
|
364 |
zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
|
|
365 |
diff_mult_distrib2 RS sym,
|
|
366 |
div_termination RS ltD]) 1);
|
|
367 |
qed "div_cancel";
|
|
368 |
|
|
369 |
Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \
|
|
370 |
\ (k#*m) mod (k#*n) = k #* (m mod n)";
|
|
371 |
by (eres_inst_tac [("i","m")] complete_induct 1);
|
|
372 |
by (excluded_middle_tac "x<n" 1);
|
|
373 |
by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff,
|
|
374 |
mult_lt_mono2]) 2);
|
|
375 |
by (asm_full_simp_tac
|
|
376 |
(simpset() addsimps [not_lt_iff_le,
|
|
377 |
zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
|
|
378 |
diff_mult_distrib2 RS sym,
|
|
379 |
div_termination RS ltD]) 1);
|
|
380 |
qed "mult_mod_distrib";
|
|
381 |
|
|
382 |
(*Lemma for gcd*)
|
|
383 |
Goal "m = m#*n ==> natify(n)=1 | m=0";
|
|
384 |
by (subgoal_tac "m: nat" 1);
|
|
385 |
by (etac ssubst 2);
|
|
386 |
by (rtac disjCI 1);
|
|
387 |
by (dtac sym 1);
|
|
388 |
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
|
|
389 |
by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
|
|
390 |
by Auto_tac;
|
|
391 |
by (subgoal_tac "m #* n = 0" 1);
|
|
392 |
by (stac (mult_natify2 RS sym) 2);
|
|
393 |
by (auto_tac (claset(), simpset() delsimps [mult_natify2]));
|
|
394 |
qed "mult_eq_self_implies_10";
|
|
395 |
|
|
396 |
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
|
|
397 |
by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
|
|
398 |
by (etac rev_mp 1);
|
|
399 |
by (induct_tac "n" 1);
|
|
400 |
by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
|
|
401 |
by (blast_tac (claset() addSEs [leE]
|
|
402 |
addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
|
|
403 |
qed_spec_mp "less_imp_succ_add";
|
|
404 |
|
|
405 |
|
|
406 |
|