(* ========================================================================= *)
(* Create "terminatorTheory" setting up the HOL theory of terminator         *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Load and open relevant theories.                                          *)
(* (Comment out "load"s and "quietdec"s for compilation.)                    *)
(* ------------------------------------------------------------------------- *)
(*
val () = app load
  ["bossLib", "metisLib", "res_quanTools",
   "optionTheory", "listTheory",
   "arithmeticTheory", "dividesTheory", "gcdTheory",
   "pred_setTheory", "pred_setSyntax",
   "llistTheory"];
val () = quietdec := true;
*)

open HolKernel Parse boolLib bossLib metisLib res_quanTools;
open optionTheory listTheory;
open prim_recTheory arithmeticTheory dividesTheory gcdTheory;
open pred_setTheory llistTheory;

(*
val () = quietdec := false;
*)

(* ------------------------------------------------------------------------- *)
(* Start a new theory called "terminator".                                   *)
(* ------------------------------------------------------------------------- *)

val _ = new_theory "terminator";

(* ------------------------------------------------------------------------- *)
(* Helper proof tools.                                                       *)
(* ------------------------------------------------------------------------- *)

infixr 0 <<
infixr 1 ++ ||
infix 2 >>

val op ++ = op THEN;
val op << = op THENL;
val op >> = op THEN1;
val op || = op ORELSE;
val Know = Q_TAC KNOW_TAC;
val Suff = Q_TAC SUFF_TAC;
val REVERSE = Tactical.REVERSE;
val lemma = Tactical.prove;

val norm_rule =
    SIMP_RULE (simpLib.++ (pureSimps.pure_ss, resq_SS))
      [GSYM LEFT_FORALL_IMP_THM, GSYM RIGHT_FORALL_IMP_THM,
       AND_IMP_INTRO, GSYM CONJ_ASSOC];

fun match_tac th =
    let
      val th = norm_rule th
      val (_,tm) = strip_forall (concl th)
    in
      (if is_imp tm then MATCH_MP_TAC else MATCH_ACCEPT_TAC) th
    end;

(* ------------------------------------------------------------------------- *)
(* Helper theorems.                                                          *)
(* ------------------------------------------------------------------------- *)

val less_than_def = Define `less_than n = { k | k < n }`;

val lpred_def = Define
  `lpred p i l = case LNTH i l of SOME x_i -> p x_i || _ -> F`;

val lpred2_def = Define
  `lpred2 p i j l =
   case (LNTH i l, LNTH j l) of (SOME x_i, SOME x_j) -> p x_i x_j || _ -> F`;

val llist_all_def = Define
  `llist_all l p = !i. ~lpred (\x. ~p x) i l`;

val llist_all2_def = Define
  `llist_all2 s l p = !i j. s i j ==> ~lpred2 (\x_i x_j. ~p x_i x_j) i j l`;

val llist_all_suc_def = Define
  `llist_all_suc l p = llist_all2 (\i j. j = i + 1) l p`;

val finite_num = store_thm
  ("finite_num",
   ``!s. FINITE s = ?n. !m. m IN s ==> m < n``,
   RW_TAC std_ss []
   ++ EQ_TAC
   >> (Q.SPEC_TAC (`s`,`s`)
       ++ HO_MATCH_MP_TAC FINITE_INDUCT
       ++ RW_TAC arith_ss [NOT_IN_EMPTY, IN_INSERT]
       ++ Q.EXISTS_TAC `MAX n (SUC e)`
       ++ RW_TAC arith_ss []
       ++ RES_TAC
       ++ DECIDE_TAC)
   ++ STRIP_TAC
   ++ POP_ASSUM MP_TAC
   ++ Q.SPEC_TAC (`s`,`s`)
   ++ Induct_on `n`
   >> (RW_TAC arith_ss []
       ++ Suff `s = {}` >> RW_TAC std_ss [FINITE_EMPTY]
       ++ ONCE_REWRITE_TAC [EXTENSION]
       ++ RW_TAC std_ss [NOT_IN_EMPTY])
   ++ RW_TAC std_ss []
   ++ MATCH_MP_TAC
        (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]
         SUBSET_FINITE)
   ++ Q.EXISTS_TAC `n INSERT (s DELETE n)`
   ++ REVERSE CONJ_TAC
   >> (ONCE_REWRITE_TAC [EXTENSION]
       ++ RW_TAC std_ss [IN_INSERT, SUBSET_DEF, IN_DELETE])
   ++ RW_TAC std_ss [FINITE_INSERT]
   ++ FIRST_ASSUM MATCH_MP_TAC
   ++ RW_TAC arith_ss [IN_DELETE]
   ++ RES_TAC
   ++ DECIDE_TAC);

