(* ===================================================================== *)
(* FILE          : mk_prim_rec.sml                                       *)
(* DESCRIPTION   : The primitive recursion theorem from Peano's axioms.  *)
(*                 Translated from hol88.                                *)
(*                                                                       *)
(* AUTHORS       : (c) Mike Gordon and                                   *)
(*                     Tom Melham, University of Cambridge               *)
(* TRANSLATOR    : Konrad Slind, University of Calgary                   *)
(* DATE          : September 15, 1991                                    *)
(* ===================================================================== *)


(*---------------------------------------------------------------------------
 * In this file, we prove the primitive recursion theorem directly
 * from Peano's axioms (which are actually theorems in HOL).
 * These `axioms' define the type ":num" and two
 * constants "0:num" and "SUC:num->num", they are:
 *
 *    NOT_SUC   |- !n. ~(SUC n = 0)
 *
 *    INV_SUC   |- !m n. (SUC m = SUC n) ==> (m = n)
 *
 *    INDUCTION |- !P. (P 0 /\ (!n. P n ==> P(SUC n))) ==> !n. P n
 *
 * Using INDUCTION one can define an induction rule and tactic.
 * The rule is an ML function:
 *
 *  INDUCT: (thm # thm) -> thm
 *
 *    A1 |- t[0]      A2 |- !n. t[n] ==> t[SUC n]
 *  -----------------------------------------------
 *              A1 u A2 |- !n. t[n]
 *
 * The tactic is:
 *
 *             [A] !n.t[n]
 *   ================================
 *    [A] t[0]  ,  [A,t[n]] t[SUC x]
 *
 * From now on we only make (non-recursive) definitions and prove theorems.
 *
 * The following definition of < is from Hodges's article in "The Handbook of
 * Philosophical Logic" (page 111):
 *
 *    m < n = ?P. (!n. P(SUC n) ==> P n) /\ P m /\ ~(P n)
 *
 *
 * The following consequence of INV_SUC will be useful for rewriting:
 *
 *  |- !m n. (SUC m = SUC n)  =  (m = n)
 *
 * It is used in SUC_ID and PRIM_REC_EXISTS below. We establish it by
 * forward proof.
 *
 * After proving this we prove some standard properties of <.
 *---------------------------------------------------------------------------*)

open HolKernel boolLib Prim_rec Parse

type thm = Thm.thm

val _ = new_theory "prim_rec";

val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false;

(* Added TFM 88.04.02                                           *)

val NOT_SUC     = numTheory.NOT_SUC
and INV_SUC     = numTheory.INV_SUC
and INDUCTION   = numTheory.INDUCTION;

fun INDUCT_TAC g = INDUCT_THEN INDUCTION ASSUME_TAC g;

val LESS_DEF = new_definition (
  "LESS_DEF",
  Term `$< m n = ?P. (!n. P(SUC n) ==> P n) /\ P m /\ ~(P n)`)
val _ = set_fixity "<" (Infix(NONASSOC, 450))
val _ = TeX_notation {hol = "<", TeX = ("\\HOLTokenLt{}", 1)}
val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="prim_rec",Name="<"},name=(["Number","Natural"],"<")}

val INV_SUC_EQ = save_thm("INV_SUC_EQ",
   GENL [“m:num”, “n:num”]
        (IMP_ANTISYM_RULE
             (SPEC_ALL INV_SUC)
             (DISCH (“m:num = n”)
                    (AP_TERM (“SUC”)
                             (ASSUME (“m:num = n”))))));

(*---------------------------------------------------------------------------
 * First we define a partial inverse to SUC called PRE such that:
 *
 *   (PRE 0 = 0) /\ (!m. PRE(SUC m) = m)
 *---------------------------------------------------------------------------*)
val PRE_DEF = new_definition("PRE_DEF",
    “PRE m = (if (m=0) then 0 else @n. m = SUC n)”);
val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="prim_rec",Name="PRE"},name=(["Number","Natural"],"pre")}

val PRE =
 store_thm
  ("PRE",
   “(PRE 0 = 0) /\ (!m. PRE(SUC m) = m)”,
   REPEAT STRIP_TAC
    THEN REWRITE_TAC[PRE_DEF, INV_SUC_EQ, NOT_SUC, SELECT_REFL_2]);

val LESS_REFL = store_thm( "LESS_REFL", “!n. ~(n < n)”,
   GEN_TAC THEN
   REWRITE_TAC[LESS_DEF, NOT_AND]);


val SUC_LESS =
 store_thm
   ("SUC_LESS",
    “!m n. (SUC m < n) ==>  m < n”,
   REWRITE_TAC[LESS_DEF]
    THEN REPEAT STRIP_TAC
    THEN EXISTS_TAC (“P:num->bool”)
    THEN RES_TAC
    THEN ASM_REWRITE_TAC[]);

val NOT_LESS_0 =
 store_thm
   ("NOT_LESS_0",
    “!n. ~(n < 0)”,
   INDUCT_TAC
    THEN REWRITE_TAC[LESS_REFL]
    THEN IMP_RES_TAC(CONTRAPOS
            (SPECL[“n:num”, “0”] SUC_LESS))
    THEN ASM_REWRITE_TAC[]);

val LESS_0 = store_thm("LESS_0",
   “!n. 0 < (SUC n)”,
   GEN_TAC
    THEN REWRITE_TAC[LESS_DEF]
    THEN EXISTS_TAC (“\x.x = 0”)
    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
    THEN REWRITE_TAC[NOT_SUC]);

val LESS_0_0 =
 store_thm
  ("LESS_0_0",
   “0 < SUC 0”,
   REWRITE_TAC[LESS_0]) ;

val LESS_MONO =
 store_thm
  ("LESS_MONO",
   “!m n. (m < n) ==> (SUC m < SUC n)”,
   REWRITE_TAC[LESS_DEF]
    THEN REPEAT STRIP_TAC
    THEN EXISTS_TAC ``\n : num. P (PRE n) : bool``
    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
    THEN ASM_REWRITE_TAC [PRE]
    THEN INDUCT_TAC (* don't have num_CASES yet *)
    THEN ASM_REWRITE_TAC [PRE]) ;

val LESS_MONO_REV =
 store_thm
  ("LESS_MONO_REV",
   “!m n. (SUC m < SUC n) ==> (m < n)”,
   REWRITE_TAC[LESS_DEF]
    THEN REPEAT STRIP_TAC
    THEN EXISTS_TAC ``\n : num. P (SUC n) : bool``
    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
    THEN ASM_REWRITE_TAC []) ;

val LESS_MONO_EQ =
 store_thm
  ("LESS_MONO_EQ",
   “!m n. (SUC m < SUC n) = (m < n)”,
   REPEAT GEN_TAC THEN EQ_TAC
    THEN REWRITE_TAC [LESS_MONO, LESS_MONO_REV]) ;

(* now show that < is the transitive closure of the successor relation *)

val TC_LESS_0 = prove ( “!n. TC (\x y. y = SUC x) 0 (SUC n)”,
  INDUCT_TAC
  THENL [ irule relationTheory.TC_SUBSET THEN BETA_TAC THEN REFL_TAC,
    ONCE_REWRITE_TAC [relationTheory.TC_CASES2] THEN DISJ2_TAC
    THEN EXISTS_TAC ``SUC n`` THEN BETA_TAC THEN ASM_REWRITE_TAC [] ]) ;

val TC_NOT_LESS_0 = prove ( “!n. ~(TC (\x y. y = SUC x) n 0)”,
  ONCE_REWRITE_TAC [relationTheory.TC_CASES2]
  THEN BETA_TAC THEN REWRITE_TAC [GSYM NOT_SUC] ) ;

val TC_IM_RTC_SUC = store_thm ("TC_IM_RTC_SUC",
  ``!m n. TC (\x y. y = SUC x) m (SUC n) = RTC (\x y. y = SUC x) m n``,
  ONCE_REWRITE_TAC [relationTheory.TC_CASES2] THEN BETA_TAC
    THEN REWRITE_TAC [relationTheory.RTC_CASES_TC, INV_SUC_EQ]
    THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)
    THEN ASM_REWRITE_TAC []
    THEN DISJ2_TAC THEN EXISTS_TAC ``n : num``
    THEN ASM_REWRITE_TAC []) ;

val RTC_IM_TC = store_thm ("RTC_IM_TC",
  ``!m n. RTC (\x y. y = f x) (f m) n = TC (\x y. y = f x) m n``,
  REWRITE_TAC [relationTheory.EXTEND_RTC_TC_EQN]
   THEN BETA_TAC THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)
   THENL [Q.EXISTS_TAC `f m`,
     FIRST_X_ASSUM (ASSUME_TAC o SYM)]
   THEN ASM_REWRITE_TAC []) ;

val TC_LESS_MONO_EQ = prove (
  ``!m n. TC (\x y. y = SUC x) (SUC m) (SUC n) = TC (\x y. y = SUC x) m n``,
  REWRITE_TAC [TC_IM_RTC_SUC, RTC_IM_TC] ) ;

val LESS_ALT = store_thm ("LESS_ALT",
  ``$< = TC (\x y. y = SUC x)``,
  REWRITE_TAC [FUN_EQ_THM] THEN
  INDUCT_TAC THEN INDUCT_TAC THEN
  REWRITE_TAC [NOT_LESS_0, TC_NOT_LESS_0, LESS_0, TC_LESS_0,
    TC_LESS_MONO_EQ, LESS_MONO_EQ]
  THEN FIRST_ASSUM MATCH_ACCEPT_TAC) ;

val LESS_SUC_REFL =
 store_thm
  ("LESS_SUC_REFL",
   “!n. n < SUC n”,
   INDUCT_TAC
    THEN REWRITE_TAC[LESS_0_0]
    THEN IMP_RES_TAC LESS_MONO
    THEN ASM_REWRITE_TAC[]);

val LESS_SUC =
 store_thm
 ("LESS_SUC",
  “!m n. (m < n) ==> (m < SUC n)”,
  REWRITE_TAC [LESS_DEF]
   THEN REPEAT STRIP_TAC
   THEN EXISTS_TAC (“P:num->bool”)
   THEN IMP_RES_TAC
         (CONTRAPOS(SPEC (“(n:num)”)
                         (ASSUME (“  !n'. P(SUC n')  ==>  P n'  ”))))
   THEN ASM_REWRITE_TAC[]);

val LESS_LEMMA1 =
 store_thm
  ("LESS_LEMMA1",
   “!m n. (m < SUC n) ==> (m = n) \/ (m < n)”,
  REWRITE_TAC [LESS_ALT, TC_IM_RTC_SUC, relationTheory.RTC_CASES_TC]) ;

val LESS_LEMMA2 =
 store_thm
  ("LESS_LEMMA2",
   “!m n. ((m = n) \/ (m < n)) ==> (m < SUC n)”,
   REPEAT STRIP_TAC
    THEN (IMP_RES_TAC LESS_SUC)
    THEN ASM_REWRITE_TAC[LESS_SUC_REFL]);

(* |- !m n. m < (SUC n)  =  (m  =  n)  \/  m < n *)
val LESS_THM = save_thm("LESS_THM",
    GENL [“m:num”, “n:num”]
         (IMP_ANTISYM_RULE(SPEC_ALL LESS_LEMMA1)
                          (SPEC_ALL LESS_LEMMA2)));

val LESS_SUC_IMP =
 store_thm
  ("LESS_SUC_IMP",
   “!m n. (m < SUC n) ==> ~(m = n) ==> (m < n)”,
   REWRITE_TAC[LESS_THM]
    THEN REPEAT STRIP_TAC
    THEN RES_TAC
    THEN ASM_REWRITE_TAC[]);

val EQ_LESS =
 store_thm
  ("EQ_LESS",
   “!n. (SUC m = n) ==> (m < n)”,
   INDUCT_TAC
    THEN REWRITE_TAC[NOT_SUC, LESS_THM]
    THEN DISCH_TAC
    THEN IMP_RES_TAC INV_SUC
    THEN ASM_REWRITE_TAC[]);

val SUC_ID =
 store_thm
  ("SUC_ID",
   “!n. ~(SUC n = n)”,
   INDUCT_TAC
    THEN ASM_REWRITE_TAC[NOT_SUC, INV_SUC_EQ]);

val NOT_LESS_EQ =
 store_thm
  ("NOT_LESS_EQ",
   “!m n. (m = n) ==> ~(m < n)”,
   REPEAT GEN_TAC
    THEN DISCH_TAC
    THEN ASM_REWRITE_TAC[LESS_REFL]);

val LESS_NOT_EQ =
 store_thm
  ("LESS_NOT_EQ",
   “!m n. (m < n) ==> ~(m = n)”,
   REPEAT STRIP_TAC
    THEN IMP_RES_TAC
          (DISCH_ALL(SUBS[ASSUME (“(m:num) = n”)]
                         (ASSUME (“m < n”))))
    THEN IMP_RES_TAC LESS_REFL
    THEN RES_TAC
    THEN ASM_REWRITE_TAC[]);

(*---------------------------------------------------------------------------
 * Now we will prove that:
 *
 *   |- !x f. ?fun.
 *       (fun 0 = x) /\
 *       (!m. fun(SUC m) = f(fun m)m)
 *
 *  We start by defining a (higher order) function SIMP_REC and
 *  proving that:
 *
 *    |- !m x f.
 *        (SIMP_REC x f 0 = x) /\
 *        (SIMP_REC x f (SUC m) = f(SIMP_REC x f m))
 *
 *  We then define a function PRIM_REC in terms of SIMP_REC and prove that:
 *
 *    |- !m x f.
 *        (PRIM_REC x f 0  = x) /\
 *        (PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m)
 *
 *  This is sufficient to justify any primitive recursive definition
 *  because a definition:
 *
 *      fun 0 x1 ... xn       = f1(x1, ... ,xn)
 *
 *      fun (SUC m) x1 ... xn = f2(fun m x1 ... xn, m, x1, ... ,xn)
 *
 *  is equivalent to:
 *
 *      fun 0       = \x1 ... xn. f1(x1, ... ,xn)
 *
 *      fun (SUC m) = \x1 ... xn. f2(fun m x1 ... xn, m, x1, ... ,xn)
 *                  = (\f m x1 ... xn. f2(f x1 ... xn, m, x1, ... ,xn))(fun m)m
 *
 *  which defines fun to be:
 *
 *      PRIM_REC
 *       (\x1 ... xn. f1(x1, ... ,xn))
 *       (\f m x1 ... xn. f2(f x1 ... xn, m, x1, ... ,xn))
 *---------------------------------------------------------------------------*)

val SIMP_REC_REL =
 new_definition
  ("SIMP_REC_REL",
   Term`!(fun:num->'a) (x:'a) (f:'a->'a) (n:num).
            SIMP_REC_REL fun x f n =
                (fun 0 = x) /\
                !m. (m < n) ==> (fun(SUC m) = f(fun m))`);

val SIMP_REC_EXISTS = store_thm("SIMP_REC_EXISTS",
   “!x f n. ?fun:num->'a. SIMP_REC_REL fun x f n”,
   GEN_TAC THEN GEN_TAC THEN INDUCT_THEN INDUCTION STRIP_ASSUME_TAC THEN
   PURE_REWRITE_TAC[SIMP_REC_REL] THENL [
     EXISTS_TAC (“\p:num. (x:'a)”) THEN REWRITE_TAC[NOT_LESS_0],
     Q.EXISTS_TAC `\p. if p = SUC n then f (fun n) else fun p` THEN
     BETA_TAC THEN REWRITE_TAC [INV_SUC_EQ, GSYM NOT_SUC] THEN
     POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [SIMP_REC_REL]) THEN
     ASM_REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
     Q.ASM_CASES_TAC `m = SUC n` THENL [
       POP_ASSUM SUBST_ALL_TAC THEN IMP_RES_TAC LESS_REFL,
       ALL_TAC
     ] THEN ASM_REWRITE_TAC [] THEN COND_CASES_TAC THEN
     ASM_REWRITE_TAC [] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
     IMP_RES_TAC LESS_SUC_IMP
   ]);

val SIMP_REC_REL_UNIQUE = store_thm(
  "SIMP_REC_REL_UNIQUE",
  Term`!x f g1 g2 m1 m2.
          SIMP_REC_REL g1 x f m1 /\ SIMP_REC_REL g2 x f m2 ==>
          !n. n < m1 /\ n < m2 ==> (g1 n = g2 n)`,
  REWRITE_TAC [SIMP_REC_REL] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
  INDUCT_THEN INDUCTION STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC [] THEN
  DISCH_THEN (CONJUNCTS_THEN (ASSUME_TAC o MATCH_MP SUC_LESS)) THEN
  RES_TAC THEN ASM_REWRITE_TAC []);

open simpLib boolSimps
val SIMP_REC_REL_UNIQUE_RESULT = store_thm(
  "SIMP_REC_REL_UNIQUE_RESULT",
  Term`!x f n.
         ?!y. ?g. SIMP_REC_REL g x f (SUC n) /\ (y = g n)`,
  REPEAT GEN_TAC THEN
  SIMP_TAC bool_ss [EXISTS_UNIQUE_THM, SIMP_REC_EXISTS] THEN
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
  ASSUME_TAC (Q.SPEC `n` LESS_SUC_REFL) THEN
  IMP_RES_TAC SIMP_REC_REL_UNIQUE);

val SIMP_REC = new_specification
  ("SIMP_REC",["SIMP_REC"],
  ((CONJUNCT1 o
              SIMP_RULE bool_ss [EXISTS_UNIQUE_THM] o
              SIMP_RULE bool_ss [UNIQUE_SKOLEM_THM])
             SIMP_REC_REL_UNIQUE_RESULT));

val LESS_SUC_SUC =
 store_thm
  ("LESS_SUC_SUC",
   “!m. (m < SUC m) /\ (m < SUC(SUC m))”,
   INDUCT_TAC
    THEN ASM_REWRITE_TAC[LESS_THM]);

val SIMP_REC_THM = store_thm (
  "SIMP_REC_THM",
  “!(x:'a) f.
       (SIMP_REC x f 0 = x) /\
       (!m. SIMP_REC x f (SUC m) = f(SIMP_REC x f m))”,
  REPEAT GEN_TAC THEN
  ASSUME_TAC (SPECL [Term`x:'a`, Term`f:'a -> 'a`] SIMP_REC) THEN
  CONJ_TAC THENL [
    POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [SIMP_REC_REL] o
               Q.SPEC `0`) THEN ASM_REWRITE_TAC [],
    GEN_TAC THEN
    FIRST_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `SUC m`) THEN
    FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `m`) THEN
    ASM_REWRITE_TAC [] THEN
    Q.SUBGOAL_THEN `g (SUC m) = f (g m)` SUBST1_TAC THENL [
      FULL_SIMP_TAC bool_ss [SIMP_REC_REL, LESS_SUC_SUC],
      ALL_TAC
    ] THEN AP_TERM_TAC THEN STRIP_ASSUME_TAC (Q.SPEC `m` LESS_SUC_SUC) THEN
    IMP_RES_TAC SIMP_REC_REL_UNIQUE
  ]);

