|
1 (* Title : PNat.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : The positive naturals -- proofs |
|
5 : mainly as in Nat.thy |
|
6 *) |
|
7 |
|
8 open PNat; |
|
9 |
|
10 Goal "mono(%X. {1} Un (Suc``X))"; |
|
11 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1)); |
|
12 qed "pnat_fun_mono"; |
|
13 |
|
14 val pnat_unfold = pnat_fun_mono RS (pnat_def RS def_lfp_Tarski); |
|
15 |
|
16 Goal "1 : pnat"; |
|
17 by (stac pnat_unfold 1); |
|
18 by (rtac (singletonI RS UnI1) 1); |
|
19 qed "one_RepI"; |
|
20 |
|
21 Addsimps [one_RepI]; |
|
22 |
|
23 Goal "i: pnat ==> Suc(i) : pnat"; |
|
24 by (stac pnat_unfold 1); |
|
25 by (etac (imageI RS UnI2) 1); |
|
26 qed "pnat_Suc_RepI"; |
|
27 |
|
28 Goal "2 : pnat"; |
|
29 by (rtac (one_RepI RS pnat_Suc_RepI) 1); |
|
30 qed "two_RepI"; |
|
31 |
|
32 (*** Induction ***) |
|
33 |
|
34 val major::prems = goal thy |
|
35 "[| i: pnat; P(1); \ |
|
36 \ !!j. [| j: pnat; P(j) |] ==> P(Suc(j)) |] ==> P(i)"; |
|
37 by (rtac ([pnat_def, pnat_fun_mono, major] MRS def_induct) 1); |
|
38 by (blast_tac (claset() addIs prems) 1); |
|
39 qed "PNat_induct"; |
|
40 |
|
41 val prems = goalw thy [pnat_one_def,pnat_Suc_def] |
|
42 "[| P(1p); \ |
|
43 \ !!n. P(n) ==> P(pSuc n) |] ==> P(n)"; |
|
44 by (rtac (Rep_pnat_inverse RS subst) 1); |
|
45 by (rtac (Rep_pnat RS PNat_induct) 1); |
|
46 by (REPEAT (ares_tac prems 1 |
|
47 ORELSE eresolve_tac [Abs_pnat_inverse RS subst] 1)); |
|
48 qed "pnat_induct"; |
|
49 |
|
50 (*Perform induction on n. *) |
|
51 local fun raw_pnat_ind_tac a i = |
|
52 res_inst_tac [("n",a)] pnat_induct i THEN rename_last_tac a [""] (i+1) |
|
53 in |
|
54 val pnat_ind_tac = Datatype.occs_in_prems raw_pnat_ind_tac |
|
55 end; |
|
56 |
|
57 val prems = goal thy |
|
58 "[| !!x. P x 1p; \ |
|
59 \ !!y. P 1p (pSuc y); \ |
|
60 \ !!x y. [| P x y |] ==> P (pSuc x) (pSuc y) \ |
|
61 \ |] ==> P m n"; |
|
62 by (res_inst_tac [("x","m")] spec 1); |
|
63 by (pnat_ind_tac "n" 1); |
|
64 by (rtac allI 2); |
|
65 by (pnat_ind_tac "x" 2); |
|
66 by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1)); |
|
67 qed "pnat_diff_induct"; |
|
68 |
|
69 (*Case analysis on the natural numbers*) |
|
70 val prems = goal thy |
|
71 "[| n=1p ==> P; !!x. n = pSuc(x) ==> P |] ==> P"; |
|
72 by (subgoal_tac "n=1p | (EX x. n = pSuc(x))" 1); |
|
73 by (fast_tac (claset() addSEs prems) 1); |
|
74 by (pnat_ind_tac "n" 1); |
|
75 by (rtac (refl RS disjI1) 1); |
|
76 by (Blast_tac 1); |
|
77 qed "pnatE"; |
|
78 |
|
79 (*** Isomorphisms: Abs_Nat and Rep_Nat ***) |
|
80 |
|
81 Goal "inj_on Abs_pnat pnat"; |
|
82 by (rtac inj_on_inverseI 1); |
|
83 by (etac Abs_pnat_inverse 1); |
|
84 qed "inj_on_Abs_pnat"; |
|
85 |
|
86 Addsimps [inj_on_Abs_pnat RS inj_on_iff]; |
|
87 |
|
88 Goal "inj(Rep_pnat)"; |
|
89 by (rtac inj_inverseI 1); |
|
90 by (rtac Rep_pnat_inverse 1); |
|
91 qed "inj_Rep_pnat"; |
|
92 |
|
93 bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym); |
|
94 |
|
95 Goal "0 ~: pnat"; |
|
96 by (stac pnat_unfold 1); |
|
97 by Auto_tac; |
|
98 qed "zero_not_mem_pnat"; |
|
99 |
|
100 (* 0 : pnat ==> P *) |
|
101 bind_thm ("zero_not_mem_pnatE", zero_not_mem_pnat RS notE); |
|
102 |
|
103 Addsimps [zero_not_mem_pnat]; |
|
104 |
|
105 Goal "!!x. x : pnat ==> 0 < x"; |
|
106 by (dtac (pnat_unfold RS subst) 1); |
|
107 by Auto_tac; |
|
108 qed "mem_pnat_gt_zero"; |
|
109 |
|
110 Goal "!!x. 0 < x ==> x: pnat"; |
|
111 by (stac pnat_unfold 1); |
|
112 by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); |
|
113 by (etac exE 1 THEN Asm_simp_tac 1); |
|
114 by (induct_tac "m" 1); |
|
115 by (auto_tac (claset(),simpset() |
|
116 addsimps [one_RepI]) THEN dtac pnat_Suc_RepI 1); |
|
117 by (Blast_tac 1); |
|
118 qed "gt_0_mem_pnat"; |
|
119 |
|
120 Goal "(x: pnat) = (0 < x)"; |
|
121 by (blast_tac (claset() addDs [mem_pnat_gt_zero,gt_0_mem_pnat]) 1); |
|
122 qed "mem_pnat_gt_0_iff"; |
|
123 |
|
124 Goal "0 < Rep_pnat x"; |
|
125 by (rtac (Rep_pnat RS mem_pnat_gt_zero) 1); |
|
126 qed "Rep_pnat_gt_zero"; |
|
127 |
|
128 Goalw [pnat_add_def] "(x::pnat) + y = y + x"; |
|
129 by (simp_tac (simpset() addsimps [add_commute]) 1); |
|
130 qed "pnat_add_commute"; |
|
131 |
|
132 (** alternative definition for pnat **) |
|
133 (** order isomorphism **) |
|
134 Goal "pnat = {x::nat. 0 < x}"; |
|
135 by (rtac set_ext 1); |
|
136 by (simp_tac (simpset() addsimps |
|
137 [mem_pnat_gt_0_iff]) 1); |
|
138 qed "Collect_pnat_gt_0"; |
|
139 |
|
140 (*** Distinctness of constructors ***) |
|
141 |
|
142 Goalw [pnat_one_def,pnat_Suc_def] "pSuc(m) ~= 1p"; |
|
143 by (rtac (inj_on_Abs_pnat RS inj_on_contraD) 1); |
|
144 by (rtac (Rep_pnat_gt_zero RS Suc_mono RS less_not_refl2) 1); |
|
145 by (REPEAT (resolve_tac [Rep_pnat RS pnat_Suc_RepI, one_RepI] 1)); |
|
146 qed "pSuc_not_one"; |
|
147 |
|
148 bind_thm ("one_not_pSuc", pSuc_not_one RS not_sym); |
|
149 |
|
150 AddIffs [pSuc_not_one,one_not_pSuc]; |
|
151 |
|
152 bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE)); |
|
153 val one_neq_pSuc = sym RS pSuc_neq_one; |
|
154 |
|
155 (** Injectiveness of pSuc **) |
|
156 |
|
157 Goalw [pnat_Suc_def] "inj(pSuc)"; |
|
158 by (rtac injI 1); |
|
159 by (dtac (inj_on_Abs_pnat RS inj_onD) 1); |
|
160 by (REPEAT (resolve_tac [Rep_pnat, pnat_Suc_RepI] 1)); |
|
161 by (dtac (inj_Suc RS injD) 1); |
|
162 by (etac (inj_Rep_pnat RS injD) 1); |
|
163 qed "inj_pSuc"; |
|
164 |
|
165 val pSuc_inject = inj_pSuc RS injD; |
|
166 |
|
167 Goal "(pSuc(m)=pSuc(n)) = (m=n)"; |
|
168 by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]); |
|
169 qed "pSuc_pSuc_eq"; |
|
170 |
|
171 AddIffs [pSuc_pSuc_eq]; |
|
172 |
|
173 Goal "n ~= pSuc(n)"; |
|
174 by (pnat_ind_tac "n" 1); |
|
175 by (ALLGOALS Asm_simp_tac); |
|
176 qed "n_not_pSuc_n"; |
|
177 |
|
178 bind_thm ("pSuc_n_not_n", n_not_pSuc_n RS not_sym); |
|
179 |
|
180 Goal "!!n. n ~= 1p ==> EX m. n = pSuc m"; |
|
181 by (rtac pnatE 1); |
|
182 by (REPEAT (Blast_tac 1)); |
|
183 qed "not1p_implies_pSuc"; |
|
184 |
|
185 Goal "pSuc m = m + 1p"; |
|
186 by (auto_tac (claset(),simpset() addsimps [pnat_Suc_def, |
|
187 pnat_one_def,Abs_pnat_inverse,pnat_add_def])); |
|
188 qed "pSuc_is_plus_one"; |
|
189 |
|
190 Goal |
|
191 "(Rep_pnat x + Rep_pnat y): pnat"; |
|
192 by (cut_facts_tac [[Rep_pnat_gt_zero, |
|
193 Rep_pnat_gt_zero] MRS add_less_mono,Collect_pnat_gt_0] 1); |
|
194 by (etac ssubst 1); |
|
195 by Auto_tac; |
|
196 qed "sum_Rep_pnat"; |
|
197 |
|
198 Goalw [pnat_add_def] |
|
199 "Rep_pnat x + Rep_pnat y = Rep_pnat (x + y)"; |
|
200 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS |
|
201 Abs_pnat_inverse]) 1); |
|
202 qed "sum_Rep_pnat_sum"; |
|
203 |
|
204 Goalw [pnat_add_def] |
|
205 "(x + y) + z = x + (y + (z::pnat))"; |
|
206 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
207 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS |
|
208 Abs_pnat_inverse,add_assoc]) 1); |
|
209 qed "pnat_add_assoc"; |
|
210 |
|
211 Goalw [pnat_add_def] "x + (y + z) = y + (x + (z::pnat))"; |
|
212 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
213 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS |
|
214 Abs_pnat_inverse,add_left_commute]) 1); |
|
215 qed "pnat_add_left_commute"; |
|
216 |
|
217 (*Addition is an AC-operator*) |
|
218 val pnat_add_ac = [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]; |
|
219 |
|
220 Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)"; |
|
221 by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD), |
|
222 inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat])); |
|
223 qed "pnat_add_left_cancel"; |
|
224 |
|
225 Goalw [pnat_add_def] "(y + (x::pnat) = z + x) = (y = z)"; |
|
226 by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD), |
|
227 inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat])); |
|
228 qed "pnat_add_right_cancel"; |
|
229 |
|
230 Goalw [pnat_add_def] "!(y::pnat). x + y ~= x"; |
|
231 by (rtac (Rep_pnat_inverse RS subst) 1); |
|
232 by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)] |
|
233 addSDs [add_eq_self_zero], |
|
234 simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse, |
|
235 Rep_pnat_gt_zero RS less_not_refl2])); |
|
236 qed "pnat_no_add_ident"; |
|
237 |
|
238 |
|
239 (***) (***) (***) (***) (***) (***) (***) (***) (***) |
|
240 |
|
241 (*** pnat_less ***) |
|
242 |
|
243 Goalw [pnat_less_def] |
|
244 "!!x. [| x < (y::pnat); y < z |] ==> x < z"; |
|
245 by ((etac less_trans 1) THEN assume_tac 1); |
|
246 qed "pnat_less_trans"; |
|
247 |
|
248 Goalw [pnat_less_def] "!!x. x < (y::pnat) ==> ~ y < x"; |
|
249 by (etac less_not_sym 1); |
|
250 qed "pnat_less_not_sym"; |
|
251 |
|
252 (* [| x < y; y < x |] ==> P *) |
|
253 bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE); |
|
254 |
|
255 Goalw [pnat_less_def] "!!x. ~ y < (y::pnat)"; |
|
256 by Auto_tac; |
|
257 qed "pnat_less_not_refl"; |
|
258 |
|
259 bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE); |
|
260 |
|
261 Goalw [pnat_less_def] |
|
262 "!!x. x < (y::pnat) ==> x ~= y"; |
|
263 by Auto_tac; |
|
264 qed "pnat_less_not_refl2"; |
|
265 |
|
266 Goal "~ Rep_pnat y < 0"; |
|
267 by Auto_tac; |
|
268 qed "Rep_pnat_not_less0"; |
|
269 |
|
270 (*** Rep_pnat < 0 ==> P ***) |
|
271 bind_thm ("Rep_pnat_less_zeroE",Rep_pnat_not_less0 RS notE); |
|
272 |
|
273 Goal "~ Rep_pnat y < 1"; |
|
274 by (auto_tac (claset(),simpset() addsimps [less_Suc_eq, |
|
275 Rep_pnat_gt_zero,less_not_refl2])); |
|
276 qed "Rep_pnat_not_less_one"; |
|
277 |
|
278 (*** Rep_pnat < 1 ==> P ***) |
|
279 bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE); |
|
280 |
|
281 Goalw [pnat_less_def] |
|
282 "!!x. x < (y::pnat) ==> Rep_pnat y ~= 1"; |
|
283 by (auto_tac (claset(),simpset() |
|
284 addsimps [Rep_pnat_not_less_one] delsimps [less_one])); |
|
285 qed "Rep_pnat_gt_implies_not0"; |
|
286 |
|
287 Goalw [pnat_less_def] |
|
288 "(x::pnat) < y | x = y | y < x"; |
|
289 by (cut_facts_tac [less_linear] 1); |
|
290 by (fast_tac (claset() addIs [inj_Rep_pnat RS injD]) 1); |
|
291 qed "pnat_less_linear"; |
|
292 |
|
293 Goalw [le_def] "1 <= Rep_pnat x"; |
|
294 by (rtac Rep_pnat_not_less_one 1); |
|
295 qed "Rep_pnat_le_one"; |
|
296 |
|
297 Goalw [pnat_less_def] |
|
298 "!! (z1::nat). z1 < z2 ==> ? z3. z1 + Rep_pnat z3 = z2"; |
|
299 by (dtac less_imp_add_positive 1); |
|
300 by (auto_tac (claset() addSIs [Abs_pnat_inverse], |
|
301 simpset() addsimps [Collect_pnat_gt_0])); |
|
302 qed "lemma_less_ex_sum_Rep_pnat"; |
|
303 |
|
304 |
|
305 (*** pnat_le ***) |
|
306 |
|
307 Goalw [pnat_le_def] "!!x. ~ (x::pnat) < y ==> y <= x"; |
|
308 by (assume_tac 1); |
|
309 qed "pnat_leI"; |
|
310 |
|
311 Goalw [pnat_le_def] "!!x. (x::pnat) <= y ==> ~ y < x"; |
|
312 by (assume_tac 1); |
|
313 qed "pnat_leD"; |
|
314 |
|
315 val pnat_leE = make_elim pnat_leD; |
|
316 |
|
317 Goal "(~ (x::pnat) < y) = (y <= x)"; |
|
318 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1); |
|
319 qed "pnat_not_less_iff_le"; |
|
320 |
|
321 Goalw [pnat_le_def] "!!x. ~(x::pnat) <= y ==> y < x"; |
|
322 by (Blast_tac 1); |
|
323 qed "pnat_not_leE"; |
|
324 |
|
325 Goalw [pnat_le_def] "!!x. (x::pnat) < y ==> x <= y"; |
|
326 by (blast_tac (claset() addEs [pnat_less_asym]) 1); |
|
327 qed "pnat_less_imp_le"; |
|
328 |
|
329 (** Equivalence of m<=n and m<n | m=n **) |
|
330 |
|
331 Goalw [pnat_le_def] "!!m. m <= n ==> m < n | m=(n::pnat)"; |
|
332 by (cut_facts_tac [pnat_less_linear] 1); |
|
333 by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1); |
|
334 qed "pnat_le_imp_less_or_eq"; |
|
335 |
|
336 Goalw [pnat_le_def] "!!m. m<n | m=n ==> m <=(n::pnat)"; |
|
337 by (cut_facts_tac [pnat_less_linear] 1); |
|
338 by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1); |
|
339 qed "pnat_less_or_eq_imp_le"; |
|
340 |
|
341 Goal "(m <= (n::pnat)) = (m < n | m=n)"; |
|
342 by (REPEAT(ares_tac [iffI,pnat_less_or_eq_imp_le,pnat_le_imp_less_or_eq] 1)); |
|
343 qed "pnat_le_eq_less_or_eq"; |
|
344 |
|
345 Goal "n <= (n::pnat)"; |
|
346 by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1); |
|
347 qed "pnat_le_refl"; |
|
348 |
|
349 val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::pnat)"; |
|
350 by (dtac pnat_le_imp_less_or_eq 1); |
|
351 by (blast_tac (claset() addIs [pnat_less_trans]) 1); |
|
352 qed "pnat_le_less_trans"; |
|
353 |
|
354 Goal "!!i. [| i < j; j <= k |] ==> i < (k::pnat)"; |
|
355 by (dtac pnat_le_imp_less_or_eq 1); |
|
356 by (blast_tac (claset() addIs [pnat_less_trans]) 1); |
|
357 qed "pnat_less_le_trans"; |
|
358 |
|
359 Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::pnat)"; |
|
360 by (EVERY1[dtac pnat_le_imp_less_or_eq, |
|
361 dtac pnat_le_imp_less_or_eq, |
|
362 rtac pnat_less_or_eq_imp_le, |
|
363 blast_tac (claset() addIs [pnat_less_trans])]); |
|
364 qed "pnat_le_trans"; |
|
365 |
|
366 Goal "!!m. [| m <= n; n <= m |] ==> m = (n::pnat)"; |
|
367 by (EVERY1[dtac pnat_le_imp_less_or_eq, |
|
368 dtac pnat_le_imp_less_or_eq, |
|
369 blast_tac (claset() addIs [pnat_less_asym])]); |
|
370 qed "pnat_le_anti_sym"; |
|
371 |
|
372 Goal "(m::pnat) < n = (m <= n & m ~= n)"; |
|
373 by (rtac iffI 1); |
|
374 by (rtac conjI 1); |
|
375 by (etac pnat_less_imp_le 1); |
|
376 by (etac pnat_less_not_refl2 1); |
|
377 by (blast_tac (claset() addSDs [pnat_le_imp_less_or_eq]) 1); |
|
378 qed "pnat_less_le"; |
|
379 |
|
380 (** LEAST -- the least number operator **) |
|
381 |
|
382 Goal "(! m::pnat. P m --> n <= m) = (! m. m < n --> ~ P m)"; |
|
383 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1); |
|
384 val lemma = result(); |
|
385 |
|
386 (* Comment below from NatDef.ML where Least_nat_def is proved*) |
|
387 (* This is an old def of Least for nat, which is derived for compatibility *) |
|
388 Goalw [Least_def] |
|
389 "(LEAST n::pnat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))"; |
|
390 by (simp_tac (simpset() addsimps [lemma]) 1); |
|
391 qed "Least_pnat_def"; |
|
392 |
|
393 val [prem1,prem2] = goalw thy [Least_pnat_def] |
|
394 "[| P(k::pnat); !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k"; |
|
395 by (rtac select_equality 1); |
|
396 by (blast_tac (claset() addSIs [prem1,prem2]) 1); |
|
397 by (cut_facts_tac [pnat_less_linear] 1); |
|
398 by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1); |
|
399 qed "pnat_Least_equality"; |
|
400 |
|
401 (***) (***) (***) (***) (***) (***) (***) (***) |
|
402 |
|
403 (*** alternative definition for pnat_le ***) |
|
404 Goalw [pnat_le_def,pnat_less_def] |
|
405 "((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)"; |
|
406 by (auto_tac (claset() addSIs [leI] addSEs [leD],simpset())); |
|
407 qed "pnat_le_iff_Rep_pnat_le"; |
|
408 |
|
409 Goal "!!k::pnat. (k + m <= k + n) = (m<=n)"; |
|
410 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
411 sum_Rep_pnat_sum RS sym]) 1); |
|
412 qed "pnat_add_left_cancel_le"; |
|
413 |
|
414 Goalw [pnat_less_def] "!!k::pnat. (k + m < k + n) = (m<n)"; |
|
415 by (simp_tac (simpset() addsimps [sum_Rep_pnat_sum RS sym]) 1); |
|
416 qed "pnat_add_left_cancel_less"; |
|
417 |
|
418 Addsimps [pnat_add_left_cancel, pnat_add_right_cancel, |
|
419 pnat_add_left_cancel_le, pnat_add_left_cancel_less]; |
|
420 |
|
421 Goal "n <= ((m + n)::pnat)"; |
|
422 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
423 sum_Rep_pnat_sum RS sym,le_add2]) 1); |
|
424 qed "pnat_le_add2"; |
|
425 |
|
426 Goal "n <= ((n + m)::pnat)"; |
|
427 by (simp_tac (simpset() addsimps pnat_add_ac) 1); |
|
428 by (rtac pnat_le_add2 1); |
|
429 qed "pnat_le_add1"; |
|
430 |
|
431 (*** "i <= j ==> i <= j + m" ***) |
|
432 bind_thm ("pnat_trans_le_add1", pnat_le_add1 RSN (2,pnat_le_trans)); |
|
433 |
|
434 (*** "i <= j ==> i <= m + j" ***) |
|
435 bind_thm ("pnat_trans_le_add2", pnat_le_add2 RSN (2,pnat_le_trans)); |
|
436 |
|
437 (*"i < j ==> i < j + m"*) |
|
438 bind_thm ("pnat_trans_less_add1", pnat_le_add1 RSN (2,pnat_less_le_trans)); |
|
439 |
|
440 (*"i < j ==> i < m + j"*) |
|
441 bind_thm ("pnat_trans_less_add2", pnat_le_add2 RSN (2,pnat_less_le_trans)); |
|
442 |
|
443 Goalw [pnat_less_def] "!!i. i+j < (k::pnat) ==> i<k"; |
|
444 by (auto_tac (claset() addEs [add_lessD1], |
|
445 simpset() addsimps [sum_Rep_pnat_sum RS sym])); |
|
446 qed "pnat_add_lessD1"; |
|
447 |
|
448 Goal "!!i::pnat. ~ (i+j < i)"; |
|
449 by (rtac notI 1); |
|
450 by (etac (pnat_add_lessD1 RS pnat_less_irrefl) 1); |
|
451 qed "pnat_not_add_less1"; |
|
452 |
|
453 Goal "!!i::pnat. ~ (j+i < i)"; |
|
454 by (simp_tac (simpset() addsimps [pnat_add_commute, pnat_not_add_less1]) 1); |
|
455 qed "pnat_not_add_less2"; |
|
456 |
|
457 AddIffs [pnat_not_add_less1, pnat_not_add_less2]; |
|
458 |
|
459 Goal "!!k::pnat. m <= n ==> m <= n + k"; |
|
460 by (etac pnat_le_trans 1); |
|
461 by (rtac pnat_le_add1 1); |
|
462 qed "pnat_le_imp_add_le"; |
|
463 |
|
464 Goal "!!k::pnat. m < n ==> m < n + k"; |
|
465 by (etac pnat_less_le_trans 1); |
|
466 by (rtac pnat_le_add1 1); |
|
467 qed "pnat_less_imp_add_less"; |
|
468 |
|
469 Goal "m + k <= n --> m <= (n::pnat)"; |
|
470 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
471 sum_Rep_pnat_sum RS sym]) 1); |
|
472 by (fast_tac (claset() addIs [add_leD1]) 1); |
|
473 qed_spec_mp "pnat_add_leD1"; |
|
474 |
|
475 Goal "!!n::pnat. m + k <= n ==> k <= n"; |
|
476 by (full_simp_tac (simpset() addsimps [pnat_add_commute]) 1); |
|
477 by (etac pnat_add_leD1 1); |
|
478 qed_spec_mp "pnat_add_leD2"; |
|
479 |
|
480 Goal "!!n::pnat. m + k <= n ==> m <= n & k <= n"; |
|
481 by (blast_tac (claset() addDs [pnat_add_leD1, pnat_add_leD2]) 1); |
|
482 bind_thm ("pnat_add_leE", result() RS conjE); |
|
483 |
|
484 Goalw [pnat_less_def] |
|
485 "!!k l::pnat. [| k < l; m + l = k + n |] ==> m < n"; |
|
486 by (rtac less_add_eq_less 1 THEN assume_tac 1); |
|
487 by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum])); |
|
488 qed "pnat_less_add_eq_less"; |
|
489 |
|
490 (* ordering on positive naturals in terms of existence of sum *) |
|
491 (* could provide alternative definition -- Gleason *) |
|
492 Goalw [pnat_less_def,pnat_add_def] |
|
493 "(z1::pnat) < z2 = (? z3. z1 + z3 = z2)"; |
|
494 by (rtac iffI 1); |
|
495 by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1); |
|
496 by (dtac lemma_less_ex_sum_Rep_pnat 1); |
|
497 by (etac exE 1 THEN res_inst_tac [("x","z3")] exI 1); |
|
498 by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum,Rep_pnat_inverse])); |
|
499 by (res_inst_tac [("t","Rep_pnat z1")] (add_0_right RS subst) 1); |
|
500 by (auto_tac (claset(),simpset() addsimps [sum_Rep_pnat_sum RS sym, |
|
501 Rep_pnat_gt_zero] delsimps [add_0_right])); |
|
502 qed "pnat_less_iff"; |
|
503 |
|
504 Goal "(? (x::pnat). z1 + x = z2) | z1 = z2 \ |
|
505 \ |(? x. z2 + x = z1)"; |
|
506 by (cut_facts_tac [pnat_less_linear] 1); |
|
507 by (asm_full_simp_tac (simpset() addsimps [pnat_less_iff]) 1); |
|
508 qed "pnat_linear_Ex_eq"; |
|
509 |
|
510 Goal "!!(x::pnat). x + y = z ==> x < z"; |
|
511 by (rtac (pnat_less_iff RS iffD2) 1); |
|
512 by (Blast_tac 1); |
|
513 qed "pnat_eq_lessI"; |
|
514 |
|
515 (*** Monotonicity of Addition ***) |
|
516 |
|
517 (*strict, in 1st argument*) |
|
518 Goalw [pnat_less_def] "!!i j k::pnat. i < j ==> i + k < j + k"; |
|
519 by (auto_tac (claset() addIs [add_less_mono1], |
|
520 simpset() addsimps [sum_Rep_pnat_sum RS sym])); |
|
521 qed "pnat_add_less_mono1"; |
|
522 |
|
523 Goalw [pnat_less_def] "!!i j k::pnat. [|i < j; k < l|] ==> i + k < j + l"; |
|
524 by (auto_tac (claset() addIs [add_less_mono], |
|
525 simpset() addsimps [sum_Rep_pnat_sum RS sym])); |
|
526 qed "pnat_add_less_mono"; |
|
527 |
|
528 Goalw [pnat_less_def] |
|
529 "!!f. [| !!i j::pnat. i<j ==> f(i) < f(j); \ |
|
530 \ i <= j \ |
|
531 \ |] ==> f(i) <= (f(j)::pnat)"; |
|
532 by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD], |
|
533 simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
534 le_eq_less_or_eq])); |
|
535 qed "pnat_less_mono_imp_le_mono"; |
|
536 |
|
537 Goal "!!i j k::pnat. i<=j ==> i + k <= j + k"; |
|
538 by (res_inst_tac [("f", "%j. j+k")] pnat_less_mono_imp_le_mono 1); |
|
539 by (etac pnat_add_less_mono1 1); |
|
540 by (assume_tac 1); |
|
541 qed "pnat_add_le_mono1"; |
|
542 |
|
543 Goal "!!k l::pnat. [|i<=j; k<=l |] ==> i + k <= j + l"; |
|
544 by (etac (pnat_add_le_mono1 RS pnat_le_trans) 1); |
|
545 by (simp_tac (simpset() addsimps [pnat_add_commute]) 1); |
|
546 (*j moves to the end because it is free while k, l are bound*) |
|
547 by (etac pnat_add_le_mono1 1); |
|
548 qed "pnad_add_le_mono"; |
|
549 |
|
550 Goal "1 * Rep_pnat n = Rep_pnat n"; |
|
551 by (Asm_simp_tac 1); |
|
552 qed "Rep_pnat_mult_1"; |
|
553 |
|
554 Goal "Rep_pnat n * 1 = Rep_pnat n"; |
|
555 by (Asm_simp_tac 1); |
|
556 qed "Rep_pnat_mult_1_right"; |
|
557 |
|
558 Goal |
|
559 "(Rep_pnat x * Rep_pnat y): pnat"; |
|
560 by (cut_facts_tac [[Rep_pnat_gt_zero, |
|
561 Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1); |
|
562 by (etac ssubst 1); |
|
563 by Auto_tac; |
|
564 qed "mult_Rep_pnat"; |
|
565 |
|
566 Goalw [pnat_mult_def] |
|
567 "Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)"; |
|
568 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS |
|
569 Abs_pnat_inverse]) 1); |
|
570 qed "mult_Rep_pnat_mult"; |
|
571 |
|
572 Goalw [pnat_mult_def] "m * n = n * (m::pnat)"; |
|
573 by (full_simp_tac (simpset() addsimps [mult_commute]) 1); |
|
574 qed "pnat_mult_commute"; |
|
575 |
|
576 Goalw [pnat_mult_def,pnat_add_def] "(m + n)*k = (m*k) + ((n*k)::pnat)"; |
|
577 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
578 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS |
|
579 Abs_pnat_inverse,sum_Rep_pnat RS |
|
580 Abs_pnat_inverse, add_mult_distrib]) 1); |
|
581 qed "pnat_add_mult_distrib"; |
|
582 |
|
583 Goalw [pnat_mult_def,pnat_add_def] "k*(m + n) = (k*m) + ((k*n)::pnat)"; |
|
584 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
585 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS |
|
586 Abs_pnat_inverse,sum_Rep_pnat RS |
|
587 Abs_pnat_inverse, add_mult_distrib2]) 1); |
|
588 qed "pnat_add_mult_distrib2"; |
|
589 |
|
590 Goalw [pnat_mult_def] |
|
591 "(x * y) * z = x * (y * (z::pnat))"; |
|
592 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
593 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS |
|
594 Abs_pnat_inverse,mult_assoc]) 1); |
|
595 qed "pnat_mult_assoc"; |
|
596 |
|
597 Goalw [pnat_mult_def] "x * (y * z) = y * (x * (z::pnat))"; |
|
598 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
599 by (simp_tac (simpset() addsimps [mult_Rep_pnat RS |
|
600 Abs_pnat_inverse,mult_left_commute]) 1); |
|
601 qed "pnat_mult_left_commute"; |
|
602 |
|
603 Goalw [pnat_mult_def] "x * (Abs_pnat 1) = x"; |
|
604 by (full_simp_tac (simpset() addsimps [one_RepI RS Abs_pnat_inverse, |
|
605 Rep_pnat_inverse]) 1); |
|
606 qed "pnat_mult_1"; |
|
607 |
|
608 Goal "Abs_pnat 1 * x = x"; |
|
609 by (full_simp_tac (simpset() addsimps [pnat_mult_1, |
|
610 pnat_mult_commute]) 1); |
|
611 qed "pnat_mult_1_left"; |
|
612 |
|
613 (*Multiplication is an AC-operator*) |
|
614 val pnat_mult_ac = [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]; |
|
615 |
|
616 Goal "!!i j k::pnat. i<=j ==> i * k <= j * k"; |
|
617 by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
618 mult_Rep_pnat_mult RS sym,mult_le_mono1]) 1); |
|
619 qed "pnat_mult_le_mono1"; |
|
620 |
|
621 Goal "!!i::pnat. [| i<=j; k<=l |] ==> i*k<=j*l"; |
|
622 by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le, |
|
623 mult_Rep_pnat_mult RS sym,mult_le_mono]) 1); |
|
624 qed "pnat_mult_le_mono"; |
|
625 |
|
626 Goal "!!i::pnat. i<j ==> k*i < k*j"; |
|
627 by (asm_full_simp_tac (simpset() addsimps [pnat_less_def, |
|
628 mult_Rep_pnat_mult RS sym,Rep_pnat_gt_zero,mult_less_mono2]) 1); |
|
629 qed "pnat_mult_less_mono2"; |
|
630 |
|
631 Goal "!!i::pnat. i<j ==> i*k < j*k"; |
|
632 by (dtac pnat_mult_less_mono2 1); |
|
633 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [pnat_mult_commute]))); |
|
634 qed "pnat_mult_less_mono1"; |
|
635 |
|
636 Goalw [pnat_less_def] "(m*(k::pnat) < n*k) = (m<n)"; |
|
637 by (asm_full_simp_tac (simpset() addsimps [mult_Rep_pnat_mult |
|
638 RS sym,Rep_pnat_gt_zero]) 1); |
|
639 qed "pnat_mult_less_cancel2"; |
|
640 |
|
641 Goalw [pnat_less_def] "((k::pnat)*m < k*n) = (m<n)"; |
|
642 by (asm_full_simp_tac (simpset() addsimps [mult_Rep_pnat_mult |
|
643 RS sym,Rep_pnat_gt_zero]) 1); |
|
644 qed "pnat_mult_less_cancel1"; |
|
645 |
|
646 Addsimps [pnat_mult_less_cancel1, pnat_mult_less_cancel2]; |
|
647 |
|
648 Goalw [pnat_mult_def] "(m*(k::pnat) = n*k) = (m=n)"; |
|
649 by (auto_tac (claset() addSDs [inj_on_Abs_pnat RS inj_onD, |
|
650 inj_Rep_pnat RS injD] addIs [mult_Rep_pnat], |
|
651 simpset() addsimps [Rep_pnat_gt_zero RS mult_cancel2])); |
|
652 qed "pnat_mult_cancel2"; |
|
653 |
|
654 Goal "((k::pnat)*m = k*n) = (m=n)"; |
|
655 by (rtac (pnat_mult_cancel2 RS subst) 1); |
|
656 by (auto_tac (claset () addIs [pnat_mult_commute RS subst],simpset())); |
|
657 qed "pnat_mult_cancel1"; |
|
658 |
|
659 Addsimps [pnat_mult_cancel1, pnat_mult_cancel2]; |
|
660 |
|
661 Goal |
|
662 "!!(z1::pnat). z2*z3 = z4*z5 ==> z2*(z1*z3) = z4*(z1*z5)"; |
|
663 by (auto_tac (claset() addIs [pnat_mult_cancel1 RS iffD2], |
|
664 simpset() addsimps [pnat_mult_left_commute])); |
|
665 qed "pnat_same_multI2"; |
|
666 |
|
667 val [prem] = goal thy |
|
668 "(!!u. z = Abs_pnat(u) ==> P) ==> P"; |
|
669 by (cut_inst_tac [("x1","z")] |
|
670 (rewrite_rule [pnat_def] (Rep_pnat RS Abs_pnat_inverse)) 1); |
|
671 by (res_inst_tac [("u","Rep_pnat z")] prem 1); |
|
672 by (dtac (inj_Rep_pnat RS injD) 1); |
|
673 by (Asm_simp_tac 1); |
|
674 qed "eq_Abs_pnat"; |
|
675 |
|
676 (** embedding of naturals in positive naturals **) |
|
677 |
|
678 (* pnat_one_eq! *) |
|
679 Goalw [pnat_nat_def,pnat_one_def]"1p = *#0"; |
|
680 by (Full_simp_tac 1); |
|
681 qed "pnat_one_iff"; |
|
682 |
|
683 Goalw [pnat_nat_def,pnat_one_def,pnat_add_def] "1p + 1p = *#1"; |
|
684 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
685 by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)], |
|
686 simpset())); |
|
687 qed "pnat_two_eq"; |
|
688 |
|
689 Goal "inj(pnat_nat)"; |
|
690 by (rtac injI 1); |
|
691 by (rewtac pnat_nat_def); |
|
692 by (dtac (inj_on_Abs_pnat RS inj_onD) 1); |
|
693 by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset())); |
|
694 qed "inj_pnat_nat"; |
|
695 |
|
696 Goal "0 < n + 1"; |
|
697 by Auto_tac; |
|
698 qed "nat_add_one_less"; |
|
699 |
|
700 Goal "0 < n1 + n2 + 1"; |
|
701 by Auto_tac; |
|
702 qed "nat_add_one_less1"; |
|
703 |
|
704 (* this worked with one call to auto_tac before! *) |
|
705 Goalw [pnat_add_def,pnat_nat_def,pnat_one_def] |
|
706 "*#n1 + *#n2 = *#(n1 + n2) + 1p"; |
|
707 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
|
708 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1); |
|
709 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2); |
|
710 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 3); |
|
711 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 4); |
|
712 by (auto_tac (claset(), |
|
713 simpset() addsimps [sum_Rep_pnat_sum, |
|
714 nat_add_one_less,nat_add_one_less1])); |
|
715 qed "pnat_nat_add"; |
|
716 |
|
717 Goalw [pnat_nat_def,pnat_less_def] "(n < m) = (*#n < *#m)"; |
|
718 by (auto_tac (claset(),simpset() |
|
719 addsimps [Abs_pnat_inverse,Collect_pnat_gt_0])); |
|
720 qed "pnat_nat_less_iff"; |
|
721 |
|
722 Addsimps [pnat_nat_less_iff RS sym]; |
|
723 |