(*
use "set_relationScript.sml";
*)

open HolKernel boolLib bossLib pred_setTheory pairTheory arithmeticTheory;
open optionTheory;

val _ = new_theory "set_relation";

fun FSTAC thms = FULL_SIMP_TAC (srw_ss()) thms;
fun RWTAC thms = SRW_TAC [] thms;

val UNION_LEM = Q.prove (
`!P Q. { x | P x \/ Q x } = {x | P x} UNION {x | Q x}`,
RWTAC [EXTENSION]);

val INTER_LEM = Q.prove (
`!P Q. { x | P x /\ Q x } = {x | P x} INTER {x | Q x}`,
RWTAC [EXTENSION]);

(* ------------------------------------------------------------------------ *)
(*  Basic concepts                                                          *)
(* ------------------------------------------------------------------------ *)

val rextension = Q.store_thm ("rextension",
`!s t. (s = t) = !x y. (x,y) IN s = (x,y) IN t`,
RWTAC [] THEN
EQ_TAC THEN
RWTAC [EXTENSION] THEN
Cases_on `x` THEN
RWTAC []);

val domain_def = Define `
  domain r = {x | ?y. (x, y) IN r}`;

val range_def = Define `
  range r = {y | ?x. (x, y) IN r}`;

val rrestrict_def = Define `
  rrestrict r s = {(x, y) | (x, y) IN r /\ x IN s /\ y IN s}`;

val in_rrestrict = Q.store_thm ("in_rrestrict",
`!x y r s. (x, y) IN rrestrict r s = (x, y) IN r /\ x IN s /\ y IN s`,
RWTAC [rrestrict_def]);

val rrestrict_union = Q.store_thm ("rrestrict_union",
`!r1 r2 s. rrestrict (r1 UNION r2) s = (rrestrict r1 s) UNION (rrestrict r2 s)`,
RWTAC [rrestrict_def, EXTENSION] THEN
METIS_TAC []);

val rrestrict_rrestrict = Q.store_thm ("rrestrict_rrestrict",
`!r x y. rrestrict (rrestrict r x) y = rrestrict r (x INTER y)`,
RWTAC [rrestrict_def, EXTENSION] THEN 
EQ_TAC THEN
RWTAC []);

val rcomp_def = Define `
  rcomp r1 r2 = { (x, y) | ?z. (x, z) IN r1 /\ (z, y) IN r2}`;

val strict_def = Define `
  strict r = {(x, y) | (x, y) IN r /\ x <> y}`;

val strict_rrestrict = Q.store_thm ("strict_rrestrict",
`!r s. strict (rrestrict r s) = rrestrict (strict r) s`,
RWTAC [strict_def, rrestrict_def, EXTENSION] THEN
METIS_TAC []);

val univ_reln_def = Define `
  univ_reln xs = {(x1, x2) | x1 IN xs /\ x2 IN xs}`;

val finite_prefixes_def = Define `
  finite_prefixes r s = !e. e IN s ==> FINITE {e' | (e', e) IN r}`;

val finite_prefixes_subset = Q.store_thm ("finite_prefixes_subset",
`!r s s'. finite_prefixes r s /\ s' SUBSET s ==> finite_prefixes r s'`,
RWTAC [finite_prefixes_def, SUBSET_DEF]);

val finite_prefixes_subset = Q.store_thm ("finite_prefixes_subset",
`!r s s'. 
  finite_prefixes r s /\ s' SUBSET s 
  ==> 
  finite_prefixes r s' /\ finite_prefixes (rrestrict r s') s'`,
RWTAC [finite_prefixes_def, SUBSET_DEF, rrestrict_def, INTER_LEM] THEN
METIS_TAC [INTER_FINITE, INTER_COMM]);

val finite_prefixes_union = Q.store_thm ("finite_prefixes_union",
`!r1 r2 s1 s2.
  finite_prefixes r1 s1 /\ finite_prefixes r2 s2
  ==>
  finite_prefixes (r1 UNION r2) (s1 INTER s2)`,
RWTAC [finite_prefixes_def, UNION_LEM]);

val finite_prefixes_comp = Q.store_thm ("finite_prefixes_comp",
`!r1 r2 s1 s2.
  finite_prefixes r1 s1 /\ finite_prefixes r2 s2 /\
  { x | ?y. y IN s2 /\ (x, y) IN r2 } SUBSET s1
  ==>
  finite_prefixes (rcomp r1 r2) s2`,
RWTAC [finite_prefixes_def, SUBSET_DEF, rcomp_def] THEN
`{ e' | ?z. (e', z) IN r1 /\ (z, e) IN r2 } =
 BIGUNION (IMAGE (\z. { e' | (e', z) IN r1}) { z | (z, e) IN r2 })`
        by (RWTAC [EXTENSION] THEN
            EQ_TAC THEN
            RWTAC [] THENL
            [Q.EXISTS_TAC `{ x | (x, z) IN r1 }` THEN
                 RWTAC [] THEN
                 METIS_TAC [],
             METIS_TAC []]) THEN
RWTAC [] THEN
METIS_TAC []);

val finite_prefixes_inj_image = Q.store_thm ("finite_prefixes_inj_image",
`!f r s. 
  (!x y. (f x = f y) ==> (x = y)) /\
  finite_prefixes r s 
  ==> 
  finite_prefixes { (f x, f y) | (x, y) IN r } (IMAGE f s)`,
RWTAC [finite_prefixes_def] THEN
`{e' | ?x' y. ((e' = f x') /\ (f x = f y)) /\ (x',y) IN r}
 SUBSET
 IMAGE f { e' | (e', x) IN r }` 
        by (RWTAC [SUBSET_DEF] THEN
            METIS_TAC []) THEN
METIS_TAC [SUBSET_FINITE, IMAGE_FINITE]);

val finite_prefixes_range = Q.store_thm ("finite_prefixes_range",
`!r s t. finite_prefixes r s /\ DISJOINT t (range r) ==>
  finite_prefixes r (s UNION t)`,
RWTAC [finite_prefixes_def, DISJOINT_DEF, range_def, INTER_DEF, EXTENSION] THEN1
METIS_TAC [] THEN
`{e' | (e', e) IN r} = {}`
         by (RWTAC [EXTENSION] THEN
             METIS_TAC []) THEN
METIS_TAC [FINITE_EMPTY]);

(* ------------------------------------------------------------------------ *)
(* Transitive closure                                                       *)
(* ------------------------------------------------------------------------ *)

val (tc_rules, tc_ind, tc_cases) = Hol_reln `
(!x y. r (x, y) ==> tc r (x, y)) /\
(!x y. (?z. tc r (x, z) /\ tc r (z, y)) ==> tc r (x, y))`;

val tc_rules = Q.store_thm ("tc_rules",
`!r. 
  (!x y. (x,y) IN r ==> (x, y) IN tc r) /\
  (!x y. (?z. (x, z) IN tc r /\ (z, y) IN tc r) ==> (x, y) IN tc r)`,
RWTAC [SPECIFICATION, tc_rules]);

val tc_cases = Q.store_thm ("tc_cases",
`!r x y.
  (x, y) IN tc r =
  ((x, y) IN r) \/
  (?z. (x, z) IN tc r /\ (z, y) IN tc r)`,
RWTAC [SPECIFICATION] THEN
RWTAC [Once (Q.SPECL [`r`, `(x, y)`] tc_cases)]);

