(**************************************************************************)
(*     ARM/Power Multiprocessor Machine Code Semantics: HOL sources       *)
(*                                                                        *)
(*                                                                        *)
(*  Jade Alglave (2), Anthony Fox (1), Samin Isthiaq (3),                 *)
(*  Magnus Myreen (1), Susmit Sarkar (1), Peter Sewell (1),               *)
(*  Francesco Zappa Nardelli (2)                                          *)
(*                                                                        *)
(*   (1) Computer Laboratory, University of Cambridge                     *)
(*   (2) Moscova project, INRIA Paris-Rocquencourt                        *)
(*   (3) Microsoft Research Cambridge                                     *)
(*                                                                        *)
(*     Copyright 2007-2008                                                *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*                                                                        *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*  3. The names of the authors may not be used to endorse or promote     *)
(*     products derived from this software without specific prior         *)
(*     written permission.                                                *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,          *)
(*  WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING             *)
(*  NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS    *)
(*  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.          *)
(*                                                                        *)
(**************************************************************************)

open HolKernel boolLib bossLib pred_setTheory pairTheory relationTheory
open res_quanTheory arithmeticTheory optionTheory;

val _ = new_theory "util";

val is_permutation_def = Define `
  is_permutation xlist xset =
    (set xlist = xset) /\ (ALL_DISTINCT xlist)`;

val sINV_def = Define `
sINV r = {(x, y) | (y, x) IN r}`;

val (sTC_rules, sTC_ind, sTC_cases) = Hol_reln `
(!x y. r (x, y) ==> sTC r (x, y)) /\
(!x y. (?z. sTC r (x, z) /\ sTC r (z, y)) ==> sTC r (x, y))`;

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

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

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

val sTC_cases_lem = Q.prove (
`!x y. 
  (x, y) IN sTC r 
  ==> 
  (x, y) IN r \/
  ((?z. (x, z) IN sTC r /\ (z, y) IN r) /\
   (?z. (x, z) IN r /\ (z, y) IN sTC r))`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
METIS_TAC [sTC_rules]);

val sTC_cases_right = Q.store_thm ("sTC_cases_right",
`!r x y.
  (x, y) IN sTC r =
  ((x, y) IN r) \/
  (?z. (x, z) IN sTC r /\ (z, y) IN r)`,
METIS_TAC [sTC_cases_lem, sTC_rules]);

val sTC_cases_left = Q.store_thm ("sTC_cases_left",
`!r x y.
  (x, y) IN sTC r =
  ((x, y) IN r) \/
  (?z. (x, z) IN r /\ (z, y) IN sTC r)`,
METIS_TAC [sTC_cases_lem, sTC_rules]);

val sTC_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 sTC r ==> (!z. P x y /\ P y z ==> P x z) /\ P x y)`,
NTAC 3 STRIP_TAC THEN
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
METIS_TAC []);

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

val sTC_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 sTC r ==> (!z. P z x /\ P x y ==> P z y) /\ P x y)`,
NTAC 3 STRIP_TAC THEN
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
METIS_TAC []);

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

val sTC_UNION_lem = Q.store_thm ("sTC_UNION_lem",
`!x y. (x, y) IN sTC r1 ==> !r2. (x, y) IN sTC (r1 UNION r2)`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THENL
[SRW_TAC [] [Once sTC_cases],
 METIS_TAC [sTC_rules]]);

val sTC_implication_lem = Q.prove (
`!x y. (x, y) IN sTC r1 ==> !r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==> (x, y) IN sTC r2`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
METIS_TAC [sTC_rules]);

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

val sTC_EMPTY = Q.prove (
`!x y. (x, y) IN sTC {} ==> F`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] []);

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

val acyclic_def = Define `
  acyclic r = !x. ~((x, x) IN sTC r)`;

