wellorderScript.sml
1Theory wellorder[bare]
2Ancestors
3 relation set_relation pred_set pair arithmetic option
4Libs
5 HolKernel Parse boolLib boolSimps mesonLib numLib InductiveDefinition tautLib
6 BasicProvers metisLib Lib simpLib pred_setLib QLib TotalDefn
7
8val _ = temp_delsimps ["NORMEQ_CONV"]
9
10fun K_TAC _ = ALL_TAC;
11fun METIS ths tm = prove(tm,METIS_TAC ths);
12
13fun SET_TAC L =
14 POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT COND_CASES_TAC THEN
15 REWRITE_TAC (append [EXTENSION, SUBSET_DEF, PSUBSET_DEF, DISJOINT_DEF,
16 SING_DEF] L) THEN
17 SIMP_TAC std_ss [NOT_IN_EMPTY, IN_UNIV, IN_UNION, IN_INTER, IN_DIFF,
18 IN_INSERT, IN_DELETE, IN_REST, IN_BIGINTER, IN_BIGUNION, IN_IMAGE,
19 GSPECIFICATION, IN_DEF, EXISTS_PROD] THEN METIS_TAC [];
20
21val FORALL_PROD = pairTheory.FORALL_PROD
22val EXISTS_PROD = pairTheory.EXISTS_PROD
23val EXISTS_SUM = sumTheory.EXISTS_SUM
24val FORALL_SUM = sumTheory.FORALL_SUM
25val ARITH_ss = numSimps.ARITH_ss
26
27fun bossify stac ths g ctxt =
28 stac (srw_ss_of ctxt ++ numSimps.ARITH_ss) ths g ctxt
29val simp = bossify asm_simp_tac
30val fs = bossify full_simp_tac
31val gvs = bossify (global_simp_tac {droptrues = true, elimvars = true,
32 oldestfirst = true, strip = true})
33val gs = bossify (global_simp_tac {droptrues = true, elimvars = false,
34 oldestfirst = true, strip = true})
35val rw = srw_tac[numSimps.ARITH_ss]
36val metis_tac = METIS_TAC
37
38Type inf = ``:num + 'a``
39
40Theorem let_thm[simp,local] = LET_THM
41
42(* there's another ``wellfounded`` in prim_recTheory with different type *)
43val _ = hide "wellfounded";
44
45Definition wellfounded_def:
46 wellfounded R <=>
47 !s. (?w. w IN s) ==> ?min. min IN s /\ !w. (w,min) IN R ==> w NOTIN s
48End
49Overload Wellfounded = ``wellfounded``
50
51Theorem wellfounded_WF:
52 !R. wellfounded R <=> WF (CURRY R)
53Proof
54 rw[wellfounded_def, WF_DEF, SPECIFICATION]
55QED
56
57Definition wellorder_def:
58 wellorder R <=>
59 wellfounded (strict R) /\ linear_order R (domain R UNION range R) /\
60 reflexive R (domain R UNION range R)
61End
62
63(* well order examples *)
64Theorem wellorder_EMPTY:
65 wellorder {}
66Proof
67 rw[wellorder_def, wellfounded_def, linear_order_def, transitive_def,
68 antisym_def, domain_def, range_def, reflexive_def, strict_def]
69QED
70
71Theorem wellorder_SING:
72 !x y. wellorder {(x,y)} <=> (x = y)
73Proof
74 rw[wellorder_def, wellfounded_def, strict_def, reflexive_def,
75 domain_def, range_def] >>
76 eq_tac >| [
77 metis_tac[],
78 simp[linear_order_def, transitive_def, domain_def, range_def, antisym_def]
79 ]
80QED
81
82Theorem rrestrict_SUBSET:
83 !r s. rrestrict r s SUBSET r
84Proof
85 rw[SUBSET_DEF,rrestrict_def] >> rw[]
86QED
87
88Theorem wellfounded_subset:
89 !r0 r. wellfounded r /\ r0 SUBSET r ==> wellfounded r0
90Proof
91 rw[wellfounded_def] >>
92 `?min. min IN s /\ !w. (w,min) IN r ==> w NOTIN s` by metis_tac [] >>
93 metis_tac [SUBSET_DEF]
94QED
95
96val wellorder_results = newtypeTools.rich_new_type
97 {tyname = "wellorder",
98 exthm = prove(``?x. wellorder x``, qexists_tac `{}` >> simp[wellorder_EMPTY]),
99 ABS = "mkWO",
100 REP = "destWO"};
101
102Theorem mkWO_destWO[simp] = #absrep_id wellorder_results
103Theorem destWO_mkWO = #repabs_pseudo_id wellorder_results
104
105val termP_term_REP = #termP_term_REP wellorder_results
106
107Definition elsOf_def:
108 elsOf w = domain (destWO w) UNION range (destWO w)
109End
110
111Overload WIN = ``\p w. p IN strict (destWO w)``
112val _ = set_fixity "WIN" (Infix(NONASSOC, 425))
113Overload WLE = ``\p w. p IN destWO w``
114val _ = set_fixity "WLE" (Infix(NONASSOC, 425))
115Overload wrange = ``\w. range (destWO w)``
116
117Theorem WIN_elsOf:
118 (x,y) WIN w ==> x IN elsOf w /\ y IN elsOf w
119Proof
120 rw[elsOf_def, range_def, domain_def, strict_def] >> metis_tac[]
121QED
122
123Theorem WLE_elsOf:
124 (x,y) WLE w ==> x IN elsOf w /\ y IN elsOf w
125Proof
126 rw[elsOf_def, range_def, domain_def] >> metis_tac[]
127QED
128
129Theorem WIN_trichotomy:
130 !x y. x IN elsOf w /\ y IN elsOf w ==>
131 (x,y) WIN w \/ (x = y) \/ (y,x) WIN w
132Proof
133 rpt strip_tac >>
134 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
135 fs[elsOf_def, wellorder_def, strict_def, linear_order_def] >> metis_tac[]
136QED
137
138Theorem WIN_REFL[simp]:
139 (x,x) WIN w <=> F
140Proof
141 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
142 fs[wellorder_def, strict_def]
143QED
144
145Theorem WLE_TRANS:
146 (x,y) WLE w /\ (y,z) WLE w ==> (x,z) WLE w
147Proof
148 strip_tac >>
149 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
150 fs[wellorder_def, linear_order_def, transitive_def] >> metis_tac[]
151QED
152
153Theorem WLE_ANTISYM:
154 (x,y) WLE w /\ (y,x) WLE w ==> (x = y)
155Proof
156 strip_tac >>
157 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
158 fs[wellorder_def, linear_order_def, antisym_def]
159QED
160
161Theorem WIN_WLE:
162 (x,y) WIN w ==> (x,y) WLE w
163Proof
164 rw[strict_def]
165QED
166
167Theorem elsOf_WLE:
168 x IN elsOf w <=> (x,x) WLE w
169Proof
170 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
171 fs[wellorder_def, elsOf_def, reflexive_def, in_domain, in_range] >>
172 metis_tac[]
173QED
174
175Theorem transitive_strict:
176 transitive r /\ antisym r ==> transitive (strict r)
177Proof
178 simp[transitive_def, strict_def, antisym_def] >> metis_tac[]
179QED
180
181Theorem WIN_TRANS:
182 (x,y) WIN w /\ (y,z) WIN w ==> (x,z) WIN w
183Proof
184 `transitive (destWO w) /\ antisym (destWO w)`
185 by metis_tac [termP_term_REP, wellorder_def, linear_order_def] >>
186 metis_tac [transitive_def, transitive_strict]
187QED
188
189Theorem WIN_WF:
190 wellfounded (\p. p WIN w)
191Proof
192 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
193 fs[wellorder_def] >>
194 qsuff_tac `(\p. p WIN w) = strict (destWO w)` >- simp[] >>
195 simp[FUN_EQ_THM, SPECIFICATION]
196QED
197
198val CURRY_def = pairTheory.CURRY_DEF |> SPEC_ALL |> ABS ``y:'b``
199 |> ABS ``x:'a``
200 |> SIMP_RULE (bool_ss ++ ETA_ss) []
201
202Theorem WIN_WF2 =
203 WIN_WF |> SIMP_RULE (srw_ss()) [wellfounded_WF, CURRY_def]
204
205Definition iseg_def: iseg w x = { y | (y,x) WIN w }
206End
207
208Theorem strict_subset:
209 r1 SUBSET r2 ==> strict r1 SUBSET strict r2
210Proof
211 simp[strict_def, SUBSET_DEF, FORALL_PROD]
212QED
213
214Theorem transitive_rrestrict:
215 transitive r ==> transitive (rrestrict r s)
216Proof
217 rw[transitive_def, rrestrict_def] >> metis_tac[]
218QED
219
220Theorem antisym_rrestrict:
221 antisym r ==> antisym (rrestrict r s)
222Proof
223 rw[antisym_def, rrestrict_def] >> metis_tac[]
224QED
225
226Theorem linear_order_rrestrict:
227 linear_order r (domain r UNION range r) ==>
228 linear_order (rrestrict r s)
229 (domain (rrestrict r s) UNION range (rrestrict r s))
230Proof
231 rw[linear_order_def, in_domain, in_range, antisym_rrestrict,
232 transitive_rrestrict] >>
233 fs[rrestrict_def] >> metis_tac[]
234QED
235
236Theorem reflexive_rrestrict:
237 reflexive r (domain r UNION range r) ==>
238 reflexive (rrestrict r s)
239 (domain (rrestrict r s) UNION range (rrestrict r s))
240Proof
241 rw[reflexive_def, rrestrict_def, in_domain, in_range] >> metis_tac[]
242QED
243
244Theorem wellorder_rrestrict:
245 wellorder (rrestrict (destWO w) s)
246Proof
247 `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
248 fs[wellorder_def] >>
249 rw[linear_order_rrestrict, reflexive_rrestrict] >>
250 match_mp_tac wellfounded_subset >>
251 qexists_tac `strict(destWO w)` >>
252 rw[rrestrict_SUBSET, strict_subset]
253QED
254
255Definition wobound_def:
256 wobound x w = mkWO (rrestrict (destWO w) (iseg w x))
257End
258
259Theorem WIN_wobound:
260 (x,y) WIN wobound z w <=> (x,z) WIN w /\ (y,z) WIN w /\ (x,y) WIN w
261Proof
262 rw[wobound_def, wellorder_rrestrict, destWO_mkWO,
263 strict_def] >>
264 rw[rrestrict_def, iseg_def, strict_def] >> metis_tac []
265QED
266
267Theorem WLE_wobound:
268 (x,y) WLE wobound z w <=> (x,z) WIN w /\ (y,z) WIN w /\ (x,y) WLE w
269Proof
270 rw[wobound_def, wellorder_rrestrict, destWO_mkWO] >>
271 rw[rrestrict_def, iseg_def] >> metis_tac[]
272QED
273
274Theorem wellorder_cases:
275 !w. ?s. wellorder s /\ (w = mkWO s)
276Proof
277 rw[Once (#termP_exists wellorder_results)] >>
278 simp_tac (srw_ss() ++ DNF_ss)[#absrep_id wellorder_results]
279QED
280
281Theorem WEXTENSION:
282 (w1 = w2) <=> !a b. (a,b) WLE w1 <=> (a,b) WLE w2
283Proof
284 qspec_then `w1` strip_assume_tac wellorder_cases >>
285 qspec_then `w2` strip_assume_tac wellorder_cases >>
286 simp[#term_ABS_pseudo11 wellorder_results, EXTENSION, FORALL_PROD,
287 destWO_mkWO]
288QED
289
290Theorem wobound2:
291 (a,b) WIN w ==> (wobound a (wobound b w) = wobound a w)
292Proof
293 simp[WEXTENSION, WLE_wobound, WIN_wobound] >> metis_tac [WIN_TRANS]
294QED
295
296Theorem wellorder_fromNat:
297 wellorder { (i,j) | i <= j /\ j < n }
298Proof
299 rw[wellorder_def, wellfounded_def, linear_order_def, in_range, in_domain,
300 reflexive_def,transitive_def,antisym_def] >>
301 qexists_tac `LEAST m. m IN s` >> numLib.LEAST_ELIM_TAC >> rw[strict_def] >>
302 metis_tac []
303QED
304
305Theorem INJ_preserves_transitive:
306 transitive r /\ INJ f (domain r UNION range r) t ==>
307 transitive (IMAGE (f ## f) r)
308Proof
309 simp[transitive_def, EXISTS_PROD] >> strip_tac >>
310 map_every qx_gen_tac [`x`, `y`, `z`] >>
311 simp[GSYM AND_IMP_INTRO] >>
312 disch_then (Q.X_CHOOSE_THEN `a` (Q.X_CHOOSE_THEN `b` strip_assume_tac)) >>
313 disch_then (Q.X_CHOOSE_THEN `b'` (Q.X_CHOOSE_THEN `c` strip_assume_tac)) >>
314 rw[] >> qabbrev_tac `DR = domain r UNION range r` >>
315 `b IN DR /\ b' IN DR` by (rw[Abbr`DR`, in_domain, in_range] >> metis_tac[]) >>
316 `b' = b` by metis_tac [INJ_DEF] >> rw[] >> metis_tac[]
317QED
318
319Theorem INJ_preserves_antisym:
320 antisym r /\ INJ f (domain r UNION range r) t ==> antisym (IMAGE (f ## f) r)
321Proof
322 simp[antisym_def, EXISTS_PROD] >> strip_tac >>
323 map_every qx_gen_tac [`x`, `y`] >> simp[GSYM AND_IMP_INTRO] >>
324 disch_then (Q.X_CHOOSE_THEN `a` (Q.X_CHOOSE_THEN `b` strip_assume_tac)) >>
325 disch_then (Q.X_CHOOSE_THEN `a'` (Q.X_CHOOSE_THEN `b'` strip_assume_tac)) >>
326 rw[] >> qabbrev_tac `DR = domain r UNION range r` >>
327 metis_tac [INJ_DEF, IN_UNION, in_domain, in_range]
328QED
329
330
331Theorem INJ_preserves_linear_order:
332 linear_order r (domain r UNION range r) /\ INJ f (domain r UNION range r) t ==>
333 linear_order (IMAGE (f ## f) r) (IMAGE f (domain r UNION range r))
334Proof
335 simp[linear_order_def, EXISTS_PROD] >> rpt strip_tac >| [
336 simp[SUBSET_DEF, in_domain, EXISTS_PROD] >> metis_tac[],
337 simp[SUBSET_DEF, in_range, EXISTS_PROD] >> metis_tac[],
338 metis_tac [INJ_preserves_transitive],
339 metis_tac [INJ_preserves_antisym],
340 prove_tac [INJ_DEF, IN_UNION, in_domain, in_range],
341 prove_tac [INJ_DEF, IN_UNION, in_domain, in_range],
342 prove_tac [INJ_DEF, IN_UNION, in_domain, in_range],
343 prove_tac [INJ_DEF, IN_UNION, in_domain, in_range]
344 ]
345QED
346
347Theorem domain_IMAGE_ff:
348 domain (IMAGE (f ## g) r) = IMAGE f (domain r)
349Proof
350 simp[domain_def, EXTENSION, EXISTS_PROD] >> prove_tac[]
351QED
352Theorem range_IMAGE_ff:
353 range (IMAGE (f ## g) r) = IMAGE g (range r)
354Proof
355 simp[range_def, EXTENSION, EXISTS_PROD] >> prove_tac[]
356QED
357
358Theorem INJ_preserves_wellorder:
359 wellorder r /\ INJ f (domain r UNION range r) t ==> wellorder (IMAGE (f ## f) r)
360Proof
361 simp[wellorder_def] >> rpt strip_tac >| [
362 fs[wellfounded_def, strict_def] >> qx_gen_tac `s` >>
363 disch_then (Q.X_CHOOSE_THEN `e` assume_tac) >>
364 asm_simp_tac (srw_ss() ++ DNF_ss) [EXISTS_PROD] >>
365 Cases_on `s INTER IMAGE f (domain r UNION range r) = {}` >-
366 (qexists_tac `e` >> fs[EXTENSION, in_domain, in_range] >> metis_tac[]) >>
367 pop_assum mp_tac >> qabbrev_tac `DR = domain r UNION range r` >>
368 asm_simp_tac (srw_ss() ++ DNF_ss)[EXTENSION] >>
369 qx_gen_tac `x` >> strip_tac >>
370 first_x_assum (qspec_then `{ x | x IN DR /\ f x IN s }` mp_tac) >>
371 asm_simp_tac (srw_ss() ++ SatisfySimps.SATISFY_ss) [] >>
372 disch_then (Q.X_CHOOSE_THEN `min` strip_assume_tac) >>
373 qexists_tac `f min` >> simp[] >> map_every qx_gen_tac [`a`, `b`] >>
374 rpt strip_tac >>
375 `a IN DR /\ b IN DR` by (rw[Abbr`DR`, in_domain, in_range] >> metis_tac[]) >>
376 `b = min` by metis_tac [INJ_DEF] >> metis_tac[],
377 simp[domain_IMAGE_ff, range_IMAGE_ff] >>
378 metis_tac [IMAGE_UNION, INJ_preserves_linear_order],
379 fs[reflexive_def, EXISTS_PROD, in_domain, in_range] >>
380 metis_tac[]
381 ]
382QED
383
384Theorem wellorder_fromNat_SUM:
385 wellorder { (INL i, INL j) | i <= j /\ j < n }
386Proof
387 qmatch_abbrev_tac `wellorder w` >>
388 qabbrev_tac `w0 = { (i,j) | i <= j /\ j < n }` >>
389 `w = IMAGE (INL ## INL) w0`
390 by simp[EXTENSION, Abbr`w`, Abbr`w0`, EXISTS_PROD] >>
391 simp[] >> match_mp_tac (GEN_ALL INJ_preserves_wellorder) >>
392 `wellorder w0` by simp[Abbr`w0`, wellorder_fromNat] >>
393 simp[INJ_DEF] >>
394 qexists_tac `IMAGE INL (domain w0 UNION range w0)` >>
395 simp[]
396QED
397
398Definition fromNatWO_def:
399 fromNatWO n = mkWO { (INL i, INL j) | i <= j /\ j < n }
400End
401
402Theorem fromNatWO_11:
403 (fromNatWO i = fromNatWO j) <=> (i = j)
404Proof
405 rw[fromNatWO_def, WEXTENSION, wellorder_fromNat_SUM,
406 destWO_mkWO] >>
407 simp[Once EQ_IMP_THM] >> strip_tac >>
408 spose_not_then assume_tac >>
409 `i < j \/ j < i` by DECIDE_TAC >| [
410 first_x_assum (qspecl_then [`INL i`, `INL i`] mp_tac),
411 first_x_assum (qspecl_then [`INL j`, `INL j`] mp_tac)
412 ] >> srw_tac[ARITH_ss][]
413QED
414
415Theorem elsOf_fromNatWO:
416 elsOf (fromNatWO n) = IMAGE INL (count n)
417Proof
418 simp[fromNatWO_def, EXTENSION, elsOf_def, destWO_mkWO,
419 wellorder_fromNat_SUM, in_domain, in_range, EQ_IMP_THM] >>
420 simp_tac (srw_ss() ++ DNF_ss ++ ARITH_ss) [] >>
421 qx_gen_tac `x` >> strip_tac >> disj1_tac >> qexists_tac `x` >> rw[]
422QED
423
424
425
426Theorem WLE_WIN:
427 (x,y) WLE w ==> (x = y) \/ (x,y) WIN w
428Proof
429 rw[strict_def]
430QED
431
432Theorem elsOf_wobound:
433 elsOf (wobound x w) = { y | (y,x) WIN w }
434Proof
435 simp[wobound_def, EXTENSION] >> qx_gen_tac `a` >>
436 simp[elsOf_def, wellorder_rrestrict, destWO_mkWO] >>
437 simp[rrestrict_def, iseg_def, domain_def, range_def] >>
438 metis_tac [elsOf_WLE, WIN_elsOf]
439QED
440
441Definition orderiso_def:
442 orderiso w1 w2 <=>
443 ?f. (!x. x IN elsOf w1 ==> f x IN elsOf w2) /\
444 (!x1 x2. x1 IN elsOf w1 /\ x2 IN elsOf w1 ==>
445 ((f x1 = f x2) = (x1 = x2))) /\
446 (!y. y IN elsOf w2 ==> ?x. x IN elsOf w1 /\ (f x = y)) /\
447 (!x y. (x,y) WIN w1 ==> (f x, f y) WIN w2)
448End
449
450Theorem orderiso_thm:
451 orderiso w1 w2 <=>
452 ?f. BIJ f (elsOf w1) (elsOf w2) /\
453 !x y. (x,y) WIN w1 ==> (f x, f y) WIN w2
454Proof
455 rw[orderiso_def, BIJ_DEF, INJ_DEF, SURJ_DEF] >> eq_tac >> rpt strip_tac >>
456 qexists_tac `f` >> metis_tac []
457QED
458
459Theorem orderiso_REFL:
460 !w. orderiso w w
461Proof
462 rw[orderiso_def] >> qexists_tac `\x.x` >> rw[]
463QED
464
465Theorem orderiso_SYM:
466 !w1 w2. orderiso w1 w2 ==> orderiso w2 w1
467Proof
468 rw[orderiso_thm] >>
469 qabbrev_tac `g = LINV f (elsOf w1)` >>
470 `BIJ g (elsOf w2) (elsOf w1)` by metis_tac [BIJ_LINV_BIJ] >>
471 qexists_tac `g` >> simp[] >>
472 rpt strip_tac >>
473 `x IN elsOf w2 /\ y IN elsOf w2` by metis_tac [WIN_elsOf] >>
474 `g x IN elsOf w1 /\ g y IN elsOf w1` by metis_tac [BIJ_DEF, INJ_DEF] >>
475 `(g x, g y) WIN w1 \/ (g x = g y) \/ (g y, g x) WIN w1`
476 by metis_tac [WIN_trichotomy]
477 >- (`x = y` by metis_tac [BIJ_DEF, INJ_DEF] >> fs[WIN_REFL]) >>
478 `(f (g y), f (g x)) WIN w2` by metis_tac [WIN_TRANS] >>
479 `(y,x) WIN w2` by metis_tac [BIJ_LINV_INV] >>
480 metis_tac [WIN_TRANS, WIN_REFL]
481QED
482
483Theorem orderiso_TRANS:
484 !w1 w2 w3. orderiso w1 w2 /\ orderiso w2 w3 ==> orderiso w1 w3
485Proof
486 rw[orderiso_def] >> qexists_tac `f' o f` >>
487 rw[] >> metis_tac []
488QED
489
490Definition orderlt_def:
491 orderlt w1 w2 = ?x. x IN elsOf w2 /\ orderiso w1 (wobound x w2)
492End
493
494Theorem orderlt_REFL:
495 orderlt w w = F
496Proof
497 simp[orderlt_def] >> qx_gen_tac `x` >> Cases_on `x IN elsOf w` >> simp[] >>
498 simp[orderiso_thm] >> qx_gen_tac `f` >>
499 Cases_on `BIJ f (elsOf w) (elsOf (wobound x w))` >> simp[strict_def] >>
500 spose_not_then strip_assume_tac >>
501 `f x IN elsOf (wobound x w)` by metis_tac [BIJ_IFF_INV] >>
502 `elsOf (wobound x w) = {y | (y,x) WIN w}`
503 by fs[elsOf_wobound] >>
504 `!n. (FUNPOW f (SUC n) x, FUNPOW f n x) WIN w`
505 by (Induct >> simp[] >- fs[] >>
506 `(FUNPOW f (SUC (SUC n)) x, FUNPOW f (SUC n) x) WIN wobound x w`
507 by metis_tac [arithmeticTheory.FUNPOW_SUC, WIN_WLE, WIN_REFL,
508 WLE_WIN] >>
509 fs [WIN_wobound]) >>
510 mp_tac WIN_WF >> simp[wellfounded_def] >>
511 qexists_tac `{ FUNPOW f n x | n | T }` >> simp[] >>
512 simp_tac (srw_ss() ++ DNF_ss)[] >> qx_gen_tac `min` >>
513 Cases_on `!n. min <> FUNPOW f n x` >- simp[] >>
514 fs[] >> DISJ2_TAC >> rw[] >> qexists_tac `SUC n` >>
515 rw[Once SPECIFICATION]
516QED
517
518Theorem FINITE_IMAGE_INJfn[local]:
519 !s. (!x y. x IN s /\ y IN s ==> ((f x = f y) = (x = y))) ==>
520 (FINITE (IMAGE f s) = FINITE s)
521Proof
522 rpt strip_tac >> simp[EQ_IMP_THM, IMAGE_FINITE] >>
523 qsuff_tac `!t. FINITE t ==>
524 !s'. s' SUBSET s /\ (t = IMAGE f s') ==> FINITE s'`
525 >- metis_tac[SUBSET_REFL] >>
526 Induct_on `FINITE t` >> conj_tac >- metis_tac[IMAGE_EQ_EMPTY, FINITE_EMPTY] >>
527 qx_gen_tac `t` >> strip_tac >> qx_gen_tac `e` >> strip_tac >>
528 qx_gen_tac `s'` >> strip_tac >>
529 `?d. (e = f d) /\ d IN s'`
530 by (pop_assum mp_tac >> simp[EXTENSION] >> metis_tac[]) >>
531 qsuff_tac `t = IMAGE f (s' DELETE d)`
532 >- metis_tac [FINITE_DELETE, DELETE_SUBSET, SUBSET_TRANS] >>
533 Q.UNDISCH_THEN `e INSERT t = IMAGE f s'` mp_tac >> simp[EXTENSION] >>
534 strip_tac >> qx_gen_tac `x` >>
535 `!x. x IN s' ==> x IN s` by fs[SUBSET_DEF] >>
536 Cases_on `x = f d` >> asm_simp_tac(srw_ss() ++ CONJ_ss)[] >- rw[] >>
537 first_x_assum (qspec_then `x` mp_tac) >> simp[] >> metis_tac []
538QED
539
540Theorem IMAGE_CARD_INJfn[local]:
541 !s. FINITE s /\ (!x y. x IN s /\ y IN s ==> ((f x = f y) = (x = y))) ==>
542 (CARD (IMAGE f s) = CARD s)
543Proof
544 rpt strip_tac >>
545 qsuff_tac `!t. FINITE t ==> t SUBSET s ==> (CARD (IMAGE f t) = CARD t)`
546 >- metis_tac [SUBSET_REFL] >>
547 Induct_on `FINITE t` >> simp[] >> rpt strip_tac >>
548 `!x. x IN t ==> x IN s` by fs[SUBSET_DEF] >>
549 asm_simp_tac (srw_ss() ++ CONJ_ss) []
550QED
551
552Theorem wobounds_preserve_bijections:
553 BIJ f (elsOf w1) (elsOf w2) /\ x IN elsOf w1 /\
554 (!x y. (x,y) WIN w1 ==> (f x, f y) WIN w2) ==>
555 BIJ f (elsOf (wobound x w1)) (elsOf (wobound (f x) w2))
556Proof
557 simp[BIJ_IFF_INV,elsOf_wobound] >> strip_tac >>
558 qexists_tac `g` >> rpt conj_tac >| [
559 qx_gen_tac `y` >> strip_tac >>
560 `y IN elsOf w2` by metis_tac [WIN_elsOf] >>
561 `g y IN elsOf w1` by metis_tac[] >>
562 metis_tac [WIN_trichotomy, WIN_REFL, WIN_TRANS],
563 metis_tac [WIN_elsOf],
564 metis_tac [WIN_elsOf]
565 ]
566QED
567
568Theorem orderlt_TRANS:
569 !w1 w2 w3. orderlt w1 w2 /\ orderlt w2 w3 ==> orderlt w1 w3
570Proof
571 simp[orderlt_def] >> rpt gen_tac >>
572 disch_then (CONJUNCTS_THEN2
573 (Q.X_CHOOSE_THEN `a` strip_assume_tac)
574 (Q.X_CHOOSE_THEN `b` strip_assume_tac)) >>
575 `(?f. BIJ f (elsOf w1) (elsOf (wobound a w2)) /\
576 !x y. (x,y) WIN w1 ==> (f x, f y) WIN wobound a w2) /\
577 (?g. BIJ g (elsOf w2) (elsOf (wobound b w3)) /\
578 !x y. (x,y) WIN w2 ==> (g x, g y) WIN wobound b w3)`
579 by metis_tac[orderiso_thm] >>
580 `g a IN elsOf (wobound b w3)` by metis_tac [BIJ_IFF_INV] >>
581 `(g a, b) WIN w3` by fs[elsOf_wobound, in_domain, in_range] >>
582 qexists_tac `g a` >> conj_tac >- metis_tac[WIN_elsOf] >>
583 match_mp_tac orderiso_TRANS >> qexists_tac `wobound a w2` >>
584 rw[] >> rw[orderiso_thm] >> qexists_tac `g` >> conj_tac >| [
585 `wobound (g a) w3 = wobound (g a) (wobound b w3)`
586 by rw[wobound2] >>
587 pop_assum SUBST1_TAC >>
588 match_mp_tac wobounds_preserve_bijections >> rw[],
589 fs[WIN_wobound]
590 ]
591QED
592
593Definition wleast_def:
594 wleast w s =
595 some x. x IN elsOf w /\ x NOTIN s /\
596 !y. y IN elsOf w /\ y NOTIN s /\ x <> y ==> (x,y) WIN w
597End
598
599Definition wo2wo_def:
600 wo2wo w1 w2 =
601 WFREC (\x y. (x,y) WIN w1)
602 (\f x. let s0 = IMAGE f (iseg w1 x) in
603 let s1 = IMAGE THE (s0 DELETE NONE)
604 in
605 if s1 = elsOf w2 then NONE
606 else wleast w2 s1)
607End
608
609Theorem restrict_away[local]:
610 IMAGE (RESTRICT f (\x y. (x,y) WIN w) x) (iseg w x) = IMAGE f (iseg w x)
611Proof
612 rw[EXTENSION, RESTRICT_DEF, iseg_def] >> srw_tac[CONJ_ss][]
613QED
614
615Theorem wo2wo_thm =
616 wo2wo_def |> concl |> strip_forall |> #2 |> rhs |> strip_comb |> #2
617 |> C ISPECL WFREC_THM
618 |> C MATCH_MP WIN_WF2
619 |> SIMP_RULE (srw_ss()) [Excl "let_thm"]
620 |> REWRITE_RULE [GSYM wo2wo_def, restrict_away]
621
622val WO_INDUCTION =
623 WF_INDUCTION_THM |> C MATCH_MP WIN_WF2 |> Q.GEN `w`
624 |> BETA_RULE
625
626Theorem wleast_IN_wo:
627 (wleast w s = SOME x) ==>
628 x IN elsOf w /\ x NOTIN s /\
629 !y. y IN elsOf w /\ y NOTIN s /\ x <> y ==> (x,y) WIN w
630Proof
631 simp[wleast_def] >> DEEP_INTRO_TAC some_intro >>
632 simp[]
633QED
634
635Theorem wleast_EQ_NONE:
636 (wleast w s = NONE) ==> elsOf w SUBSET s
637Proof
638 simp[wleast_def] >> DEEP_INTRO_TAC some_intro >> rw[] >>
639 simp[SUBSET_DEF] >>
640 qspec_then `w` ho_match_mp_tac WO_INDUCTION >>
641 qx_gen_tac `x` >> rpt strip_tac >>
642 first_x_assum (fn th => qspec_then `x` mp_tac th >> simp[] >>
643 disch_then strip_assume_tac) >>
644 `(y,x) WIN w` by metis_tac [WIN_trichotomy] >> metis_tac[]
645QED
646
647Theorem wo2wo_IN_w2:
648 !x y. (wo2wo w1 w2 x = SOME y) ==> y IN elsOf w2
649Proof
650 rw[Once wo2wo_thm, LET_THM] >> metis_tac [wleast_IN_wo]
651QED
652
653Theorem IMAGE_wo2wo_SUBSET:
654 IMAGE THE (IMAGE (wo2wo w1 w2) (iseg w1 x) DELETE NONE) SUBSET elsOf w2
655Proof
656 simp_tac (srw_ss() ++ DNF_ss) [SUBSET_DEF] >> qx_gen_tac `a` >>
657 Cases_on `wo2wo w1 w2 a` >> rw[] >> metis_tac [wo2wo_IN_w2]
658QED
659
660Theorem wo2wo_EQ_NONE:
661 !x. (wo2wo w1 w2 x = NONE) ==>
662 !y. (x,y) WIN w1 ==> (wo2wo w1 w2 y = NONE)
663Proof
664 ONCE_REWRITE_TAC [wo2wo_thm] >> rw[LET_THM] >>
665 fs[IMAGE_wo2wo_SUBSET,SET_EQ_SUBSET]
666 >- (
667 qsuff_tac `elsOf w2 ⊆ IMAGE THE (IMAGE (wo2wo w1 w2) (iseg w1 y) DELETE NONE)` >- fs[] >>
668 MATCH_MP_TAC SUBSET_TRANS >>
669 first_x_assum (irule_at (Pos hd)) >>
670 simp_tac (srw_ss() ++ DNF_ss) [SUBSET_DEF] >>
671 qsuff_tac `!a. a IN iseg w1 x ==> a IN iseg w1 y` >- metis_tac[] >>
672 rw[iseg_def] >> METIS_TAC[WIN_TRANS])
673 >- imp_res_tac wleast_EQ_NONE
674QED
675
676Theorem wo2wo_EQ_SOME_downwards:
677 !x y. (wo2wo w1 w2 x = SOME y) ==>
678 !x0. (x0,x) WIN w1 ==> ?y0. wo2wo w1 w2 x0 = SOME y0
679Proof
680 metis_tac [wo2wo_EQ_NONE, option_CASES]
681QED
682
683Overload woseg =
684 ``\w1 w2 x. IMAGE THE (IMAGE (wo2wo w1 w2) (iseg w1 x) DELETE NONE)``
685
686Theorem mono_woseg:
687 (x1,x2) WIN w1 ==> woseg w1 w2 x1 SUBSET woseg w1 w2 x2
688Proof
689 simp_tac(srw_ss() ++ DNF_ss) [SUBSET_DEF, iseg_def]>> metis_tac [WIN_TRANS]
690QED
691
692Theorem wo2wo_injlemma[local]:
693 (x,y) WIN w1 /\ (wo2wo w1 w2 y = SOME z) ==> (wo2wo w1 w2 x <> SOME z)
694Proof
695 rw[Once wo2wo_thm, LET_THM, SimpL ``$==>``] >> strip_tac >>
696 `z IN woseg w1 w2 y`
697 by (asm_simp_tac (srw_ss() ++ DNF_ss) [] >> qexists_tac `x` >>
698 simp[iseg_def]) >>
699 metis_tac [wleast_IN_wo]
700QED
701
702Theorem wo2wo_11:
703 x1 IN elsOf w1 /\ x2 IN elsOf w1 /\ (wo2wo w1 w2 x1 = SOME y) /\
704 (wo2wo w1 w2 x2 = SOME y) ==> (x1 = x2)
705Proof
706 rpt strip_tac >>
707 `(x1 = x2) \/ (x1,x2) WIN w1 \/ (x2,x1) WIN w1`
708 by metis_tac [WIN_trichotomy] >>
709 metis_tac [wo2wo_injlemma]
710QED
711
712Theorem wleast_SUBSET:
713 (wleast w s1 = SOME x) /\ (wleast w s2 = SOME y) /\ s1 SUBSET s2 ==>
714 (x = y) \/ (x,y) WIN w
715Proof
716 simp[wleast_def] >> DEEP_INTRO_TAC some_intro >> simp[] >>
717 DEEP_INTRO_TAC some_intro >> simp[] >> metis_tac[SUBSET_DEF]
718QED
719
720Theorem wo2wo_mono:
721 (wo2wo w1 w2 x0 = SOME y0) /\ (wo2wo w1 w2 x = SOME y) /\ (x0,x) WIN w1 ==>
722 (y0,y) WIN w2
723Proof
724 rpt strip_tac >>
725 `x0 IN elsOf w1 /\ x IN elsOf w1` by metis_tac [WIN_elsOf] >>
726 `y0 <> y` by metis_tac [WIN_REFL, wo2wo_11] >>
727 rpt (qpat_x_assum `wo2wo X Y Z = WW` mp_tac) >>
728 ONCE_REWRITE_TAC [wo2wo_thm] >> rw[LET_THM] >>
729 metis_tac [mono_woseg, wleast_SUBSET]
730QED
731
732Theorem wo2wo_ONTO:
733 x IN elsOf w1 /\ (wo2wo w1 w2 x = SOME y) /\ (y0,y) WIN w2 ==>
734 ?x0. x0 IN elsOf w1 /\ (wo2wo w1 w2 x0 = SOME y0)
735Proof
736 simp[SimpL ``$==>``, Once wo2wo_thm] >> rw[] >>
737 spose_not_then strip_assume_tac >>
738 `y0 NOTIN woseg w1 w2 x`
739 by (asm_simp_tac (srw_ss() ++ DNF_ss) [] >> qx_gen_tac `a` >>
740 `(wo2wo w1 w2 a = NONE) \/ ?y'. wo2wo w1 w2 a = SOME y'`
741 by metis_tac [option_CASES] >> simp[iseg_def] >>
742 metis_tac[WIN_elsOf]) >>
743 `y0 <> y` by metis_tac [WIN_REFL] >>
744 `y0 IN elsOf w2 /\ y IN elsOf w2` by metis_tac [WIN_elsOf] >>
745 metis_tac [WIN_TRANS, WIN_REFL, wleast_IN_wo]
746QED
747
748Theorem wo2wo_EQ_NONE_woseg:
749 (wo2wo w1 w2 x = NONE) ==> (elsOf w2 = woseg w1 w2 x)
750Proof
751 rw[Once wo2wo_thm, LET_THM] >>
752 spose_not_then strip_assume_tac >>
753 last_x_assum mp_tac >> simp[] >>
754 spose_not_then strip_assume_tac >>
755 fs[NOT_IS_SOME_EQ_NONE] >>
756 imp_res_tac wleast_EQ_NONE >>
757 metis_tac[IMAGE_wo2wo_SUBSET,SUBSET_DEF,EXTENSION]
758QED
759
760Theorem orderlt_trichotomy:
761 orderlt w1 w2 \/ orderiso w1 w2 \/ orderlt w2 w1
762Proof
763 Cases_on `?x. x IN elsOf w1 /\ (wo2wo w1 w2 x = NONE)` >| [
764 `?x0. wleast w1 { x | ?y. wo2wo w1 w2 x = SOME y } = SOME x0`
765 by (Cases_on `wleast w1 { x | ?y. wo2wo w1 w2 x = SOME y }` >>
766 rw[] >> imp_res_tac wleast_EQ_NONE >>
767 pop_assum mp_tac >> simp[SUBSET_DEF] >> qexists_tac `x` >>
768 rw[]) >>
769 pop_assum (mp_tac o MATCH_MP (GEN_ALL wleast_IN_wo)) >>
770 rw[] >>
771 `!x. (x,x0) WIN w1 ==> ?y. wo2wo w1 w2 x = SOME y`
772 by metis_tac [WIN_TRANS, WIN_REFL, WIN_elsOf] >>
773 qsuff_tac `orderlt w2 w1` >- rw[] >>
774 simp[orderlt_def] >> qexists_tac `x0` >> rw[] >>
775 MATCH_MP_TAC orderiso_SYM >>
776 rw[orderiso_def] >>
777 qexists_tac `THE o wo2wo w1 w2` >>
778 `elsOf (wobound x0 w1) = { x | (x,x0) WIN w1 }` by rw[elsOf_wobound] >>
779 simp[] >> rpt conj_tac >| [
780 metis_tac [wo2wo_IN_w2, THE_DEF],
781 metis_tac [wo2wo_11, THE_DEF, WIN_elsOf],
782 `elsOf w2 = woseg w1 w2 x0`
783 by metis_tac [wo2wo_EQ_NONE_woseg, option_CASES] >>
784 asm_simp_tac (srw_ss() ++ DNF_ss) [iseg_def] >>
785 metis_tac [option_CASES],
786 simp[WIN_wobound] >> metis_tac [THE_DEF, wo2wo_mono]
787 ],
788 ALL_TAC
789 ] >>
790 fs[METIS_PROVE []``(!x. ~P x \/ Q x) = (!x. P x ==> Q x)``,
791 METIS_PROVE [option_CASES, NOT_SOME_NONE]
792 ``(x <> NONE) <=> ?y. x = SOME y``] >>
793 Cases_on `elsOf w2 = { y | ?x. x IN elsOf w1 /\ (wo2wo w1 w2 x = SOME y) }`
794 >| [
795 qsuff_tac `orderiso w1 w2` >- rw[] >>
796 rw[orderiso_def] >> qexists_tac `THE o wo2wo w1 w2` >>
797 pop_assum (strip_assume_tac o SIMP_RULE (srw_ss()) [EXTENSION]) >>
798 simp[] >> rpt conj_tac >| [
799 metis_tac [THE_DEF, option_CASES],
800 metis_tac [wo2wo_11, THE_DEF, option_CASES],
801 metis_tac [THE_DEF],
802 metis_tac [THE_DEF, wo2wo_mono, WIN_elsOf,
803 option_CASES]
804 ],
805 ALL_TAC
806 ] >>
807 `?y. y IN elsOf w2 /\ !x. x IN elsOf w1 ==> (wo2wo w1 w2 x <> SOME y)`
808 by (pop_assum mp_tac >> simp[EXTENSION] >> metis_tac [wo2wo_IN_w2]) >>
809 qabbrev_tac `
810 y0_opt = wleast w2 { y | ?x. x IN elsOf w1 /\ (wo2wo w1 w2 x = SOME y) }
811 ` >>
812 `y0_opt <> NONE`
813 by (qunabbrev_tac `y0_opt` >> strip_tac >>
814 imp_res_tac wleast_EQ_NONE >> fs[SUBSET_DEF] >> metis_tac[]) >>
815 `?y0. y0_opt = SOME y0` by metis_tac [option_CASES] >>
816 qunabbrev_tac `y0_opt` >>
817 pop_assum (strip_assume_tac o MATCH_MP wleast_IN_wo) >> fs[] >>
818 qsuff_tac `orderlt w1 w2` >- rw[] >> simp[orderlt_def] >>
819 qexists_tac `y0` >> simp[orderiso_def] >>
820 qexists_tac `THE o wo2wo w1 w2` >>
821 `!a b. a IN elsOf w1 /\ (wo2wo w1 w2 a = SOME b) ==> (b,y0) WIN w2`
822 by (rpt strip_tac >>
823 `b <> y0` by metis_tac [] >>
824 `~((y0,b) WIN w2)`
825 by metis_tac [wo2wo_ONTO, NOT_SOME_NONE] >>
826 metis_tac [WIN_trichotomy, wo2wo_IN_w2]) >>
827 simp[elsOf_wobound] >> rpt conj_tac >| [
828 metis_tac [THE_DEF, option_CASES],
829 metis_tac [THE_DEF, wo2wo_11, option_CASES],
830 metis_tac [WIN_REFL, WIN_TRANS, WIN_elsOf, THE_DEF, option_CASES],
831 simp[WIN_wobound] >>
832 metis_tac [wo2wo_mono, THE_DEF, WIN_elsOf, option_CASES]
833 ]
834QED
835
836Definition wZERO_def: wZERO = mkWO {}
837End
838
839Theorem elsOf_wZERO[simp]:
840 elsOf wZERO = {}
841Proof
842 simp[wZERO_def, elsOf_def, destWO_mkWO,
843 wellorder_EMPTY, EXTENSION, in_domain, in_range]
844QED
845
846Theorem WIN_wZERO[simp]:
847 (x,y) WIN wZERO <=> F
848Proof
849 simp[wZERO_def, destWO_mkWO, wellorder_EMPTY,
850 strict_def]
851QED
852
853Theorem WLE_wZERO[simp]:
854 (x,y) WLE wZERO <=> F
855Proof
856 simp[wZERO_def, destWO_mkWO, wellorder_EMPTY]
857QED
858
859Theorem orderiso_wZERO:
860 orderiso wZERO w <=> (w = wZERO)
861Proof
862 simp[orderiso_thm, BIJ_EMPTY, EQ_IMP_THM] >>
863 Q.ISPEC_THEN `w` strip_assume_tac wellorder_cases >>
864 simp[elsOf_def, EXTENSION, in_range, in_domain, wZERO_def,
865 #term_ABS_pseudo11 wellorder_results, wellorder_EMPTY,
866 destWO_mkWO,
867 FORALL_PROD]
868QED
869
870Theorem elsOf_EQ_EMPTY[simp]:
871 (elsOf w = {}) <=> (w = wZERO)
872Proof
873 simp[EQ_IMP_THM] >> strip_tac >>
874 qsuff_tac `orderiso w wZERO` >- metis_tac [orderiso_wZERO, orderiso_SYM] >>
875 simp[orderiso_thm, BIJ_EMPTY] >> metis_tac [WIN_elsOf, NOT_IN_EMPTY]
876QED
877
878Theorem LT_wZERO:
879 orderlt w wZERO = F
880Proof
881 simp[orderlt_def]
882QED
883
884Theorem orderlt_WF:
885 WF (orderlt : 'a wellorder -> 'a wellorder -> bool)
886Proof
887 rw[prim_recTheory.WF_IFF_WELLFOUNDED, prim_recTheory.wellfounded_def] >>
888 spose_not_then strip_assume_tac >>
889 qabbrev_tac `w0 = f 0` >>
890 qsuff_tac `~ WF (\x y. (x,y) WIN w0)` >- rw[WIN_WF2] >>
891 simp[WF_DEF] >>
892 `!n. orderlt (f (SUC n)) w0`
893 by (Induct >- metis_tac [arithmeticTheory.ONE] >>
894 metis_tac [orderlt_TRANS]) >>
895 `!n. ?x. x IN elsOf w0 /\ orderiso (wobound x w0) (f (SUC n))`
896 by metis_tac [orderlt_def, orderiso_SYM] >>
897 qexists_tac `
898 \e. ?n. e IN elsOf w0 /\ orderiso (wobound e w0) (f (SUC n))
899 ` >> simp[] >> conj_tac >- metis_tac[] >>
900 qx_gen_tac `y` >>
901 Cases_on `y IN elsOf w0` >> simp[] >>
902 Cases_on `!n. ~ orderiso (wobound y w0) (f (SUC n))` >> simp[] >>
903 pop_assum (Q.X_CHOOSE_THEN `m` strip_assume_tac o SIMP_RULE (srw_ss()) []) >>
904 `orderlt (f (SUC (SUC m))) (f (SUC m))` by metis_tac[] >>
905 pop_assum (Q.X_CHOOSE_THEN `p` strip_assume_tac o
906 SIMP_RULE (srw_ss()) [orderlt_def]) >>
907 `?h. BIJ h (elsOf (f (SUC m))) (elsOf (wobound y w0)) /\
908 !a b. (a,b) WIN f (SUC m) ==> (h a, h b) WIN wobound y w0`
909 by metis_tac [orderiso_thm, orderiso_SYM] >>
910 qexists_tac `h p` >>
911 `h p IN elsOf (wobound y w0)` by metis_tac [BIJ_IFF_INV] >>
912 pop_assum mp_tac >> simp[elsOf_wobound] >> rw[] >>
913 qexists_tac `SUC m` >> conj_tac >- metis_tac [WIN_elsOf] >>
914 match_mp_tac (INST_TYPE [beta |-> alpha] orderiso_TRANS) >>
915 qexists_tac `wobound p (f (SUC m))` >>
916 Tactical.REVERSE conj_tac >- metis_tac [orderiso_SYM] >>
917 match_mp_tac orderiso_SYM >> simp[orderiso_thm] >> qexists_tac `h` >>
918 conj_tac
919 >- (`wobound (h p) w0 = wobound (h p) (wobound y w0)` by rw [wobound2] >>
920 pop_assum SUBST1_TAC >>
921 match_mp_tac wobounds_preserve_bijections >> rw[]) >>
922 fs[WIN_wobound]
923QED
924
925Theorem orderlt_orderiso:
926 orderiso x0 y0 /\ orderiso a0 b0 ==> (orderlt x0 a0 <=> orderlt y0 b0)
927Proof
928 rw[orderlt_def, EQ_IMP_THM] >| [
929 `orderiso y0 (wobound x a0)` by metis_tac [orderiso_SYM, orderiso_TRANS] >>
930 `?f. BIJ f (elsOf a0) (elsOf b0) /\
931 (!x y. (x,y) WIN a0 ==> (f x, f y) WIN b0)`
932 by metis_tac [orderiso_thm] >>
933 qexists_tac `f x` >> conj_tac
934 >- metis_tac [BIJ_DEF, INJ_DEF] >>
935 qsuff_tac `orderiso (wobound x a0) (wobound (f x) b0)`
936 >- metis_tac [orderiso_TRANS] >>
937 rw[orderiso_thm] >> qexists_tac `f` >> rw[WIN_wobound] >>
938 match_mp_tac wobounds_preserve_bijections >>
939 fs[orderiso_thm],
940 `orderiso x0 (wobound x b0)` by metis_tac [orderiso_TRANS] >>
941 `?f. BIJ f (elsOf b0) (elsOf a0) /\
942 (!x y. (x,y) WIN b0 ==> (f x, f y) WIN a0)`
943 by metis_tac [orderiso_thm, orderiso_SYM] >>
944 qexists_tac `f x` >> conj_tac >- metis_tac [BIJ_IFF_INV] >>
945 qsuff_tac `orderiso (wobound x b0) (wobound (f x) a0)`
946 >- metis_tac [orderiso_TRANS] >>
947 rw[orderiso_thm] >> qexists_tac `f` >> rw[WIN_wobound] >>
948 match_mp_tac wobounds_preserve_bijections >>
949 metis_tac [orderiso_thm, orderiso_SYM]
950 ]
951QED
952
953Definition finite_def:
954 finite w = FINITE (elsOf w)
955End
956
957Theorem finite_iso:
958 orderiso w1 w2 ==> (finite w1 <=> finite w2)
959Proof
960 rw[orderiso_thm, finite_def] >> metis_tac [BIJ_FINITE, BIJ_LINV_BIJ]
961QED
962
963Theorem finite_wZERO:
964 finite wZERO
965Proof
966 rw[finite_def]
967QED
968
969Theorem orderiso_unique:
970 BIJ f1 (elsOf w1) (elsOf w2) /\ BIJ f2 (elsOf w1) (elsOf w2) /\
971 (!x y. (x,y) WIN w1 ==> (f1 x, f1 y) WIN w2) /\
972 (!x y. (x,y) WIN w1 ==> (f2 x, f2 y) WIN w2) ==>
973 !x. x IN elsOf w1 ==> (f1 x = f2 x)
974Proof
975 rpt strip_tac >> spose_not_then strip_assume_tac >>
976 `wellorder (destWO w1)` by rw[termP_term_REP] >>
977 fs[wellorder_def, wellfounded_def] >>
978 first_x_assum (qspec_then `elsOf w1 INTER {x | f1 x <> f2 x}` mp_tac) >>
979 asm_simp_tac (srw_ss() ++ SatisfySimps.SATISFY_ss) [] >>
980 qx_gen_tac `min` >> Cases_on `min IN elsOf w1` >> fs[] >>
981 Cases_on `f1 min = f2 min` >> simp[] >>
982 Cases_on `(f1 min, f2 min) WIN w2` >| [
983 `?a. (f2 a = f1 min) /\ a IN elsOf w1` by metis_tac [BIJ_IFF_INV] >>
984 `(a,min) WIN w1` by metis_tac [WIN_trichotomy, WIN_TRANS, WIN_REFL] >>
985 metis_tac [BIJ_IFF_INV],
986 `(f2 min, f1 min) WIN w2` by metis_tac [BIJ_IFF_INV, WIN_trichotomy] >>
987 `?a. (f1 a = f2 min) /\ a IN elsOf w1` by metis_tac [BIJ_IFF_INV] >>
988 `(a,min) WIN w1` by metis_tac [WIN_trichotomy, WIN_TRANS, WIN_REFL] >>
989 metis_tac [BIJ_IFF_INV]
990 ]
991QED
992
993Theorem seteq_wlog:
994 !f.
995 (!a b. P a b ==> P b a) /\ (!x a b. P a b /\ x IN f a ==> x IN f b) ==>
996 (!a b. P a b ==> (f a = f b))
997Proof
998 rpt strip_tac >> match_mp_tac SUBSET_ANTISYM >> metis_tac[SUBSET_DEF]
999QED
1000
1001Theorem wo_INDUCTION =
1002 MATCH_MP WF_INDUCTION_THM WIN_WF2
1003 |> SIMP_RULE (srw_ss()) []
1004 |> Q.SPEC `\x. x IN elsOf w ==> P x`
1005 |> SIMP_RULE (srw_ss()) []
1006 |> Q.GEN `w` |> Q.GEN `P`
1007
1008Theorem FORALL_NUM:
1009 (!n. P n) <=> P 0 /\ !n. P (SUC n)
1010Proof
1011 metis_tac [arithmeticTheory.num_CASES]
1012QED
1013
1014Theorem strict_UNION:
1015 strict (r1 UNION r2) = strict r1 UNION strict r2
1016Proof
1017 simp[EXTENSION, FORALL_PROD, strict_def] >> metis_tac[]
1018QED
1019
1020Theorem WLE_WIN_EQ:
1021 (x,y) WLE w <=> (x = y) /\ x IN elsOf w \/ (x,y) WIN w
1022Proof
1023 metis_tac [elsOf_WLE, WLE_WIN, WIN_WLE]
1024QED
1025
1026Definition remove_def:
1027 remove e w = mkWO { (x,y) | x <> e /\ y <> e /\ (x,y) WLE w }
1028End
1029
1030Theorem wellorder_remove:
1031 wellorder { (x,y) | x <> e /\ y <> e /\ (x,y) WLE w }
1032Proof
1033 qspec_then `w` assume_tac (GEN_ALL termP_term_REP) >>
1034 qmatch_abbrev_tac `wellorder r` >>
1035 `r = rrestrict (destWO w) (elsOf w DELETE e)`
1036 by (simp[EXTENSION, Abbr`r`, rrestrict_def, FORALL_PROD] >>
1037 metis_tac [WLE_elsOf]) >>
1038 simp[wellorder_rrestrict]
1039QED
1040
1041Theorem elsOf_remove:
1042 elsOf (remove e w) = elsOf w DELETE e
1043Proof
1044 simp[elsOf_def, remove_def, wellorder_remove,
1045 destWO_mkWO] >>
1046 simp[domain_def, range_def, EXTENSION] >>
1047 metis_tac[WLE_elsOf, WLE_WIN_EQ]
1048QED
1049
1050Theorem WIN_remove:
1051 (x,y) WIN remove e w <=> x <> e /\ y <> e /\ (x,y) WIN w
1052Proof
1053 simp[remove_def, destWO_mkWO, wellorder_remove, strict_def]
1054QED
1055
1056Definition ADD1_def:
1057 ADD1 e w =
1058 if e IN elsOf w then w
1059 else
1060 mkWO (destWO w UNION {(x,e) | x IN elsOf w} UNION {(e,e)})
1061End
1062
1063Theorem wellorder_ADD1:
1064 e NOTIN elsOf w ==>
1065 wellorder (destWO w UNION {(x,e) | x IN elsOf w} UNION {(e,e)})
1066Proof
1067 `wellorder (destWO w)` by rw [termP_term_REP] >>
1068 rw[wellorder_def] >| [
1069 simp[wellfounded_def, strict_def] >> qx_gen_tac `s` >>
1070 disch_then (Q.X_CHOOSE_THEN `a` assume_tac) >>
1071 Cases_on `?b. b IN s /\ b IN elsOf w` >> fs[] >| [
1072 fs[wellorder_def, wellfounded_def] >>
1073 first_x_assum (qspec_then `elsOf w INTER s` mp_tac) >>
1074 asm_simp_tac (srw_ss() ++ SatisfySimps.SATISFY_ss)[] >>
1075 metis_tac [WLE_elsOf, WLE_WIN],
1076 qexists_tac `a` >> metis_tac [WLE_elsOf]
1077 ],
1078 fs[linear_order_def, wellorder_def] >>
1079 `domain (destWO w UNION {(x,e) | x IN elsOf w} UNION {(e,e)}) =
1080 e INSERT elsOf w`
1081 by (rw[EXTENSION, in_domain, in_range, EQ_IMP_THM] >>
1082 metis_tac [WLE_elsOf]) >>
1083 `range (destWO w UNION {(x,e) | x IN elsOf w} UNION {(e,e)}) =
1084 e INSERT elsOf w`
1085 by (rw[EXTENSION, in_domain, in_range] >>
1086 metis_tac [elsOf_WLE, WLE_elsOf]) >>
1087 simp[] >> rpt conj_tac >| [
1088 fs[transitive_def] >> metis_tac[WLE_elsOf, elsOf_WLE],
1089 fs[antisym_def] >> metis_tac[WLE_elsOf, elsOf_WLE],
1090 fs[in_domain, in_range] >> metis_tac[WLE_elsOf, elsOf_WLE]
1091 ],
1092 fs[wellorder_def, reflexive_def, in_domain, in_range] >>
1093 metis_tac[WLE_elsOf, elsOf_WLE]
1094 ]
1095QED
1096
1097Theorem elsOf_ADD1:
1098 elsOf (ADD1 e w) = e INSERT elsOf w
1099Proof
1100 simp[EXTENSION, ADD1_def, Once elsOf_def, SimpLHS] >>
1101 qx_gen_tac `x` >>
1102 rw[#repabs_pseudo_id wellorder_results, wellorder_ADD1] >| [
1103 fs[elsOf_def] >> metis_tac[],
1104 simp[in_domain, in_range] >> metis_tac [WLE_elsOf]
1105 ]
1106QED
1107
1108Theorem WIN_ADD1:
1109 (x,y) WIN ADD1 e w <=>
1110 e NOTIN elsOf w /\ x IN elsOf w /\ (y = e) \/
1111 (x,y) WIN w
1112Proof
1113 rw[#repabs_pseudo_id wellorder_results, wellorder_ADD1, ADD1_def,
1114 strict_def] >> metis_tac[]
1115QED
1116
1117Theorem elsOf_cardeq_iso:
1118 INJ f (elsOf (wo:'b wellorder)) univ(:'a) ==>
1119 ?wo':'a wellorder. orderiso wo wo'
1120Proof
1121 simp[elsOf_def] >> strip_tac >>
1122 `wellorder (destWO wo)` by simp[#termP_term_REP wellorder_results] >>
1123 qexists_tac `mkWO (IMAGE (f ## f) (destWO wo))` >>
1124 simp[orderiso_thm] >>
1125 `wellorder (IMAGE (f ## f) (destWO wo))`
1126 by imp_res_tac INJ_preserves_wellorder >>
1127 qexists_tac `f` >>
1128 simp[destWO_mkWO, elsOf_def, domain_IMAGE_ff, range_IMAGE_ff] >>
1129 simp_tac bool_ss [GSYM IMAGE_UNION] >>
1130 qabbrev_tac `
1131 els = domain (destWO wo) UNION range (destWO wo)` >>
1132 simp[BIJ_DEF, SURJ_IMAGE] >>
1133 simp[strict_def, EXISTS_PROD] >>
1134 fs[INJ_DEF] >>
1135 map_every qx_gen_tac [`x`, `y`] >> strip_tac >>
1136 `x IN elsOf wo /\ y IN elsOf wo` by metis_tac [WLE_elsOf] >>
1137 fs[elsOf_def] >> metis_tac[IN_UNION]
1138QED
1139
1140fun unabbrev_in_goal s = let
1141 fun check th = let
1142 val c = concl th
1143 val _ = match_term ``Abbrev b`` c
1144 val (v,ty) = c |> rand |> lhand |> dest_var
1145 in
1146 if v = s then let
1147 val th' = PURE_REWRITE_RULE [markerTheory.Abbrev_def] th
1148 in
1149 SUBST1_TAC th'
1150 end
1151 else NO_TAC
1152 end
1153in
1154 first_assum check
1155end
1156
1157Theorem allsets_wellorderable:
1158 !s. ?wo. elsOf wo = s
1159Proof
1160 gen_tac >>
1161 qabbrev_tac `A = { w | elsOf w SUBSET s }` >>
1162 qabbrev_tac `
1163 R = { (w1,w2) | w1 IN A /\ w2 IN A /\
1164 ((w1 = w2) \/ ?x. x IN elsOf w2 /\ (w1 = wobound x w2)) }
1165 ` >>
1166 `A <> {}` by (simp[EXTENSION, Abbr`A`] >> qexists_tac `wZERO` >> simp[]) >>
1167 `partial_order R A`
1168 by (simp[partial_order_def, Abbr`R`, domain_def, range_def] >>
1169 rpt conj_tac
1170 >- simp_tac (srw_ss() ++ DNF_ss) [SUBSET_DEF]
1171 >- simp_tac (srw_ss() ++ DNF_ss) [SUBSET_DEF]
1172 >- (simp[transitive_def] >> rw[] >> fs[elsOf_wobound] >>
1173 metis_tac[wobound2, WIN_elsOf])
1174 >- simp[reflexive_def]
1175 >> simp[antisym_def] >> rw[] >> fs[elsOf_wobound] >>
1176 metis_tac[orderlt_def, orderiso_REFL, orderlt_REFL,
1177 wobound2, WIN_elsOf]) >>
1178 `!c. chain c R ==> upper_bounds c R <> {}`
1179 by (simp[EXTENSION, chain_def, upper_bounds_def] >> gen_tac >> strip_tac >>
1180 qabbrev_tac `Ls = BIGUNION (IMAGE destWO c)` >>
1181 `!x y. (x,y) IN Ls <=> ?w. w IN c /\ (x,y) WLE w`
1182 by (simp_tac (srw_ss() ++ DNF_ss) [Abbr`Ls`] >> metis_tac[]) >>
1183 `!w1 w2. w1 IN c /\ w2 IN c ==> elsOf w1 SUBSET elsOf w2 \/ elsOf w2 SUBSET elsOf w1`
1184 by (rpt strip_tac >> `(w1,w2) IN R \/ (w2,w1) IN R` by metis_tac[] >>
1185 pop_assum mp_tac >> simp[Abbr`R`] >> rw[] >- simp[]
1186 >- (simp[SUBSET_DEF, elsOf_wobound] >> metis_tac [WIN_elsOf])
1187 >- simp[] >>
1188 simp[SUBSET_DEF, elsOf_wobound] >> metis_tac [WIN_elsOf]) >>
1189 `!e. e IN (domain Ls UNION range Ls) <=> ?w. w IN c /\ e IN elsOf w`
1190 by (simp[domain_def, range_def] >> gen_tac >>
1191 eq_tac >- metis_tac [WLE_elsOf] >>
1192 metis_tac [elsOf_WLE]) >>
1193 `wellorder Ls`
1194 by (simp[wellorder_def] >> rpt conj_tac
1195 >- ((* WF *)simp[wellfounded_def, strict_def] >>
1196 simp_tac(srw_ss() ++ DNF_ss)[] >>
1197 map_every qx_gen_tac [`ss`, `x`] >> strip_tac >>
1198 Cases_on `?w. w IN c /\ ss INTER elsOf w <> {}`
1199 >- (fs[] >>
1200 `wellorder (destWO w)` by simp [termP_term_REP] >>
1201 `wellfounded (strict (destWO w))` by fs[wellorder_def] >>
1202 pop_assum (qspec_then `ss INTER elsOf w` mp_tac o
1203 SIMP_RULE (srw_ss()) [wellfounded_def]) >>
1204 simp_tac (srw_ss() ++ DNF_ss)[] >>
1205 `?y. y IN ss /\ y IN elsOf w`
1206 by (fs[EXTENSION] >> metis_tac[]) >>
1207 disch_then (qspec_then `y` mp_tac) >> simp[] >>
1208 disch_then (Q.X_CHOOSE_THEN `min` strip_assume_tac) >>
1209 qexists_tac `min` >> simp[] >>
1210 map_every qx_gen_tac [`z`, `w'`] >> strip_tac >>
1211 `!u. (u,min) WIN w ==> u NOTIN ss` by metis_tac [WIN_elsOf] >>
1212 Cases_on `w = w'` >- metis_tac[WLE_WIN_EQ] >>
1213 `(w,w') IN R \/ (w',w) IN R` by metis_tac[] >>
1214 pop_assum mp_tac >>
1215 asm_simp_tac (srw_ss() ++ DNF_ss) [Abbr`R`] >>
1216 qx_gen_tac `b` >> strip_tac >>
1217 first_x_assum match_mp_tac
1218 >- (simp[WIN_wobound] >> fs[elsOf_wobound] >>
1219 metis_tac[WLE_WIN_EQ, WIN_TRANS]) >>
1220 metis_tac [WIN_wobound, WLE_WIN_EQ]) >>
1221 fs[] >> qexists_tac `x` >> simp[] >>
1222 fs[EXTENSION] >> metis_tac[WLE_elsOf])
1223 >- ((* linear *)
1224 simp[linear_order_def] >> rpt conj_tac
1225 >- ((* transitive *)
1226 simp[transitive_def] >>
1227 map_every qx_gen_tac [`x`, `y`, `z`] >>
1228 disch_then (CONJUNCTS_THEN2
1229 (Q.X_CHOOSE_THEN `w1` strip_assume_tac)
1230 (Q.X_CHOOSE_THEN `w2` strip_assume_tac)) >>
1231 `(w1,w2) IN R \/ (w2,w1) IN R` by simp[] >>
1232 pop_assum mp_tac >> simp[Abbr`R`] >>
1233 Cases_on `w1 = w2` >- metis_tac [WLE_TRANS] >> simp[]>>
1234 rw[] >> fs[WLE_wobound] >> metis_tac[WLE_TRANS])
1235 >- ((* antisym *)
1236 simp[antisym_def] >>
1237 map_every qx_gen_tac [`x`, `y`] >>
1238 disch_then (CONJUNCTS_THEN2
1239 (Q.X_CHOOSE_THEN `w1` strip_assume_tac)
1240 (Q.X_CHOOSE_THEN `w2` strip_assume_tac)) >>
1241 `(w1,w2) IN R \/ (w2,w1) IN R` by simp[] >>
1242 pop_assum mp_tac >> simp[Abbr`R`] >>
1243 Cases_on `w1 = w2` >- metis_tac [WLE_ANTISYM] >> simp[]>>
1244 rw[] >> fs[WLE_wobound] >> metis_tac [WLE_ANTISYM]) >>
1245 (* trichotomous *)
1246 map_every qx_gen_tac [`x`, `y`] >>
1247 disch_then (CONJUNCTS_THEN2
1248 (Q.X_CHOOSE_THEN `w1` strip_assume_tac)
1249 (Q.X_CHOOSE_THEN `w2` strip_assume_tac)) >>
1250 `(w1,w2) IN R \/ (w2,w1) IN R` by simp[] >>
1251 pop_assum mp_tac >> simp[Abbr`R`] >>
1252 Cases_on `w1 = w2`
1253 >- metis_tac [WIN_trichotomy, WLE_WIN_EQ] >> simp[]>>
1254 rw[] >> fs[elsOf_wobound] >>
1255 metis_tac [WIN_elsOf, WIN_trichotomy, WLE_WIN_EQ]) >>
1256 (* reflexive *)
1257 simp[reflexive_def] >> simp[elsOf_WLE]) >>
1258 qexists_tac `mkWO Ls` >> conj_tac
1259 >- ((* mkWO Ls IN range R *)
1260 simp[range_def] >> qexists_tac `wZERO` >>
1261 map_every unabbrev_in_goal ["R", "A"] >> simp[] >> conj_tac
1262 >- (asm_simp_tac bool_ss [elsOf_def, SUBSET_DEF, destWO_mkWO] >>
1263 simp_tac bool_ss [GSYM elsOf_def] >> qx_gen_tac `x` >>
1264 disch_then (Q.X_CHOOSE_THEN `w` strip_assume_tac) >>
1265 qpat_x_assum `w IN c`
1266 (fn th =>
1267 first_x_assum
1268 (fn imp => mp_tac (MATCH_MP imp (CONJ th th)) >>
1269 simp[SUBSET_DEF, Abbr`R`, Abbr`A`] >>
1270 NO_TAC))) >>
1271 Cases_on `c = {}` >- fs[Abbr`Ls`, wZERO_def] >>
1272 Cases_on `c = {wZERO}` >- fs[Abbr`Ls`] >>
1273 `?w. w IN c /\ w <> wZERO` by (fs[EXTENSION] >> metis_tac[]) >>
1274 DISJ2_TAC >> qexists_tac `THE (wleast w {})` >>
1275 Cases_on `wleast w {}` >- (imp_res_tac wleast_EQ_NONE >> fs[]) >>
1276 pop_assum (mp_tac o MATCH_MP wleast_IN_wo) >> simp[] >>
1277 strip_tac >> asm_simp_tac bool_ss [elsOf_def, destWO_mkWO] >>
1278 simp_tac bool_ss [GSYM elsOf_def] >> conj_tac >- metis_tac[] >>
1279 simp[wobound_def,iseg_def, destWO_mkWO, strict_def] >>
1280 qmatch_abbrev_tac `wZERO = mkWO (rrestrict Ls ss)` >>
1281 qsuff_tac `ss = {}` >- simp[wZERO_def, rrestrict_def] >>
1282 qunabbrev_tac `ss` >> simp[EXTENSION] >>
1283 qx_gen_tac `y` >> Cases_on `x = y` >> simp[] >>
1284 qx_gen_tac `w'` >> Cases_on `w' IN c` >> simp[] >>
1285 `(w,w') IN R \/ (w',w) IN R` by simp[] >>
1286 pop_assum mp_tac >> simp[Abbr`R`] >>
1287 Cases_on `w = w'` >> simp[]
1288 >- metis_tac[WLE_WIN_EQ, WIN_elsOf, WIN_TRANS, WIN_REFL]
1289 >- (rw[] >> fs[elsOf_wobound, WIN_wobound] >>
1290 metis_tac [WLE_WIN_EQ, WIN_TRANS, WIN_REFL])
1291 >- metis_tac[WLE_WIN_EQ, WIN_elsOf, WIN_TRANS, WIN_REFL] >>
1292 rw[] >> rw[WLE_wobound] >>
1293 metis_tac [WIN_TRANS, WIN_REFL, WLE_WIN_EQ, WIN_elsOf]) >>
1294 (* mkWO Ls actually is u.b. *)
1295 qx_gen_tac `y` >> Cases_on `y IN c` >> simp[] >>
1296 `(y,y) IN R` by metis_tac[] >> pop_assum mp_tac >>
1297 unabbrev_in_goal "R" >> simp[] >> disch_then (K ALL_TAC) >>
1298 `mkWO Ls IN A`
1299 by (simp[Abbr`A`] >>
1300 asm_simp_tac bool_ss [elsOf_def, destWO_mkWO, SUBSET_DEF] >>
1301 simp_tac bool_ss [GSYM elsOf_def] >> qx_gen_tac `x` >>
1302 disch_then (Q.X_CHOOSE_THEN `w` strip_assume_tac) >>
1303 `(w,w) IN R` by metis_tac [] >> pop_assum mp_tac >>
1304 simp[Abbr`R`, SUBSET_DEF]) >> simp[] >>
1305 Cases_on `y = mkWO Ls` >> simp[] >>
1306 `elsOf y SUBSET elsOf (mkWO Ls)`
1307 by (asm_simp_tac bool_ss [SUBSET_DEF, elsOf_def, destWO_mkWO] >>
1308 metis_tac[]) >>
1309 `elsOf y <> elsOf (mkWO Ls)`
1310 by (strip_tac >>
1311 `y = mkWO Ls`
1312 by (ONCE_REWRITE_TAC [SYM (#term_REP_11 wellorder_results)] >>
1313 simp[EXTENSION, destWO_mkWO, FORALL_PROD] >>
1314 map_every qx_gen_tac [`a`, `b`] >> eq_tac >- metis_tac[] >>
1315 disch_then (Q.X_CHOOSE_THEN `w` strip_assume_tac) >>
1316 `(y,w) IN R \/ (w,y) IN R` by simp[] >>
1317 pop_assum mp_tac >> simp[Abbr`R`] >> Cases_on `w = y` >>
1318 simp[] >> TRY (fs[] >> NO_TAC) >>
1319 asm_simp_tac (srw_ss() ++ DNF_ss) [] >>
1320 qx_gen_tac `x` >> strip_tac >> rw[]
1321 >- (`x NOTIN elsOf (wobound x w)`
1322 by simp_tac(srw_ss())[elsOf_wobound] >>
1323 `x IN elsOf (mkWO Ls)`
1324 by (asm_simp_tac bool_ss [destWO_mkWO, elsOf_def] >>
1325 simp_tac bool_ss [GSYM elsOf_def] >>
1326 metis_tac[]) >> metis_tac[]) >>
1327 fs[WLE_wobound])) >>
1328 `?a. a IN elsOf (mkWO Ls) /\ a NOTIN elsOf y`
1329 by (fs[EXTENSION, SUBSET_DEF] >> metis_tac[]) >>
1330 qexists_tac `THE (wleast (mkWO Ls) (elsOf y))` >>
1331 `(wleast (mkWO Ls) (elsOf y) = NONE) \/
1332 ?b. wleast (mkWO Ls) (elsOf y) = SOME b`
1333 by (Cases_on `wleast (mkWO Ls) (elsOf y)` >> simp[])
1334 >- (imp_res_tac wleast_EQ_NONE >> metis_tac [SUBSET_ANTISYM]) >>
1335 simp[] >>
1336 pop_assum (mp_tac o MATCH_MP wleast_IN_wo) >> strip_tac >> simp[] >>
1337 ONCE_REWRITE_TAC [SYM (#term_REP_11 wellorder_results)] >>
1338 simp[EXTENSION, WLE_wobound, FORALL_PROD, destWO_mkWO, strict_def] >>
1339 map_every qx_gen_tac [`d`, `e`] >> eq_tac
1340 >- (`?w. w IN c /\ b IN elsOf w` by metis_tac[elsOf_def, destWO_mkWO] >>
1341 strip_tac >>
1342 `d IN elsOf w /\ e IN elsOf w`
1343 by metis_tac[WLE_elsOf, SUBSET_DEF] >>
1344 `(w,y) IN R \/ (y,w) IN R` by simp[]
1345 >- (pop_assum mp_tac >> simp[Abbr`R`] >> `w <> y` by metis_tac[] >>
1346 simp[GSYM RIGHT_EXISTS_AND_THM] >>
1347 disch_then (Q.X_CHOOSE_THEN `x` strip_assume_tac) >>
1348 rw[] >> fs[elsOf_wobound] >> metis_tac [WIN_elsOf]) >>
1349 pop_assum mp_tac >> simp[Abbr`R`] >> `w <> y` by metis_tac[] >>
1350 simp[GSYM RIGHT_EXISTS_AND_THM] >>
1351 disch_then (Q.X_CHOOSE_THEN `x` strip_assume_tac) >>
1352 fs[WLE_wobound, elsOf_wobound] >> qexists_tac `w` >> simp[] >>
1353 `b = x`
1354 by (`x IN elsOf (mkWO Ls)`
1355 by (simp[elsOf_def, destWO_mkWO] >>
1356 metis_tac [IN_UNION, elsOf_def]) >>
1357 first_x_assum (qspec_then `x` mp_tac) >> simp[] >>
1358 Cases_on `b = x` >> simp[destWO_mkWO] >>
1359 simp_tac (srw_ss()) [strict_def] >> DISJ1_TAC >>
1360 `(x,b) WIN w` by metis_tac [WIN_trichotomy] >>
1361 `(x,b) IN Ls` by metis_tac [WLE_WIN_EQ] >> strip_tac >>
1362 metis_tac [WLE_ANTISYM, destWO_mkWO]) >>
1363 pop_assum SUBST_ALL_TAC >> metis_tac [WIN_REFL, WLE_WIN_EQ]) >>
1364 simp_tac (srw_ss() ++ CONJ_ss) [WLE_WIN_EQ] >>
1365 `!i w. w IN c /\ (i,b) WIN w ==> i IN elsOf y`
1366 by (rpt strip_tac >> first_x_assum (qspec_then `i` mp_tac) >>
1367 `b <> i` by metis_tac [WIN_REFL] >>
1368 `i IN elsOf (mkWO Ls)`
1369 by metis_tac [WIN_elsOf, elsOf_def, destWO_mkWO] >>
1370 simp[destWO_mkWO] >> simp_tac (srw_ss()) [strict_def] >>
1371 `(i,b) IN Ls` by metis_tac[WLE_WIN_EQ] >>
1372 metis_tac[destWO_mkWO, WLE_ANTISYM]) >>
1373 Cases_on `d <> b` >> simp[] >> Cases_on `e = b` >> simp[] >>
1374 Cases_on `d = e` >> simp[] >>
1375 metis_tac[WIN_trichotomy, WLE_WIN_EQ, WLE_ANTISYM, destWO_mkWO]) >>
1376 `?M. M IN maximal_elements A R` by metis_tac [zorns_lemma] >>
1377 pop_assum mp_tac >> simp[maximal_elements_def] >> strip_tac >>
1378 Cases_on `elsOf M = s` >- metis_tac[] >>
1379 `elsOf M SUBSET s` by fs[Abbr`A`] >>
1380 `?a. a IN s /\ a NOTIN elsOf M`
1381 by (fs[EXTENSION, SUBSET_DEF] >> metis_tac[]) >>
1382 qabbrev_tac `Ms = destWO M UNION {(x,a) | x IN elsOf M} UNION {(a,a)}` >>
1383 `ADD1 a M IN A` by simp[Abbr`A`, elsOf_ADD1] >>
1384 `M <> ADD1 a M`
1385 by (disch_then (mp_tac o Q.AP_TERM `elsOf`) >>
1386 simp[EXTENSION, elsOf_ADD1] >> metis_tac[]) >>
1387 `(M,ADD1 a M) IN R`
1388 by (unabbrev_in_goal "R" >> simp[] >> qexists_tac `a` >>
1389 simp[WEXTENSION, WLE_wobound, WIN_ADD1, WLE_WIN_EQ, elsOf_ADD1] >>
1390 `!x. ~((x,a) WIN M)` by metis_tac [WIN_elsOf] >> simp[] >>
1391 metis_tac[WIN_elsOf]) >>
1392 metis_tac[]
1393QED
1394
1395Theorem reln_to_rel[local]:
1396 reln_to_rel = CURRY
1397Proof
1398 simp[FUN_EQ_THM, reln_to_rel_def, IN_DEF]
1399QED
1400
1401Theorem StrongWellOrderExists:
1402 ?R:'a -> 'a -> bool. StrongLinearOrder R /\ WF R
1403Proof
1404 qspec_then ‘univ(:'a)’ (qx_choose_then ‘wo’ assume_tac)
1405 allsets_wellorderable >>
1406 qspec_then ‘wo’ mp_tac (GEN_ALL termP_term_REP) >>
1407 simp[wellorder_def] >> gs[elsOf_def] >>
1408 strip_tac >> qexists_tac ‘CURRY $ strict $ destWO wo’ >>
1409 gs[wellfounded_WF] >>
1410 simp[GSYM strict_linear_order_reln_to_rel_conv_UNIV, GSYM reln_to_rel,
1411 strict_linear_order]
1412QED
1413
1414
1415(* ------------------------------------------------------------------------- *)
1416(* Wellfoundedness (WF) from hol-light's iterateTheory *)
1417(* ------------------------------------------------------------------------- *)
1418
1419(* Only used as a variable; don't want to contaminate other uses.
1420 In particular, this is used at quite a different precedence for left-shift
1421 in descendents of words
1422*)
1423val _ = temp_set_fixity "<<" (Infix(NONASSOC, 450));
1424
1425
1426Theorem WF:
1427 WF(<<) <=> !P:'a->bool. (?x. P(x)) ==> (?x. P(x) /\ !y. y << x ==> ~P(y))
1428Proof
1429 METIS_TAC [WF_DEF]
1430QED
1431
1432(* ------------------------------------------------------------------------- *)
1433(* Strengthen it to equality. *)
1434(* ------------------------------------------------------------------------- *)
1435
1436Theorem WF_EQ:
1437 WF(<<) <=> !P:'a->bool. (?x. P(x)) <=> (?x. P(x) /\ !y. y << x ==> ~P(y))
1438Proof
1439 REWRITE_TAC[WF] THEN MESON_TAC[]
1440QED
1441
1442(* ------------------------------------------------------------------------- *)
1443(* Equivalence of wellfounded induction. *)
1444(* ------------------------------------------------------------------------- *)
1445
1446Theorem WF_IND:
1447 WF(<<) <=> !P:'a->bool. (!x. (!y. y << x ==> P(y)) ==> P(x)) ==> !x. P(x)
1448Proof
1449 REWRITE_TAC[WF] THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC THEN
1450 POP_ASSUM(MP_TAC o SPEC ``\x:'a. ~(P:'a->bool)(x)``) THEN REWRITE_TAC[] THEN MESON_TAC[]
1451QED
1452
1453(* ------------------------------------------------------------------------- *)
1454(* Equivalence of the "infinite descending chains" version. *)
1455(* ------------------------------------------------------------------------- *)
1456
1457Theorem WF_DCHAIN:
1458 WF(<<) <=> ~(?s:num->'a. !n. s(SUC n) << s(n))
1459Proof
1460 SIMP_TAC std_ss [WF, TAUT `(a <=> ~b) <=> (~a <=> b)`, NOT_FORALL_THM] THEN
1461 EQ_TAC THEN DISCH_THEN CHOOSE_TAC THENL
1462 [POP_ASSUM(MP_TAC o REWRITE_RULE[NOT_IMP]) THEN
1463 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC ``a:'a``) ASSUME_TAC) THEN
1464 SUBGOAL_THEN ``!x:'a. ?y. P(x) ==> P(y) /\ y << x`` MP_TAC THENL
1465 [ASM_MESON_TAC[], SIMP_TAC std_ss [SKOLEM_THM]] THEN
1466 DISCH_THEN(X_CHOOSE_THEN ``f:'a->'a`` STRIP_ASSUME_TAC) THEN
1467 KNOW_TAC ``?s. (s (0:num) = a) /\ (!n. s (SUC n) = f (s n))`` THENL
1468 [ASSUME_TAC prim_recTheory.num_Axiom_old THEN
1469 POP_ASSUM (MP_TAC o Q.SPECL [`a:'a`, `(\m n. f m)`]) THEN
1470 METIS_TAC [], STRIP_TAC] THEN
1471 EXISTS_TAC ``s:num->'a`` THEN ASM_REWRITE_TAC[] THEN
1472 SUBGOAL_THEN ``!n. P(s n) /\ s(SUC n):'a << s(n)``
1473 (fn th => ASM_MESON_TAC[th]) THEN
1474 INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[],
1475 EXISTS_TAC ``\y:'a. ?n:num. y = s(n)`` THEN REWRITE_TAC[] THEN
1476 ASM_MESON_TAC[]]
1477QED
1478
1479(* ------------------------------------------------------------------------- *)
1480(* Equivalent to just *uniqueness* part of recursion. *)
1481(* ------------------------------------------------------------------------- *)
1482
1483Theorem WF_UREC:
1484 WF(<<) ==>
1485 !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
1486 ==> !(f:'a->'b) g. (!x. f x = H f x) /\ (!x. g x = H g x)
1487 ==> (f = g)
1488Proof
1489 REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN REWRITE_TAC [FUN_EQ_THM] THEN
1490 UNDISCH_TAC `` !(P :'a -> bool).
1491 (!(x :'a). (!(y :'a). y << x ==> P y) ==> P x) ==> !(x :'a). P x`` THEN
1492 DISCH_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `(\x. (f:'a->'b) x = g x)`) THEN
1493 SIMP_TAC std_ss [] THEN
1494 DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
1495 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[]
1496QED
1497
1498Theorem WF_UREC_WF:
1499 (!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
1500 ==> !(f:'a->bool) g. (!x. f x = H f x) /\ (!x. g x = H g x)
1501 ==> (f = g)) ==> WF(<<)
1502Proof
1503 REWRITE_TAC[WF_IND] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
1504 FIRST_X_ASSUM(MP_TAC o SPEC ``\f x. P(x:'a) \/ !z:'a. z << x ==> f(z)``) THEN
1505 BETA_TAC THEN
1506 W(C SUBGOAL_THEN (fn t => REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
1507 [MESON_TAC[], DISCH_THEN(MP_TAC o SPECL [``P:'a->bool``, ``\x:'a. T``]) THEN
1508 REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]]
1509QED
1510
1511(* ------------------------------------------------------------------------- *)
1512(* Stronger form of recursion with "inductive invariant" (Krstic/Matthews). *)
1513(* ------------------------------------------------------------------------- *)
1514
1515val lemma = prove_nonschematic_inductive_relations_exist bool_monoset
1516 ``!f:'a->'b x. (!z. z << x ==> R z (f z)) ==> R x (H f x)``;
1517
1518Theorem WF_REC_INVARIANT:
1519 WF(<<) ==>
1520 !H S. (!f g x. (!z. z << x ==> f z = g z /\ S z (f z)) ==>
1521 H f x = H g x /\ S x (H f x)) ==>
1522 ?f:'a->'b. !x. f x = H f x
1523Proof
1524 REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
1525 X_CHOOSE_THEN ``R:'a->'b->bool`` STRIP_ASSUME_TAC lemma THEN
1526 SUBGOAL_THEN ``!x:'a. ?!y:'b. R x y`` (fn th => ASM_MESON_TAC[th]) THEN
1527 ONCE_REWRITE_TAC [METIS [] ``(?!y. R x y) = (\x. ?!y. R x y) x``] THEN
1528 FIRST_X_ASSUM MATCH_MP_TAC THEN BETA_TAC THEN REPEAT STRIP_TAC THEN
1529 first_x_assum (CONV_TAC o BINDER_CONV o REWR_CONV) >>
1530 SUBGOAL_THEN ``!x:'a y:'b. R x y ==> S' x y`` MP_TAC THEN METIS_TAC[]
1531QED
1532
1533(* ------------------------------------------------------------------------- *)
1534(* Equivalent to just *existence* part of recursion. *)
1535(* ------------------------------------------------------------------------- *)
1536
1537Theorem WF_REC:
1538 WF(<<)
1539 ==> !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
1540 ==> ?f:'a->'b. !x. f x = H f x
1541Proof
1542 REPEAT STRIP_TAC THEN
1543 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC_INVARIANT) THEN
1544 EXISTS_TAC ``\x:'a y:'b. T`` THEN ASM_REWRITE_TAC[]
1545QED
1546
1547(* ------------------------------------------------------------------------- *)
1548(* Wellfoundedness properties of natural numbers. *)
1549(* ------------------------------------------------------------------------- *)
1550
1551Theorem WF_num:
1552 WF((<):num->num->bool)
1553Proof
1554 REWRITE_TAC[WF_IND, arithmeticTheory.COMPLETE_INDUCTION]
1555QED
1556
1557Theorem WF_REC_num:
1558 !H. (!f g n. (!m. m < n ==> (f m = g m)) ==> (H f n = H g n))
1559 ==> ?f:num->'a. !n. f n = H f n
1560Proof
1561 MATCH_ACCEPT_TAC(MATCH_MP WF_REC WF_num)
1562QED
1563
1564Theorem TARSKI_SET:
1565 !f. (!s t. s SUBSET t ==> f(s) SUBSET f(t)) ==> ?s:'a->bool. f(s) = s
1566Proof
1567 REPEAT STRIP_TAC THEN
1568 MAP_EVERY Q.ABBREV_TAC
1569 [`Y = {b:'a->bool | f(b) SUBSET b}`, `a:'a->bool = BIGINTER Y`] THEN
1570 ‘!b:'a->bool. b IN Y <=> f(b) SUBSET b’
1571 by SIMP_TAC std_ss [GSPECIFICATION, Abbr‘Y’] THEN
1572 ‘!b:'a->bool. b IN Y ==> f(a:'a->bool) SUBSET b’
1573 by METIS_TAC[SUBSET_TRANS, IN_BIGINTER, SUBSET_DEF] THEN
1574 ‘f(a:'a->bool) SUBSET a’ by METIS_TAC[IN_BIGINTER, SUBSET_DEF] THEN
1575 METIS_TAC[SUBSET_ANTISYM, IN_BIGINTER]
1576QED