val tc_ind = Q.store_thm ("tc_ind",
`!r tc'.
  (!x y. (x, y) IN r ==> tc' x y) /\
  (!x y. (?z. tc' x z /\ tc' z y) ==> tc' x y) ==>
  !x y. (x, y) IN tc r ==> tc' x y`,
RWTAC [SPECIFICATION] THEN
IMP_RES_TAC (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM]
             (Q.SPECL [`r`, `\(x, y). tc' x y`] tc_ind)));

val tc_cases_lem = Q.prove (
`!x y. 
  (x, y) IN tc r 
  ==> 
  (x, y) IN r \/
  ((?z. (x, z) IN tc r /\ (z, y) IN r) /\
   (?z. (x, z) IN r /\ (z, y) IN tc r))`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
METIS_TAC [tc_rules]);

val tc_cases_right = Q.store_thm ("tc_cases_right",
`!r x y.
  (x, y) IN tc r =
  ((x, y) IN r) \/
  (?z. (x, z) IN tc r /\ (z, y) IN r)`,
METIS_TAC [tc_cases_lem, tc_rules]);

val tc_cases_left = Q.store_thm ("tc_cases_left",
`!r x y.
  (x, y) IN tc r =
  ((x, y) IN r) \/
  (?z. (x, z) IN r /\ (z, y) IN tc r)`,
METIS_TAC [tc_cases_lem, tc_rules]);

val tc_ind_left_lem = Q.prove (
`!r P.
  (!x y. (x, y) IN r ==> P x y) /\
  (!x y. (?z. (x, z) IN r /\ P z y) ==> P x y)
  ==>
  (!x y. (x, y) IN tc r ==> (!z. P x y /\ P y z ==> P x z) /\ P x y)`,
NTAC 3 STRIP_TAC THEN
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
METIS_TAC []);

val tc_ind_left = Q.store_thm ("tc_ind_left",
`!r tc'.
  (!x y. (x, y) IN r ==> tc' x y) /\
  (!x y. (?z. (x, z) IN r /\ tc' z y) ==> tc' x y)
  ==>
  (!x y. (x, y) IN tc r ==> tc' x y)`,
METIS_TAC [tc_ind_left_lem]);

val tc_ind_right_lem = Q.prove (
`!r P.
  (!x y. (x, y) IN r ==> P x y) /\
  (!x y. (?z. P x z /\ (z, y) IN r) ==> P x y)
  ==>
  (!x y. (x, y) IN tc r ==> (!z. P z x /\ P x y ==> P z y) /\ P x y)`,
NTAC 3 STRIP_TAC THEN
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
METIS_TAC []);

val tc_ind_right = Q.store_thm ("tc_ind_right",
`!r tc'.
  (!x y. (x, y) IN r ==> tc' x y) /\
  (!x y. (?z. tc' x z /\ (z, y) IN r) ==> tc' x y)
  ==>
  (!x y. (x, y) IN tc r ==> tc' x y)`,
METIS_TAC [tc_ind_right_lem]);

val tc_union = Q.store_thm ("tc_union",
`!x y. (x, y) IN tc r1 ==> !r2. (x, y) IN tc (r1 UNION r2)`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THENL
[RWTAC [Once tc_cases],
 METIS_TAC [tc_rules]]);

val tc_implication_lem = Q.prove (
`!x y. (x, y) IN tc r1 ==> !r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==> (x, y)
IN tc r2`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
METIS_TAC [tc_rules]);

val tc_implication = Q.store_thm ("tc_implication",
`!r1 r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==>
         (!x y. (x, y) IN tc r1 ==> (x, y) IN tc r2)`,
METIS_TAC [tc_implication_lem]);

val tc_empty = Q.prove (
`!x y. (x, y) IN tc {} ==> F`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC []);

val _ = save_thm ("tc_empty", SIMP_RULE (srw_ss()) [] tc_empty);

val tc_domain_range = Q.store_thm ("tc_domain_range",
`!x y. (x, y) IN tc r ==> x IN domain r /\ y IN range r`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [domain_def, range_def] THEN
METIS_TAC []);

val rrestrict_tc = Q.store_thm ("rrestrict_tc",
`!e e'. (e, e') IN tc (rrestrict r x) ==> (e, e') IN tc r`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [rrestrict_def] THEN
METIS_TAC [tc_rules]);

(* ------------------------------------------------------------------------ *)
(* Acyclic relations                                                        *)
(* ------------------------------------------------------------------------ *)

val acyclic_def = Define `
  acyclic r = !x. (x, x) NOTIN tc r`;

val acyclic_subset = Q.store_thm ("acyclic_subset",
`!r1 r2. acyclic r1 /\ r2 SUBSET r1 ==> acyclic r2`,
RWTAC [acyclic_def, SUBSET_DEF] THEN
METIS_TAC [tc_implication_lem]);

val acyclic_union = Q.store_thm ("acyclic_union",
`!r1 r2. acyclic (r1 UNION r2) ==> acyclic r1 /\ acyclic r2`,
RWTAC [acyclic_def] THEN
METIS_TAC [tc_union, UNION_COMM]);

val acyclic_rrestrict = Q.store_thm ("acyclic_rrestrict",
`!r s. acyclic r ==> acyclic (rrestrict r s)`,
RWTAC [rrestrict_def] THEN
`r = {(x,y) | (x,y) IN r /\ x IN s /\ y IN s} UNION r` 
         by RWTAC [UNION_DEF, rextension] THEN
METIS_TAC [acyclic_union]);

val acyclic_irreflexive = Q.store_thm ("acyclic_irreflexive",
`!r x. acyclic r ==> (x, x) NOTIN r`,
RWTAC [acyclic_def] THEN
METIS_TAC [tc_cases]);

val tc_BIGUNION_lem = Q.prove (
`!x y. (x, y) IN tc (BIGUNION rs) ==>
(!r r'. 
  r IN rs /\ r' IN rs /\ r <> r' 
  ==> 
  DISJOINT (domain r UNION range r) (domain r' UNION range r')) ==>
?r. r IN rs /\ (x, y) IN tc r`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN1
METIS_TAC [tc_rules] THEN
RES_TAC THEN
IMP_RES_TAC tc_domain_range THEN
FSTAC [DISJOINT_DEF, EXTENSION] THEN
`r = r'` by (RWTAC [EXTENSION] THEN METIS_TAC []) THEN
METIS_TAC [tc_rules]);

val acyclic_bigunion = Q.store_thm ("acyclic_bigunion",
`!rs.
  (!r r'. 
    r IN rs /\ r' IN rs /\ r <> r' 
    ==> 
    DISJOINT (domain r UNION range r) (domain r' UNION range r')) /\
  (!r. r IN rs ==> acyclic r)
  ==>
  acyclic (BIGUNION rs)`,
RWTAC [acyclic_def] THEN
CCONTR_TAC THEN
FSTAC [] THEN
IMP_RES_TAC tc_BIGUNION_lem THEN
FSTAC [] THEN
METIS_TAC []);