val acyclic_union_thm = Q.store_thm ("acyclic_union_thm",
`!r1 r2. acyclic (r1 UNION r2) ==> acyclic r1 /\ acyclic r2`,
SRW_TAC [] [acyclic_def] THEN
METIS_TAC [sTC_UNION_lem, UNION_COMM]);
 
val strict_def = Define `
  strict r = {(x, y) | (x, y) IN r /\ ~(x = y)}`;

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

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

val _ = Define `
FIELD r = (DOM r) UNION (RANGE r)
`;

val linear_order_def = Define `
  linear_order r xs = 
    ((DOM r) UNION (RANGE r)) SUBSET xs /\
    (!x1 x2 x3. (x1, x2) IN r /\ (x2, x3) IN r ==> (x1, x3) IN r) /\
    (!x1 x2. (x1, x2) IN r /\ (x2, x1) IN r ==> (x1 = x2)) /\
    (!x1 x2 :: xs. (x1, x2) IN r \/ (x2, x1) IN r)`; 

val strict_linear_order_def = Define `
  strict_linear_order r xs = 
    ((DOM r) UNION (RANGE r)) SUBSET xs /\
    (!x1 x2 x3. (x1, x2) IN r /\ (x2, x3) IN r ==> (x1, x3) IN r) /\
    (!x. ~((x, x) IN r)) /\
    (!x1 x2 :: xs. ~(x1 = x2) ==> (x1, x2) IN r \/ (x2, x1) IN r)`; 

val PER_def = Define `
  PER xs xss =
    (BIGUNION xss) SUBSET xs /\ ~({} IN xss) /\ !xs1 xs2 :: xss. ~(xs1 = xs2) ==> DISJOINT xs1 xs2`;

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

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

val RRESTRICT_UNION = Q.store_thm ("RRESTRICT_UNION",
`!r1 r2 s. RRESTRICT (r1 UNION r2) s = (RRESTRICT r1 s) UNION (RRESTRICT r2 s)`,
SRW_TAC [] [RRESTRICT_def, EXTENSION] THEN
METIS_TAC []);

val strict_RRESTRICT = Q.store_thm ("strict_RRESTRICT",
`!r s. strict (RRESTRICT r s) = RRESTRICT (strict r) s`,
SRW_TAC [] [strict_def, RRESTRICT_def, EXTENSION] THEN
METIS_TAC []);


val PER_RESTRICT_def = Define `
  PER_RESTRICT xss xs = {xs' INTER xs | xs' IN xss} DELETE {}`;

val strict_linearisations_def = Define `
  strict_linearisations xs = {r | strict_linear_order r xs}`;

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

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 sTC_path_max_lem = Q.prove (
`!s. FINITE s ==> ~(s = {}) ==> !r. acyclic r ==> ?x. x IN maximal_elements s (sTC r)`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
SRW_TAC [] [] THEN
Cases_on `s={}` THEN1
SRW_TAC [] [maximal_elements_def] THEN
RES_TAC THEN
Cases_on `(x, e) IN (sTC r)` THENL
[Q.EXISTS_TAC `e` THEN
     SRW_TAC [] [maximal_elements_def] THEN
     `(x, x'') IN (sTC r)` by METIS_TAC [sTC_rules] THEN
     FULL_SIMP_TAC (srw_ss()) [acyclic_def, maximal_elements_def] THEN
     METIS_TAC [],
 FULL_SIMP_TAC (srw_ss()) [maximal_elements_def] THEN
     METIS_TAC []]);


val finite_acyclic_has_maximal_thm = Q.store_thm ("finite_acyclic_has_maximal_thm",
`!s. FINITE s ==> ~(s = {}) ==> !r. acyclic r ==> ?x. x IN maximal_elements s r`,
SRW_TAC [] [] THEN
IMP_RES_TAC sTC_path_max_lem THEN
FULL_SIMP_TAC (srw_ss()) [maximal_elements_def] THEN
METIS_TAC [sTC_rules]);

val lem1 = Q.prove (
`!x y. (x, y) IN sTC r ==> ?z. (x, z) IN r /\ (~(x = y) ==> ~(x = z))`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
METIS_TAC []);