(*---------------------------------------------------------------------------
 * We now use simple recursion to prove that:
 *
 *   |- !x f. ?fun.
 *       (fun ZERO = x) /\
 *       (!m. fun(SUC m) = f(fun m)m)
 *
 *  We proceed by defining a function PRIM_REC and proving that:
 *
 *   |- !m x f.
 *       (PRIM_REC x f 0  = x) /\
 *       (PRIM_REC x f (SUC m) = f(PRIM_REC x f m)m)
 *---------------------------------------------------------------------------*)


val PRIM_REC_FUN =
 new_definition
  ("PRIM_REC_FUN",
   “PRIM_REC_FUN (x:'a) (f:'a->num->'a) =
        SIMP_REC (\n:num. x) (\fun n. f(fun(PRE n))n)”);

val PRIM_REC_EQN =
 store_thm
  ("PRIM_REC_EQN",
   “!(x:'a) f.
     (!n. PRIM_REC_FUN x f 0 n = x) /\
     (!m n. PRIM_REC_FUN x f (SUC m) n = f (PRIM_REC_FUN x f m (PRE n)) n)”,
   REPEAT STRIP_TAC
    THEN REWRITE_TAC [PRIM_REC_FUN, SIMP_REC_THM]
    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
    THEN REWRITE_TAC[]);

val PRIM_REC =
 new_definition
  ("PRIM_REC",
   “PRIM_REC (x:'a) f m = PRIM_REC_FUN x f m (PRE m)”);

val PRIM_REC_THM =
 store_thm
  ("PRIM_REC_THM",
   “!x f.
     (PRIM_REC (x:'a) f 0 = x) /\
     (!m. PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m)”,
   REPEAT STRIP_TAC
    THEN REWRITE_TAC[PRIM_REC, PRIM_REC_FUN, SIMP_REC_THM]
    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
    THEN REWRITE_TAC[PRE]);


(*---------------------------------------------------------------------------*
 * The axiom of dependent choice (DC).                                       *
 *---------------------------------------------------------------------------*)

local
  val DCkey = BETA_RULE (SPEC
                (Term`\y. P y /\ R (SIMP_REC a (\x. @y. P y /\ R x y) n) y`)
                     SELECT_AX)
  val totalDClem = prove
    (Term`!P R a. P a /\ (!x. P x ==> ?y. P y /\ R x y)
                   ==>
                   !n. P (SIMP_REC a (\x. @y. P y /\ R x y) n)`,
     REPEAT GEN_TAC THEN STRIP_TAC
       THEN INDUCT_THEN numTheory.INDUCTION ASSUME_TAC
       THEN ASM_REWRITE_TAC [SIMP_REC_THM]
       THEN BETA_TAC THEN RES_TAC THEN IMP_RES_TAC DCkey)
in
val DC = store_thm("DC",
Term
  `!P R a.
      P a /\ (!x. P x ==> ?y. P y /\ R x y)
          ==>
      ?f. (f 0 = a) /\ (!n. P (f n) /\ R (f n) (f (SUC n)))`,
REPEAT STRIP_TAC
  THEN EXISTS_TAC (Term`SIMP_REC a (\x. @y. P y /\ R x y)`)
  THEN REWRITE_TAC [SIMP_REC_THM] THEN BETA_TAC THEN GEN_TAC
  THEN SUBGOAL_THEN
       (Term`P (SIMP_REC a (\x. @y. P y /\ R x y) n)`) ASSUME_TAC THENL
  [MATCH_MP_TAC totalDClem THEN ASM_REWRITE_TAC[],
   ASM_REWRITE_TAC[] THEN RES_THEN MP_TAC THEN DISCH_THEN (K ALL_TAC)
  THEN DISCH_THEN (CHOOSE_THEN (ACCEPT_TAC o CONJUNCT2 o MATCH_MP DCkey))])
end;


(*----------------------------------------------------------------------*)
(* Unique existence theorem for prim rec definitions on num.            *)
(*                                                                      *)
(* ADDED TFM 88.04.02                                                   *)
(*----------------------------------------------------------------------*)

val num_Axiom_old = store_thm(
  "num_Axiom_old",
   “!e:'a. !f. ?! fn1. (fn1 0 = e) /\
                         (!n. fn1 (SUC n) = f (fn1 n) n)”,
   REPEAT GEN_TAC THEN
   CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL
   [EXISTS_TAC “PRIM_REC (e:'a) (f:'a->num->'a)” THEN
    REWRITE_TAC [PRIM_REC_THM],
    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
    REPEAT STRIP_TAC THEN
    CONV_TAC FUN_EQ_CONV THEN
    INDUCT_TAC THEN ASM_REWRITE_TAC []]);

val num_Axiom = store_thm(
  "num_Axiom",
  Term`!(e:'a) f. ?fn. (fn 0 = e) /\ !n. fn (SUC n) = f n (fn n)`,
  REPEAT GEN_TAC THEN
  STRIP_ASSUME_TAC
     (CONV_RULE EXISTS_UNIQUE_CONV
        (SPECL [Term`e:'a`, Term`\a:'a n:num. f n a:'a`] num_Axiom_old)) THEN
  EXISTS_TAC (Term`fn1 : num -> 'a`) THEN
  RULE_ASSUM_TAC BETA_RULE THEN ASM_REWRITE_TAC []);

(*---------------------------------------------------------------------------*
 * Wellfoundedness taken as no infinite descending chains in 'a. This defn   *
 * is conceptually simpler (to some) than the original definition of         *
 * wellfoundedness, which is solely in terms of sets (and therefore          *
 * logically simpler).                                                       *
 *---------------------------------------------------------------------------*)

val wellfounded_def =
Q.new_definition
  ("wellfounded_def",
   `wellfounded (R:'a->'a->bool) = ~?f. !n. R (f (SUC n)) (f n)`);

val _ = overload_on ("Wellfounded", ``wellfounded``);

(*---------------------------------------------------------------------------
 * First half of showing that the two definitions of wellfoundedness agree.
 *---------------------------------------------------------------------------*)

val WF_IMP_WELLFOUNDED = Q.prove(
`!R. WF R ==> wellfounded R`,
 GEN_TAC THEN CONV_TAC CONTRAPOS_CONV
 THEN REWRITE_TAC[wellfounded_def,relationTheory.WF_DEF]
 THEN STRIP_TAC
 THEN Ho_Rewrite.REWRITE_TAC
        [NOT_FORALL_THM,NOT_EXISTS_THM,boolTheory.NOT_IMP,DE_MORGAN_THM]
 THEN Q.EXISTS_TAC`\p:'a. ?n:num. p = f n`
 THEN BETA_TAC THEN CONJ_TAC THENL
  [MAP_EVERY Q.EXISTS_TAC [`(f:num->'a) n`,  `n`] THEN REFL_TAC,
   REWRITE_TAC[GSYM IMP_DISJ_THM]
    THEN GEN_TAC THEN DISCH_THEN (CHOOSE_THEN SUBST1_TAC)
    THEN Q.EXISTS_TAC`f(SUC n)` THEN ASM_REWRITE_TAC[]
    THEN Q.EXISTS_TAC`SUC n` THEN REFL_TAC]);

(*---------------------------------------------------------------------------
 * Second half.
 *---------------------------------------------------------------------------*)

val WELLFOUNDED_IMP_WF = Q.prove(
`!R. wellfounded R ==> WF R`,
 REWRITE_TAC[wellfounded_def,relationTheory.WF_DEF]
  THEN GEN_TAC THEN CONV_TAC CONTRAPOS_CONV
  THEN Ho_Rewrite.REWRITE_TAC
        [NOT_FORALL_THM,NOT_EXISTS_THM,NOT_IMP,DE_MORGAN_THM]
  THEN REWRITE_TAC [GSYM IMP_DISJ_THM]
  THEN REPEAT STRIP_TAC
  THEN Q.EXISTS_TAC`SIMP_REC w (\x. @q. R q x /\ B q)` THEN GEN_TAC
  THEN Q.SUBGOAL_THEN `!n. B(SIMP_REC w (\x. @q. R q x /\ B q) n)`
                      (ASSUME_TAC o SPEC_ALL)
  THENL [INDUCT_TAC,ALL_TAC]
  THEN ASM_REWRITE_TAC[SIMP_REC_THM] THEN BETA_TAC
  THEN RES_TAC
  THEN IMP_RES_TAC(BETA_RULE
     (Q.SPEC `\q. R q (SIMP_REC w (\x. @q. R q x /\ B q) n) /\ B q`
              boolTheory.SELECT_AX)));


val WF_IFF_WELLFOUNDED = Q.store_thm("WF_IFF_WELLFOUNDED",
`!R. WF R = wellfounded R`,
GEN_TAC THEN EQ_TAC THEN STRIP_TAC
  THENL [IMP_RES_TAC WF_IMP_WELLFOUNDED,
         IMP_RES_TAC WELLFOUNDED_IMP_WF]);


val WF_PRED =
Q.store_thm
("WF_PRED",
  `WF \x y. y = SUC x`,
 REWRITE_TAC[relationTheory.WF_DEF] THEN BETA_TAC THEN GEN_TAC
  THEN CONV_TAC CONTRAPOS_CONV
  THEN Ho_Rewrite.REWRITE_TAC
        [NOT_FORALL_THM,NOT_EXISTS_THM,NOT_IMP,DE_MORGAN_THM]
  THEN REWRITE_TAC [GSYM IMP_DISJ_THM]
  THEN DISCH_TAC
  THEN INDUCT_TAC THEN CCONTR_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE[])
  THEN RES_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[INV_SUC_EQ, GSYM NOT_SUC])
  THENL (map FIRST_ASSUM [ACCEPT_TAC, MATCH_MP_TAC])
  THEN FILTER_ASM_REWRITE_TAC is_eq [] THEN ASM_REWRITE_TAC[]);


(*----------------------------------------------------------------------------
 * This theorem is now a lot nicer as < can be defined as the transitive
 * closure of predecessor.
 *---------------------------------------------------------------------------*)

val WF_LESS = Q.store_thm("WF_LESS", `WF $<`,
  REWRITE_TAC[LESS_ALT, relationTheory.WF_TC_EQN, WF_PRED]) ;

val _ = BasicProvers.export_rewrites ["WF_LESS"]


(*---------------------------------------------------------------------------
 * Measure functions are definable as inverse image into (<). Every relation
 * arising from a measure function is wellfounded, which is really great!
 *---------------------------------------------------------------------------*)

val measure_def = Q.new_definition ("measure_def", `measure = inv_image $<`);
val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="prim_rec",Name="measure"},name=(["Relation"],"measure")}

val WF_measure =
Q.store_thm("WF_measure", `!m. WF (measure m)`,
REWRITE_TAC[measure_def]
 THEN MATCH_MP_TAC relationTheory.WF_inv_image
 THEN ACCEPT_TAC WF_LESS);
val _ = BasicProvers.export_rewrites ["WF_measure"]

val measure_thm = Q.store_thm
("measure_thm",
 `!f x y. measure f x y = f x < f y`,
 REWRITE_TAC [measure_def,relationTheory.inv_image_def]
   THEN BETA_TAC
   THEN REWRITE_TAC []);
val _ = BasicProvers.export_rewrites ["measure_thm"]

val _ = export_theory() ;