val acyclic_union = Q.store_thm ("acyclic_union",
`!r r'. 
  DISJOINT (domain r UNION range r) (domain r' UNION range r') /\
  acyclic r /\
  acyclic r'
  ==>
  acyclic (r UNION r')`,
RWTAC [] THEN
MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.SPEC `{r; r'}` acyclic_bigunion)) THEN
RWTAC [] THEN
METIS_TAC [DISJOINT_SYM]);

(* ------------------------------------------------------------------------ *)
(* Minimal and maximal elements                                             *)
(* ------------------------------------------------------------------------ *)

val maximal_elements_def = Define `
  maximal_elements xs r = 
    {x | x IN xs /\ !x'. x' IN xs /\ (x, x') IN r ==> (x = x')}`;

val minimal_elements_def = Define `
  minimal_elements xs r = 
    {x | x IN xs /\ !x'. x' IN xs /\ (x', x) IN r ==> (x = x')}`;

val maximal_union = Q.store_thm ("maximal_union",
`!e s r1 r2.
  e IN maximal_elements s (r1 UNION r2) 
  ==>
  e IN maximal_elements s r1 /\
  e IN maximal_elements s r2`,
RWTAC [maximal_elements_def]);

val minimal_union = Q.store_thm ("minimal_union",
`!e s r1 r2.
  e IN minimal_elements s (r1 UNION r2) 
  ==>
  e IN minimal_elements s r1 /\
  e IN minimal_elements s r2`,
RWTAC [minimal_elements_def]);

val tc_path_max_lem = Q.prove (
`!s. FINITE s ==> 
     s <> {} ==> !r. acyclic r ==> ?x. x IN maximal_elements s (tc r)`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
RWTAC [] THEN
Cases_on `s={}` THEN1
RWTAC [maximal_elements_def] THEN
RES_TAC THEN
Cases_on `(x, e) IN (tc r)` THENL
[Q.EXISTS_TAC `e` THEN
     RWTAC [maximal_elements_def] THEN
     `(x, x'') IN (tc r)` by METIS_TAC [tc_rules] THEN
     FSTAC [acyclic_def, maximal_elements_def] THEN
     METIS_TAC [],
 FSTAC [maximal_elements_def] THEN
     METIS_TAC []]);

val tc_path_min_lem = Q.prove (
`!s. FINITE s ==> 
     s <> {} ==> !r. acyclic r ==> ?x. x IN minimal_elements s (tc r)`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
RWTAC [] THEN
Cases_on `s={}` THEN1
RWTAC [minimal_elements_def] THEN
RES_TAC THEN
Cases_on `(e, x) IN (tc r)` THENL
[Q.EXISTS_TAC `e` THEN
     RWTAC [minimal_elements_def] THEN
     `(x'', x) IN (tc r)` by METIS_TAC [tc_rules] THEN
     FSTAC [acyclic_def, minimal_elements_def] THEN
     METIS_TAC [],
 FSTAC [minimal_elements_def] THEN
     METIS_TAC []]);

val finite_acyclic_has_maximal = Q.store_thm ("finite_acyclic_has_maximal",
`!s. FINITE s ==> s <> {} ==> !r. acyclic r ==> ?x. x IN maximal_elements s r`,
RWTAC [] THEN
IMP_RES_TAC tc_path_max_lem THEN
FSTAC [maximal_elements_def] THEN
METIS_TAC [tc_rules]);

val finite_acyclic_has_minimal = Q.store_thm ("finite_acyclic_has_minimal",
`!s. FINITE s ==> s <> {} ==> !r. acyclic r ==> ?x. x IN minimal_elements s r`,
RWTAC [] THEN
IMP_RES_TAC tc_path_min_lem THEN
FSTAC [minimal_elements_def] THEN
METIS_TAC [tc_rules]);

val lem1 = Q.prove (
`!x y. (x, y) IN tc r ==> ?z. (x, z) IN r /\ (x <> y ==> x <> z)`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
METIS_TAC []);

val maximal_tc = Q.store_thm ("maximal_TC",
`!s r.
  domain r SUBSET s /\ range r SUBSET s
  ==>
  (maximal_elements s (tc r) = maximal_elements s r)`,
RWTAC [EXTENSION, maximal_elements_def, domain_def, range_def, 
            SUBSET_DEF] THEN
EQ_TAC THEN
RWTAC [] THEN
METIS_TAC [lem1, tc_rules]);

val lem1 = Q.prove (
`!y x. (y, x) IN tc r ==> ?z. (z, x) IN r /\ (x <> y ==> x <> z)`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
METIS_TAC []);

val minimal_tc = Q.store_thm ("minimal_TC",
`!s r.
  domain r SUBSET s /\ range r SUBSET s
  ==>
  (minimal_elements s (tc r) = minimal_elements s r)`,
RWTAC [EXTENSION, minimal_elements_def, domain_def, range_def, 
            SUBSET_DEF] THEN
EQ_TAC THEN
RWTAC [] THEN
METIS_TAC [lem1, tc_rules]);

val tc_path_max_lem2 = Q.prove (
`!s. 
  FINITE s 
  ==> 
  !r x. 
    acyclic r /\ 
    x IN s /\
    x NOTIN maximal_elements s (tc r)
    ==>
    ?y. y IN maximal_elements s (tc r) /\ (x, y) IN tc r`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
RWTAC [] THEN
Cases_on `s={}` THENL
[FSTAC [maximal_elements_def],
 `?e'. (e, e') IN tc r /\ e' IN s` 
          by (FSTAC [maximal_elements_def] THEN
              METIS_TAC [tc_rules]) THEN
     Cases_on `e' IN maximal_elements s (tc r)` THENL
     [Q.EXISTS_TAC `e'` THEN
          RWTAC [] THEN
          FSTAC [maximal_elements_def, acyclic_def] THEN
          RWTAC [] THEN
          METIS_TAC [tc_rules],
      `?y. y IN maximal_elements s (tc r) /\ (e', y) IN tc r` by METIS_TAC [] THEN
          Q.EXISTS_TAC `y` THEN
          RWTAC [] THENL
          [FSTAC [maximal_elements_def, acyclic_def] THEN
               RWTAC [] THEN
               METIS_TAC [tc_rules],
           METIS_TAC [tc_rules]]],
 FSTAC [maximal_elements_def],
 Cases_on `x NOTIN maximal_elements s (tc r)` THENL
     [`?y. y IN maximal_elements s (tc r) /\ (x, y) IN tc r` by METIS_TAC [] THEN
          FSTAC [maximal_elements_def, acyclic_def] THEN
          METIS_TAC [tc_rules],
      Cases_on `(x, e) IN tc r` THENL
          [Q.EXISTS_TAC `e`,
           Q.EXISTS_TAC `x`] THEN
          FSTAC [maximal_elements_def, acyclic_def] THEN
          METIS_TAC [tc_rules]]]);