val maximal_TC_thm = Q.store_thm ("maximal_TC_thm",
`!x s r.
  DOM r SUBSET s /\
  RANGE r SUBSET s /\
  x IN maximal_elements s r 
  ==> 
  x IN maximal_elements s (sTC r)`,
SRW_TAC [] [maximal_elements_def, DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC [lem1]);

val sTC_path_max_lem2 = Q.prove (
`!s. 
  FINITE s 
  ==> 
  !r x. 
    acyclic r /\ 
    x IN s /\
    ~(x IN maximal_elements s (sTC r))
    ==>
    ?y. y IN maximal_elements s (sTC r) /\ (x, y) IN sTC r`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
SRW_TAC [] [] THEN
Cases_on `s={}` THENL
[FULL_SIMP_TAC (srw_ss()) [maximal_elements_def],
 `?e'. (e, e') IN sTC r /\ e' IN s` 
          by (FULL_SIMP_TAC (srw_ss()) [maximal_elements_def] THEN
              METIS_TAC [sTC_rules]) THEN
     Cases_on `e' IN maximal_elements s (sTC r)` THENL
     [Q.EXISTS_TAC `e'` THEN
          SRW_TAC [] [] THEN
          FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, acyclic_def] THEN
          SRW_TAC [] [] THEN
          METIS_TAC [sTC_rules],
      `?y. y IN maximal_elements s (sTC r) /\ (e', y) IN sTC r` by METIS_TAC [] THEN
          Q.EXISTS_TAC `y` THEN
          SRW_TAC [] [] THENL
          [FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, acyclic_def] THEN
               SRW_TAC [] [] THEN
               METIS_TAC [sTC_rules],
           METIS_TAC [sTC_rules]]],
 FULL_SIMP_TAC (srw_ss()) [maximal_elements_def],
 Cases_on `~(x IN maximal_elements s (sTC r))` THENL
     [`?y. y IN maximal_elements s (sTC r) /\ (x, y) IN sTC r` by METIS_TAC [] THEN
          FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, acyclic_def] THEN
          METIS_TAC [sTC_rules],
      Cases_on `(x, e) IN sTC r` THENL
          [Q.EXISTS_TAC `e`,
           Q.EXISTS_TAC `x`] THEN
          FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, acyclic_def] THEN
          METIS_TAC [sTC_rules]]]);

val sTC_path_min_lem2 = Q.prove (
`!s. 
  FINITE s 
  ==> 
  !r x. 
    acyclic r /\ 
    x IN s /\
    ~(x IN minimal_elements s (sTC r))
    ==>
    ?y. y IN minimal_elements s (sTC r) /\ (y, x) IN sTC r`,
HO_MATCH_MP_TAC FINITE_INDUCT THEN 
SRW_TAC [] [] THEN
Cases_on `s={}` THENL
[FULL_SIMP_TAC (srw_ss()) [minimal_elements_def],
 `?e'. (e', e) IN sTC r /\ e' IN s` 
          by (FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN
              METIS_TAC [sTC_rules]) THEN
     Cases_on `e' IN minimal_elements s (sTC r)` THENL
     [Q.EXISTS_TAC `e'` THEN
          SRW_TAC [] [] THEN
          FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, acyclic_def] THEN
          SRW_TAC [] [] THEN
          METIS_TAC [sTC_rules],
      `?y. y IN minimal_elements s (sTC r) /\ (y, e') IN sTC r` by METIS_TAC [] THEN
          Q.EXISTS_TAC `y` THEN
          SRW_TAC [] [] THENL
          [FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, acyclic_def] THEN
               SRW_TAC [] [] THEN
               METIS_TAC [sTC_rules],
           METIS_TAC [sTC_rules]]],
 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def],
 Cases_on `~(x IN minimal_elements s (sTC r))` THENL
     [`?y. y IN minimal_elements s (sTC r) /\ (y, x) IN sTC r` by METIS_TAC [] THEN
          FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, acyclic_def] THEN
          METIS_TAC [sTC_rules],
      Cases_on `(e, x) IN sTC r` THENL
          [Q.EXISTS_TAC `e`,
           Q.EXISTS_TAC `x`] THEN
          FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, acyclic_def] THEN
          METIS_TAC [sTC_rules]]]);

