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