val tc_path_min_lem2 = Q.prove (
`!s. 
  FINITE s 
  ==> 
  !r x. 
    acyclic r /\ 
    x IN s /\
    x NOTIN minimal_elements s (tc r)
    ==>
    ?y. y IN minimal_elements s (tc r) /\ (y, x) IN tc r`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
RWTAC [] THEN
Cases_on `s={}` THENL
[FSTAC [minimal_elements_def],
 `?e'. (e', e) IN tc r /\ e' IN s` 
          by (FSTAC [minimal_elements_def] THEN
              METIS_TAC [tc_rules]) THEN
     Cases_on `e' IN minimal_elements s (tc r)` THENL
     [Q.EXISTS_TAC `e'` THEN
          RWTAC [] THEN
          FSTAC [minimal_elements_def, acyclic_def] THEN
          RWTAC [] THEN
          METIS_TAC [tc_rules],
      `?y. y IN minimal_elements s (tc r) /\ (y, e') IN tc r` by METIS_TAC [] THEN
          Q.EXISTS_TAC `y` THEN
          RWTAC [] THENL
          [FSTAC [minimal_elements_def, acyclic_def] THEN
               RWTAC [] THEN
               METIS_TAC [tc_rules],
           METIS_TAC [tc_rules]]],
 FSTAC [minimal_elements_def],
 Cases_on `x NOTIN minimal_elements s (tc r)` THENL
     [`?y. y IN minimal_elements s (tc r) /\ (y, x) IN tc r` by METIS_TAC [] THEN
          FSTAC [minimal_elements_def, acyclic_def] THEN
          METIS_TAC [tc_rules],
      Cases_on `(e, x) IN tc r` THENL
          [Q.EXISTS_TAC `e`,
           Q.EXISTS_TAC `x`] THEN
          FSTAC [minimal_elements_def, acyclic_def] THEN
          METIS_TAC [tc_rules]]]);

val finite_acyclic_has_maximal_path = Q.store_thm ("finite_acyclic_has_maximal_path",
`!s r x. 
  FINITE s /\
  acyclic r /\ 
  x IN s /\
  x NOTIN maximal_elements s r
  ==>
  ?y. y IN maximal_elements s r /\ (x, y) IN tc r`,
RWTAC [] THEN
IMP_RES_TAC tc_path_max_lem2 THEN
FSTAC [maximal_elements_def] THEN
METIS_TAC [tc_rules]);

val finite_acyclic_has_minimal_path = Q.store_thm ("finite_acyclic_has_minimal_path",
`!s r x. 
  FINITE s /\
  acyclic r /\ 
  x IN s /\
  x NOTIN minimal_elements s r
  ==>
  ?y. y IN minimal_elements s r /\ (y, x) IN tc r`,
RWTAC [] THEN
IMP_RES_TAC tc_path_min_lem2 THEN
FSTAC [minimal_elements_def] THEN
METIS_TAC [tc_rules]);

(* ------------------------------------------------------------------------ *)
(*  Orders                                                                  *)
(* ------------------------------------------------------------------------ *)

val reflexive_def = Define `
  reflexive r s = !x. x IN s ==> (x, x) IN r`;

val transitive_def = Define `
  transitive r = 
    !x y z.  (x, y) IN r /\ (y, z) IN r ==> (x, z) IN r`;

val transitive_tc_lem = Q.prove (
`!x y. (x, y) IN tc r ==> transitive r ==> (x, y) IN r`,
HO_MATCH_MP_TAC tc_ind THEN
RWTAC [] THEN
RES_TAC THEN
FSTAC [transitive_def] THEN
METIS_TAC []);

val transitive_tc = Q.store_thm ("transitive_tc",
`!r. transitive r ==> (tc r = r)`,
RWTAC [EXTENSION] THEN
EQ_TAC THEN
RWTAC [] THEN
Cases_on `x` THEN1
METIS_TAC [transitive_tc_lem] THEN
FSTAC [transitive_def] THEN
METIS_TAC [tc_rules]);

val tc_transitive = Q.store_thm ("tc_transitive",
`!r. transitive (tc r)`,
RWTAC [transitive_def] THEN
METIS_TAC [tc_rules]);

val antisym_def = Define `
  antisym r = !x y. (x, y) IN r /\ (y, x) IN r ==> (x = y)`;

val partial_order_def = Define `
  partial_order r s = 
       domain r SUBSET s /\ range r SUBSET s /\
       transitive r /\ reflexive r s /\ antisym r`; 

val partial_order_subset = Q.store_thm ("partial_order_subset",
`!r s s'. 
  partial_order r s /\ s' SUBSET s ==> partial_order (rrestrict r s') s'`,
RWTAC [partial_order_def, SUBSET_DEF, reflexive_def, transitive_def, 
       antisym_def, domain_def, range_def, rrestrict_def] THEN
METIS_TAC []);

val strict_partial_order = Q.store_thm ("strict_partial_order",
`!r s. 
  partial_order r s 
  ==> 
  domain (strict r) SUBSET s /\ range (strict r) SUBSET s /\
  transitive (strict r) /\ antisym (strict r)`,
RWTAC [domain_def, SUBSET_DEF, range_def, partial_order_def, strict_def] THENL
[METIS_TAC [],
 METIS_TAC [],
 FSTAC [transitive_def, strict_def, antisym_def] THEN
     METIS_TAC [],
 FSTAC [antisym_def] THEN
     METIS_TAC []]);

val strict_partial_order_acyclic = Q.store_thm ("strict_partial_order_acyclic",
`!r s. partial_order r s ==> acyclic (strict r)`,
RWTAC [acyclic_def] THEN
IMP_RES_TAC strict_partial_order THEN
RWTAC [transitive_tc, strict_def]);

val finite_prefix_po_has_minimal_path = Q.store_thm ("finite_prefix_po_has_minimal_path",
`!r s x s'.
  partial_order r s /\ 
  finite_prefixes r s /\ 
  x NOTIN minimal_elements s' r /\
  x IN s' /\
  s' SUBSET s
  ==>
  ?x'. x' IN minimal_elements s' r /\ (x', x) IN r`,
RWTAC [finite_prefixes_def] THEN
IMP_RES_TAC strict_partial_order_acyclic THEN
`?x'. x' IN minimal_elements (s' INTER {x' | (x', x) IN r})
                             (strict r) /\ 
      (x', x) IN tc (strict r)` by
          (MATCH_MP_TAC finite_acyclic_has_minimal_path THEN
           RWTAC [] THEN
           FSTAC [minimal_elements_def, strict_def, SUBSET_DEF,
                  partial_order_def, reflexive_def] THEN
           METIS_TAC [INTER_FINITE, INTER_COMM]) THEN
Q.EXISTS_TAC `x'` THEN
RWTAC [] THEN
FSTAC [minimal_elements_def] THEN
RWTAC [] THEN
FSTAC [partial_order_def, domain_def, SUBSET_DEF,
       transitive_def, strict_def] THEN
METIS_TAC []);

val linear_order_def = Define `
  linear_order r s = 
    domain r SUBSET s /\ range r SUBSET s /\
    transitive r /\ antisym r /\
    (!x y. x IN s /\ y IN s ==> (x, y) IN r \/ (y, x) IN r)`; 

val linear_order_subset = Q.store_thm ("linear_order_subset",
`!r s s'. 
  linear_order r s /\ s' SUBSET s ==> linear_order (rrestrict r s') s'`,
RWTAC [linear_order_def, SUBSET_DEF, transitive_def, 
       antisym_def, domain_def, range_def, rrestrict_def] THEN
METIS_TAC []);

