set_relationScript.sml

1Theory set_relation[bare]
2Ancestors
3  pred_set pair arithmetic option relation
4Libs
5  HolKernel boolLib BasicProvers simpLib numLib metisLib
6  markerLib pred_setSimps hurdUtils TotalDefn
7
8local
9  open OpenTheoryMap
10  val ns = ["Relation"]
11in
12  fun ot0 x y =
13    OpenTheory_const_name{const={Thy="set_relation",Name=x},name=(ns,y)}
14  fun ot x = ot0 x x
15end
16
17fun simp ths = ASM_SIMP_TAC (srw_ss()) ths
18
19(* ------------------------------------------------------------------------ *)
20(*  Basic concepts                                                          *)
21(* ------------------------------------------------------------------------ *)
22
23Type reln = ``:'a # 'a -> bool``
24
25Theorem rextension:
26  !s t. (s = t) <=> !x y. (x, y) IN s <=> (x, y) IN t
27Proof
28  SRW_TAC [] []
29  THEN EQ_TAC
30  THEN SRW_TAC [] [EXTENSION]
31  THEN Cases_on `x`
32  THEN SRW_TAC [] []
33QED
34
35Definition domain_def:
36  domain r = {x | ?y. (x, y) IN r}
37End
38
39val _ = ot "domain"
40
41Definition range_def:
42  range r = {y | ?x. (x, y) IN r}
43End
44
45val _ = ot "range"
46
47Theorem in_domain:
48  !x r. x IN domain r <=> ?y. (x, y) IN r
49Proof
50  SRW_TAC [] [domain_def]
51QED
52
53Theorem in_range:
54  !y r. y IN range r <=> ?x. (x, y) IN r
55Proof
56  SRW_TAC [] [range_def]
57QED
58
59Theorem in_dom_rg:
60  (x, y) IN r ==> x IN domain r /\ y IN range r
61Proof
62  REWRITE_TAC [in_domain, in_range] THEN PROVE_TAC []
63QED
64
65Theorem domain_mono:
66  r SUBSET r' ==> domain r SUBSET domain r'
67Proof
68  REWRITE_TAC [in_domain, SUBSET_DEF]
69  THEN REPEAT STRIP_TAC
70  THEN Q.EXISTS_TAC `y`
71  THEN RES_TAC
72QED
73
74Theorem range_mono:
75  r SUBSET r' ==> range r SUBSET range r'
76Proof
77  REWRITE_TAC [in_range, SUBSET_DEF]
78  THEN REPEAT STRIP_TAC
79  THEN Q.EXISTS_TAC `x'`
80  THEN RES_TAC
81QED
82
83Definition rrestrict_def:
84  rrestrict r s = {(x, y) | (x, y) IN r /\ x IN s /\ y IN s}
85End
86
87val _ = ot0 "rrestrict"
88
89Theorem in_rrestrict:
90  !x y r s. (x, y) IN rrestrict r s <=> (x, y) IN r /\ x IN s /\ y IN s
91Proof
92  SRW_TAC [] [rrestrict_def]
93QED
94
95Theorem in_rrestrict_alt:
96  x IN rrestrict r s <=> x IN r /\ FST x IN s /\ SND x IN s
97Proof
98  Cases_on `x` THEN REWRITE_TAC [in_rrestrict, FST, SND]
99QED
100
101Theorem rrestrict_SUBSET:
102  rrestrict r s SUBSET r
103Proof
104  REWRITE_TAC [in_rrestrict_alt, SUBSET_DEF] THEN REPEAT STRIP_TAC
105QED
106
107Theorem rrestrict_union:
108  !r1 r2 s. rrestrict (r1 UNION r2) s = (rrestrict r1 s) UNION (rrestrict r2 s)
109Proof
110  SRW_TAC [] [rrestrict_def, EXTENSION]
111  THEN METIS_TAC []
112QED
113
114Theorem rrestrict_rrestrict:
115  !r x y. rrestrict (rrestrict r x) y = rrestrict r (x INTER y)
116Proof
117  SRW_TAC [] [rrestrict_def, EXTENSION]
118  THEN EQ_TAC
119  THEN SRW_TAC [] []
120QED
121
122Theorem domain_rrestrict_SUBSET:
123  domain (rrestrict r s) SUBSET s
124Proof
125  REWRITE_TAC [in_domain, SUBSET_DEF, in_rrestrict] THEN REPEAT STRIP_TAC
126QED
127
128Theorem range_rrestrict_SUBSET:
129  range (rrestrict r s) SUBSET s
130Proof
131  REWRITE_TAC [in_range, SUBSET_DEF, in_rrestrict] THEN REPEAT STRIP_TAC
132QED
133
134Definition rcomp_def:
135  rcomp r1 r2 = { (x, y) | ?z. (x, z) IN r1 /\ (z, y) IN r2}
136End
137
138Overload "OO" = ``rcomp``
139
140val _ = Parse.set_fixity "OO" (Parse.Infixr 800)
141
142Definition strict_def:
143  strict r = {(x, y) | (x, y) IN r /\ x <> y}
144End
145
146Theorem strict_rrestrict:
147  !r s. strict (rrestrict r s) = rrestrict (strict r) s
148Proof
149  SRW_TAC [] [strict_def, rrestrict_def, EXTENSION]
150  THEN METIS_TAC []
151QED
152
153Definition univ_reln_def:
154  univ_reln xs = {(x1, x2) | x1 IN xs /\ x2 IN xs}
155End
156
157Definition finite_prefixes_def:
158  finite_prefixes r s = !e. e IN s ==> FINITE {e' | (e', e) IN r}
159End
160
161val _ = ot0 "finite_prefixes" "finitePrefixes"
162
163Theorem finite_prefixes_subset_s:
164  !r s s'. finite_prefixes r s /\ s' SUBSET s ==> finite_prefixes r s'
165Proof
166  SRW_TAC [] [finite_prefixes_def, SUBSET_DEF]
167QED
168
169Theorem finite_prefixes_subset_r:
170  !r r' s. finite_prefixes r s /\ r' SUBSET r ==> finite_prefixes r' s
171Proof
172  SRW_TAC [] [finite_prefixes_def, SUBSET_DEF]
173  THEN RES_TAC
174  THEN IMP_RES_THEN MATCH_MP_TAC SUBSET_FINITE
175  THEN SRW_TAC [] [SUBSET_DEF]
176QED
177
178Theorem finite_prefixes_subset_rs:
179  !r s r' s'.
180   finite_prefixes r s ==> r' SUBSET r ==> s' SUBSET s ==> finite_prefixes r' s'
181Proof
182  REPEAT STRIP_TAC
183  THEN IMP_RES_TAC finite_prefixes_subset_r
184  THEN IMP_RES_TAC finite_prefixes_subset_s
185QED
186
187Theorem finite_prefixes_subset:
188  !r s s'.
189    finite_prefixes r s /\ s' SUBSET s ==>
190    finite_prefixes r s' /\ finite_prefixes (rrestrict r s') s'
191Proof
192  SRW_TAC [] [finite_prefixes_def, SUBSET_DEF, rrestrict_def, GSPEC_AND]
193  THEN METIS_TAC [INTER_FINITE, INTER_COMM]
194QED
195
196Theorem finite_prefixes_union:
197  !r1 r2 s1 s2.
198    finite_prefixes r1 s1 /\ finite_prefixes r2 s2 ==>
199    finite_prefixes (r1 UNION r2) (s1 INTER s2)
200Proof
201  SRW_TAC [] [finite_prefixes_def, GSPEC_OR]
202QED
203
204Theorem finite_prefixes_comp:
205  !r1 r2 s1 s2.
206    finite_prefixes r1 s1 /\ finite_prefixes r2 s2 /\
207    { x | ?y. y IN s2 /\ (x, y) IN r2 } SUBSET s1 ==>
208    finite_prefixes (rcomp r1 r2) s2
209Proof
210  SRW_TAC [] [finite_prefixes_def, SUBSET_DEF, rcomp_def]
211  THEN `{ e' | ?z. (e', z) IN r1 /\ (z, e) IN r2 } =
212        BIGUNION (IMAGE (\z. { e' | (e', z) IN r1}) { z | (z, e) IN r2 })`
213    by (SRW_TAC [] [EXTENSION]
214        THEN EQ_TAC
215        THEN SRW_TAC [] []
216        THENL [
217          Q.EXISTS_TAC `{ x | (x, z) IN r1 }`
218          THEN SRW_TAC [] []
219          THEN METIS_TAC [],
220          METIS_TAC []
221        ])
222  THEN SRW_TAC [] []
223  THEN METIS_TAC []
224QED
225
226Theorem finite_prefixes_inj_image:
227  !f r s.
228    (!x y. (f x = f y) ==> (x = y)) /\ finite_prefixes r s ==>
229    finite_prefixes { (f x, f y) | (x, y) IN r } (IMAGE f s)
230Proof
231  SRW_TAC [] [finite_prefixes_def]
232  THEN `{e' | ?x' y. ((e' = f x') /\ (f x = f y)) /\ (x',y) IN r} SUBSET
233        IMAGE f { e' | (e', x) IN r }`
234    by (SRW_TAC [] [SUBSET_DEF] THEN METIS_TAC [])
235  THEN METIS_TAC [SUBSET_FINITE, IMAGE_FINITE]
236QED
237
238Theorem finite_prefixes_range:
239  !r s t.
240    finite_prefixes r s /\ DISJOINT t (range r) ==>
241    finite_prefixes r (s UNION t)
242Proof
243  SRW_TAC [] [finite_prefixes_def, DISJOINT_DEF, range_def, INTER_DEF,
244              EXTENSION]
245  THEN1 METIS_TAC []
246  THEN `{e' | (e', e) IN r} = {}` by (SRW_TAC [] [EXTENSION] THEN METIS_TAC [])
247  THEN METIS_TAC [FINITE_EMPTY]
248QED
249
250(* ------------------------------------------------------------------------ *)
251(* Transitive closure                                                       *)
252(* ------------------------------------------------------------------------ *)
253
254Inductive transitive_closure :
255  (!x y. r (x,y) ==> transitive_closure r (x,y)) /\
256  (!x y. (?z. transitive_closure r (x,z) /\ transitive_closure r (z,y)) ==>
257         transitive_closure r (x,y))
258End
259Overload tc[local] = “transitive_closure”
260
261Theorem tc_rules:
262  !r.
263    (!x y. (x,y) IN r ==> (x,y) IN tc r) /\
264    (!x y. (?z. (x,z) IN tc r /\ (z,y) IN tc r) ==> (x,y) IN tc r)
265Proof
266  SRW_TAC [] [SPECIFICATION, transitive_closure_rules]
267QED
268
269Theorem tc_cases:
270  !r x y. (x,y) IN tc r <=> (x,y) IN r \/ ?z. (x,z) IN tc r /\ (z,y) IN tc r
271Proof
272  SRW_TAC [] [SPECIFICATION]
273  THEN SRW_TAC [] [Once (Q.SPECL [`r`, `(x, y)`] transitive_closure_cases)]
274QED
275
276Theorem tc_ind:
277  !r tc'.
278    (!x y. (x,y) IN r ==> tc' x y) /\
279    (!x y. (?z. tc' x z /\ tc' z y) ==> tc' x y) ==>
280    !x y. (x,y) IN tc r ==> tc' x y
281Proof
282  SRW_TAC [] [SPECIFICATION]
283  THEN IMP_RES_TAC
284         (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM]
285            (Q.SPECL [`r`, `\(x, y). tc' x y`] transitive_closure_ind))
286QED
287
288val [tc_rule1', tc_rule2] = CONJUNCTS (SPEC_ALL tc_rules)
289val tc_rule1 = Ho_Rewrite.REWRITE_RULE [GSYM FORALL_PROD] tc_rule1'
290
291(** closure rules for tc **)
292
293Theorem tc_closure:
294  r SUBSET tc s ==> tc r SUBSET tc s
295Proof
296  Ho_Rewrite.REWRITE_TAC [SUBSET_DEF, FORALL_PROD]
297  THEN DISCH_TAC
298  THEN HO_MATCH_MP_TAC tc_ind
299  THEN CONJ_TAC
300  THENL [POP_ASSUM ACCEPT_TAC, MATCH_ACCEPT_TAC tc_rule2]
301QED
302
303Theorem subset_tc:
304  r SUBSET tc r
305Proof
306  Ho_Rewrite.REWRITE_TAC [SUBSET_DEF, FORALL_PROD]
307  THEN MATCH_ACCEPT_TAC tc_rule1
308QED
309
310Theorem tc_idemp:
311  tc (tc r) = tc r
312Proof
313  REWRITE_TAC [SET_EQ_SUBSET]
314  THEN CONJ_TAC
315  THENL [irule tc_closure THEN irule SUBSET_REFL, irule subset_tc]
316QED
317
318Theorem tc_mono:
319  r SUBSET s ==> tc r SUBSET tc s
320Proof
321  DISCH_TAC THEN irule tc_closure
322  THEN irule SUBSET_TRANS
323  THEN Q.EXISTS_TAC `s`
324  THEN ASM_REWRITE_TAC [subset_tc]
325QED
326
327Theorem tc_strongind:
328  !r tc'.
329    (!x y. (x, y) IN r ==> tc' x y) /\
330    (!x y. (?z. (x, z) IN tc r /\ tc' x z /\ (z, y) IN tc r /\ tc' z y) ==>
331           tc' x y) ==>
332    !x y. (x, y) IN tc r ==> tc' x y
333Proof
334  SRW_TAC [] [SPECIFICATION]
335  THEN IMP_RES_TAC
336         (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM]
337            (Q.SPECL [`r`, `\(x, y). tc' x y`] transitive_closure_strongind))
338QED
339
340Theorem tc_cases_lem[local]:
341  !x y.
342    (x, y) IN tc r ==>
343    (x, y) IN r \/
344    ((?z. (x, z) IN tc r /\ (z, y) IN r) /\
345     (?z. (x, z) IN r /\ (z, y) IN tc r))
346Proof
347  HO_MATCH_MP_TAC tc_ind
348  THEN SRW_TAC [] []
349  THEN METIS_TAC [tc_rules]
350QED
351
352Theorem tc_cases_right:
353  !r x y. (x, y) IN tc r <=> (x, y) IN r \/ ?z. (x, z) IN tc r /\ (z, y) IN r
354Proof
355  METIS_TAC [tc_cases_lem, tc_rules]
356QED
357
358Theorem tc_cases_left:
359  !r x y. (x, y) IN tc r <=> (x, y) IN r \/ ?z. (x, z) IN r /\ (z, y) IN tc r
360Proof
361  METIS_TAC [tc_cases_lem, tc_rules]
362QED
363
364Theorem tc_ind_left_lem[local]:
365  !r P.
366    (!x y. (x, y) IN r ==> P x y) /\
367    (!x y. (?z. (x, z) IN r /\ P z y) ==> P x y) ==>
368    (!x y. (x, y) IN tc r ==> (!z. P x y /\ P y z ==> P x z) /\ P x y)
369Proof
370  NTAC 3 STRIP_TAC
371  THEN HO_MATCH_MP_TAC tc_ind
372  THEN SRW_TAC [] []
373  THEN METIS_TAC []
374QED
375
376Theorem tc_ind_left:
377  !r tc'.
378    (!x y. (x, y) IN r ==> tc' x y) /\
379    (!x y. (?z. (x, z) IN r /\ tc' z y) ==> tc' x y) ==>
380    (!x y. (x, y) IN tc r ==> tc' x y)
381Proof
382  METIS_TAC [tc_ind_left_lem]
383QED
384
385Theorem tc_strongind_left_lem[local]:
386  !r P.
387    (!x y. (x, y) IN r ==> P x y) /\
388    (!x y. (?z. (x, z) IN r /\ (z, y) IN tc r /\ P z y) ==> P x y) ==>
389    (!x y. (x, y) IN tc r ==>
390           (!z. P x y /\ P y z /\ (y, z) IN tc r ==> P x z) /\ P x y)
391Proof
392  NTAC 3 STRIP_TAC
393  THEN HO_MATCH_MP_TAC tc_strongind
394  THEN SRW_TAC [] []
395  THEN METIS_TAC [tc_rules]
396QED
397
398Theorem tc_strongind_left:
399  !r tc'.
400    (!x y. (x, y) IN r ==> tc' x y) /\
401    (!x y. (?z. (x, z) IN r /\ (z, y) IN tc r /\ tc' z y) ==> tc' x y) ==>
402    (!x y. (x, y) IN tc r ==> tc' x y)
403Proof
404  METIS_TAC [tc_strongind_left_lem]
405QED
406
407Theorem tc_ind_right_lem[local]:
408  !r P.
409    (!x y. (x, y) IN r ==> P x y) /\
410    (!x y. (?z. P x z /\ (z, y) IN r) ==> P x y) ==>
411    (!x y. (x, y) IN tc r ==> (!z. P z x /\ P x y ==> P z y) /\ P x y)
412Proof
413  NTAC 3 STRIP_TAC
414  THEN HO_MATCH_MP_TAC tc_ind
415  THEN SRW_TAC [] []
416  THEN METIS_TAC []
417QED
418
419Theorem tc_ind_right:
420  !r tc'.
421    (!x y. (x, y) IN r ==> tc' x y) /\
422    (!x y. (?z. tc' x z /\ (z, y) IN r) ==> tc' x y) ==>
423    (!x y. (x, y) IN tc r ==> tc' x y)
424Proof
425  METIS_TAC [tc_ind_right_lem]
426QED
427
428Theorem rtc_ind_right:
429  !r tc'.
430    (!x. x IN domain r \/ x IN range r ==> tc' x x) /\
431    (!x y. (?z. tc' x z /\ (z, y) IN r) ==> tc' x y) ==>
432    (!x y. (x, y) IN tc r ==> tc' x y)
433Proof
434  NTAC 3 STRIP_TAC
435  THEN HO_MATCH_MP_TAC tc_ind_right
436  THEN SRW_TAC [] []
437  THEN FULL_SIMP_TAC (srw_ss()) [domain_def, range_def]
438  THEN METIS_TAC []
439QED
440
441Theorem tc_strongind_right_lem[local]:
442  !r P.
443    (!x y. (x, y) IN r ==> P x y) /\
444    (!x y. (?z. (x, z) IN tc r /\ P x z /\ (z, y) IN r) ==> P x y) ==>
445    (!x y. (x, y) IN tc r ==>
446           (!z. (z, x) IN tc r /\ P z x /\ P x y ==> P z y) /\ P x y)
447Proof
448  NTAC 3 STRIP_TAC
449  THEN HO_MATCH_MP_TAC tc_strongind
450  THEN SRW_TAC [] []
451  THEN METIS_TAC [tc_rules]
452QED
453
454Theorem tc_strongind_right:
455  !r tc'.
456    (!x y. (x, y) IN r ==> tc' x y) /\
457    (!x y. (?z. (x, z) IN tc r /\ tc' x z /\ (z, y) IN r) ==> tc' x y) ==>
458    (!x y. (x, y) IN tc r ==> tc' x y)
459Proof
460  METIS_TAC [tc_strongind_right_lem]
461QED
462
463Theorem tc_union:
464  !x y. (x, y) IN tc r1 ==> !r2. (x, y) IN tc (r1 UNION r2)
465Proof
466  HO_MATCH_MP_TAC tc_ind
467  THEN SRW_TAC [] []
468  THENL [SRW_TAC [] [Once tc_cases], METIS_TAC [tc_rules]]
469QED
470
471Theorem tc_implication_lem[local]:
472  !x y. (x, y) IN tc r1 ==>
473        !r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==> (x, y) IN tc r2
474Proof
475  HO_MATCH_MP_TAC tc_ind
476  THEN SRW_TAC [] []
477  THEN METIS_TAC [tc_rules]
478QED
479
480Theorem tc_implication:
481  !r1 r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==>
482          (!x y. (x, y) IN tc r1 ==> (x, y) IN tc r2)
483Proof
484  METIS_TAC [tc_implication_lem]
485QED
486
487Theorem tc_empty[local]:
488  !x y. (x, y) IN tc {} ==> F
489Proof
490  HO_MATCH_MP_TAC tc_ind THEN SRW_TAC [] []
491QED
492
493Theorem tc_empty = SIMP_RULE (srw_ss()) [] tc_empty
494
495Theorem tc_empty_eqn[simp]:
496  tc {} = {}
497Proof
498  asm_simp_tac (srw_ss()) [EXTENSION, pairTheory.FORALL_PROD, tc_empty]
499QED
500
501Theorem tc_domain_range:
502  !x y. (x, y) IN tc r ==> x IN domain r /\ y IN range r
503Proof
504  HO_MATCH_MP_TAC tc_ind
505  THEN SRW_TAC [] [domain_def, range_def]
506  THEN METIS_TAC []
507QED
508
509Theorem rrestrict_tc:
510  !e e'. (e, e') IN tc (rrestrict r x) ==> (e, e') IN tc r
511Proof
512  HO_MATCH_MP_TAC tc_ind
513  THEN SRW_TAC [] [rrestrict_def]
514  THEN METIS_TAC [tc_rules]
515QED
516
517Theorem pair_in_IMAGE_SWAP[local]:
518  ((a, b) IN IMAGE SWAP r) = ((b, a) IN r)
519Proof
520  Ho_Rewrite.REWRITE_TAC [IN_IMAGE, EXISTS_PROD, SWAP_def, FST, SND, PAIR_EQ]
521  THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)
522  THEN PROVE_TAC []
523QED
524
525val tc_ind' = Ho_Rewrite.REWRITE_RULE [PULL_FORALL] tc_ind
526
527Theorem tc_SWAP:
528  tc (IMAGE SWAP r) = IMAGE SWAP (tc r)
529Proof
530  Ho_Rewrite.REWRITE_TAC
531    [SET_EQ_SUBSET, SUBSET_DEF, FORALL_PROD, pair_in_IMAGE_SWAP]
532  THEN CONJ_TAC
533  THENL [
534    HO_MATCH_MP_TAC tc_ind
535    THEN REWRITE_TAC [pair_in_IMAGE_SWAP]
536    THEN REPEAT STRIP_TAC
537    THENL [IMP_RES_TAC tc_rule1, IMP_RES_TAC tc_rule2],
538    REPEAT GEN_TAC
539    THEN HO_MATCH_MP_TAC tc_ind'
540    THEN REPEAT STRIP_TAC
541    THENL [
542      irule tc_rule1 THEN ASM_REWRITE_TAC [pair_in_IMAGE_SWAP],
543      IMP_RES_TAC tc_rule2
544    ]
545  ]
546QED
547
548(* ------------------------------------------------------------------------ *)
549(* Acyclic relations                                                        *)
550(* ------------------------------------------------------------------------ *)
551
552Definition acyclic_def:
553  acyclic r = !x. (x, x) NOTIN tc r
554End
555
556Theorem acyclic_subset:
557  !r1 r2. acyclic r1 /\ r2 SUBSET r1 ==> acyclic r2
558Proof
559  SRW_TAC [] [acyclic_def, SUBSET_DEF]
560  THEN METIS_TAC [tc_implication_lem]
561QED
562
563Theorem acyclic_union_E:
564  !r1 r2. acyclic (r1 UNION r2) ==> acyclic r1 /\ acyclic r2
565Proof
566  SRW_TAC [] [acyclic_def]
567  THEN METIS_TAC [tc_union, UNION_COMM]
568QED
569
570Theorem acyclic_rrestrict:
571  !r s. acyclic r ==> acyclic (rrestrict r s)
572Proof
573  SRW_TAC [] [rrestrict_def]
574  THEN `r = {(x, y) | (x ,y) IN r /\ x IN s /\ y IN s} UNION r`
575    by SRW_TAC [] [UNION_DEF, rextension, EQ_IMP_THM]
576  THEN METIS_TAC [acyclic_union_E]
577QED
578
579Theorem acyclic_irreflexive:
580  !r x. acyclic r ==> (x, x) NOTIN r
581Proof
582  SRW_TAC [] [acyclic_def]
583  THEN METIS_TAC [tc_cases]
584QED
585
586Theorem acyclic_SWAP:
587  acyclic (IMAGE SWAP r) = acyclic r
588Proof
589  REWRITE_TAC [acyclic_def, tc_SWAP, pair_in_IMAGE_SWAP]
590QED
591
592Theorem tc_BIGUNION_lem[local]:
593  !x y.
594    (x, y) IN tc (BIGUNION rs) ==>
595    (!r r'.
596      r IN rs /\ r' IN rs /\ r <> r' ==>
597      DISJOINT (domain r UNION range r) (domain r' UNION range r')) ==>
598    ?r. r IN rs /\ (x, y) IN tc r
599Proof
600  HO_MATCH_MP_TAC tc_ind
601  THEN SRW_TAC [] []
602  THEN1 METIS_TAC [tc_rules]
603  THEN RES_TAC
604  THEN IMP_RES_TAC tc_domain_range
605  THEN FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION]
606  THEN `r = r'` by (SRW_TAC [] [EXTENSION] THEN METIS_TAC [])
607  THEN METIS_TAC [tc_rules]
608QED
609
610Theorem acyclic_bigunion:
611  !rs.
612    (!r r'.
613      r IN rs /\ r' IN rs /\ r <> r' ==>
614      DISJOINT (domain r UNION range r) (domain r' UNION range r')) /\
615    (!r. r IN rs ==> acyclic r) ==>
616    acyclic (BIGUNION rs)
617Proof
618  SRW_TAC [] [acyclic_def]
619  THEN CCONTR_TAC
620  THEN FULL_SIMP_TAC (srw_ss()) []
621  THEN IMP_RES_TAC tc_BIGUNION_lem
622  THEN FULL_SIMP_TAC (srw_ss()) []
623  THEN METIS_TAC []
624QED
625
626Theorem acyclic_union_I:
627  !r r'.
628    DISJOINT (domain r UNION range r) (domain r' UNION range r') /\
629    acyclic r /\
630    acyclic r' ==>
631    acyclic (r UNION r')
632Proof
633  SRW_TAC [] []
634  THEN MATCH_MP_TAC
635         (SIMP_RULE (srw_ss()) [] (Q.SPEC `{r; r'}` acyclic_bigunion))
636  THEN SRW_TAC [] []
637  THEN METIS_TAC [DISJOINT_SYM]
638QED
639
640(* ------------------------------------------------------------------------ *)
641(*  Orders                                                                  *)
642(* ------------------------------------------------------------------------ *)
643
644Definition reflexive_def:
645  reflexive r s = !x. x IN s ==> (x, x) IN r
646End
647
648Definition irreflexive_def:
649  irreflexive r s = !x. x IN s ==> (x, x) NOTIN r
650End
651
652Definition transitive_def:
653  transitive r = !x y z.  (x, y) IN r /\ (y, z) IN r ==> (x, z) IN r
654End
655
656val _ = ot "transitive"
657
658Theorem transitive_tc_lem[local]:
659  !x y. (x, y) IN tc r ==> transitive r ==> (x, y) IN r
660Proof
661  HO_MATCH_MP_TAC tc_ind
662  THEN SRW_TAC [] []
663  THEN RES_TAC
664  THEN FULL_SIMP_TAC (srw_ss()) [transitive_def]
665  THEN METIS_TAC []
666QED
667
668Theorem transitive_tc:
669  !r. transitive r ==> (tc r = r)
670Proof
671  SRW_TAC [] [EXTENSION]
672  THEN EQ_TAC
673  THEN SRW_TAC [] []
674  THEN Cases_on `x`
675  THEN1 METIS_TAC [transitive_tc_lem]
676  THEN FULL_SIMP_TAC (srw_ss()) [transitive_def]
677  THEN METIS_TAC [tc_rules]
678QED
679
680Theorem tc_transitive:
681  !r. transitive (tc r)
682Proof
683  SRW_TAC [] [transitive_def]
684  THEN METIS_TAC [tc_rules]
685QED
686
687Definition antisym_def:
688  antisym r = !x y. (x, y) IN r /\ (y, x) IN r ==> (x = y)
689End
690
691val _ = ot0 "antisym" "antisymmetric"
692
693Definition partial_order_def:
694  partial_order r s <=>
695    domain r SUBSET s /\ range r SUBSET s /\
696    transitive r /\ reflexive r s /\ antisym r
697End
698
699Theorem antisym_subset:
700  antisym t ==> s SUBSET t ==> antisym s
701Proof
702  REWRITE_TAC [antisym_def, SUBSET_DEF]
703  THEN REPEAT STRIP_TAC
704  THEN RES_TAC
705  THEN FIRST_ASSUM MATCH_MP_TAC
706  THEN ASM_REWRITE_TAC []
707QED
708
709Theorem partial_order_dom_rng:
710  !r s x y. (x, y) IN r /\ partial_order r s ==> x IN s /\ y IN s
711Proof
712  SRW_TAC [] [partial_order_def, domain_def, range_def, SUBSET_DEF]
713  THEN METIS_TAC []
714QED
715
716Theorem partial_order_subset:
717  !r s s'.
718    partial_order r s /\ s' SUBSET s ==> partial_order (rrestrict r s') s'
719Proof
720  SRW_TAC [] [partial_order_def, SUBSET_DEF, reflexive_def, transitive_def,
721              antisym_def, domain_def, range_def, rrestrict_def]
722  THEN METIS_TAC []
723QED
724
725Theorem strict_partial_order:
726  !r s.
727    partial_order r s ==>
728    domain (strict r) SUBSET s /\ range (strict r) SUBSET s /\
729    transitive (strict r) /\ antisym (strict r)
730Proof
731  SRW_TAC [] [domain_def, SUBSET_DEF, range_def, partial_order_def, strict_def]
732  THENL [
733    METIS_TAC [],
734    METIS_TAC [],
735    FULL_SIMP_TAC (srw_ss()) [transitive_def, strict_def, antisym_def]
736    THEN METIS_TAC [],
737    FULL_SIMP_TAC (srw_ss()) [antisym_def]
738    THEN METIS_TAC []
739  ]
740QED
741
742Theorem strict_partial_order_acyclic:
743  !r s. partial_order r s ==> acyclic (strict r)
744Proof
745  SRW_TAC [] [acyclic_def]
746  THEN IMP_RES_TAC strict_partial_order
747  THEN SRW_TAC [] [transitive_tc, strict_def]
748QED
749
750Definition linear_order_def:
751  linear_order r s <=>
752    domain r SUBSET s /\ range r SUBSET s /\
753    transitive r /\ antisym r /\
754    (!x y. x IN s /\ y IN s ==> (x, y) IN r \/ (y, x) IN r)
755End
756
757val _ = ot0 "linear_order" "linearOrder"
758
759Theorem linear_order_subset:
760  !r s s'.
761    linear_order r s /\ s' SUBSET s ==> linear_order (rrestrict r s') s'
762Proof
763  SRW_TAC [] [linear_order_def, SUBSET_DEF, transitive_def,
764              antisym_def, domain_def, range_def, rrestrict_def]
765  THEN METIS_TAC []
766QED
767
768Theorem partial_order_linear_order:
769  !r s. linear_order r s ==> partial_order r s
770Proof
771  SRW_TAC [] [linear_order_def, partial_order_def, reflexive_def]
772  THEN METIS_TAC []
773QED
774
775Definition strict_linear_order_def:
776  strict_linear_order r s <=>
777    domain r SUBSET s /\ range r SUBSET s /\
778    transitive r /\
779    (!x. (x, x) NOTIN r) /\
780    (!x y. x IN s /\ y IN s /\ x <> y ==> (x, y) IN r \/ (y, x) IN r)
781End
782
783Theorem strict_linear_order_dom_rng:
784  !r s x y. (x, y) IN r /\ strict_linear_order r s ==> x IN s /\ y IN s
785Proof
786  SRW_TAC [] [strict_linear_order_def, domain_def, range_def, SUBSET_DEF]
787  THEN METIS_TAC []
788QED
789
790Theorem linear_order_dom_rng:
791  !r s x y. (x, y) IN r /\ linear_order r s ==> x IN s /\ y IN s
792Proof
793  SRW_TAC [] [linear_order_def, domain_def, range_def, SUBSET_DEF]
794  THEN METIS_TAC []
795QED
796
797(* ------------------------------------------------------------------------ *)
798(* Symmetric closure (sc)                                                   *)
799(* ------------------------------------------------------------------------ *)
800
801Definition symmetric_def:
802    symmetric r s <=> !x y. x IN s /\ y IN s ==> ((x,y) IN r <=> (y,x) IN r)
803End
804
805Theorem symmetric_union:
806    !r1 r2 s. symmetric r1 s /\ symmetric r2 s ==> symmetric (r1 UNION r2) s
807Proof
808    SRW_TAC [][symmetric_def]
809QED
810
811Theorem irreflexive_union:
812    !r1 r2 s. irreflexive r1 s /\ irreflexive r2 s ==> irreflexive (r1 UNION r2) s
813Proof
814    SRW_TAC [][irreflexive_def]
815QED
816
817Inductive symmetric_closure:
818    (!x y. r (x,y) ==> symmetric_closure r (x,y)) /\
819    (!x y. symmetric_closure r (x,y) ==> symmetric_closure r (y,x))
820End
821Overload sc[local] = “symmetric_closure”
822
823Theorem sc_rules:
824    !r. (!x y. (x,y) IN r ==> (x,y) IN sc r) /\
825         !x y. (x,y) IN sc r ==> (y,x) IN sc r
826Proof
827    simp [IN_APP]
828 >> METIS_TAC [symmetric_closure_rules]
829QED
830
831Theorem sc_cases:
832    !r x y. (x,y) IN sc r <=> (x,y) IN r \/ (y,x) IN sc r
833Proof
834  SRW_TAC [] [SPECIFICATION]
835  THEN SRW_TAC [] [Once (Q.SPECL [`r`, `(x, y)`] symmetric_closure_cases)]
836QED
837
838Theorem sc_ind:
839    !r sc'.
840        (!x y. (x,y) IN r ==> sc' x y) /\ (!x y. sc' x y ==> sc' y x) ==>
841        !x y. (x,y) IN sc r ==> sc' x y
842Proof
843  SRW_TAC [] [SPECIFICATION]
844  THEN IMP_RES_TAC
845         (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM]
846            (Q.SPECL [`r`, `\(x, y). sc' x y`] symmetric_closure_ind))
847QED
848
849Theorem sc_strongind:
850  !r sc'.
851        (!x y. (x,y) IN r ==> sc' x y) /\
852        (!x y. (x,y) IN sc r /\ sc' x y ==> sc' y x) ==>
853        !x y. (x,y) IN sc r ==> sc' x y
854Proof
855  SRW_TAC [] [SPECIFICATION]
856  THEN IMP_RES_TAC
857         (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM]
858            (Q.SPECL [`r`, `\(x, y). sc' x y`] symmetric_closure_strongind))
859QED
860
861Theorem sc_swap:
862    !x y r. (x,y) IN sc r <=> (y,x) IN sc r
863Proof
864    rpt GEN_TAC
865 >> EQ_TAC >> STRIP_TAC
866 >> MATCH_MP_TAC (cj 2 sc_rules) >> art []
867QED
868
869Theorem sc_symmetric[simp]:
870    symmetric (sc r) s
871Proof
872    SRW_TAC [][symmetric_def, Once sc_swap]
873QED
874
875Theorem sc_irreflexive_lemma[local]:
876    !x r. (x,x) NOTIN r ==> (x,x) NOTIN sc r
877Proof
878    rpt GEN_TAC
879 >> simp [Once MONO_NOT_EQ]
880 >> Suff ‘!z. z IN sc r ==> FST z = SND z ==> z IN r’ >- SRW_TAC [][]
881 >> SIMP_TAC bool_ss [FORALL_PROD]
882 >> HO_MATCH_MP_TAC sc_ind
883 >> SRW_TAC [][]
884QED
885
886Theorem sc_irreflexive:
887    !r s. irreflexive r s ==> irreflexive (sc r) s
888Proof
889    SRW_TAC [][irreflexive_def]
890 >> MATCH_MP_TAC sc_irreflexive_lemma
891 >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
892QED
893
894Theorem sc_empty[simp]:
895    sc {} = {}
896Proof
897    SRW_TAC [][Once EXTENSION]
898 >> Suff ‘!x. x IN sc {} ==> F’ >- SRW_TAC [][]
899 >> SIMP_TAC bool_ss [FORALL_PROD]
900 >> Suff ‘!x y. (x,y) IN sc {} ==> F’ >- SRW_TAC [][]
901 >> HO_MATCH_MP_TAC sc_ind
902 >> SRW_TAC [][]
903QED
904
905Theorem sc_def:
906    !r. sc r = {(x,y) | (x,y) IN r \/ (y,x) IN r}
907Proof
908    SRW_TAC [][Once EXTENSION]
909 >> reverse EQ_TAC
910 >- (SRW_TAC [][] >- (MATCH_MP_TAC (cj 1 sc_rules) >> art []) \\
911     SRW_TAC [][Once sc_swap] \\
912     MATCH_MP_TAC (cj 1 sc_rules) >> art [])
913 >> Q.ID_SPEC_TAC ‘x’
914 >> simp [FORALL_PROD]
915 >> HO_MATCH_MP_TAC sc_ind >> NTAC 2 (SRW_TAC [][])
916QED
917
918Theorem finite_sc:
919    !r. FINITE r ==> FINITE (sc r)
920Proof
921    SRW_TAC [][sc_def]
922 >> Q.MATCH_ABBREV_TAC ‘FINITE s’
923 >> Know ‘s = r UNION (IMAGE (\z. (SND z,FST z)) r)’
924 >- (SRW_TAC [][Once EXTENSION, Abbr ‘s’] \\
925     Cases_on ‘x’ >> EQ_TAC >> NTAC 2 (SRW_TAC [][]) \\
926     DISJ2_TAC \\
927     Q.RENAME_TAC [‘(x,y) IN r’] \\
928     Q.EXISTS_TAC ‘(x,y)’ >> SRW_TAC [][])
929 >> Rewr'
930 >> SRW_TAC [][FINITE_UNION]
931QED
932
933(* ------------------------------------------------------------------------ *)
934(*  Link to relation theory                                                 *)
935(* ------------------------------------------------------------------------ *)
936
937Definition reln_to_rel_def:
938  reln_to_rel r = (\x y. (x, y) IN r)
939End
940
941Definition rel_to_reln_def:
942  rel_to_reln R = {(x, y) | x, y | R x y}
943End
944
945Definition RRUNIV_def:
946  RRUNIV s = (\x y. x IN s /\ y IN s)
947End
948
949Definition RREFL_EXP_def:
950  RREFL_EXP R s = (R RUNION (\x y. (x = y) /\ ~(x IN s)))
951End
952
953Theorem RREFL_EXP_RSUBSET:
954  R RSUBSET (RREFL_EXP R s)
955Proof
956  SRW_TAC [] [RSUBSET, RREFL_EXP_def, RUNION]
957QED
958
959Theorem RREFL_EXP_UNIV:
960  RREFL_EXP R UNIV = R
961Proof
962  SRW_TAC [] [FUN_EQ_THM, RREFL_EXP_def, RUNION]
963QED
964
965Theorem REL_RESTRICT_UNIV:
966  REL_RESTRICT R UNIV = R
967Proof
968  SRW_TAC [] [FUN_EQ_THM, REL_RESTRICT_DEF, RINTER, RRUNIV_def]
969QED
970
971Theorem in_rel_to_reln:
972  xy IN (rel_to_reln R) <=> R (FST xy) (SND xy)
973Proof
974  Cases_on `xy` THEN SRW_TAC [] [rel_to_reln_def]
975QED
976
977Theorem reln_to_rel_app[simp]:
978  (reln_to_rel r) x y <=> (x, y) IN r
979Proof
980  SRW_TAC [] [reln_to_rel_def]
981QED
982
983Theorem rel_to_reln_IS_UNCURRY:
984  rel_to_reln = UNCURRY
985Proof
986  REWRITE_TAC [FUN_EQ_THM, REWRITE_RULE [IN_APP] in_rel_to_reln, UNCURRY_VAR]
987QED
988
989Theorem reln_to_rel_IS_CURRY:
990  reln_to_rel = CURRY
991Proof
992  REWRITE_TAC [FUN_EQ_THM, CURRY_DEF, reln_to_rel_app, IN_APP]
993QED
994
995Theorem rel_to_reln_inv[simp]:
996  reln_to_rel (rel_to_reln R) = R
997Proof
998  SRW_TAC [] [reln_to_rel_def, rel_to_reln_def, FUN_EQ_THM]
999QED
1000
1001Theorem reln_to_rel_inv[simp]:
1002  rel_to_reln (reln_to_rel r) = r
1003Proof
1004  SRW_TAC [] [reln_to_rel_app, EXTENSION, in_rel_to_reln]
1005QED
1006
1007Theorem reln_to_rel_11[simp]:
1008  (reln_to_rel r1 = reln_to_rel r2) <=> (r1 = r2)
1009Proof
1010  SRW_TAC [] [reln_to_rel_app, FUN_EQ_THM, FORALL_PROD, IN_DEF]
1011QED
1012
1013Theorem rel_to_reln_11[simp]:
1014  (rel_to_reln R1 = rel_to_reln R2) <=> (R1 = R2)
1015Proof
1016  SRW_TAC [] [in_rel_to_reln, EXTENSION, FORALL_PROD]
1017  THEN SRW_TAC [] [FUN_EQ_THM]
1018QED
1019
1020val reln_rel_conv_props =
1021  LIST_CONJ [in_rel_to_reln, reln_to_rel_app, rel_to_reln_inv, reln_to_rel_inv,
1022             reln_to_rel_11, rel_to_reln_11]
1023
1024Theorem rel_to_reln_swap:
1025  (r = rel_to_reln R) <=> (reln_to_rel r = R)
1026Proof
1027  METIS_TAC [rel_to_reln_inv, reln_to_rel_inv]
1028QED
1029
1030Theorem domain_to_rel_conv:
1031  domain r = RDOM (reln_to_rel r)
1032Proof
1033  SRW_TAC [] [domain_def, EXTENSION, IN_RDOM, reln_rel_conv_props]
1034QED
1035
1036Theorem range_to_rel_conv:
1037  range r = RRANGE (reln_to_rel r)
1038Proof
1039  SRW_TAC [] [range_def, EXTENSION, IN_RRANGE, reln_rel_conv_props]
1040QED
1041
1042Theorem strict_to_rel_conv:
1043  strict r = rel_to_reln (STRORD (reln_to_rel r))
1044Proof
1045  SRW_TAC [] [strict_def, rextension, reln_rel_conv_props, STRORD]
1046QED
1047
1048Theorem rrestrict_to_rel_conv:
1049  rrestrict r s = rel_to_reln (REL_RESTRICT (reln_to_rel r) s)
1050Proof
1051  SRW_TAC [boolSimps.EQUIV_EXTRACT_ss]
1052    [rrestrict_def, rextension, reln_rel_conv_props, REL_RESTRICT_DEF, RINTER,
1053     RRUNIV_def]
1054QED
1055
1056Theorem rcomp_to_rel_conv:
1057  r1 OO r2 = rel_to_reln ((reln_to_rel r2) O (reln_to_rel r1))
1058Proof
1059  SRW_TAC [] [rcomp_def, rextension, reln_rel_conv_props, relationTheory.O_DEF]
1060QED
1061
1062Theorem univ_reln_to_rel_conv:
1063  univ_reln s = rel_to_reln (RRUNIV s)
1064Proof
1065  SRW_TAC [] [univ_reln_def, rextension, reln_rel_conv_props, RRUNIV_def]
1066QED
1067
1068Theorem tc_to_rel_conv:
1069  tc r = rel_to_reln ((reln_to_rel r)^+)
1070Proof
1071  SRW_TAC [] [rextension, reln_rel_conv_props]
1072  THEN EQ_TAC
1073  THENL [
1074    MATCH_MP_TAC tc_ind
1075    THEN METIS_TAC [TC_RULES, reln_to_rel_app],
1076    Q.SPEC_TAC (`y`, `y`)
1077    THEN Q.SPEC_TAC (`x`, `x`)
1078    THEN HO_MATCH_MP_TAC TC_INDUCT
1079    THEN METIS_TAC [tc_rules, reln_to_rel_app]
1080  ]
1081QED
1082
1083Theorem acyclic_reln_to_rel_conv:
1084  acyclic r = irreflexive ((reln_to_rel r)^+)
1085Proof
1086  SRW_TAC [] [acyclic_def, tc_to_rel_conv, reln_rel_conv_props]
1087  THEN SRW_TAC [] [FUN_EQ_THM, relationTheory.irreflexive_def]
1088QED
1089
1090Theorem irreflexive_reln_to_rel_conv:
1091  (set_relation$irreflexive) r s =
1092  (relation$irreflexive) (REL_RESTRICT (reln_to_rel r) s)
1093Proof
1094  SRW_TAC [] [irreflexive_def, relationTheory.irreflexive_def, REL_RESTRICT_DEF,
1095              RINTER, RRUNIV_def, reln_rel_conv_props]
1096  THEN PROVE_TAC []
1097QED
1098
1099Theorem irreflexive_reln_to_rel_conv_UNIV:
1100  (set_relation$irreflexive) r UNIV = (relation$irreflexive) (reln_to_rel r)
1101Proof
1102  SIMP_TAC std_ss [irreflexive_reln_to_rel_conv, REL_RESTRICT_UNIV]
1103QED
1104
1105Theorem reflexive_reln_to_rel_conv:
1106  (set_relation$reflexive) r s =
1107  (relation$reflexive) (RREFL_EXP (reln_to_rel r) s)
1108Proof
1109  SRW_TAC [] [reflexive_def, relationTheory.reflexive_def, reln_rel_conv_props,
1110              RREFL_EXP_def, RUNION, RRUNIV_def]
1111  THEN PROVE_TAC[]
1112QED
1113
1114Theorem reflexive_reln_to_rel_conv_UNIV:
1115  (set_relation$reflexive) r UNIV = (relation$reflexive) (reln_to_rel r)
1116Proof
1117  REWRITE_TAC[reflexive_reln_to_rel_conv, RREFL_EXP_UNIV]
1118QED
1119
1120Theorem transitive_reln_to_rel_conv:
1121  (set_relation$transitive) r = (relation$transitive) (reln_to_rel r)
1122Proof
1123  SRW_TAC [] [transitive_def, relationTheory.transitive_def,
1124              reln_rel_conv_props]
1125QED
1126
1127Theorem antisym_reln_to_rel_conv:
1128  (set_relation$antisym) r = (relation$antisymmetric) (reln_to_rel r)
1129Proof
1130  SRW_TAC [] [antisym_def, relationTheory.antisymmetric_def,
1131              reln_rel_conv_props]
1132QED
1133
1134Theorem aux1[local]:
1135  ((reln_to_rel r) RSUBSET RRUNIV s) = (domain r SUBSET s /\ range r SUBSET s)
1136Proof
1137  SRW_TAC [] [RSUBSET, RRUNIV_def, domain_def, range_def, reln_to_rel_app,
1138              SUBSET_DEF]
1139  THEN PROVE_TAC []
1140QED
1141
1142Theorem aux2[local]:
1143  (domain r SUBSET s /\ range r SUBSET s) ==>
1144  (transitive (RREFL_EXP (reln_to_rel r) s) = transitive (reln_to_rel r))
1145Proof
1146  SRW_TAC [] [relationTheory.transitive_def, RREFL_EXP_def, RUNION,
1147              reln_to_rel_app, SUBSET_DEF, in_range, in_domain,
1148              GSYM LEFT_FORALL_IMP_THM]
1149  THEN PROVE_TAC []
1150QED
1151
1152Theorem aux3[local]:
1153  (domain r SUBSET s /\ range r SUBSET s) ==>
1154  (antisymmetric (RREFL_EXP (reln_to_rel r) s) = antisymmetric (reln_to_rel r))
1155Proof
1156  SRW_TAC [] [relationTheory.antisymmetric_def, RREFL_EXP_def, RUNION,
1157              reln_to_rel_app, SUBSET_DEF, in_range, in_domain,
1158              GSYM LEFT_FORALL_IMP_THM]
1159  THEN PROVE_TAC []
1160QED
1161
1162Theorem partial_order_reln_to_rel_conv:
1163  partial_order r s <=> reln_to_rel r RSUBSET RRUNIV s /\
1164                        WeakOrder (RREFL_EXP (reln_to_rel r) s)
1165Proof
1166  SRW_TAC [boolSimps.EQUIV_EXTRACT_ss]
1167    [partial_order_def, WeakOrder, reflexive_reln_to_rel_conv,
1168     transitive_reln_to_rel_conv, antisym_reln_to_rel_conv,
1169     aux1, aux2, aux3]
1170QED
1171
1172Theorem partial_order_reln_to_rel_conv_UNIV:
1173  partial_order r UNIV = WeakOrder (reln_to_rel r)
1174Proof
1175  SRW_TAC [] [partial_order_reln_to_rel_conv, RREFL_EXP_UNIV, RSUBSET,
1176              RRUNIV_def]
1177QED
1178
1179Theorem linear_order_reln_to_rel_conv_UNIV:
1180  linear_order r UNIV = WeakLinearOrder (reln_to_rel r)
1181Proof
1182  SRW_TAC [] [linear_order_def, WeakLinearOrder_dichotomy,
1183              reflexive_reln_to_rel_conv_UNIV, transitive_reln_to_rel_conv,
1184              antisym_reln_to_rel_conv, WeakOrder, relationTheory.reflexive_def,
1185              reln_to_rel_app]
1186  THEN PROVE_TAC []
1187QED
1188
1189Theorem strict_linear_order_reln_to_rel_conv_UNIV:
1190  strict_linear_order r UNIV = StrongLinearOrder (reln_to_rel r)
1191Proof
1192  SRW_TAC [] [strict_linear_order_def, StrongLinearOrder,
1193              reflexive_reln_to_rel_conv_UNIV, transitive_reln_to_rel_conv,
1194              antisym_reln_to_rel_conv, StrongOrder,
1195              relationTheory.irreflexive_def, reln_to_rel_app, trichotomous]
1196  THEN PROVE_TAC []
1197QED
1198
1199Theorem reln_rel_conv_thms =
1200  LIST_CONJ [
1201    reln_rel_conv_props,
1202    RREFL_EXP_UNIV,
1203    REL_RESTRICT_UNIV,
1204    domain_to_rel_conv,
1205    range_to_rel_conv,
1206    strict_to_rel_conv,
1207    rrestrict_to_rel_conv,
1208    rcomp_to_rel_conv,
1209    univ_reln_to_rel_conv,
1210    tc_to_rel_conv,
1211    acyclic_reln_to_rel_conv,
1212    irreflexive_reln_to_rel_conv,
1213    reflexive_reln_to_rel_conv,
1214    transitive_reln_to_rel_conv,
1215    antisym_reln_to_rel_conv,
1216    partial_order_reln_to_rel_conv_UNIV,
1217    linear_order_reln_to_rel_conv_UNIV,
1218    strict_linear_order_reln_to_rel_conv_UNIV
1219  ]
1220
1221Theorem acyclic_WF:
1222  FINITE s /\ acyclic r /\ domain r SUBSET s /\ range r SUBSET s ==>
1223  WF (reln_to_rel r)
1224Proof
1225  REPEAT STRIP_TAC
1226  THEN `(REL_RESTRICT (reln_to_rel r) s) = (reln_to_rel r)`
1227    by (FULL_SIMP_TAC std_ss [SUBSET_DEF, in_domain, in_range,
1228                              GSYM LEFT_FORALL_IMP_THM, FUN_EQ_THM,
1229                              REL_RESTRICT_DEF, reln_to_rel_app]
1230        THEN PROVE_TAC[])
1231  THEN FULL_SIMP_TAC std_ss [acyclic_reln_to_rel_conv]
1232  THEN PROVE_TAC [FINITE_WF_noloops]
1233QED
1234
1235Theorem WF_acyclic :
1236    !r. WF (reln_to_rel r) ==> acyclic r
1237Proof
1238    rpt STRIP_TAC
1239 >> SRW_TAC [][acyclic_def, tc_to_rel_conv, in_rel_to_reln]
1240 >> Q.ABBREV_TAC ‘R = reln_to_rel r’
1241 >> METIS_TAC [WF_noloops]
1242QED
1243
1244(* ------------------------------------------------------------------------ *)
1245(* Minimal and maximal elements                                             *)
1246(* ------------------------------------------------------------------------ *)
1247
1248Definition maximal_elements_def:
1249  maximal_elements xs r =
1250    {x | x IN xs /\ !x'. x' IN xs /\ (x, x') IN r ==> (x = x')}
1251End
1252
1253Definition minimal_elements_def:
1254  minimal_elements xs r =
1255    {x | x IN xs /\ !x'. x' IN xs /\ (x', x) IN r ==> (x = x')}
1256End
1257
1258val _ = ot0 "minimal_elements" "minimalElements"
1259
1260Theorem minimal_elements_subset:
1261  minimal_elements s lo SUBSET s
1262Proof
1263  SRW_TAC [] [SUBSET_DEF, minimal_elements_def]
1264QED
1265
1266Theorem minimal_elements_SWAP:
1267  minimal_elements xs (IMAGE SWAP r) = maximal_elements xs r
1268Proof
1269  REWRITE_TAC [minimal_elements_def, maximal_elements_def, EXTENSION,
1270               pair_in_IMAGE_SWAP]
1271QED
1272
1273Theorem maximal_union:
1274  !e s r1 r2.
1275    e IN maximal_elements s (r1 UNION r2) ==>
1276    e IN maximal_elements s r1 /\
1277    e IN maximal_elements s r2
1278Proof
1279  SRW_TAC [] [maximal_elements_def]
1280QED
1281
1282Theorem minimal_union:
1283  !e s r1 r2.
1284    e IN minimal_elements s (r1 UNION r2) ==>
1285    e IN minimal_elements s r1 /\
1286    e IN minimal_elements s r2
1287Proof
1288  SRW_TAC [] [minimal_elements_def]
1289QED
1290
1291Theorem minimal_elements_mono:
1292  r SUBSET r' ==> minimal_elements xs r' SUBSET minimal_elements xs r
1293Proof
1294  Ho_Rewrite.REWRITE_TAC [minimal_elements_def, SUBSET_DEF, IN_GSPEC_IFF]
1295  THEN REPEAT STRIP_TAC
1296  THENL [FIRST_ASSUM ACCEPT_TAC, REPEAT RES_TAC]
1297QED
1298
1299Theorem minimal_elements_rrestrict:
1300  minimal_elements xs (rrestrict r xs) = minimal_elements xs r
1301Proof
1302  Ho_Rewrite.REWRITE_TAC
1303    [minimal_elements_def, in_rrestrict, EXTENSION, IN_GSPEC_IFF]
1304  THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)
1305  THEN (FIRST_ASSUM ACCEPT_TAC ORELSE RES_TAC)
1306QED
1307
1308Theorem WF_has_minimal_path:
1309  WF (reln_to_rel r) ==> x IN s ==>
1310  ?y. y IN minimal_elements s r /\ ((y, x) IN tc r \/ (y = x))
1311Proof
1312  Ho_Rewrite.REWRITE_TAC
1313    [WF_DEF, reln_to_rel_app, minimal_elements_def, IN_GSPEC_IFF]
1314  THEN REPEAT STRIP_TAC
1315  THEN VALIDATE
1316         (FIRST_X_ASSUM
1317           (ASSUME_TAC o UNDISCH o
1318            Q.SPEC `\z. z IN s /\ ((z, x) IN tc r \/ (z = x))`))
1319  THENL [
1320    Q.EXISTS_TAC `x`
1321    THEN BETA_TAC
1322    THEN ASM_REWRITE_TAC [],
1323    POP_ASSUM CHOOSE_TAC
1324    THEN Q.EXISTS_TAC `min`
1325    THEN RULE_L_ASSUM_TAC (CONJUNCTS o BETA_RULE)
1326    THEN ASM_REWRITE_TAC []
1327    THEN REPEAT STRIP_TAC
1328    THEN RES_TAC
1329    THEN IMP_RES_TAC tc_rule1
1330    THEN FIRST_ASSUM DISJ_CASES_TAC
1331    THENL [
1332      IMP_RES_TAC tc_rule2,
1333      BasicProvers.VAR_EQ_TAC
1334    ]
1335    THEN RES_TAC
1336  ]
1337QED
1338
1339Theorem tc_path_max_lem[local]:
1340  !s. FINITE s ==>
1341      s <> {} ==> !r. acyclic r ==> ?x. x IN maximal_elements s (tc r)
1342Proof
1343  HO_MATCH_MP_TAC FINITE_INDUCT
1344  THEN SRW_TAC [] []
1345  THEN Cases_on `s={}`
1346  THEN1 SRW_TAC [] [maximal_elements_def]
1347  THEN RES_TAC
1348  THEN Cases_on `(x, e) IN (tc r)`
1349  THENL [
1350    Q.EXISTS_TAC `e`
1351    THEN SRW_TAC [] [maximal_elements_def]
1352    THEN `(x, x'') IN (tc r)` by METIS_TAC [tc_rules]
1353    THEN FULL_SIMP_TAC (srw_ss()) [acyclic_def, maximal_elements_def]
1354    THEN METIS_TAC [],
1355    FULL_SIMP_TAC (srw_ss()) [maximal_elements_def]
1356    THEN METIS_TAC []
1357  ]
1358QED
1359
1360Theorem tc_path_min_lem[local]:
1361  !s. FINITE s ==>
1362      s <> {} ==> !r. acyclic r ==> ?x. x IN minimal_elements s (tc r)
1363Proof
1364  HO_MATCH_MP_TAC FINITE_INDUCT
1365  THEN SRW_TAC [] []
1366  THEN Cases_on `s={}`
1367  THEN1 SRW_TAC [] [minimal_elements_def]
1368  THEN RES_TAC
1369  THEN Cases_on `(e, x) IN (tc r)`
1370  THENL [
1371    Q.EXISTS_TAC `e`
1372    THEN SRW_TAC [] [minimal_elements_def]
1373    THEN `(x'', x) IN (tc r)` by METIS_TAC [tc_rules]
1374    THEN FULL_SIMP_TAC (srw_ss()) [acyclic_def, minimal_elements_def]
1375    THEN METIS_TAC [],
1376    FULL_SIMP_TAC (srw_ss()) [minimal_elements_def]
1377    THEN METIS_TAC []
1378  ]
1379QED
1380
1381Theorem finite_acyclic_has_maximal:
1382  !s. FINITE s ==> s <> {} ==> !r. acyclic r ==> ?x. x IN maximal_elements s r
1383Proof
1384  SRW_TAC [] []
1385  THEN IMP_RES_TAC tc_path_max_lem
1386  THEN FULL_SIMP_TAC (srw_ss()) [maximal_elements_def]
1387  THEN METIS_TAC [tc_rules]
1388QED
1389
1390Theorem finite_acyclic_has_minimal:
1391  !s. FINITE s ==> s <> {} ==> !r. acyclic r ==> ?x. x IN minimal_elements s r
1392Proof
1393  SRW_TAC [] []
1394  THEN IMP_RES_TAC tc_path_min_lem
1395  THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def]
1396  THEN METIS_TAC [tc_rules]
1397QED
1398
1399Theorem lemma1[local]:
1400  !x y. (x, y) IN tc r ==> ?z. (x, z) IN r /\ (x <> y ==> x <> z)
1401Proof
1402  HO_MATCH_MP_TAC tc_ind
1403  THEN SRW_TAC [] []
1404  THEN METIS_TAC []
1405QED
1406
1407Theorem maximal_TC:
1408  !s r.
1409    domain r SUBSET s /\ range r SUBSET s ==>
1410    (maximal_elements s (tc r) = maximal_elements s r)
1411Proof
1412  SRW_TAC [] [EXTENSION, maximal_elements_def, domain_def, range_def,
1413              SUBSET_DEF]
1414  THEN EQ_TAC
1415  THEN SRW_TAC [] []
1416  THEN METIS_TAC [lemma1, tc_rules]
1417QED
1418
1419Theorem lemma1[local]:
1420  !y x. (y, x) IN tc r ==> ?z. (z, x) IN r /\ (x <> y ==> x <> z)
1421Proof
1422  HO_MATCH_MP_TAC tc_ind
1423  THEN SRW_TAC [] []
1424  THEN METIS_TAC []
1425QED
1426
1427Theorem minimal_TC:
1428  !s r.
1429    domain r SUBSET s /\ range r SUBSET s ==>
1430    (minimal_elements s (tc r) = minimal_elements s r)
1431Proof
1432  SRW_TAC [] [EXTENSION, minimal_elements_def, domain_def, range_def,
1433              SUBSET_DEF]
1434  THEN EQ_TAC
1435  THEN SRW_TAC [] []
1436  THEN METIS_TAC [lemma1, tc_rules]
1437QED
1438
1439val rr_acyclic_WF = Q.INST [`r` |-> `rrestrict r s`] acyclic_WF
1440val rme = MATCH_MP WF_has_minimal_path (UNDISCH_ALL rr_acyclic_WF)
1441val irme = Q.INST [`s'` |-> `s`] rme
1442val urme = REWRITE_RULE [domain_rrestrict_SUBSET, range_rrestrict_SUBSET,
1443                         minimal_elements_rrestrict] (DISCH_ALL irme)
1444val tcrr = REWRITE_RULE [SUBSET_DEF] (MATCH_MP tc_mono rrestrict_SUBSET)
1445
1446Theorem finite_acyclic_has_minimal_path:
1447  !s r x.
1448    FINITE s /\
1449    acyclic r /\
1450    x IN s /\
1451    x NOTIN minimal_elements s r ==>
1452    ?y. y IN minimal_elements s r /\ (y, x) IN tc r
1453Proof
1454  REPEAT STRIP_TAC
1455  THEN IMP_RES_THEN (ASSUME_TAC o Q.SPEC `s`) acyclic_rrestrict
1456  THEN IMP_RES_TAC urme
1457  THEN TRY (BasicProvers.VAR_EQ_TAC THEN RES_TAC)
1458  THEN Q.EXISTS_TAC `y'`
1459  THEN ASM_REWRITE_TAC []
1460  THEN IMP_RES_TAC tcrr
1461QED
1462
1463val tc_SWAP' = REWRITE_RULE [rextension, pair_in_IMAGE_SWAP] tc_SWAP
1464
1465Theorem finite_acyclic_has_maximal_path:
1466  !s r x.
1467    FINITE s /\
1468    acyclic r /\
1469    x IN s /\
1470    x NOTIN maximal_elements s r ==>
1471    ?y. y IN maximal_elements s r /\ (x, y) IN tc r
1472Proof
1473  ONCE_REWRITE_TAC
1474    [GSYM tc_SWAP', GSYM minimal_elements_SWAP, GSYM acyclic_SWAP]
1475  THEN REPEAT STRIP_TAC
1476  THEN irule finite_acyclic_has_minimal_path
1477  THEN rpt conj_tac
1478  THEN FIRST_ASSUM ACCEPT_TAC
1479QED
1480
1481Theorem finite_prefix_po_has_minimal_path:
1482  !r s x s'.
1483    partial_order r s /\
1484    finite_prefixes r s /\
1485    x NOTIN minimal_elements s' r /\
1486    x IN s' /\
1487    s' SUBSET s ==>
1488    ?x'. x' IN minimal_elements s' r /\ (x', x) IN r
1489Proof
1490  SRW_TAC [] [finite_prefixes_def]
1491  THEN IMP_RES_TAC strict_partial_order_acyclic
1492  THEN `?x'. x' IN minimal_elements (s' INTER {x' | (x', x) IN r}) (strict r) /\
1493        (x', x) IN tc (strict r)`
1494    by (MATCH_MP_TAC finite_acyclic_has_minimal_path
1495        THEN SRW_TAC [] []
1496        THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, strict_def,
1497                                       SUBSET_DEF, partial_order_def,
1498                                       reflexive_def]
1499        THEN METIS_TAC [INTER_FINITE, INTER_COMM])
1500  THEN Q.EXISTS_TAC `x'`
1501  THEN SRW_TAC [] []
1502  THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def]
1503  THEN SRW_TAC [] []
1504  THEN FULL_SIMP_TAC (srw_ss()) [partial_order_def, domain_def, SUBSET_DEF,
1505                                 transitive_def, strict_def]
1506  THEN METIS_TAC []
1507QED
1508
1509Theorem empty_strict_linear_order:
1510  !r. strict_linear_order r {} = (r = {})
1511Proof
1512  SRW_TAC [] [strict_linear_order_def, RES_FORALL_THM, domain_def, range_def,
1513              transitive_def, EXTENSION]
1514  THEN EQ_TAC
1515  THEN SRW_TAC [] []
1516  THEN Cases_on `x`
1517  THEN SRW_TAC [] []
1518QED
1519
1520Theorem empty_linear_order:
1521  !r. linear_order r {} = (r = {})
1522Proof
1523  SRW_TAC [] [linear_order_def, RES_FORALL_THM, domain_def, range_def,
1524              transitive_def, antisym_def, EXTENSION]
1525  THEN EQ_TAC
1526  THEN SRW_TAC [] []
1527  THEN Cases_on `x`
1528  THEN SRW_TAC [] []
1529QED
1530
1531Theorem linear_order_restrict:
1532  !s r s'. linear_order r s ==> linear_order (rrestrict r s') (s INTER s')
1533Proof
1534  Ho_Rewrite.REWRITE_TAC
1535    [linear_order_def, rrestrict_def, domain_def, range_def, SUBSET_DEF,
1536    transitive_def, antisym_def, IN_GSPEC_IFF, PAIR_IN_GSPEC_IFF, IN_INTER]
1537  THEN REPEAT STRIP_TAC
1538  THEN ASM_REWRITE_TAC []
1539  THEN_LT LASTGOAL (FIRST_X_ASSUM irule THEN rpt conj_tac
1540                    THEN FIRST_ASSUM ACCEPT_TAC)
1541  THEN RES_TAC
1542QED
1543
1544Theorem strict_linear_order_restrict:
1545  !s r s'.
1546    strict_linear_order r s ==>
1547    strict_linear_order (rrestrict r s') (s INTER s')
1548Proof
1549  Ho_Rewrite.REWRITE_TAC
1550    [strict_linear_order_def, rrestrict_def, domain_def, range_def,
1551     SUBSET_DEF, transitive_def, antisym_def, IN_GSPEC_IFF, PAIR_IN_GSPEC_IFF,
1552     IN_INTER]
1553  THEN REPEAT STRIP_TAC
1554  THEN ASM_REWRITE_TAC []
1555  THEN_LT LASTGOAL (FIRST_X_ASSUM irule
1556                    THEN rpt conj_tac
1557                    THEN FIRST_ASSUM ACCEPT_TAC)
1558  THEN RES_TAC
1559QED
1560
1561Theorem linear_order_dom_rg:
1562  linear_order lo X ==> (domain lo UNION range lo = X)
1563Proof
1564  REWRITE_TAC [linear_order_def]
1565  THEN STRIP_TAC
1566  THEN ASM_REWRITE_TAC [SET_EQ_SUBSET, UNION_SUBSET]
1567  THEN REWRITE_TAC [SUBSET_DEF, IN_UNION, in_domain]
1568  THEN REPEAT STRIP_TAC
1569  THEN RES_TAC
1570  THEN DISJ1_TAC
1571  THEN Q.EXISTS_TAC `x`
1572  THEN POP_ASSUM ACCEPT_TAC
1573QED
1574
1575Theorem linear_order_refl:
1576  linear_order lo X ==> x IN X ==> (x, x) IN lo
1577Proof
1578  REWRITE_TAC [linear_order_def]
1579  THEN REPEAT STRIP_TAC
1580  THEN RES_TAC
1581QED
1582
1583Theorem linear_order_in_set:
1584  linear_order lo X ==> (x, y) IN lo ==> x IN X /\ y IN X
1585Proof
1586  REPEAT DISCH_TAC
1587  THEN IMP_RES_TAC linear_order_dom_rg
1588  THEN BasicProvers.VAR_EQ_TAC
1589  THEN IMP_RES_TAC in_dom_rg
1590  THEN ASM_REWRITE_TAC [IN_UNION]
1591QED
1592
1593Theorem IN_MIN_LO:
1594  x IN X ==> linear_order lo X ==> y IN minimal_elements X lo ==> (y, x) IN lo
1595Proof
1596  Ho_Rewrite.REWRITE_TAC
1597    [minimal_elements_def, linear_order_def, EXTENSION, IN_GSPEC_IFF]
1598  THEN REPEAT STRIP_TAC
1599  THEN FIRST_X_ASSUM (ASSUME_TAC o Q.SPECL [`x`, `y`])
1600  THEN FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `x`)
1601  THEN RES_TAC
1602  THEN RES_TAC
1603  THEN FULL_SIMP_TAC std_ss []
1604QED
1605
1606Theorem extend_linear_order:
1607  !r s x.
1608    x NOTIN s /\ linear_order r s ==>
1609    linear_order (r UNION {(y, x) | y | y IN (s UNION {x})}) (s UNION {x})
1610Proof
1611  Ho_Rewrite.REWRITE_TAC
1612    [linear_order_def, domain_def, range_def, transitive_def, antisym_def,
1613     SUBSET_DEF, IN_UNION, IN_SING, PAIR_IN_GSPEC_1, PAIR_IN_GSPEC_2,
1614     IN_GSPEC_IFF]
1615  THEN REPEAT STRIP_TAC
1616  THEN ASM_REWRITE_TAC []
1617  THEN METIS_TAC []
1618QED
1619
1620Theorem strict_linear_order_acyclic:
1621  !r s. strict_linear_order r s ==> acyclic r
1622Proof
1623  SRW_TAC [] [acyclic_def, strict_linear_order_def]
1624  THEN IMP_RES_TAC transitive_tc
1625  THEN FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def, transitive_def]
1626QED
1627
1628Theorem acyclic_union[local]:
1629  acyclic (r1 UNION r2) ==> (q, r) IN r2 ==> (r, q) NOTIN r1
1630Proof
1631  REWRITE_TAC [acyclic_def]
1632  THEN REPEAT STRIP_TAC
1633  THEN VALIDATE
1634         (FIRST_ASSUM
1635            (CONTR_TAC o UNDISCH o MATCH_MP F_IMP o Q.SPEC `q`))
1636  THEN irule tc_rule2
1637  THEN Q.EXISTS_TAC `r`
1638  THEN CONJ_TAC
1639  THEN irule tc_rule1
1640  THEN ASM_REWRITE_TAC [IN_UNION]
1641QED
1642
1643Theorem strict_linear_order_union_acyclic:
1644  !r1 r2 s.
1645    strict_linear_order r1 s /\ (domain r2 UNION range r2) SUBSET s ==>
1646    (acyclic (r1 UNION r2) <=> r2 SUBSET r1)
1647Proof
1648  SRW_TAC [] []
1649  THEN EQ_TAC
1650  THEN SRW_TAC [] []
1651  THENL [
1652    FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def, domain_def,
1653                              transitive_def, range_def, SUBSET_DEF]
1654    THEN REPEAT STRIP_TAC
1655    THEN Cases_on `x`
1656    THEN RES_TAC
1657    THEN RES_TAC
1658    THEN IMP_RES_TAC acyclic_union
1659    THEN IMP_RES_TAC acyclic_irreflexive
1660    THEN CCONTR_TAC THEN FULL_SIMP_TAC std_ss [IN_UNION],
1661    `r1 UNION r2 = r1`
1662    by (FULL_SIMP_TAC (srw_ss()) [domain_def, range_def, SUBSET_DEF, EXTENSION]
1663        THEN METIS_TAC [])
1664    THEN SRW_TAC [] []
1665    THEN METIS_TAC [strict_linear_order_acyclic]
1666  ]
1667QED
1668
1669Theorem strict_linear_order:
1670  !r s. linear_order r s ==> strict_linear_order (strict r) s
1671Proof
1672  Ho_Rewrite.REWRITE_TAC
1673    [linear_order_def, strict_linear_order_def, strict_def, domain_def,
1674     range_def, SUBSET_DEF, transitive_def, antisym_def, IN_GSPEC_IFF,
1675     PAIR_IN_GSPEC_IFF]
1676  THEN REPEAT STRIP_TAC
1677  THEN REPEAT BasicProvers.VAR_EQ_TAC
1678  THEN ASM_REWRITE_TAC []
1679  THEN METIS_TAC []
1680QED
1681
1682Theorem linear_order:
1683  !r s. strict_linear_order r s ==> linear_order (r UNION {(x, x) | x IN s}) s
1684Proof
1685  Ho_Rewrite.REWRITE_TAC
1686    [linear_order_def, strict_linear_order_def, domain_def, range_def,
1687     SUBSET_DEF, transitive_def, antisym_def, IN_UNION, IN_GSPEC_IFF,
1688     PAIR_IN_GSPEC_IFF, PAIR_IN_GSPEC_same]
1689  THEN REPEAT STRIP_TAC
1690  THEN REPEAT BasicProvers.VAR_EQ_TAC
1691  THEN ASM_REWRITE_TAC []
1692  THEN METIS_TAC []
1693QED
1694
1695Theorem finite_strict_linear_order_has_maximal:
1696  !s r.
1697    FINITE s /\ strict_linear_order r s /\ s <> {} ==>
1698    ?x. x IN maximal_elements s r
1699Proof
1700  METIS_TAC [strict_linear_order_acyclic, finite_acyclic_has_maximal]
1701QED
1702
1703Theorem finite_strict_linear_order_has_minimal:
1704  !s r.
1705    FINITE s /\ strict_linear_order r s /\ s <> {} ==>
1706    ?x. x IN minimal_elements s r
1707Proof
1708  METIS_TAC [strict_linear_order_acyclic, finite_acyclic_has_minimal]
1709QED
1710
1711Theorem finite_linear_order_has_maximal:
1712  !s r.
1713    FINITE s /\ linear_order r s /\ s <> {} ==> ?x. x IN maximal_elements s r
1714Proof
1715  SRW_TAC [] []
1716  THEN IMP_RES_TAC strict_linear_order
1717  THEN IMP_RES_TAC finite_strict_linear_order_has_maximal
1718  THEN Q.EXISTS_TAC `x`
1719  THEN FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, strict_def]
1720  THEN METIS_TAC []
1721QED
1722
1723Theorem finite_linear_order_has_minimal:
1724  !s r.
1725    FINITE s /\ linear_order r s /\ s <> {} ==> ?x. x IN minimal_elements s r
1726Proof
1727  SRW_TAC [] []
1728  THEN IMP_RES_TAC strict_linear_order
1729  THEN IMP_RES_TAC finite_strict_linear_order_has_minimal
1730  THEN Q.EXISTS_TAC `x`
1731  THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, strict_def]
1732  THEN METIS_TAC []
1733QED
1734
1735Theorem maximal_linear_order:
1736  !s r x y.
1737    y IN s /\ linear_order r s /\ x IN maximal_elements s r ==> (y, x) IN r
1738Proof
1739  SRW_TAC [] [linear_order_def, maximal_elements_def]
1740  THEN METIS_TAC []
1741QED
1742
1743Theorem minimal_linear_order:
1744  !s r x y.
1745    y IN s /\ linear_order r s /\ x IN minimal_elements s r ==> (x, y) IN r
1746Proof
1747  SRW_TAC [] [linear_order_def, minimal_elements_def]
1748  THEN METIS_TAC []
1749QED
1750
1751Theorem minimal_linear_order_unique:
1752  !r s s' x y.
1753    linear_order r s /\
1754    x IN minimal_elements s' r /\
1755    y IN minimal_elements s' r /\
1756    s' SUBSET s ==>
1757    (x = y)
1758Proof
1759  SRW_TAC [] [minimal_elements_def, linear_order_def, antisym_def, SUBSET_DEF]
1760  THEN METIS_TAC []
1761QED
1762
1763Theorem finite_prefix_linear_order_has_unique_minimal:
1764  !r s s'.
1765    linear_order r s /\
1766    finite_prefixes r s /\
1767    x IN s' /\
1768    s' SUBSET s ==>
1769    SING (minimal_elements s' r)
1770Proof
1771  SRW_TAC [] [SING_DEF]
1772  THEN Cases_on `?y. y IN minimal_elements s' r`
1773  THEN1 METIS_TAC [UNIQUE_MEMBER_SING, minimal_linear_order_unique]
1774  THEN METIS_TAC [partial_order_linear_order, finite_prefix_po_has_minimal_path]
1775QED
1776
1777Theorem nat_order_iso_thm:
1778  !(f: num -> 'a option) (s : 'a set).
1779    (!n m. (f m = f n) /\ f m <> NONE ==> (m = n)) /\
1780    (!x. x IN s ==> ?m. (f m = SOME x)) /\
1781    (!m x. (f m = SOME x) ==> x IN s) ==>
1782    linear_order
1783      {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s /\
1784    finite_prefixes
1785      {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s
1786Proof
1787  SRW_TAC [] [linear_order_def, domain_def, range_def, SUBSET_DEF,
1788              transitive_def, antisym_def, finite_prefixes_def]
1789  THENL [
1790    METIS_TAC [],
1791    METIS_TAC [],
1792    METIS_TAC [LESS_EQ_TRANS, SOME_11, NOT_SOME_NONE],
1793    METIS_TAC [LESS_EQUAL_ANTISYM, SOME_11, NOT_SOME_NONE],
1794    METIS_TAC [NOT_LESS_EQUAL, LESS_IMP_LESS_OR_EQ],
1795    `?n. SOME e = f n` by METIS_TAC []
1796    THEN SRW_TAC [] []
1797    THEN `{SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} SUBSET
1798          IMAGE f (count (SUC n))`
1799      by (SRW_TAC [] [SUBSET_DEF, count_def,
1800                      DECIDE ``!x:num y. x < SUC y <=> x <= y``]
1801          THEN METIS_TAC [NOT_SOME_NONE])
1802    THEN `{x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} =
1803          IMAGE THE {SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)}`
1804      by (SRW_TAC [] [EXTENSION] THEN METIS_TAC [THE_DEF])
1805    THEN METIS_TAC [IMAGE_FINITE, SUBSET_FINITE, FINITE_COUNT]
1806  ]
1807QED
1808
1809Definition chain_def:
1810  chain s r = !x y. x IN s /\ y IN s ==> (x, y) IN r \/ (y, x) IN r
1811End
1812
1813Definition upper_bounds_def:
1814  upper_bounds s r = {x | x IN range r /\ !y. y IN s ==> (y, x) IN r}
1815End
1816
1817Theorem upper_bounds_lem:
1818  !r s x1 x2.
1819    transitive r /\ x1 IN upper_bounds s r /\ (x1, x2) IN r ==>
1820    x2 IN upper_bounds s r
1821Proof
1822  SRW_TAC [] [transitive_def, upper_bounds_def, range_def]
1823  THEN METIS_TAC []
1824QED
1825
1826(* ----------------- Zorn's lemma ---------------- *)
1827(* Following "A short proof of Zorn's Lemma" by J.D. Weston, Archiv der
1828   * Mathematik, 1957 *)
1829
1830(* Chains that are built by transfinite repetition of adding an arbitrary
1831   * minimal upper bound  *)
1832
1833Definition fchains_def:
1834  fchains r =
1835    { k | chain k r /\ k <> {} /\
1836          !C. chain C r /\ C SUBSET k /\
1837              (upper_bounds C r DIFF C) INTER k <> {} ==>
1838              (CHOICE (upper_bounds C r DIFF C) IN
1839               minimal_elements ((upper_bounds C r DIFF C) INTER k) r) }
1840End
1841
1842Theorem lemma1[local]:
1843  !x s r. chain s r /\ x IN s ==> x IN domain r /\ x IN range r
1844Proof
1845  SRW_TAC [] [chain_def, in_domain, in_range]
1846  THEN METIS_TAC []
1847QED
1848
1849Theorem lemma2[local]:
1850  !r k1 k2 x x'.
1851    transitive r /\
1852    k1 IN fchains r /\
1853    k2 IN fchains r /\
1854    x IN k1 /\
1855    x' IN k2 /\
1856    x' NOTIN k1 ==>
1857    (x, x') IN r
1858Proof
1859  SRW_TAC [] []
1860  THEN `x IN range r /\ x' IN range r`
1861    by (FULL_SIMP_TAC (srw_ss()) [fchains_def] THEN METIS_TAC [lemma1])
1862  THEN Q.ABBREV_TAC `C = {x | x IN k1 /\ x IN k2 /\ (x, x') IN r}`
1863  THEN `x' IN upper_bounds C r DIFF C`
1864    by (Q.UNABBREV_TAC `C` THEN FULL_SIMP_TAC (srw_ss()) [upper_bounds_def])
1865  THEN `chain C r /\ C SUBSET k2 /\ C SUBSET k1`
1866    by (Q.UNABBREV_TAC `C`
1867        THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF, chain_def, fchains_def])
1868  THEN `CHOICE (upper_bounds C r DIFF C) IN
1869        minimal_elements ((upper_bounds C r DIFF C) INTER k2) r`
1870    by (FULL_SIMP_TAC (srw_ss()) [fchains_def]
1871        THEN METIS_TAC [NOT_IN_EMPTY, IN_DIFF, IN_INTER])
1872  THEN `CHOICE (upper_bounds C r DIFF C) IN k2 /\
1873        (CHOICE (upper_bounds C r DIFF C), x') IN r`
1874    by (FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, chain_def, fchains_def]
1875        THEN METIS_TAC [])
1876  THEN `(upper_bounds C r DIFF C) INTER k1 = {}`
1877    by (SRW_TAC [] [EXTENSION]
1878        THEN CCONTR_TAC
1879        THEN FULL_SIMP_TAC (srw_ss()) []
1880        THEN `CHOICE (upper_bounds C r DIFF C) IN k1`
1881          by (FULL_SIMP_TAC (srw_ss())
1882                [minimal_elements_def, chain_def, fchains_def]
1883              THEN METIS_TAC [NOT_IN_EMPTY, IN_DIFF, IN_INTER])
1884        THEN `CHOICE (upper_bounds C r DIFF C) IN C`
1885          by (Q.UNABBREV_TAC `C` THEN FULL_SIMP_TAC (srw_ss()) [])
1886        THEN METIS_TAC [CHOICE_DEF, MEMBER_NOT_EMPTY, IN_DIFF])
1887   THEN `?x''. x'' IN C /\ (x, x'') IN r`
1888     by (FULL_SIMP_TAC (srw_ss()) [EXTENSION, upper_bounds_def, fchains_def,
1889                                   SUBSET_DEF, chain_def]
1890         THEN METIS_TAC [])
1891   THEN `(x'',x') IN r`
1892     by (Q.UNABBREV_TAC `C` THEN FULL_SIMP_TAC (srw_ss()) [])
1893   THEN METIS_TAC [transitive_def]
1894QED
1895
1896Theorem lemma3[local]:
1897  !r k1 k2.
1898     transitive r /\ antisym r /\ k1 IN fchains r /\ k2 IN fchains r ==>
1899     k1 SUBSET k2 \/ k2 SUBSET k1
1900Proof
1901  SRW_TAC [] [antisym_def, SUBSET_DEF]
1902  THEN CCONTR_TAC
1903  THEN FULL_SIMP_TAC (srw_ss()) []
1904  THEN `(x, x') IN r` by METIS_TAC [lemma2]
1905  THEN METIS_TAC [lemma2]
1906QED
1907
1908Theorem lemma4[local]:
1909  !r. antisym r /\ transitive r ==>
1910      chain (BIGUNION (fchains r)) r /\
1911      (!x x' k.
1912        (x',x) IN r /\
1913        x' IN BIGUNION (fchains r) /\
1914        x IN BIGUNION (fchains r) /\
1915        k IN fchains r /\
1916        x IN k ==>
1917        x' IN k)
1918Proof
1919  SRW_TAC [] [chain_def]
1920  THENL [
1921    Cases_on `y IN s`
1922    THENL [
1923      FULL_SIMP_TAC (srw_ss()) [fchains_def, chain_def]
1924      THEN METIS_TAC [],
1925      METIS_TAC [lemma2]
1926    ],
1927   METIS_TAC [lemma2, antisym_def]
1928 ]
1929QED
1930
1931Theorem lemma5[local]:
1932  !r s. range r SUBSET s /\ (range r <> {}) /\ reflexive r s ==>
1933        { CHOICE (range r) } IN fchains r
1934Proof
1935  SRW_TAC [] [fchains_def]
1936  THENL [
1937    FULL_SIMP_TAC (srw_ss()) [chain_def, reflexive_def, SUBSET_DEF]
1938    THEN METIS_TAC [CHOICE_DEF, MEMBER_NOT_EMPTY],
1939    FULL_SIMP_TAC (srw_ss()) [GSYM DISJOINT_DEF, IN_DISJOINT]
1940    THEN SRW_TAC [] [minimal_elements_def, upper_bounds_def]
1941    THEN METIS_TAC [CHOICE_DEF, MEMBER_NOT_EMPTY]
1942  ]
1943QED
1944
1945Theorem lemma6[local]:
1946  !r k x C.
1947    transitive r /\
1948    antisym r /\
1949    k IN fchains r /\
1950    x IN k /\
1951    chain C r /\
1952    x IN upper_bounds C r DIFF C /\
1953    C SUBSET BIGUNION (fchains r) ==>
1954    CHOICE (upper_bounds C r DIFF C) IN k /\
1955    (CHOICE (upper_bounds C r DIFF C),x) IN r
1956Proof
1957  SRW_TAC [] []
1958  THEN `!x'. x' IN C ==> (x',x) IN r /\ (x' <> x)`
1959    by FULL_SIMP_TAC (srw_ss()) [upper_bounds_def]
1960  THEN `C SUBSET k`
1961    by (FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF]
1962        THEN SRW_TAC [] []
1963        THEN RES_TAC
1964        THEN IMP_RES_TAC lemma4
1965        THEN METIS_TAC [IN_BIGUNION])
1966  THEN FULL_SIMP_TAC (srw_ss()) [fchains_def, minimal_elements_def, chain_def]
1967  THEN `(upper_bounds C r DIFF C) INTER k <> {}`
1968    by (FULL_SIMP_TAC (srw_ss()) [GSYM DISJOINT_DEF, IN_DISJOINT, IN_DIFF]
1969        THEN METIS_TAC [])
1970  THEN METIS_TAC []
1971QED
1972
1973Theorem lemma7[local]:
1974  !r s.
1975     range r SUBSET s /\ (range r <> {}) /\ antisym r /\ reflexive r s /\
1976     transitive r ==>
1977     BIGUNION (fchains r) IN fchains r
1978Proof
1979  SRW_TAC [] [fchains_def]
1980  THEN FULL_SIMP_TAC (srw_ss()) [GSYM fchains_def]
1981  THEN1 METIS_TAC [lemma4]
1982  THEN1 METIS_TAC [lemma5, NOT_IN_EMPTY]
1983  THENL [
1984    `{ CHOICE (range r) } IN fchains r` by METIS_TAC [lemma5]
1985    THEN CCONTR_TAC
1986    THEN FULL_SIMP_TAC (srw_ss()) [],
1987    `?x k. x IN (upper_bounds C r DIFF C) /\ x IN k /\ k IN fchains r`
1988      by METIS_TAC [GSYM DISJOINT_DEF, IN_DISJOINT, IN_BIGUNION]
1989    THEN `CHOICE (upper_bounds C r DIFF C) IN k /\
1990          (CHOICE (upper_bounds C r DIFF C),x) IN r`
1991      by METIS_TAC [lemma6]
1992    THEN SRW_TAC [] [minimal_elements_def]
1993    THEN FULL_SIMP_TAC (srw_ss()) []
1994    THEN1 METIS_TAC [CHOICE_DEF, IN_DIFF]
1995    THEN1 METIS_TAC [CHOICE_DEF, IN_DIFF]
1996    THEN1 METIS_TAC []
1997    THEN `(CHOICE (upper_bounds C r DIFF C),x'') IN r`
1998      by METIS_TAC [lemma6, IN_DIFF]
1999    THEN METIS_TAC [antisym_def]
2000  ]
2001QED
2002
2003Theorem lemma8[local]:
2004  !r s k.
2005     range r SUBSET s /\
2006     (range r <> {}) /\
2007     reflexive r s /\ antisym r /\ transitive r /\
2008     k IN fchains r /\
2009     (upper_bounds k r DIFF k <> {}) ==>
2010    (CHOICE (upper_bounds k r DIFF k) INSERT k IN fchains r)
2011Proof
2012  SRW_TAC [] [fchains_def]
2013  THEN `CHOICE (upper_bounds k r DIFF k) IN upper_bounds k r DIFF k`
2014    by METIS_TAC [IN_DIFF, IN_DISJOINT, DISJOINT_DEF, CHOICE_DEF]
2015  THENL [
2016    FULL_SIMP_TAC (srw_ss()) [chain_def, upper_bounds_def]
2017    THEN SRW_TAC [] []
2018    THEN FULL_SIMP_TAC (srw_ss()) [reflexive_def, SUBSET_DEF],
2019    `CHOICE (upper_bounds C r DIFF C) IN upper_bounds C r DIFF C`
2020      by METIS_TAC [IN_DIFF, IN_DISJOINT, DISJOINT_DEF, CHOICE_DEF]
2021    THEN `C SUBSET k`
2022      by (FULL_SIMP_TAC (srw_ss()) [IN_DISJOINT, GSYM DISJOINT_DEF,
2023                                    SUBSET_DEF, upper_bounds_def]
2024          THEN SRW_TAC [] []
2025          THEN METIS_TAC [antisym_def])
2026    THEN Cases_on `(upper_bounds C r DIFF C) INTER k <> {}`
2027    THENL [
2028      SRW_TAC [] [minimal_elements_def]
2029      THEN1 METIS_TAC [IN_DIFF]
2030      THEN1 METIS_TAC [IN_DIFF]
2031      THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def]
2032      THEN FULL_SIMP_TAC (srw_ss()) [IN_DISJOINT, GSYM DISJOINT_DEF, SUBSET_DEF,
2033                                      upper_bounds_def]
2034      THEN SRW_TAC [] []
2035      THEN METIS_TAC [antisym_def],
2036      Q_TAC SUFF_TAC `(upper_bounds C r DIFF C = upper_bounds k r DIFF k)`
2037      THENL [
2038        FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, upper_bounds_def]
2039        THEN SRW_TAC [] []
2040        THEN1 METIS_TAC []
2041        THEN1 METIS_TAC []
2042        THEN FULL_SIMP_TAC (srw_ss()) [EXTENSION]
2043        THEN METIS_TAC [],
2044        SRW_TAC [] [EXTENSION]
2045        THEN EQ_TAC
2046        THEN SRW_TAC [] []
2047        THEN FULL_SIMP_TAC (srw_ss()) [transitive_def, reflexive_def,
2048                                      chain_def, SUBSET_DEF,
2049                                      upper_bounds_def, range_def]
2050        THEN METIS_TAC []
2051      ]
2052    ]
2053  ]
2054QED
2055
2056Theorem lemma9[local]:
2057  !r s.
2058     range r SUBSET s /\
2059     (range r <> {}) /\
2060     antisym r /\ reflexive r s /\ transitive r ==>
2061     upper_bounds (BIGUNION (fchains r)) r SUBSET maximal_elements s r
2062Proof
2063  SRW_TAC [] []
2064  THEN `BIGUNION (fchains r) IN fchains r` by METIS_TAC [lemma7]
2065  THEN Cases_on
2066       `upper_bounds (BIGUNION (fchains r)) r DIFF (BIGUNION (fchains r)) <> {}`
2067  THENL [
2068    `(CHOICE (upper_bounds (BIGUNION (fchains r)) r DIFF
2069     (BIGUNION (fchains r))) INSERT (BIGUNION (fchains r)) IN fchains r)`
2070      by METIS_TAC [lemma8]
2071    THEN METIS_TAC [MEMBER_NOT_EMPTY, CHOICE_DEF, IN_BIGUNION, IN_DIFF,
2072                    IN_INSERT],
2073    SIMP_TAC (srw_ss()) [SUBSET_DEF, maximal_elements_def]
2074    THEN Q.X_GEN_TAC `u`
2075    THEN STRIP_TAC
2076    THEN CONJ_TAC
2077    THENL [
2078      ALL_TAC,
2079      Q.X_GEN_TAC `e` THEN STRIP_TAC
2080    ]
2081    THEN `?k. k IN fchains r /\ u IN k`
2082      by METIS_TAC [IN_DIFF, MEMBER_NOT_EMPTY, IN_BIGUNION]
2083    THENL [
2084      FULL_SIMP_TAC (srw_ss()) [fchains_def, chain_def, range_def, SUBSET_DEF]
2085      THEN METIS_TAC [],
2086      `e IN upper_bounds (BIGUNION (fchains r)) r`
2087        by METIS_TAC [upper_bounds_lem]
2088      THEN `u IN (BIGUNION (fchains r)) /\ e IN (BIGUNION (fchains r))`
2089        by METIS_TAC [IN_BIGUNION, IN_DIFF, MEMBER_NOT_EMPTY]
2090      THEN FULL_SIMP_TAC (srw_ss()) [upper_bounds_def, antisym_def]
2091      THEN METIS_TAC []
2092    ]
2093  ]
2094QED
2095
2096Theorem zorns_lemma:
2097  !r s.
2098    (s <> {}) /\ partial_order r s /\
2099    (!t. chain t r ==> upper_bounds t r <> {}) ==>
2100    (?x. x IN maximal_elements s r)
2101Proof
2102  SRW_TAC [] [partial_order_def]
2103  THEN Q.EXISTS_TAC `CHOICE (upper_bounds (BIGUNION (fchains r)) r)`
2104  THEN SRW_TAC [] []
2105  THEN `range r <> {}`
2106    by (FULL_SIMP_TAC (srw_ss()) [range_def, reflexive_def,
2107                                  GSYM MEMBER_NOT_EMPTY]
2108        THEN METIS_TAC [])
2109  THEN METIS_TAC [SUBSET_DEF, lemma9, MEMBER_NOT_EMPTY, CHOICE_DEF, lemma4]
2110QED
2111
2112Theorem link_lemma[local]:
2113  !x y. (x,y) IN tc ((a,b) INSERT R) ==>
2114        transitive R ==>
2115        (x = a /\ (y = b \/ (b,y) IN R)) \/
2116        (y = b /\ (x,a) IN R) \/
2117        (x,a) IN R /\ (b,y) IN R \/
2118        (x,y) IN R
2119Proof
2120  ho_match_mp_tac tc_ind >> rpt strip_tac >>
2121  FULL_SIMP_TAC (srw_ss()) [tc_rules] >> rpt var_eq_tac>>
2122  METIS_TAC[transitive_def]
2123QED
2124
2125Theorem StrongOrder_extends_to_StrongLinearOrder:
2126  !R1: 'a -> 'a -> bool.
2127    StrongOrder R1 ==> ?R2. R1 RSUBSET R2 /\ StrongLinearOrder R2
2128Proof
2129  gen_tac >> strip_tac >>
2130  Q.ABBREV_TAC ‘r1 = rel_to_reln R1’ >>
2131  ‘transitive r1 /\ irreflexive r1 UNIV’
2132    by METIS_TAC[reln_rel_conv_thms, StrongOrder] >>
2133  Q.ABBREV_TAC‘s = { r | transitive r /\ irreflexive r UNIV /\ r1 SUBSET r }’ >>
2134  ‘r1 IN s’ by simp[Abbr‘s’] >>
2135  ‘s <> {}’ by METIS_TAC[MEMBER_NOT_EMPTY] >>
2136  Q.ABBREV_TAC ‘order = { (r1,r2) | r1 SUBSET r2 /\ r1 IN s /\ r2 IN s } ’ >>
2137  ‘partial_order order s’
2138    by (simp[partial_order_def, range_def, domain_def] >>
2139        ‘transitive order’
2140          by (simp[transitive_def, Abbr‘order’] >> METIS_TAC[SUBSET_TRANS]) >>
2141        ‘antisym order’
2142          by (simp[antisym_def, Abbr‘order’] >> METIS_TAC[SUBSET_ANTISYM]) >>
2143        ‘reflexive order s’ by simp[reflexive_def, Abbr‘order’] >>
2144        simp[SUBSET_DEF, PULL_EXISTS] >> simp[Abbr‘order’]) >>
2145  dxrule_then dxrule zorns_lemma >> impl_tac
2146  >- (simp[chain_def, upper_bounds_def, range_def, Abbr‘order’] >>
2147      Q.X_GEN_TAC ‘t’ >> strip_tac >>
2148      simp[EXTENSION, PULL_EXISTS] >> irule_at Any SUBSET_REFL >>
2149      Cases_on ‘t = {}’ >- (simp[] >> METIS_TAC[]) >>
2150      Q.EXISTS_TAC ‘BIGUNION t’ >> simp[] >>
2151      ‘BIGUNION t IN s’
2152        by (‘transitive (BIGUNION t) /\ irreflexive (BIGUNION t) UNIV /\
2153             r1 SUBSET BIGUNION t’ suffices_by simp[Abbr‘s’] >>
2154            ‘transitive (BIGUNION t)’
2155              by (simp[transitive_def] >> rpt strip_tac >>
2156                  Q.RENAME_TAC[‘(x,y) IN A’, ‘(y,z) IN B’, ‘A IN t’, ‘B IN t’]>>
2157                  ‘A IN s /\ B IN s’ by METIS_TAC[] >>
2158                  ‘transitive A /\ transitive B’
2159                    by FULL_SIMP_TAC (srw_ss())[Abbr‘s’] >>
2160                  wlogLib.wlog_tac ‘A SUBSET B’ [‘A’, ‘B’, ‘x’, ‘y’, ‘z’]
2161                  >- (‘B SUBSET A’ by METIS_TAC[] >> Q.EXISTS_TAC ‘A’ >>
2162                      METIS_TAC[transitive_def, SUBSET_DEF]) >>
2163                  METIS_TAC[transitive_def, SUBSET_DEF]) >> simp[] >>
2164            ‘irreflexive (BIGUNION t) UNIV’
2165              by (simp[irreflexive_def] >> rpt gen_tac >>
2166                  Q.RENAME_TAC [‘(x,x) IN A’, ‘A IN t’] >>
2167                  Cases_on ‘A IN t’ >> simp[] >>
2168                  ‘A IN s’ by METIS_TAC[] >>
2169                  pop_assum mp_tac >> simp[Abbr‘s’, irreflexive_def]) >>
2170            simp[] >>
2171            irule SUBSET_BIGUNION_SUBSET_I >>
2172            full_simp_tac (srw_ss())[GSYM MEMBER_NOT_EMPTY] >>
2173            first_assum $ irule_at Any >> first_x_assum $ drule_then drule >>
2174            simp[Abbr‘s’]) >>
2175      simp[] >> Q.X_GEN_TAC ‘A’ >> Cases_on ‘A IN t’ >> simp[] >>
2176      METIS_TAC[SUBSET_BIGUNION_I]) >>
2177  disch_then $ Q.X_CHOOSE_THEN ‘rmax’ mp_tac >>
2178  simp[maximal_elements_def, SF boolSimps.CONJ_ss] >> strip_tac >>
2179  Q.EXISTS_TAC ‘reln_to_rel rmax’ >> simp[GSYM reln_rel_conv_thms] >>
2180  ‘R1 RSUBSET reln_to_rel rmax’
2181    by (‘r1 SUBSET rmax’ by full_simp_tac (srw_ss())[Abbr‘s’] >>
2182        pop_assum mp_tac >>
2183        simp[reln_to_rel_def, RSUBSET, SUBSET_DEF, FORALL_PROD] >>
2184        rpt strip_tac >> first_x_assum irule >>
2185        simp[Abbr‘r1’, rel_to_reln_def])>>
2186  simp[strict_linear_order_def] >>
2187  ‘transitive rmax /\ irreflexive rmax UNIV’
2188    by full_simp_tac (srw_ss())[Abbr‘s’] >>
2189  full_simp_tac (srw_ss()) [irreflexive_def] >>
2190  MAP_EVERY Q.X_GEN_TAC [‘a’, ‘b’] >> strip_tac >> CCONTR_TAC >>
2191  full_simp_tac (srw_ss()) [] >>
2192  Q.ABBREV_TAC ‘rmax' = tc ((a,b) INSERT rmax)’ >>
2193  ‘rmax <> rmax' /\ rmax SUBSET rmax'’
2194    by (simp[EXTENSION, Abbr‘rmax'’] >> conj_tac
2195        >- (Q.EXISTS_TAC ‘(a,b)’ >> simp[tc_rules]) >>
2196        simp[SUBSET_DEF, tc_rules, FORALL_PROD]) >>
2197  full_simp_tac (srw_ss()) [Abbr‘order’] >>
2198  rev_full_simp_tac (srw_ss()) [SF boolSimps.CONJ_ss] >>
2199  ‘rmax' NOTIN s’ by METIS_TAC[] >>
2200  ‘transitive rmax'’ by simp[Abbr‘rmax'’, tc_transitive] >>
2201  ‘r1 SUBSET rmax’ by full_simp_tac (srw_ss())[Abbr‘s’] >>
2202  ‘r1 SUBSET rmax'’
2203    by (simp[Abbr‘rmax'’] >> METIS_TAC[tc_rules, SUBSET_DEF]) >>
2204  Q.UNDISCH_THEN ‘rmax' NOTIN s’ mp_tac >> simp[Abbr‘s’] >>
2205  simp[Abbr‘rmax'’] >> rpt strip_tac >>
2206  drule link_lemma >> simp[SF boolSimps.CONJ_ss] >> CCONTR_TAC >>
2207  full_simp_tac (srw_ss()) [] >>
2208  METIS_TAC[transitive_def]
2209QED
2210
2211
2212(* ------------------------------------------------------------------------ *)
2213(*  Equivalences                                                            *)
2214(* ------------------------------------------------------------------------ *)
2215
2216Definition per_def:
2217  per xs xss <=>
2218    (BIGUNION xss) SUBSET xs /\ {} NOTIN xss /\
2219    !xs1 xs2. xs1 IN xss /\ xs2 IN xss /\ xs1 <> xs2 ==> DISJOINT xs1 xs2
2220End
2221
2222Definition per_restrict_def:
2223  per_restrict xss xs = {xs' INTER xs | xs' IN xss} DELETE {}
2224End
2225
2226Theorem per_delete:
2227  !xs xss e.
2228    per xs xss ==>
2229    per (xs DELETE e) {es | es IN (IMAGE (\es. es DELETE e) xss) /\ es <> {}}
2230Proof
2231  SRW_TAC [] [per_def, SUBSET_DEF, RES_FORALL_THM]
2232  THENL [
2233    FULL_SIMP_TAC (srw_ss()) [IN_DELETE]
2234    THEN METIS_TAC [],
2235    FULL_SIMP_TAC (srw_ss()) [IN_DELETE]
2236    THEN METIS_TAC [],
2237    FULL_SIMP_TAC (srw_ss()) [EXTENSION, DISJOINT_DEF]
2238    THEN METIS_TAC []
2239  ]
2240QED
2241
2242Theorem per_restrict_per:
2243  !r s s'. per s r ==> per s' (per_restrict r s')
2244Proof
2245  SRW_TAC [] [per_def, per_restrict_def, RES_FORALL_THM, SUBSET_DEF,
2246              DISJOINT_DEF]
2247  THENL [
2248    FULL_SIMP_TAC (srw_ss()) [],
2249    FULL_SIMP_TAC (srw_ss()) [EXTENSION, SPECIFICATION]
2250    THEN METIS_TAC []
2251  ]
2252QED
2253
2254Theorem countable_per:
2255  !xs xss. countable xs /\ per xs xss ==> countable xss
2256Proof
2257  SRW_TAC [] [per_def, SUBSET_DEF, DISJOINT_DEF, EXTENSION]
2258  THEN MATCH_MP_TAC
2259         (METIS_PROVE [inj_countable]
2260             ``countable xs /\ INJ CHOICE xss xs ==> countable xss``)
2261  THEN SRW_TAC [] [INJ_DEF, EXTENSION]
2262  THEN METIS_TAC [CHOICE_DEF]
2263QED
2264
2265(* ------------------------------------------------------------------------ *)
2266(*  Misc                                                                    *)
2267(* ------------------------------------------------------------------------ *)
2268
2269Definition all_choices_def:
2270  all_choices xss =
2271    {IMAGE choice xss | choice | !xs. xs IN xss ==> choice xs IN xs}
2272End
2273
2274Theorem all_choices_thm:
2275  !x s y. x IN all_choices s /\ y IN x ==> ?z. z IN s /\ y IN z
2276Proof
2277  SRW_TAC [] [all_choices_def]
2278  THEN FULL_SIMP_TAC (srw_ss()) []
2279  THEN METIS_TAC [SPECIFICATION]
2280QED
2281
2282Definition num_order_def:
2283  num_order (f:'a -> num) s = {(x, y) | x IN s /\ y IN s /\ f x <= f y}
2284End
2285
2286Theorem linear_order_num_order:
2287  !f s t. INJ f s t ==> linear_order (num_order f s) s
2288Proof
2289  SRW_TAC [] [linear_order_def, transitive_def, antisym_def, num_order_def,
2290              domain_def, range_def, SUBSET_DEF, INJ_DEF]
2291  THEN1 DECIDE_TAC
2292  THEN1 METIS_TAC [EQ_LESS_EQ]
2293  THEN1 DECIDE_TAC
2294QED
2295
2296Theorem num_order_finite_prefix:
2297  !f s t. INJ f s t ==> finite_prefixes (num_order f s) s
2298Proof
2299  SRW_TAC [] [finite_prefixes_def, num_order_def]
2300  THEN `INJ f {e' | e' IN s /\ f e' <= f e} (count (SUC (f e)))`
2301    by (FULL_SIMP_TAC (srw_ss()) [count_def, INJ_DEF]
2302        THEN SRW_TAC [] []
2303        THEN DECIDE_TAC)
2304  THEN METIS_TAC [FINITE_INJ, FINITE_COUNT]
2305QED
2306
2307(* ------------------------------------------------------------------------ *)
2308(*  A big theorem that a partial order with finite prefixes over a countable*)
2309(*  set can be extended to a linear order with finite prefixes.             *)
2310(* ------------------------------------------------------------------------ *)
2311
2312Theorem po2lolem1[local]:
2313  !(f: num -> 'a option) (s : 'a set).
2314    (!n m. (f m = f n) /\ ~(f m = NONE) ==> (m = n)) /\
2315    (!x. x IN s ==> ?m. (f m = SOME x)) /\
2316    (!m x. (f m = SOME x) ==> x IN s) ==>
2317    linear_order
2318      {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s /\
2319    finite_prefixes
2320      {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s
2321Proof
2322  SRW_TAC [] []
2323  THEN IMP_RES_TAC nat_order_iso_thm
2324  THEN SRW_TAC [] [finite_prefixes_def]
2325QED
2326
2327Definition get_min_def:
2328  get_min r' (s, r) =
2329    let mins = minimal_elements (minimal_elements s r) r' in
2330      if SING mins then
2331        SOME (CHOICE mins)
2332      else
2333        NONE
2334End
2335
2336Definition nth_min_def:
2337  (nth_min r' (s, r) 0 = get_min r' (s, r)) /\
2338  (nth_min r' (s, r) (SUC n) =
2339    let min = get_min r' (s, r) in
2340      if min = NONE then
2341        NONE
2342      else
2343        nth_min r' (s DELETE (THE min), r) n)
2344End
2345
2346Theorem nth_min_surj_lem1[local]:
2347  !r' s' x s r.
2348    linear_order r' s /\
2349    finite_prefixes r' s /\
2350    partial_order r s /\
2351    x IN minimal_elements s' r /\
2352    s' SUBSET s ==>
2353    ?m. nth_min r' (s', r) m = SOME x
2354Proof
2355  rpt gen_tac
2356  THEN Induct_on `CARD {x' | x' IN s' /\ (x', x) IN r'}`
2357  THEN SRW_TAC [] []
2358  THEN `FINITE {x' | x' IN s' /\ (x', x) IN r'}`
2359    by (FULL_SIMP_TAC (srw_ss()) [finite_prefixes_def, minimal_elements_def,
2360                                  SUBSET_DEF, GSPEC_AND]
2361        THEN METIS_TAC [INTER_COMM, INTER_FINITE])
2362  THENL [
2363    Q.EXISTS_TAC `0`
2364    THEN SRW_TAC [] [nth_min_def, get_min_def]
2365    THEN `{x' | x' IN s' /\ (x', x) IN r'} = {}` by METIS_TAC [CARD_EQ_0]
2366    THEN FULL_SIMP_TAC (srw_ss()) []
2367    THEN `mins = {x}` suffices_by SRW_TAC [] []
2368    THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def]
2369    THEN Q.UNABBREV_TAC `mins`
2370    THEN FULL_SIMP_TAC (srw_ss()) [EXTENSION, linear_order_def, SUBSET_DEF]
2371    THEN METIS_TAC [],
2372    (* -- *)
2373    first_x_assum
2374      (Q.SPECL_THEN [‘s' DELETE THE (get_min r' (s',r))’, ‘x’, ‘r'’]
2375         strip_assume_tac)
2376    THEN `SING (minimal_elements (minimal_elements s' r) r')`
2377      by (MATCH_MP_TAC finite_prefix_linear_order_has_unique_minimal
2378          THEN Q.EXISTS_TAC `s`
2379          THEN SRW_TAC [] [SUBSET_DEF, minimal_elements_def]
2380          THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF])
2381    THEN FULL_SIMP_TAC (srw_ss()) [get_min_def, LET_THM]
2382    THEN FULL_SIMP_TAC (srw_ss()) [SING_DEF]
2383    THEN FULL_SIMP_TAC (srw_ss()) []
2384    THEN Q.RENAME_TAC [‘minimal_elements (minimal_elements _ _) _ = {X}’]
2385    THEN Cases_on `x = X`
2386    THENL [
2387      Q.EXISTS_TAC `0`
2388      THEN SRW_TAC [] [nth_min_def, get_min_def, LET_THM],
2389      `x IN s' /\ X IN s'`
2390        by (FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, EXTENSION]
2391            THEN METIS_TAC [])
2392      THEN `v = CARD ({x' | x' IN s' /\ (x',x) IN r'} DELETE X)`
2393        by (SRW_TAC [] []
2394            THEN1 DECIDE_TAC
2395            THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, EXTENSION,
2396                                           linear_order_def, SUBSET_DEF]
2397            THEN METIS_TAC [])
2398      THEN `{x' | x' IN s' /\ (x',x) IN r'} DELETE X =
2399            {x'' | (x'' IN s' /\ x'' <> X) /\ (x'',x) IN r'}`
2400        by (FULL_SIMP_TAC (srw_ss()) [EXTENSION, linear_order_def,
2401                                      domain_def, SUBSET_DEF]
2402            THEN METIS_TAC [])
2403      THEN FULL_SIMP_TAC (srw_ss()) []
2404      THEN `?m. nth_min r' (s' DELETE X, r) m = SOME x`
2405        by (Q.PAT_ASSUM `P ==> ?m. Q m` MATCH_MP_TAC
2406            THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def,
2407                                           rrestrict_def, SUBSET_DEF])
2408      THEN Q.EXISTS_TAC `SUC m`
2409      THEN SRW_TAC [] [nth_min_def]
2410      THEN Q.UNABBREV_TAC `min`
2411      THEN SRW_TAC [] []
2412      THEN Cases_on `get_min r' (s', r)`
2413      THEN FULL_SIMP_TAC (srw_ss()) [get_min_def, LET_THM, SING_DEF]
2414      THEN METIS_TAC [NOT_SOME_NONE, CHOICE_SING, SOME_11]
2415    ]
2416  ]
2417QED
2418
2419Theorem nth_min_surj_lem2[local]:
2420  !r' s r m m' x x'.
2421    nth_min r' (s, r) m = SOME x /\
2422    nth_min r' (s DIFF {x | ?n. n <= m /\ (nth_min r' (s, r) n = SOME x)}, r)
2423      m' = SOME x' ==>
2424    (nth_min r' (s, r) (SUC (m + m')) = SOME x')
2425Proof
2426  Induct_on `m`
2427  THEN SRW_TAC [] [nth_min_def, LET_THM]
2428  THEN SRW_TAC [] [DELETE_DEF]
2429  THEN FULL_SIMP_TAC (srw_ss()) [LET_THM]
2430  THEN REV_FULL_SIMP_TAC (srw_ss()) []
2431  THEN Q.RENAME_TAC [‘get_min R (s, r) <> NONE’,
2432                     ‘nth_min R (s DELETE _, _) m1 = SOME x1’,
2433                     ‘nth_min R _ (SUC m1 + m2) = SOME x2’]
2434  THEN Cases_on `get_min R (s, r)`
2435  THEN FULL_SIMP_TAC (srw_ss()) [DELETE_DEF]
2436  THEN SRW_TAC [] [arithmeticTheory.ADD]
2437  THEN first_assum irule
2438  THEN SRW_TAC [] []
2439  THEN Q.RENAME_TAC [‘get_min R _ = SOME x0’, ‘s DIFF {x0} DIFF _’]
2440  THEN ‘s DIFF {x0} DIFF
2441        {x | ?n. n <= m1 /\ (nth_min R (s DIFF {x0}, r) n = SOME x)} =
2442        s DIFF {x | ?n.  n <= SUC m1 /\ (nth_min R (s, r) n = SOME x)}’
2443    by (SRW_TAC [] [EXTENSION]
2444        THEN EQ_TAC
2445        THEN SRW_TAC [] []
2446        THENL [
2447           Cases_on `n`
2448           THEN SRW_TAC [] [nth_min_def, LET_THM]
2449           THEN1 REV_FULL_SIMP_TAC (srw_ss()) [nth_min_def]
2450           THEN Q.RENAME_TAC [‘SUC m1 <= N’]
2451           THEN first_x_assum (Q.SPEC_THEN ‘N’ mp_tac)
2452           THEN SRW_TAC [] []
2453           THEN Q.PAT_X_ASSUM ‘nth_min _ _ (SUC _) = SOME _’ mp_tac
2454           THEN ASM_SIMP_TAC (srw_ss()) [LET_THM, nth_min_def]
2455           THEN strip_tac
2456           THEN FULL_SIMP_TAC (srw_ss()) [DELETE_DEF]
2457           THEN DECIDE_TAC,
2458           DISCH_THEN SUBST_ALL_TAC
2459           THEN POP_ASSUM (Q.SPEC_THEN ‘0’ MP_TAC)
2460           THEN SRW_TAC [] [nth_min_def],
2461           Q.RENAME_TAC [‘~(N <= m1)’, ‘nth_min _ _ N = SOME _’]
2462           THEN first_x_assum (Q.SPEC_THEN ‘SUC N’ MP_TAC)
2463           THEN ASM_SIMP_TAC (srw_ss()) [nth_min_def, LET_THM, DELETE_DEF]
2464           THEN DECIDE_TAC
2465         ])
2466  THEN SRW_TAC [] []
2467QED
2468
2469Theorem nth_min_surj_lem3[local]:
2470  !r' s r s' x.
2471    linear_order r' s /\
2472    finite_prefixes r' s /\
2473    partial_order r s /\
2474    finite_prefixes r s /\
2475    s' SUBSET s /\
2476    x IN s' ==>
2477    ?m. nth_min r' (s', r) m = SOME x
2478Proof
2479  NTAC 5 STRIP_TAC
2480  THEN completeInduct_on `CARD {x' | x' IN s' /\ (x', x) IN r}`
2481  THEN SRW_TAC [] []
2482  THEN Cases_on `x IN minimal_elements s' r`
2483  THEN1 METIS_TAC [nth_min_surj_lem1]
2484  THEN `?x'. x' IN minimal_elements s' r /\ (x', x) IN r`
2485    by METIS_TAC [finite_prefix_po_has_minimal_path]
2486  THEN `?m. nth_min r' (s', r) m = SOME x'` by METIS_TAC [nth_min_surj_lem1]
2487  THEN Q.ABBREV_TAC
2488         `s'' = {x | ?n. n <= m /\ (nth_min r' (s', r) n = SOME x)}`
2489  THEN `{x''' | (x''' IN s' /\ x''' NOTIN s'') /\ (x''',x) IN r} PSUBSET
2490        {x' | x' IN s' /\ (x',x) IN r}`
2491    by (SRW_TAC [] [PSUBSET_DEF, SUBSET_DEF, EXTENSION]
2492        THEN Q.EXISTS_TAC `x'`
2493        THEN SRW_TAC [] []
2494        THEN Q.UNABBREV_TAC `s''`
2495        THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def]
2496        THEN METIS_TAC [LESS_EQ_REFL])
2497  THEN `FINITE {x' | x' IN s' /\ (x',x) IN r}`
2498    by (FULL_SIMP_TAC (srw_ss()) [finite_prefixes_def, SUBSET_DEF,
2499                                  minimal_elements_def, GSPEC_AND]
2500        THEN METIS_TAC [INTER_FINITE, INTER_COMM])
2501  THEN Cases_on `x IN s' DIFF s''`
2502  THENL [
2503    FULL_SIMP_TAC (srw_ss()) [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM]
2504    THEN `?m. nth_min r' (s' DIFF s'', r) m = SOME x`
2505      by (Q.PAT_ASSUM `!s''' x'' r''. P s''' x'' r''` MATCH_MP_TAC
2506          THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF]
2507          THEN METIS_TAC [CARD_PSUBSET])
2508    THEN Q.EXISTS_TAC `SUC (m + m')`
2509    THEN METIS_TAC [nth_min_surj_lem2],
2510    FULL_SIMP_TAC (srw_ss()) []
2511    THEN1 METIS_TAC []
2512    THEN Q.UNABBREV_TAC `s''`
2513    THEN FULL_SIMP_TAC (srw_ss()) []
2514    THEN METIS_TAC []
2515  ]
2516QED
2517
2518Theorem get_min_lem1[local]:
2519  !r' s r x. (get_min r' (s, r) = SOME x) ==> x IN s
2520Proof
2521  SRW_TAC [] [get_min_def, LET_THM, SING_DEF]
2522  THEN FULL_SIMP_TAC (srw_ss()) []
2523  THEN FULL_SIMP_TAC (srw_ss()) [EXTENSION, minimal_elements_def]
2524  THEN METIS_TAC []
2525QED
2526
2527Theorem nth_min_lem1[local]:
2528  !r' s r m x. (nth_min r' (s, r) m = SOME x) ==> x IN s
2529Proof
2530  Induct_on `m`
2531  THEN SRW_TAC [] [nth_min_def, LET_DEF]
2532  THEN1 METIS_TAC [get_min_lem1]
2533  THEN RES_TAC
2534  THEN FULL_SIMP_TAC (srw_ss()) []
2535QED
2536
2537Theorem nth_min_lem2[local]:
2538  !r' s r n m.
2539    nth_min r' (s, r) m <> NONE ==>
2540    nth_min r' (s, r) m <> nth_min r' (s, r) (SUC (m + n))
2541Proof
2542  Induct_on `m`
2543  THEN SRW_TAC [] [nth_min_def, LET_THM]
2544  THEN Cases_on `get_min r' (s, r)`
2545  THEN FULL_SIMP_TAC (srw_ss()) []
2546  THENL [
2547    CCONTR_TAC
2548    THEN FULL_SIMP_TAC (srw_ss()) []
2549    THEN `x IN s DELETE x` by METIS_TAC [nth_min_lem1]
2550    THEN FULL_SIMP_TAC (srw_ss()) [],
2551    `SUC m + n = SUC (m + n)` by DECIDE_TAC
2552    THEN METIS_TAC [NOT_IS_SOME_EQ_NONE]
2553  ]
2554QED
2555
2556Theorem nth_min_inj_lem[local]:
2557  !r' s r.
2558    (nth_min r' (s, r) m = nth_min r' (s, r) n) /\
2559    nth_min r' (s, r) m <> NONE ==>
2560    (m = n)
2561Proof
2562  STRIP_ASSUME_TAC (DECIDE ``m:num < n \/ n < m \/ (m = n)``)
2563  THEN SRW_TAC [] []
2564  THENL [
2565    `SUC (m + (n - m - 1)) = n` by DECIDE_TAC
2566    THEN METIS_TAC [nth_min_lem2],
2567    Cases_on `nth_min r' (s, r) n = NONE`
2568    THEN FULL_SIMP_TAC (srw_ss()) []
2569    THEN `SUC (n + (m - n - 1)) = m` by DECIDE_TAC
2570    THEN METIS_TAC [nth_min_lem2]
2571  ]
2572QED
2573
2574Theorem nth_min_subset_lem1[local]:
2575  !m n x y s r r'.
2576    m < n /\ x <> y /\
2577    (nth_min r' (s, r) n = SOME x) /\ (nth_min r' (s, r) m = SOME y) ==>
2578    (x, y) NOTIN r
2579Proof
2580  Induct
2581  THEN SRW_TAC [] [nth_min_def]
2582  THENL [
2583    IMP_RES_TAC get_min_lem1
2584    THEN IMP_RES_TAC nth_min_lem1
2585    THEN FULL_SIMP_TAC (srw_ss()) [get_min_def, LET_THM]
2586    THEN Cases_on `SING (minimal_elements (minimal_elements s r) r')`
2587    THEN FULL_SIMP_TAC (srw_ss()) [SING_DEF]
2588    THEN FULL_SIMP_TAC (srw_ss()) []
2589    THEN SRW_TAC [] []
2590    THEN FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, EXTENSION]
2591    THEN METIS_TAC [],
2592    FULL_SIMP_TAC (srw_ss()) [LET_THM]
2593    THEN Cases_on `get_min r' (s, r)`
2594    THEN FULL_SIMP_TAC (srw_ss()) []
2595    THEN Cases_on `n`
2596    THEN FULL_SIMP_TAC (srw_ss()) [nth_min_def, LET_THM]
2597    THEN RES_TAC
2598    THEN FULL_SIMP_TAC (srw_ss()) []
2599    THEN `(x, y) IN {(x, y) | P x y} <=> P x y` by SIMP_TAC (srw_ss()) []
2600    THEN FULL_SIMP_TAC (srw_ss()) []
2601    THEN IMP_RES_TAC nth_min_lem1
2602    THEN FULL_SIMP_TAC (srw_ss()) []
2603  ]
2604QED
2605
2606Theorem nth_min_subset_lem2[local]:
2607  !r' r s.
2608    linear_order {(x, y) | ?m n. m <= n /\ (nth_min r' (s, r) m = SOME x) /\
2609                                 (nth_min r' (s, r) n = SOME y)} s /\
2610    domain r SUBSET s /\
2611    range r SUBSET s ==>
2612    r SUBSET {(x, y) | ?m n. m <= n /\ (nth_min r' (s, r) m = SOME x) /\
2613                             (nth_min r' (s, r) n = SOME y)}
2614Proof
2615  SRW_TAC [] [SUBSET_DEF]
2616  THEN Cases_on `x`
2617  THEN SRW_TAC [] []
2618  THEN `?m n. m <= n /\ (((nth_min r' (s, r) m = SOME q) /\
2619                          (nth_min r' (s, r) n = SOME r'')) \/
2620                         ((nth_min r' (s, r) n = SOME q) /\
2621                          (nth_min r' (s, r) m = SOME r'')))`
2622    by (FULL_SIMP_TAC (srw_ss()) [linear_order_def, domain_def, range_def]
2623        THEN METIS_TAC [])
2624  THEN1 METIS_TAC []
2625  THEN Cases_on `m = n`
2626  THEN1 METIS_TAC []
2627  THEN `m < n` by DECIDE_TAC
2628  THEN `~(q = r'')`
2629    by (CCONTR_TAC
2630        THEN FULL_SIMP_TAC (srw_ss()) []
2631        THEN METIS_TAC [nth_min_inj_lem, NOT_SOME_NONE])
2632  THEN METIS_TAC [nth_min_subset_lem1]
2633QED
2634
2635Theorem linear_order_of_countable_po:
2636  !r s.
2637    countable s /\ partial_order r s /\ finite_prefixes r s ==>
2638    ?r'. linear_order r' s /\ finite_prefixes r' s /\ r SUBSET r'
2639Proof
2640  SRW_TAC [] [countable_def]
2641  THEN Q.ABBREV_TAC `f' = nth_min (num_order f s) (s, r)`
2642  THEN `!n m. (f' m = f' n) /\ f' m <> NONE ==> (m = n)`
2643    by METIS_TAC [nth_min_inj_lem]
2644  THEN `!x. x IN s ==> ?m. f' m = SOME x`
2645    by METIS_TAC [nth_min_surj_lem3, linear_order_num_order, SUBSET_REFL,
2646                  num_order_finite_prefix]
2647  THEN `!m x. (f' m = SOME x) ==> x IN s` by METIS_TAC [nth_min_lem1]
2648  THEN Q.EXISTS_TAC
2649         `{(x, y) | ?m n. m <= n /\ (f' m = SOME x) /\ (f' n = SOME y)}`
2650  THEN IMP_RES_TAC po2lolem1
2651  THEN SRW_TAC [] []
2652  THEN METIS_TAC [partial_order_def, nth_min_subset_lem2]
2653QED
2654
2655val _ = List.app Theory.delete_binding
2656  ["symmetric_closure_rules",
2657   "symmetric_closure_ind",
2658   "symmetric_closure_strongind",
2659   "symmetric_closure_cases",
2660   "transitive_closure_rules",
2661   "transitive_closure_ind",
2662   "transitive_closure_strongind",
2663   "transitive_closure_cases"];
2664