val finite_acyclic_has_maximal_path_thm = Q.store_thm ("finite_acyclic_has_maximal_path_thm",
`!s r x. 
  FINITE s /\
  acyclic r /\ 
  x IN s /\
  ~(x IN maximal_elements s r)
  ==>
  ?y. y IN maximal_elements s r /\ (x, y) IN sTC r`,
SRW_TAC [] [] THEN
IMP_RES_TAC sTC_path_max_lem2 THEN
FULL_SIMP_TAC (srw_ss()) [maximal_elements_def] THEN
METIS_TAC [sTC_rules]);

val finite_acyclic_has_minimal_path_thm = Q.store_thm ("finite_acyclic_has_minimal_path_thm",
`!s r x. 
  FINITE s /\
  acyclic r /\ 
  x IN s /\
  ~(x IN minimal_elements s r)
  ==>
  ?y. y IN minimal_elements s r /\ (y, x) IN sTC r`,
SRW_TAC [] [] THEN
IMP_RES_TAC sTC_path_min_lem2 THEN
FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN
METIS_TAC [sTC_rules]);

val PAIR_RES_FORALL_THM = Q.store_thm ("PAIR_RES_FORALL_THM",
`!P f. RES_FORALL P f = !x y. (x, y) IN P ==> f (x, y)`,
SRW_TAC [] [RES_FORALL_THM] THEN
EQ_TAC THEN
SRW_TAC [] [] THEN
Cases_on `x` THEN
SRW_TAC [] []);

val PAIR_APP_THM = Q.store_thm ("PAIR_APP_THM",
`!f x y. (\(x, y). f x y) (x, y) = f x y`,
SRW_TAC [] []);

val PAIR_GSPEC_ID = Q.store_thm ("PAIR_GSPEC_ID",
`!s. {(x,y) | (x,y) IN s} = s`,
SRW_TAC [] [EXTENSION, GSPECIFICATION] THEN 
EQ_TAC THEN
SRW_TAC [] [SPECIFICATION] THENL
[Cases_on `x'` THEN 
     FULL_SIMP_TAC (srw_ss()) [],
 Q.EXISTS_TAC `x` THEN
     Cases_on `x` THEN
     SRW_TAC [] []]);

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