val partial_order_linear_order = Q.store_thm ("partial_order_linear_order",
`!r s. linear_order r s ==> partial_order r s`,
RWTAC [linear_order_def, partial_order_def, reflexive_def] THEN
METIS_TAC []);

val strict_linear_order_def = Define `
  strict_linear_order r s = 
    domain r SUBSET s /\ range r SUBSET s /\
    transitive r /\
    (!x. (x, x) NOTIN r) /\
    (!x y. x IN s /\ y IN s /\ x <> y ==> (x, y) IN r \/ (y, x) IN r)`; 

val strict_linear_order_dom_rng = Q.store_thm ("strict_linear_order_dom_rng",
`!r s x y. (x, y) IN r /\ strict_linear_order r s ==> x IN s /\ y IN s`,
RWTAC [strict_linear_order_def, domain_def, range_def, SUBSET_DEF] THEN
METIS_TAC []);

val linear_order_dom_rng = Q.store_thm ("linear_order_dom_rng",
`!r s x y. (x, y) IN r /\ linear_order r s ==> x IN s /\ y IN s`,
RWTAC [linear_order_def, domain_def, range_def, SUBSET_DEF] THEN
METIS_TAC []);

val empty_strict_linear_order = Q.store_thm ("empty_strict_linear_order",
`!r. strict_linear_order r {} = (r = {})`,
RWTAC [strict_linear_order_def, RES_FORALL_THM, domain_def, range_def, 
            transitive_def, EXTENSION] THEN
EQ_TAC THEN
RWTAC [] THEN
Cases_on `x` THEN
RWTAC []);

val empty_linear_order = Q.store_thm ("empty_linear_order",
`!r. linear_order r {} = (r = {})`,
RWTAC [linear_order_def, RES_FORALL_THM, domain_def, range_def, 
            transitive_def, antisym_def, EXTENSION] THEN
EQ_TAC THEN
RWTAC [] THEN
Cases_on `x` THEN
RWTAC []);

val linear_order_restrict = Q.store_thm ("linear_order_restrict",
`!s r s'. linear_order r s ==> linear_order (rrestrict r s') (s INTER s')`,
RWTAC [linear_order_def, rrestrict_def, domain_def, range_def,
            SUBSET_DEF, transitive_def, antisym_def] THEN
METIS_TAC []);

val strict_linear_order_restrict = Q.store_thm ("strict_linear_order_restrict",
`!s r s'.
  strict_linear_order r s 
  ==> 
  strict_linear_order (rrestrict r s') (s INTER s')`,
RWTAC [strict_linear_order_def, rrestrict_def, domain_def, range_def,
            transitive_def, SUBSET_DEF] THEN
METIS_TAC []);

val extend_linear_order = Q.store_thm ("extend_linear_order",
`!r s x.
  x NOTIN s /\
  linear_order r s 
  ==>
  linear_order (r UNION {(y, x) | y | y IN (s UNION {x})}) (s UNION {x})`,
RWTAC [linear_order_def, domain_def, range_def, 
            transitive_def, antisym_def, SUBSET_DEF] THEN
METIS_TAC []);

val strict_linear_order_acyclic = Q.store_thm ("strict_linear_order_acyclic",
`!r s. strict_linear_order r s ==> acyclic r`,
RWTAC [acyclic_def, strict_linear_order_def] THEN
IMP_RES_TAC transitive_tc THEN
FSTAC [strict_linear_order_def, transitive_def]);

val strict_linear_order_union_acyclic = Q.store_thm ("strict_linear_order_union_acyclic",
`!r1 r2 s. 
  strict_linear_order r1 s /\
  ((domain r2) UNION (range r2)) SUBSET s
  ==> 
  (acyclic (r1 UNION r2) = r2 SUBSET r1)`,
RWTAC [] THEN
EQ_TAC THEN
RWTAC [] THENL
[FSTAC [strict_linear_order_def, domain_def,
                           transitive_def, range_def, SUBSET_DEF] THEN
     Cases_on `x` THEN
     IMP_RES_TAC acyclic_irreflexive THEN
     CCONTR_TAC THEN
     FSTAC [] THEN
     METIS_TAC [acyclic_def, tc_rules, IN_UNION],
 `r1 UNION r2 = r1` 
        by (FSTAC [domain_def, range_def, SUBSET_DEF, 
                                      EXTENSION] THEN 
            METIS_TAC []) THEN
     RWTAC [] THEN
     METIS_TAC [strict_linear_order_acyclic]]);

val strict_linear_order = Q.store_thm ("strict_linear_order",
`!r s. linear_order r s ==> strict_linear_order (strict r) s`,
RWTAC [linear_order_def, strict_linear_order_def, strict_def, 
            domain_def, range_def, SUBSET_DEF, transitive_def, antisym_def] THEN
METIS_TAC []);

val linear_order = Q.store_thm ("linear_order",
`!r s. strict_linear_order r s ==> linear_order (r UNION {(x, x) | x IN s}) s`,
RWTAC [linear_order_def, strict_linear_order_def, transitive_def,
            antisym_def, domain_def, range_def, SUBSET_DEF] THEN
METIS_TAC []);

val finite_strict_linear_order_has_maximal = Q.store_thm ("finite_strict_linear_order_has_maximal",
`!s r. 
  FINITE s /\ strict_linear_order r s /\ s <> {} 
  ==> 
  ?x. x IN maximal_elements s r`,
METIS_TAC [strict_linear_order_acyclic, finite_acyclic_has_maximal]);

val finite_strict_linear_order_has_minimal = Q.store_thm ("finite_strict_linear_order_has_minimal",
`!s r. 
  FINITE s /\ strict_linear_order r s /\ s <> {} 
  ==> 
  ?x. x IN minimal_elements s r`,
METIS_TAC [strict_linear_order_acyclic, finite_acyclic_has_minimal]);

val finite_linear_order_has_maximal = Q.store_thm ("finite_linear_order_has_maximal",
`!s r. FINITE s /\ linear_order r s /\ s <> {} ==> ?x. x IN maximal_elements s r`,
RWTAC [] THEN
IMP_RES_TAC strict_linear_order THEN
IMP_RES_TAC finite_strict_linear_order_has_maximal THEN
Q.EXISTS_TAC `x` THEN
FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, strict_def] THEN
METIS_TAC []);

val finite_linear_order_has_minimal = Q.store_thm ("finite_linear_order_has_minimal",
`!s r. FINITE s /\ linear_order r s /\ s <> {} ==> ?x. x IN minimal_elements s r`,
RWTAC [] THEN
IMP_RES_TAC strict_linear_order THEN
IMP_RES_TAC finite_strict_linear_order_has_minimal THEN
Q.EXISTS_TAC `x` THEN
FSTAC [minimal_elements_def, strict_def] THEN
METIS_TAC []);

val maximal_linear_order = Q.store_thm ("maximal_linear_order",
`!s r x y. y IN s /\ linear_order r s /\ x IN maximal_elements s r ==> (y, x) IN r`,
RWTAC [linear_order_def, maximal_elements_def] THEN
METIS_TAC []);

val minimal_linear_order = Q.store_thm ("minimal_linear_order",
`!s r x y. y IN s /\ linear_order r s /\ x IN minimal_elements s r ==> (x, y) IN r`,
RWTAC [linear_order_def, minimal_elements_def] THEN
METIS_TAC []);

