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