val UNIQUE_MEMBER_SING = Q.store_thm ("UNIQUE_MEMBER_SING",
`!x s. x IN s /\ (!y. y IN s ==> (x = y)) = (s = {x})`,
SRW_TAC [] [EXTENSION] THEN
METIS_TAC []);


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`,
SRW_TAC [] [all_choices_def] THEN 
FULL_SIMP_TAC (srw_ss()) [] THEN
METIS_TAC [SPECIFICATION]);

val strict_linear_order_dom_rng_lem = Q.store_thm ("strict_linear_order_dom_rng_lem",
`!r s x y. (x, y) IN r ==> strict_linear_order r s ==> x IN s /\ y IN s`,
SRW_TAC [] [strict_linear_order_def, DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);

val linear_order_dom_rng_lem = Q.store_thm ("linear_order_dom_rng_lem",
`!r s x y. (x, y) IN r ==> linear_order r s ==> x IN s /\ y IN s`,
SRW_TAC [] [linear_order_def, DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);

val empty_strict_linear_order_thm = Q.store_thm ("empty_strict_linear_order_thm",
`!r. strict_linear_order r {} = (r = {})`,
SRW_TAC [] [strict_linear_order_def, RES_FORALL_THM, DOM_def, RANGE_def, EXTENSION] THEN
EQ_TAC THEN
SRW_TAC [] [] THEN
Cases_on `x` THEN
SRW_TAC [] []);

val empty_linear_order_thm2 = Q.store_thm ("empty_linear_order_thm2",
`!r. linear_order r {} = (r = {})`,
SRW_TAC [] [linear_order_def, RES_FORALL_THM, DOM_def, RANGE_def, EXTENSION] THEN
EQ_TAC THEN
SRW_TAC [] [] THEN
Cases_on `x` THEN
SRW_TAC [] []);

val CURRY_EMPTY = Q.store_thm ("CURRY_EMPTY",
`CURRY {} = \x. \y. F`,
SRW_TAC [] [FUN_EQ_THM, CURRY_DEF] THEN
METIS_TAC [SPECIFICATION, EMPTY_DEF]);

val TC_EMPTY = Q.store_thm ("TC_EMPTY",
`TC (\x y. F) = \x y. F`,
SRW_TAC [] [FUN_EQ_THM, TC_DEF] THEN
Q.EXISTS_TAC `\x y. F` THEN
SRW_TAC [] []);

val CARD_EQ_SUC = Q.store_thm ("CARD_EQ_SUC",
`!s. FINITE s ==> !n. (CARD s = SUC n) ==> ~(s = {})`,
SRW_TAC [] [] THEN
CCONTR_TAC THEN
FULL_SIMP_TAC (srw_ss()) []);

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 = {})}`,
SRW_TAC [] [PER_def, SUBSET_DEF, RES_FORALL_THM] THENL
[FULL_SIMP_TAC (srw_ss()) [IN_DELETE] THEN
     METIS_TAC [],
 FULL_SIMP_TAC (srw_ss()) [IN_DELETE] THEN
     METIS_TAC [],
 FULL_SIMP_TAC (srw_ss()) [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')`,
SRW_TAC [] [PER_def, PER_RESTRICT_def, RES_FORALL_THM, SUBSET_DEF, DISJOINT_DEF] THENL
[FULL_SIMP_TAC (srw_ss()) [],
 FULL_SIMP_TAC (srw_ss()) [EXTENSION, SPECIFICATION] THEN
     METIS_TAC []]); 

val acyclic_irreflexive_thm = Q.store_thm ("acyclic_irreflexive_thm",
`!r x. acyclic r ==> ~((x, x) IN r)`,
SRW_TAC [] [acyclic_def] THEN
METIS_TAC [sTC_cases]);

val acyclic_rrestrict_thm = Q.store_thm ("acyclic_rrestrict_thm",
`!r s. acyclic r ==> acyclic (RRESTRICT r s)`,
SRW_TAC [] [RRESTRICT_def] THEN
`r = {(x,y) | (x,y) IN r /\ x IN s /\ y IN s} UNION r` by SRW_TAC [] [UNION_DEF, REXTENSION] THEN
METIS_TAC [acyclic_union_thm]);
     
val linear_order_restrict_thm = Q.store_thm ("linear_order_restrict_thm",
`!s r s'. linear_order r s ==> linear_order (RRESTRICT r s') (s INTER s')`,
SRW_TAC [] [linear_order_def, RRESTRICT_def, DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);

val strict_linear_order_restrict_thm = Q.store_thm ("strict_linear_order_restrict_thm",
`!s r s'. strict_linear_order r s ==> strict_linear_order (RRESTRICT r s') (s INTER s')`,
SRW_TAC [] [strict_linear_order_def, RRESTRICT_def, DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);

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

val INTER_DELETE = Q.store_thm ("INTER_DELETE",
`!s e. s INTER (s DELETE e) = s DELETE e`,
SRW_TAC [] [EXTENSION] THEN
METIS_TAC []);

val extend_linear_order_thm = Q.store_thm ("extend_linear_order_thm",
`!r s x.
  ~(x IN s) /\
  linear_order r s 
  ==>
  linear_order (r UNION {(y, x) | y | y IN (s UNION {x})}) (s UNION {x})`,
SRW_TAC [] [RES_FORALL, linear_order_def, DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);

val strict_linear_order_sTC_lem = Q.prove (
`!x y. (x, y) IN sTC r ==> !s. strict_linear_order r s ==> (x, y) IN r`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
RES_TAC THEN
FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def] THEN
METIS_TAC []);

val strict_linear_order_sTC_thm = Q.store_thm ("strict_linear_order_sTC_thm",
`!r s. strict_linear_order r s ==> (r = sTC r)`,
SRW_TAC [] [EXTENSION] THEN
EQ_TAC THEN
SRW_TAC [] [] THEN
Cases_on `x` THENL
[FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def, RES_FORALL] THEN
     METIS_TAC [sTC_rules],
 METIS_TAC [strict_linear_order_sTC_lem]]);

val strict_linear_order_acyclic_thm = Q.store_thm ("strict_linear_order_acyclic_thm",
`!r s. strict_linear_order r s ==> acyclic r`,
SRW_TAC [] [acyclic_def] THEN
IMP_RES_TAC (GSYM strict_linear_order_sTC_thm) THEN
FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def]);

val strict_linear_order_union_acyclic_thm = Q.store_thm ("strict_linear_order_union_acyclic_thm",
`!r1 r2 s. 
  strict_linear_order r1 s /\
  ((DOM r2) UNION (RANGE r2)) SUBSET s
  ==> 
  (acyclic (r1 UNION r2) = r2 SUBSET r1)`,
SRW_TAC [] [] THEN
EQ_TAC THEN
SRW_TAC [] [] THENL
[FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def, RES_FORALL, DOM_def, RANGE_def, SUBSET_DEF] THEN
     Cases_on `x` THEN
     IMP_RES_TAC acyclic_irreflexive_thm THEN
     CCONTR_TAC THEN
     FULL_SIMP_TAC (srw_ss()) [] THEN
     METIS_TAC [acyclic_def, sTC_rules, IN_UNION],
 `r1 UNION r2 = r1` by (FULL_SIMP_TAC (srw_ss()) [DOM_def, RANGE_def, SUBSET_DEF, EXTENSION] THEN METIS_TAC []) THEN
     SRW_TAC [] [] THEN
     METIS_TAC [strict_linear_order_acyclic_thm]]);