val minimal_linear_order_unique = Q.store_thm ("minimal_linear_order_unique",
`!r s s' x y.
  linear_order r s /\
  x IN minimal_elements s' r /\
  y IN minimal_elements s' r /\
  s' SUBSET s
  ==>
  (x = y)`,
RWTAC [minimal_elements_def, linear_order_def, antisym_def, SUBSET_DEF] THEN
METIS_TAC []);

val finite_prefix_linear_order_has_unique_minimal = Q.store_thm ("finite_prefix_linear_order_has_unique_minimal",
`!r s s'.
  linear_order r s /\
  finite_prefixes r s /\
  x IN s' /\ 
  s' SUBSET s
  ==> 
  SING (minimal_elements s' r)`,
RWTAC [SING_DEF] THEN
Cases_on `?y. y IN minimal_elements s' r` THEN1
METIS_TAC [UNIQUE_MEMBER_SING, minimal_linear_order_unique] THEN
METIS_TAC [partial_order_linear_order, finite_prefix_po_has_minimal_path]);

val nat_order_iso_thm = Q.store_thm ("nat_order_iso_thm",
`!(f: num -> 'a option) (s : 'a set). 
  (!n m. (f m = f n) /\ f m <> NONE ==> (m = n)) /\
  (!x. x IN s ==> ?m. (f m = SOME x)) /\
  (!m x. (f m = SOME x) ==> x IN s)
  ==>
  linear_order {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s /\
  finite_prefixes {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s`,
RWTAC [linear_order_def, domain_def, range_def, SUBSET_DEF,
            transitive_def, antisym_def, finite_prefixes_def] THENL
[METIS_TAC [],
 METIS_TAC [],
 METIS_TAC [LESS_EQ_TRANS, SOME_11, NOT_SOME_NONE],
 METIS_TAC [LESS_EQUAL_ANTISYM, SOME_11, NOT_SOME_NONE],
 METIS_TAC [NOT_LESS_EQUAL, LESS_IMP_LESS_OR_EQ],
 `?n. SOME e = f n` by METIS_TAC [] THEN
     RWTAC [] THEN
     `{SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} SUBSET
      IMAGE f (count (SUC n))`
             by (RWTAC [SUBSET_DEF, count_def,
                             DECIDE ``!x:num y. x < SUC y = x <= y``] THEN
                 METIS_TAC [NOT_SOME_NONE]) THEN
     `{x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} =
      IMAGE THE {SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)}`
             by (RWTAC [EXTENSION] THEN
                 METIS_TAC [THE_DEF]) THEN
     METIS_TAC [IMAGE_FINITE, SUBSET_FINITE, FINITE_COUNT]]);

(* ------------------------------------------------------------------------ *)
(*  Equivalences                                                            *)
(* ------------------------------------------------------------------------ *)

val per_def = Define `
  per xs xss =
    (BIGUNION xss) SUBSET xs /\ {} NOTIN xss /\ 
    !xs1 xs2. xs1 IN xss /\ xs2 IN xss /\ xs1 <> xs2 ==> DISJOINT xs1 xs2`;

val per_restrict_def = Define `
  per_restrict xss xs = {xs' INTER xs | xs' IN xss} DELETE {}`;

val per_delete = Q.store_thm ("per_delete",
`!xs xss e. per xs xss ==> 
            per (xs DELETE e) 
                {es | es IN (IMAGE (\es. es DELETE e) xss) /\ es <> {}}`,
RWTAC [per_def, SUBSET_DEF, RES_FORALL_THM] THENL
[FSTAC [IN_DELETE] THEN
     METIS_TAC [],
 FSTAC [IN_DELETE] THEN
     METIS_TAC [],
 FSTAC [EXTENSION, DISJOINT_DEF] THEN
     METIS_TAC []]);

val per_restrict_per = Q.store_thm ("per_restrict_per",
`!r s s'. per s r ==> per s' (per_restrict r s')`,
RWTAC [per_def, per_restrict_def, RES_FORALL_THM, SUBSET_DEF, DISJOINT_DEF] THENL
[FSTAC [],
 FSTAC [EXTENSION, SPECIFICATION] THEN
     METIS_TAC []]); 


(* ------------------------------------------------------------------------ *)
(*  Misc                                                                    *)
(* ------------------------------------------------------------------------ *)

val all_choices_def = Define `
  all_choices xss = 
    {IMAGE choice xss | choice | !xs. xs IN xss ==> choice xs IN xs}`;

val all_choices_thm = Q.store_thm ("all_choices_thm",
`!x s y. x IN all_choices s /\ y IN x ==> ?z. z IN s /\ y IN z`,
RWTAC [all_choices_def] THEN 
FSTAC [] THEN
METIS_TAC [SPECIFICATION]);


val num_order_def = Define `
  num_order (f:'a -> num) s = {(x, y) | x IN s /\ y IN s /\ f x <= f y}`;

val linear_order_num_order = Q.store_thm ("linear_order_num_order",
`!f s t. INJ f s t ==> linear_order (num_order f s) s`,
RWTAC [linear_order_def, transitive_def, antisym_def, num_order_def,
       domain_def, range_def, SUBSET_DEF, INJ_DEF] THEN1
DECIDE_TAC THEN1
METIS_TAC [EQ_LESS_EQ] THEN1
DECIDE_TAC);

val num_order_finite_prefix = Q.store_thm ("num_order_finite_prefix",
`!f s t. INJ f s t ==> finite_prefixes (num_order f s) s`,
RWTAC [finite_prefixes_def, num_order_def] THEN
`INJ f {e' | e' IN s /\ f e' <= f e} (count (SUC (f e)))`
           by (FSTAC [count_def, INJ_DEF] THEN
               RWTAC [] THEN
               DECIDE_TAC) THEN
METIS_TAC [FINITE_INJ, FINITE_COUNT]);

(* ------------------------------------------------------------------------ *)
(*  A big theorem that a partial order with finite prefixes over a countable*)
(*  set can be extended to a linear order with finite prefixes.             *)
(* ------------------------------------------------------------------------ *)

val po2lolem01= Q.prove (
`!(f: num -> 'a option) (s : 'a set). 
  (!n m. (f m = f n) /\ ~(f m = NONE) ==> (m = n)) /\
  (!x. x IN s ==> ?m. (f m = SOME x)) /\
  (!m x. (f m = SOME x) ==> x IN s)
  ==>
  linear_order {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s /\
  finite_prefixes {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s`,
RWTAC [] THEN
IMP_RES_TAC nat_order_iso_thm THEN
RWTAC [finite_prefixes_def]);

val get_min_def = Define `
  get_min r' (s, r) =
    let mins = minimal_elements (minimal_elements s r) r' in
      if SING mins then
        SOME (CHOICE mins)
      else
        NONE`;

val nth_min_def = Define `
  (nth_min r' (s, r) 0 = get_min r' (s, r)) /\
  (nth_min r' (s, r) (SUC n) = 
    let min = get_min r' (s, r) in
      if min = NONE then
        NONE
      else
        nth_min r' (s DELETE (THE min), r) n)`;