val lnth_infinite = store_thm
  ("lnth_infinite",
   ``!l n. ~LFINITE l ==> IS_SOME (LNTH n l)``,
   Induct_on `n`
   >> (RW_TAC std_ss [LNTH]
       ++ MP_TAC (Q.SPEC `l` llist_CASES)
       ++ STRIP_TAC >> METIS_TAC [LFINITE_THM]
       ++ RW_TAC std_ss [LHD_THM])
   ++ RW_TAC std_ss []
   ++ MP_TAC (Q.SPEC `l` llist_CASES)
   ++ STRIP_TAC >> METIS_TAC [LFINITE_THM]
   ++ RW_TAC std_ss [LHD_THM, LTL_THM, LNTH_THM]
   ++ METIS_TAC [LFINITE_THM]);

val lpred2_infinite = store_thm
  ("lpred2_infinite",
   ``!p l i j.
       ~LFINITE l ==> (lpred2 p i j l = p (THE (LNTH i l)) (THE (LNTH j l)))``,
   RW_TAC std_ss [lpred2_def]
   ++ MP_TAC (Q.SPECL [`l`,`i`] lnth_infinite)
   ++ MP_TAC (Q.SPECL [`l`,`j`] lnth_infinite)
   ++ REPEAT CASE_TAC
   ++ RW_TAC std_ss []);