val strict_linear_order_thm = Q.store_thm ("strict_linear_order_thm",
`!r s. linear_order r s ==> strict_linear_order (strict r) s`,
SRW_TAC [] [linear_order_def, strict_linear_order_def, strict_def, 
            DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);

val linear_order_thm = Q.store_thm ("linear_order_thm",
`!r s. strict_linear_order r s ==> linear_order (r UNION {(x, x) | x IN s}) s`,
SRW_TAC [] [linear_order_def, strict_linear_order_def, 
            DOM_def, RANGE_def, SUBSET_DEF] THEN
METIS_TAC []);


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

val finite_strict_linear_order_has_maximal_thm = Q.store_thm ("finite_strict_linear_order_has_maximal_thm",
`!s r. FINITE s /\ strict_linear_order r s /\ ~(s = {}) ==> ?x. x IN maximal_elements s r`,
METIS_TAC [strict_linear_order_acyclic_thm, finite_acyclic_has_maximal_thm]);

val finite_linear_order_has_maximal_thm = Q.store_thm ("finite_linear_order_has_maximal_thm",
`!s r. FINITE s /\ linear_order r s /\ ~(s = {}) ==> ?x. x IN maximal_elements s r`,
SRW_TAC [] [] THEN
IMP_RES_TAC strict_linear_order_thm THEN
IMP_RES_TAC finite_strict_linear_order_has_maximal_thm THEN
Q.EXISTS_TAC `x` THEN
FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, strict_def] THEN
METIS_TAC []);

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