val nth_min_surj_lem1 = Q.prove (
`!r' s' x s r. 
  linear_order r' s /\
  finite_prefixes r' s /\ 
  partial_order r s /\
  x IN minimal_elements s' r /\
  s' SUBSET s
  ==>
  ?m. nth_min r' (s', r) m = SOME x`,
NTAC 5 STRIP_TAC THEN
Induct_on `CARD {x' | x' IN s' /\ (x', x) IN r'}` THEN
RWTAC [] THEN
`FINITE {x' | x' IN s' /\ (x', x) IN r'}`
          by (FSTAC [finite_prefixes_def, minimal_elements_def, SUBSET_DEF,
                     INTER_LEM] THEN
              METIS_TAC [INTER_COMM, INTER_FINITE]) THENL
[Q.EXISTS_TAC `0` THEN
     RWTAC [nth_min_def, get_min_def] THEN
     `{x' | x' IN s' /\ (x', x) IN r'} = {}` by METIS_TAC [CARD_EQ_0] THEN
     FSTAC [] THEN
     `mins = {x}` by ALL_TAC THENL
     [ALL_TAC,
      RWTAC [SING_DEF]] THEN
     FSTAC [minimal_elements_def] THEN
     Q.UNABBREV_TAC `mins` THEN
     FSTAC [EXTENSION, linear_order_def, SUBSET_DEF] THEN
     METIS_TAC [],
 Q.PAT_ASSUM `!s' x r'. P s' x r'` 
             (STRIP_ASSUME_TAC o 
              Q.SPECL [`s' DELETE THE (get_min r' (s', r))`, `x`, `r'`]) THEN
     `SING (minimal_elements (minimal_elements s' r) r')` 
         by (MATCH_MP_TAC finite_prefix_linear_order_has_unique_minimal THEN
             Q.EXISTS_TAC `s` THEN
             RWTAC [SUBSET_DEF, minimal_elements_def] THEN
             FSTAC [SUBSET_DEF]) THEN
     FSTAC [get_min_def, LET_THM] THEN
     FSTAC [SING_DEF] THEN
     FSTAC [] THEN
     Cases_on `x = x'` THENL
     [Q.EXISTS_TAC `0` THEN 
          RWTAC [nth_min_def, get_min_def] THEN
          UNABBREV_ALL_TAC THEN
          RWTAC [],
      `x IN s' /\ x' IN s'` 
                by (FSTAC [minimal_elements_def, EXTENSION] THEN 
                    METIS_TAC []) THEN
          `v = CARD ({x' | x' IN s' /\ (x',x) IN r'} DELETE x')`
                  by (RWTAC [] THEN1
                      DECIDE_TAC THEN
                      FSTAC [minimal_elements_def, EXTENSION, 
                             linear_order_def, SUBSET_DEF] THEN
                      METIS_TAC []) THEN
          `{x' | x' IN s' /\ (x',x) IN r'} DELETE x' =
           {x'' | (x'' IN s' /\ x'' <> x') /\ (x'',x) IN r'}`
                  by (FSTAC [EXTENSION, linear_order_def,
                             domain_def, SUBSET_DEF] THEN
                      METIS_TAC []) THEN
          FSTAC [] THEN
          `?m. nth_min r' (s' DELETE x', r) m = SOME x` 
                  by (Q.PAT_ASSUM `P ==> ?m. Q m` MATCH_MP_TAC THEN
                      FSTAC [minimal_elements_def, rrestrict_def,
                             SUBSET_DEF]) THEN
          Q.EXISTS_TAC `SUC m` THEN
          RWTAC [nth_min_def] THEN
          Q.UNABBREV_TAC `min` THEN
          RWTAC [] THEN
          Cases_on `get_min r' (s', r)` THEN
          FSTAC [get_min_def, LET_THM, SING_DEF] THEN
          METIS_TAC [NOT_SOME_NONE, CHOICE_SING, SOME_11]]]);

val nth_min_surj_lem02 = Q.prove (
`!r' s r m m' x x'.
  (nth_min r' (s, r) m = SOME x) /\
  (nth_min r' (s DIFF {x | ?n. n <= m /\ (nth_min r' (s,r) n = SOME x)}, r) m' =
  SOME x')
  ==>
  (nth_min r' (s, r) (SUC (m + m')) = SOME x')`,
Induct_on `m` THEN
RWTAC [nth_min_def] THEN
UNABBREV_ALL_TAC THEN
RWTAC [DELETE_DEF] THEN
FSTAC [LET_THM] THEN
Cases_on `get_min r' (s, r)` THEN
FSTAC [DELETE_DEF] THEN
RWTAC [arithmeticTheory.ADD] THEN
Q.PAT_ASSUM `!r' s r m' x x'. P r' s r m' x x'` MATCH_MP_TAC THEN
RWTAC [] THEN
`s DIFF {x''} DIFF 
        {x | ?n. n <= m /\ (nth_min r' (s DIFF {x''}, r) n = SOME x)} =
 s DIFF {x | ?n.  n <= SUC m /\ (nth_min r' (s,r) n = SOME x)}` by
          (RWTAC [EXTENSION] THEN
           EQ_TAC THEN
           RWTAC [] THENL
           [Cases_on `n` THEN
                RWTAC [nth_min_def] THEN
                UNABBREV_ALL_TAC THEN
                RWTAC [DELETE_DEF] THEN
                POP_ASSUM (MP_TAC o Q.SPEC `n'`) THEN
                RWTAC [] THENL
                [DISJ1_TAC THEN
                     DECIDE_TAC,
                 METIS_TAC []],
            CCONTR_TAC THEN
                RWTAC [] THEN
                POP_ASSUM (MP_TAC o Q.SPEC `0`) THEN
                RWTAC [nth_min_def],
            POP_ASSUM (MP_TAC o Q.SPEC `SUC n`) THEN
                RWTAC [] THENL
                [DISJ1_TAC THEN
                     DECIDE_TAC,
                 FSTAC [nth_min_def, LET_THM] THEN
                 POP_ASSUM MP_TAC THEN
                 RWTAC [DELETE_DEF]]]) THEN
RWTAC []);
 