(* ------------------------------------------------------------------------- *)
(* Ramsey's theorem                                                          *)
(* ------------------------------------------------------------------------- *)

val ramsey_graph_lemma_sets = store_thm
  ("ramsey_graph_lemma_sets",
   ``!vertex edge.
       INFINITE vertex ==>
       ?set a. !n.
         set n SUBSET vertex /\ INFINITE (set n) /\
         set (n + 1) SUBSET set n /\ a n IN set n /\
         (!k :: set (n + 1). a n < k) /\
         ((!k :: set (n + 1). edge (a n) k) \/
          (!k :: set (n + 1). ~edge (a n) k))``,
   REPEAT STRIP_TAC
   ++ Suff `?set.
              (set 0 = vertex) /\
              !n.
                INFINITE (set (n + 1)) /\ set (n + 1) SUBSET set n /\
                (!k :: set (n + 1). MIN_SET (set n) < k) /\
                ((!k :: set (n + 1). edge (MIN_SET (set n)) k) \/
                 (!k :: set (n + 1). ~edge (MIN_SET (set n)) k))`
   >> (RW_TAC std_ss []
       ++ Q.EXISTS_TAC `set`
       ++ Q.EXISTS_TAC `\n. MIN_SET (set n)`
       ++ ASM_SIMP_TAC std_ss []
       ++ GEN_TAC
       ++ CONJ_TAC
       >> (Induct_on `n` ++ METIS_TAC [ADD1, SUBSET_REFL, SUBSET_TRANS])
       ++ MATCH_MP_TAC (PROVE [] ``a /\ (a ==> b) ==> a /\ b``)
       ++ CONJ_TAC
       >> (REVERSE (Cases_on `n`) >> METIS_TAC [ADD1]
           ++ METIS_TAC [INFINITE_SUBSET])
       ++ METIS_TAC
            [MIN_SET_LEM, INFINITE_DIFF_FINITE, FINITE_EMPTY, DIFF_EMPTY])
   ++ Q.EXISTS_TAC
      `PRIM_REC
         vertex
         (\set n.
          if INFINITE
               { k | k IN set /\ MIN_SET set < k /\ edge (MIN_SET set) k }
          then { k | k IN set /\ MIN_SET set < k /\ edge (MIN_SET set) k }
          else { k | k IN set /\ MIN_SET set < k /\ ~edge (MIN_SET set) k })`
   ++ CONJ_TAC >> RW_TAC std_ss [PRIM_REC_THM]
   ++ Induct
   >> (RW_TAC resq_ss [PRIM_REC_THM, ONE, SUBSET_DEF, ADD, GSPECIFICATION]
       ++ FULL_SIMP_TAC std_ss [INFINITE_DEF]
       ++ STRIP_TAC
       ++ FULL_SIMP_TAC std_ss [finite_num, GSPECIFICATION]
       ++ Know `!m. m IN vertex /\ MIN_SET vertex < m ==> ~(MAX n n' <= m)`
       >> METIS_TAC [MAX_LE, DECIDE ``a < b = ~(b <= a)``]
       ++ RW_TAC std_ss []
       ++ POP_ASSUM (K ALL_TAC)
       ++ POP_ASSUM (K ALL_TAC)
       ++ SIMP_TAC std_ss [DECIDE ``a < b = a + 1 <= b``]
       ++ POP_ASSUM (MP_TAC o Q.SPEC `MAX (MIN_SET vertex + 1) (MAX n n')`)
       ++ RW_TAC std_ss [DECIDE ``a < b = ~(b <= a)``, MAX_LE]
       ++ Q.EXISTS_TAC `m`
       ++ METIS_TAC [])
   ++ POP_ASSUM STRIP_ASSUME_TAC
   ++ POP_ASSUM (K ALL_TAC)
   ++ POP_ASSUM (K ALL_TAC)
   ++ POP_ASSUM (K ALL_TAC)
   ++ POP_ASSUM MP_TAC
   ++ SIMP_TAC bool_ss [ADD1]
   ++ SIMP_TAC bool_ss [DECIDE ``(n + 1) + 1 = SUC (n + 1)``]
   ++ SIMP_TAC bool_ss [PRIM_REC_THM]
   ++ Q.SPEC_TAC
       (`PRIM_REC
         vertex
         (\set n.
          if INFINITE
               { k | k IN set /\ MIN_SET set < k /\ edge (MIN_SET set) k }
          then { k | k IN set /\ MIN_SET set < k /\ edge (MIN_SET set) k }
          else { k | k IN set /\ MIN_SET set < k /\ ~edge (MIN_SET set) k })
         (n + 1)`, `set`)
   ++ RW_TAC resq_ss [GSPECIFICATION, SUBSET_DEF]
   ++ FULL_SIMP_TAC std_ss [INFINITE_DEF]
   ++ STRIP_TAC
   ++ Q.PAT_ASSUM `~FINITE X` MP_TAC
   ++ FULL_SIMP_TAC std_ss [finite_num, GSPECIFICATION]
   ++ FULL_SIMP_TAC std_ss
        [DECIDE ``MIN_SET set < a = MIN_SET set + 1 <= a``]
   ++ FULL_SIMP_TAC std_ss [DECIDE ``a < b = ~(b <= a)``]
   ++ Q.EXISTS_TAC `MAX (MIN_SET set + 1) (MAX n n')`
   ++ RW_TAC std_ss [MAX_LE]
   ++ REVERSE (Cases_on `MIN_SET set + 1 <= m`) >> RW_TAC std_ss []
   ++ RW_TAC std_ss []
   ++ METIS_TAC []);

val ramsey_graph_lemma_sequence = store_thm
  ("ramsey_graph_lemma_sequence",
   ``!vertex edge.
        INFINITE (vertex : num -> bool) ==>
        ?a. !i.
          a i IN vertex /\
          (!j. a i < a j = i < j) /\
          ((!j. i < j ==> edge (a i) (a j)) \/
           (!j. i < j ==> ~edge (a i) (a j)))``,
   REPEAT STRIP_TAC
   ++ MP_TAC (Q.SPECL [`vertex`,`edge`] ramsey_graph_lemma_sets)
   ++ RW_TAC resq_ss [FORALL_AND_THM]
   ++ Q.EXISTS_TAC `a`
   ++ CONJ_TAC >> METIS_TAC [SUBSET_DEF]
   ++ Suff `!i j. i < j ==> a j IN set (i + 1)`
   >> (STRIP_TAC
       ++ REVERSE CONJ_TAC >> METIS_TAC []
       ++ RW_TAC std_ss []
       ++ MATCH_MP_TAC (PROVE [] ``(b ==> a) /\ (~b ==> ~a) ==> (a = b)``)
       ++ CONJ_TAC >> METIS_TAC []
       ++ SIMP_TAC std_ss [DECIDE ``~(a < b) = (a = b) \/ b < a``]
       ++ METIS_TAC [])
   ++ RW_TAC std_ss []
   ++ Know `i + 1 <= j` >> DECIDE_TAC
   ++ RW_TAC std_ss [LESS_EQ_EXISTS]
   ++ Suff `!n d. set (n + d) SUBSET set n`
   >> (RW_TAC std_ss [SUBSET_DEF]
       ++ METIS_TAC [ADD_ASSOC])
   ++ GEN_TAC
   ++ Q.PAT_ASSUM `!n. P n SUBSET Q n` MP_TAC
   ++ POP_ASSUM_LIST (K ALL_TAC)
   ++ STRIP_TAC
   ++ Induct
   >> RW_TAC std_ss [SUBSET_REFL, ADD_CLAUSES]
   ++ RW_TAC std_ss [ADD_CLAUSES]
   ++ METIS_TAC [SUBSET_TRANS, ADD1]);

(* Every infinite graph has an infinite subgraph that is either complete *)
(* or empty. *)

val ramsey_theorem_graph = store_thm
  ("ramsey_theorem_graph",
   ``!vertex edge.
        INFINITE vertex ==>
        ?set.
          set SUBSET vertex /\ INFINITE set /\
          ((!i j. i IN set /\ j IN set /\ i < j ==> edge i j) \/
           (!i j. i IN set /\ j IN set /\ i < j ==> ~edge i j))``,
   RW_TAC std_ss []
   ++ MP_TAC (Q.SPECL [`vertex`,`edge`] ramsey_graph_lemma_sequence)
   ++ RW_TAC std_ss [FORALL_AND_THM]
   ++ Know
      `(UNIV : num -> bool) =
       { i | !j. i < j ==> edge (a i) (a j) } UNION
       { i | !j. i < j ==> ~edge (a i) (a j) }`
   >> RW_TAC std_ss [EXTENSION, IN_UNIV, IN_UNION, GSPECIFICATION]
   ++ DISCH_THEN (MP_TAC o Q.AP_TERM `FINITE`)
   ++ Know `~FINITE (UNIV : num -> bool)`
   >> (RW_TAC std_ss [finite_num, IN_UNIV]
       ++ METIS_TAC [LESS_REFL])
   ++ RW_TAC std_ss [FINITE_UNION]
   << [Q.EXISTS_TAC `IMAGE a { i | !j. i < j ==> edge (a i) (a j) }`
       ++ CONJ_TAC >> (RW_TAC std_ss [IN_IMAGE, SUBSET_DEF] ++ METIS_TAC [])
       ++ CONJ_TAC
       >> (match_tac IMAGE_11_INFINITE
           ++ RW_TAC std_ss [INFINITE_DEF]
           ++ Suff `~(x < y) /\ ~(y < x)` >> DECIDE_TAC
           ++ METIS_TAC [LESS_REFL])
       ++ DISJ1_TAC
       ++ RW_TAC std_ss [IN_IMAGE, GSPECIFICATION]
       ++ METIS_TAC [],
       Q.EXISTS_TAC `IMAGE a { i | !j. i < j ==> ~edge (a i) (a j) }`
       ++ CONJ_TAC >> (RW_TAC std_ss [IN_IMAGE, SUBSET_DEF] ++ METIS_TAC [])
       ++ CONJ_TAC
       >> (match_tac IMAGE_11_INFINITE
           ++ RW_TAC std_ss [INFINITE_DEF]
           ++ Suff `~(x < y) /\ ~(y < x)` >> DECIDE_TAC
           ++ METIS_TAC [LESS_REFL])
       ++ DISJ2_TAC
       ++ RW_TAC std_ss [IN_IMAGE, GSPECIFICATION]
       ++ METIS_TAC []]);

(* Every complete infinite graph coloured with finitely many colours has *)
(* an infinite monochromatic subgraph. *)

val ramsey_theorem_colouring = store_thm
  ("ramsey_theorem_colouring",
   ``!carrier colouring n.
       INFINITE carrier /\
       (!i j :: carrier. i < j ==> ?k :: less_than n. colouring k i j) ==>
       ?set : num -> bool. ?k :: less_than n.
         set SUBSET carrier /\ INFINITE set /\
         !i j :: set. i < j ==> colouring k i j``,
   RW_TAC resq_ss [less_than_def, GSPECIFICATION]
   ++ REPEAT (POP_ASSUM MP_TAC)
   ++ Q.SPEC_TAC (`carrier`,`carrier`)
   ++ Induct_on `n`
   >> (RW_TAC arith_ss []
       ++ FULL_SIMP_TAC std_ss [INFINITE_DEF, finite_num]
       ++ POP_ASSUM
          (fn th =>
              MP_TAC (Q.SPEC `0` th)
              ++ RW_TAC std_ss []
              ++ ASSUME_TAC th)
       ++ Q.EXISTS_TAC `m`
       ++ RW_TAC std_ss []
       ++ POP_ASSUM (MP_TAC o Q.SPEC `m + 1`)
       ++ RW_TAC std_ss []
       ++ Q.EXISTS_TAC `m'`
       ++ RW_TAC std_ss []
       ++ DECIDE_TAC)
   ++ RW_TAC std_ss []
   ++ MP_TAC (Q.SPECL [`carrier`,
                        `\i j. colouring (n : num) i j`] ramsey_theorem_graph)
   ++ RW_TAC std_ss []
   >> METIS_TAC [DECIDE ``n < SUC n``]
   ++ Q.PAT_ASSUM `!x. P x ==> (!y. Q x y) ==> R x` (MP_TAC o Q.SPEC `set`)
   ++ ASM_SIMP_TAC std_ss []
   ++ MATCH_MP_TAC (PROVE [] ``(b ==> c) /\ a ==> ((a ==> b) ==> c)``)
   ++ CONJ_TAC >> METIS_TAC [DECIDE ``k < n ==> k < SUC n``, SUBSET_TRANS]
   ++ RW_TAC std_ss []
   ++ Q.PAT_ASSUM `!i j. P i j` (MP_TAC o Q.SPECL [`i`,`j`])
   ++ RW_TAC std_ss []
   ++ Q.PAT_ASSUM `!i. P i` (MP_TAC o Q.SPEC `i`)
   ++ FULL_SIMP_TAC std_ss [SUBSET_DEF]
   ++ DISCH_THEN (MP_TAC o Q.SPEC `j`)
   ++ RW_TAC std_ss []
   ++ Q.EXISTS_TAC `k`
   ++ RW_TAC std_ss []
   ++ Suff `~(k = n)` >> DECIDE_TAC
   ++ METIS_TAC []);

(* ------------------------------------------------------------------------- *)
(* Definitions                                                               *)
(* ------------------------------------------------------------------------- *)

val () = Hol_datatype
  `program = <| states : 'state -> bool;
                location : 'state -> 'location;
                initial : 'state -> bool;
                transition : 'state -> 'state -> bool |>`;
                
val locations_def = Define
  `locations p = IMAGE p.location p.states`;

val programs_def = Define
  `programs =
   { p |
     FINITE (locations p) /\
     p.initial SUBSET p.states /\
     !s s'. p.transition s s' ==> s IN p.states /\ s' IN p.states }`;

val traces_def = Define
  `traces p =
   { t |
     lpred (\x. x IN p.initial) 0 t /\
     llist_all_suc t p.transition }`;

val terminates_def = Define `terminates p = !t :: traces p. LFINITE t`;

val trace_at_location_def = Define
  `trace_at_location p l t = LFILTER (\x. p.location x = l) t`;

val cut_sets_def = Define
  `cut_sets p =
   { locs |
     locs SUBSET locations p /\
     !t :: traces p.
       ~LFINITE t ==> ?l :: locs. ~LFINITE (trace_at_location p l t) }`;

val terminator_property_at_location_def = Define
  `terminator_property_at_location p loc =
   (?R.
      WF R /\
      !t :: traces p.
        llist_all_suc (trace_at_location p loc t) (\x x'. R x' x))
   \/
   (?R n.
      (!k :: less_than n. WF (R k)) /\
      !t :: traces p.
        llist_all2
          (\i j. i < j)
          (trace_at_location p loc t)
          (\x_i x_j. ?k :: less_than n. R k x_j x_i))`;

val terminator_property_def = Define
  `terminator_property p =
   ?cut :: cut_sets p. !loc :: cut. terminator_property_at_location p loc`;

(* ------------------------------------------------------------------------- *)
(* Theorems                                                                  *)
(* ------------------------------------------------------------------------- *)

(* If the terminator property holds at a location, then no program trace *)
(* can visit that location an infinite number of times. *)

val program_terminates_at_location = store_thm
  ("program_terminates_at_location",
   ``!p :: programs. !loc :: locations p.
       terminator_property_at_location p loc ==>
       !t :: traces p. LFINITE (trace_at_location p loc t)``,
   RW_TAC resq_ss
     [terminator_property_at_location_def, less_than_def, GSPECIFICATION]
   >> (Q.PAT_ASSUM `!t. P t` (MP_TAC o Q.SPEC `t`)
       ++ ASM_SIMP_TAC std_ss []
       ++ Q.SPEC_TAC (`trace_at_location p loc t`,`l`)
       ++ Q.PAT_ASSUM `p IN programs` (K ALL_TAC)
       ++ Q.PAT_ASSUM `loc IN locations p` (K ALL_TAC)
       ++ Q.PAT_ASSUM `t IN traces p` (K ALL_TAC)
       ++ RW_TAC std_ss [llist_all_suc_def,llist_all2_def]
       ++ CCONTR_TAC
       ++ Q.PAT_ASSUM `WF R` MP_TAC
       ++ RW_TAC std_ss [relationTheory.WF_DEF]
       ++ Q.EXISTS_TAC `\state. state IN IMAGE (\i. THE (LNTH i l)) UNIV`
       ++ RW_TAC std_ss [IN_IMAGE, IN_UNIV]
       ++ MATCH_MP_TAC (PROVE [] ``(~a ==> b) ==> a \/ b``)
       ++ RW_TAC std_ss []
       ++ Q.PAT_ASSUM `!i. P i` MP_TAC
       ++ RW_TAC std_ss [lpred2_infinite]
       ++ METIS_TAC [])
   ++ Q.PAT_ASSUM `!t. P t` (MP_TAC o Q.SPEC `t`)
   ++ ASM_SIMP_TAC std_ss []
   ++ Q.SPEC_TAC (`trace_at_location p loc t`,`l`)
   ++ Q.PAT_ASSUM `p IN Program` (K ALL_TAC)
   ++ Q.PAT_ASSUM `loc IN locations p` (K ALL_TAC)
   ++ Q.PAT_ASSUM `t IN traces p` (K ALL_TAC)
   ++ RW_TAC std_ss [llist_all2_def]
   ++ CCONTR_TAC
   ++ Q.PAT_ASSUM `!k. k < n ==> P k` MP_TAC
   ++ MP_TAC
        (Q.SPECL
           [`UNIV`,`\k i j. R k (THE (LNTH j l) : 'b) (THE (LNTH i l))`,`n`]
           ramsey_theorem_colouring)
   ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``)
   ++ CONJ_TAC
   >> (RW_TAC resq_ss
         [IN_UNIV, less_than_def, GSPECIFICATION, INFINITE_DEF,
          finite_num]
       >> METIS_TAC [LESS_REFL]
       ++ Q.PAT_ASSUM `!i j. P i j` (MP_TAC o Q.SPECL [`i`,`j`])
       ++ RW_TAC std_ss [lpred2_infinite]
       ++ METIS_TAC [])
   ++ RW_TAC resq_ss [SUBSET_UNIV, less_than_def, GSPECIFICATION]
   ++ Q.EXISTS_TAC `k`
   ++ RW_TAC std_ss [relationTheory.WF_DEF]
   ++ Q.EXISTS_TAC `\state. state IN IMAGE (\i. THE (LNTH i l)) set`
   ++ RW_TAC std_ss [IN_IMAGE] >> METIS_TAC [INFINITE_INHAB]
   ++ MATCH_MP_TAC (PROVE [] ``(~a ==> b) ==> a \/ b``)
   ++ RW_TAC std_ss []
   ++ Q.PAT_ASSUM `INFINITE set` MP_TAC
   ++ RW_TAC std_ss [INFINITE_DEF, finite_num]
   ++ POP_ASSUM (MP_TAC o Q.SPEC `i + 1`)
   ++ RW_TAC std_ss [DECIDE ``~(m < i + 1) = i < m``]
   ++ METIS_TAC []);

(* If the terminator property holds at all the locations in a cut set, *)
(* then all program traces are finite. *)

val program_terminates = store_thm
  ("program_terminates",
   ``!p :: programs. terminator_property p ==> terminates p``,
   RW_TAC resq_ss
     [terminator_property_def, cut_sets_def, GSPECIFICATION, terminates_def]
   ++ CCONTR_TAC
   ++ Q.PAT_ASSUM `!t. P t ==> Q t ==> R t` (MP_TAC o Q.SPEC `t`)
   ++ RW_TAC std_ss []
   ++ MATCH_MP_TAC (PROVE [] ``(a ==> b) ==> (~a \/ b)``)
   ++ RW_TAC std_ss []
   ++ Q.PAT_ASSUM `!l. P l` (MP_TAC o Q.SPEC `l`)
   ++ RW_TAC std_ss []
   ++ match_tac program_terminates_at_location
   ++ RW_TAC std_ss []
   ++ METIS_TAC [SUBSET_DEF]);

val () = export_theory ();