val sTC_DOM_RNG_thm = Q.store_thm ("sTC_DOM_RNG_thm",
`!x y. (x, y) IN sTC r ==> x IN DOM r /\ y IN RANGE r`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [DOM_def, RANGE_def] THEN
METIS_TAC []);

val sTC_BIGUNION_lem = Q.prove (
`!x y. (x, y) IN sTC (BIGUNION rs) ==>
(!r r'. 
  r IN rs /\ r' IN rs /\ ~(r = r') 
  ==> 
  DISJOINT (DOM r UNION RANGE r) (DOM r' UNION RANGE r')) ==>
?r. r IN rs /\ (x, y) IN sTC r`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN1
METIS_TAC [sTC_rules] THEN
RES_TAC THEN
IMP_RES_TAC sTC_DOM_RNG_thm THEN
FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION] THEN
`r = r'` by (SRW_TAC [] [EXTENSION] THEN METIS_TAC []) THEN
METIS_TAC [sTC_rules]);

val acyclic_bigunion_thm = Q.store_thm ("acyclic_bigunion_thm",
`!rs.
  (!r r'. 
    r IN rs /\ r' IN rs /\ ~(r = r') 
    ==> 
    DISJOINT (DOM r UNION RANGE r) (DOM r' UNION RANGE r')) /\
  (!r. r IN rs ==> acyclic r)
  ==>
  acyclic (BIGUNION rs)`,
SRW_TAC [] [acyclic_def] THEN
CCONTR_TAC THEN
FULL_SIMP_TAC (srw_ss()) [] THEN
IMP_RES_TAC sTC_BIGUNION_lem THEN
FULL_SIMP_TAC (srw_ss()) [] THEN
METIS_TAC []);

val acyclic_union_lem = Q.store_thm ("acyclic_union_lem",
`!r r'. 
  DISJOINT (DOM r UNION RANGE r) (DOM r' UNION RANGE r') /\
  acyclic r /\
  acyclic r'
  ==>
  acyclic (r UNION r')`,
SRW_TAC [] [] THEN
MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.SPEC `{r; r'}` acyclic_bigunion_thm)) THEN
SRW_TAC [] [] THEN
METIS_TAC [DISJOINT_SYM]);

val linear_order_sTC_lem = Q.prove (
`!x y. (x, y) IN sTC r ==> !s. linear_order r s ==> (x, y) IN r`,
HO_MATCH_MP_TAC sTC_ind THEN
SRW_TAC [] [] THEN
RES_TAC THEN
FULL_SIMP_TAC (srw_ss()) [linear_order_def] THEN
METIS_TAC []);

val linear_order_sTC_thm = Q.store_thm ("linear_order_sTC_thm",
`!r s. linear_order r s ==> (r = sTC r)`,
SRW_TAC [] [EXTENSION] THEN
EQ_TAC THEN
SRW_TAC [] [] THEN
Cases_on `x` THENL
[FULL_SIMP_TAC (srw_ss()) [linear_order_def, RES_FORALL] THEN
     METIS_TAC [sTC_rules],
 METIS_TAC [linear_order_sTC_lem]]);

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 /\
  !y. FINITE {x | (x, y) IN {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)}}`,
SRW_TAC [] [linear_order_def, DOM_def, RANGE_def, SUBSET_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],
 Cases_on `y IN s` THENL
     [`?n. SOME y = f n` by METIS_TAC [] THEN
          SRW_TAC [] [] THEN
          `{SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} SUBSET IMAGE f (count (SUC n))`
                  by (SRW_TAC [] [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 (SRW_TAC [] [EXTENSION] THEN METIS_TAC [THE_DEF]) THEN
          METIS_TAC [IMAGE_FINITE, SUBSET_FINITE, FINITE_COUNT],
      `{x | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} = {}`
                  by (SRW_TAC [] [EXTENSION] THEN METIS_TAC []) THEN
          METIS_TAC [FINITE_EMPTY]]]);

val _ = Define `DOMAIN f = { x | ~(f x = NONE) } `;


val _ = export_theory ();