val nth_min_surj_lem03 = Q.prove (
`!r' s r s' x. 
  linear_order r' s /\
  finite_prefixes r' s /\
  partial_order r s /\
  finite_prefixes r s /\
  s' SUBSET s /\
  x IN s'
  ==> 
  ?m. nth_min r' (s', r) m = SOME x`,
NTAC 5 STRIP_TAC THEN
completeInduct_on `CARD {x' | x' IN s' /\ (x', x) IN r}` THEN
RWTAC [] THEN
Cases_on `x IN minimal_elements s' r` THEN1
METIS_TAC [nth_min_surj_lem1] THEN
`?x'. x' IN minimal_elements s' r /\ (x', x) IN r` 
            by METIS_TAC [finite_prefix_po_has_minimal_path] THEN
`?m. nth_min r' (s', r) m = SOME x'` by METIS_TAC [nth_min_surj_lem1] THEN
Q.ABBREV_TAC `s'' = {x | ?n. n <= m /\ (nth_min r' (s', r) n = SOME x)}` THEN
`{x''' | (x''' IN s' /\ x''' NOTIN s'') /\ (x''',x) IN r} PSUBSET
 {x' | x' IN s' /\ (x',x) IN r}`
           by (RWTAC [PSUBSET_DEF, SUBSET_DEF, EXTENSION] THEN
               Q.EXISTS_TAC `x'` THEN
               RWTAC [] THEN
               Q.UNABBREV_TAC `s''` THEN
               FSTAC [minimal_elements_def] THEN
               METIS_TAC [LESS_EQ_REFL]) THEN
`FINITE {x' | x' IN s' /\ (x',x) IN r}`
           by (FSTAC [finite_prefixes_def, SUBSET_DEF, minimal_elements_def,
                      INTER_LEM] THEN
               METIS_TAC [INTER_FINITE, INTER_COMM]) THEN
Cases_on `x IN s' DIFF s''` THENL
[FSTAC [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] THEN
     `?m. nth_min r' (s' DIFF s'', r) m = SOME x` by 
               (Q.PAT_ASSUM `!s''' x'' r''. P s''' x'' r''` MATCH_MP_TAC THEN
                FSTAC [SUBSET_DEF] THEN
                METIS_TAC [CARD_PSUBSET]) THEN
     Q.EXISTS_TAC `SUC (m + m')` THEN 
     METIS_TAC [nth_min_surj_lem02],
 FSTAC [] THEN1
     METIS_TAC [] THEN
     Q.UNABBREV_TAC `s''` THEN
     FSTAC [] THEN
     METIS_TAC []]);

val get_min_lem01 = Q.prove (
`!r' s r x. (get_min r' (s, r) = SOME x) ==> x IN s`,
RWTAC [get_min_def, LET_THM, SING_DEF] THEN
FSTAC [EXTENSION, minimal_elements_def] THEN
METIS_TAC []);

val nth_min_lem01 = Q.prove (
`!r' s r m x. (nth_min r' (s, r) m = SOME x) ==> x IN s`,
Induct_on `m` THEN
RWTAC [nth_min_def, LET_DEF] THEN1
METIS_TAC [get_min_lem01] THEN
RES_TAC THEN
FSTAC []);

val nth_min_lem02 = Q.prove (
`!r' s r n m. 
  nth_min r' (s, r) m <> NONE 
  ==> 
  nth_min r' (s, r) m <> nth_min r' (s, r) (SUC (m + n))`,
Induct_on `m` THEN
RWTAC [nth_min_def, LET_THM] THEN
Cases_on `get_min r' (s, r)` THEN
FSTAC [] THENL
[CCONTR_TAC THEN
     FSTAC [] THEN
     `x IN s DELETE x` by METIS_TAC [nth_min_lem01] THEN
     FSTAC [],
 `SUC m + n = SUC (m + n)` by DECIDE_TAC THEN
     METIS_TAC []]);

val nth_min_inj_lem = Q.prove (
`!r' s r. 
  (nth_min r' (s, r) m = nth_min r' (s, r) n) /\ nth_min r' (s, r) m <> NONE
  ==> 
  (m = n)`,
STRIP_ASSUME_TAC (DECIDE ``m:num < n \/ n < m \/ (m = n)``) THEN
RWTAC [] THENL
[`SUC (m + (n - m - 1)) = n` by DECIDE_TAC THEN
     METIS_TAC [nth_min_lem02],
 Cases_on `nth_min r' (s, r) n = NONE` THEN
     FSTAC [] THEN
     `SUC (n + (m - n - 1)) = m` by DECIDE_TAC THEN
     METIS_TAC [nth_min_lem02]]);

val nth_min_subset_lem01 = Q.prove (
`!m n x y s r r'.
  m < n /\ x <> y /\ 
  (nth_min r' (s, r) n = SOME x) /\ (nth_min r' (s, r) m = SOME y) 
  ==> 
  (x, y) NOTIN r`,
Induct THEN
RWTAC [nth_min_def] THENL
[IMP_RES_TAC get_min_lem01 THEN
     IMP_RES_TAC nth_min_lem01 THEN 
     FSTAC [get_min_def, LET_THM] THEN
     Cases_on `SING (minimal_elements (minimal_elements s r) r')` THEN
     FSTAC [SING_DEF] THEN
     FSTAC [] THEN
     RWTAC [] THEN
     FSTAC [minimal_elements_def, EXTENSION] THEN
     METIS_TAC [],
 FSTAC [LET_THM] THEN
     Cases_on `get_min r' (s, r)` THEN
     FSTAC [] THEN
     Cases_on `n` THEN
     FSTAC [nth_min_def, LET_THM] THEN
     RES_TAC THEN
     FSTAC [] THEN
     FSTAC [Q.prove (`(x, y) IN {(x, y) | P x y} = P x y`, RWTAC [])] THEN
     IMP_RES_TAC nth_min_lem01 THEN
     FSTAC []]);

val nth_min_subset_lem02 = Q.prove (
`!r' r s. 
  linear_order {(x, y) | ?m n. m <= n /\ (nth_min r' (s, r) m = SOME x) /\ 
                               (nth_min r' (s, r) n = SOME y)} s /\
  domain r SUBSET s /\
  range r SUBSET s
  ==> 
  r SUBSET {(x, y) | ?m n. m <= n /\ (nth_min r' (s, r) m = SOME x) /\ 
                           (nth_min r' (s, r) n = SOME y)}`,
RWTAC [SUBSET_DEF] THEN
Cases_on `x` THEN
RWTAC [] THEN
`?m n. m <= n /\ (((nth_min r' (s, r) m = SOME q) /\ 
                   (nth_min r' (s, r) n = SOME r'')) \/
                  ((nth_min r' (s, r) n = SOME q) /\ 
                   (nth_min r' (s, r) m = SOME r'')))` by
                (FSTAC [linear_order_def, domain_def, range_def] THEN
                 METIS_TAC []) THEN1
METIS_TAC [] THEN 
Cases_on `m = n` THEN1
METIS_TAC [] THEN
`m < n` by DECIDE_TAC THEN
`~(q = r'')` by (CCONTR_TAC THEN
                FSTAC [] THEN
                METIS_TAC [nth_min_inj_lem, NOT_SOME_NONE]) THEN
METIS_TAC [nth_min_subset_lem01]);

val linear_order_of_countable_po = Q.store_thm ("linear_order_of_countable_po",
`!r s. 
  countable s /\ partial_order r s /\ finite_prefixes r s 
  ==>
  ?r'. linear_order r' s /\ finite_prefixes r' s /\ r SUBSET r'`,
RWTAC [countable_def] THEN
Q.ABBREV_TAC `f' = nth_min (num_order f s) (s, r)` THEN
`!n m. (f' m = f' n) /\ f' m <> NONE ==> (m = n)` by METIS_TAC [nth_min_inj_lem] THEN
`!x. x IN s ==> ?m. f' m = SOME x` 
       by METIS_TAC [nth_min_surj_lem03, linear_order_num_order, SUBSET_REFL, 
                     num_order_finite_prefix] THEN
`!m x. (f' m = SOME x) ==> x IN s` by METIS_TAC [nth_min_lem01] THEN
Q.EXISTS_TAC `{(x,y) | ?m n. m <= n /\ (f' m = SOME x) /\ (f' n = SOME y)}` THEN
IMP_RES_TAC po2lolem01 THEN
RWTAC [] THEN
METIS_TAC [partial_order_def, nth_min_subset_lem02]);


val _ = export_theory ();