(* ========================================================================= *)
(* Theory of wellfounded relations.                                          *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

needs "arith.ml";;

(* ------------------------------------------------------------------------- *)
(* Definition of wellfoundedness for arbitrary (infix) relation <<           *)
(* ------------------------------------------------------------------------- *)

parse_as_infix("<<",(12,"right"));;

let WF = new_definition
  `WF(<<) <=> !P:A->bool. (?x. P(x)) ==> (?x. P(x) /\ !y. y << x ==> ~P(y))`;;

(* ------------------------------------------------------------------------- *)
(* Strengthen it to equality.                                                *)
(* ------------------------------------------------------------------------- *)

let WF_EQ = prove
 (`WF(<<) <=> !P:A->bool. (?x. P(x)) <=> (?x. P(x) /\ !y. y << x ==> ~P(y))`,
  REWRITE_TAC[WF] THEN MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Equivalence of wellfounded induction.                                     *)
(* ------------------------------------------------------------------------- *)

let WF_IND = prove
 (`WF(<<) <=> !P:A->bool. (!x. (!y. y << x ==> P(y)) ==> P(x)) ==> !x. P(x)`,
  REWRITE_TAC[WF] THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC THEN
  POP_ASSUM(MP_TAC o SPEC `\x:A. ~P(x)`) THEN REWRITE_TAC[] THEN MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Equivalence of the "infinite descending chains" version.                  *)
(* ------------------------------------------------------------------------- *)

let WF_DCHAIN = prove
 (`WF(<<) <=> ~(?s:num->A. !n. s(SUC n) << s(n))`,
  REWRITE_TAC[WF; TAUT `(a <=> ~b) <=> (~a <=> b)`; NOT_FORALL_THM] THEN
  EQ_TAC THEN DISCH_THEN CHOOSE_TAC THENL
   [POP_ASSUM(MP_TAC o REWRITE_RULE[NOT_IMP]) THEN
    DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:A`) ASSUME_TAC) THEN
    SUBGOAL_THEN `!x:A. ?y. P(x) ==> P(y) /\ y << x` MP_TAC THENL
     [ASM_MESON_TAC[]; REWRITE_TAC[SKOLEM_THM]] THEN
    DISCH_THEN(X_CHOOSE_THEN `f:A->A` STRIP_ASSUME_TAC) THEN
    CHOOSE_TAC(prove_recursive_functions_exist num_RECURSION
     `(s(0) = a:A) /\ (!n. s(SUC n) = f(s n))`) THEN
    EXISTS_TAC `s:num->A` THEN ASM_REWRITE_TAC[] THEN
    SUBGOAL_THEN `!n. P(s n) /\ s(SUC n):A << s(n)`
      (fun th -> ASM_MESON_TAC[th]) THEN
    INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
    EXISTS_TAC `\y:A. ?n:num. y = s(n)` THEN REWRITE_TAC[] THEN
    ASM_MESON_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Equivalent to just *uniqueness* part of recursion.                        *)
(* ------------------------------------------------------------------------- *)

let WF_UREC = prove
 (`WF(<<) ==>
       !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
            ==> !(f:A->B) g. (!x. f x = H f x) /\ (!x. g x = H g x)
                              ==> (f = g)`,
  REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
  FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
  DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[]);;

let WF_UREC_WF = prove
 (`(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
        ==> !(f:A->bool) g. (!x. f x = H f x) /\ (!x. g x = H g x)
                          ==> (f = g))
   ==> WF(<<)`,
  REWRITE_TAC[WF_IND] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `\f x. P(x:A) \/ !z:A. z << x ==> f(z)`) THEN
  REWRITE_TAC[] THEN
  W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
   [MESON_TAC[]; DISCH_THEN(MP_TAC o SPECL [`P:A->bool`; `\x:A. T`]) THEN
    REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Stronger form of recursion with "inductive invariant" (Krstic/Matthews).  *)
(* ------------------------------------------------------------------------- *)

let WF_REC_INVARIANT = prove
 (`WF(<<)
   ==> !H S. (!f g x. (!z. z << x ==> (f z = g z) /\ S z (f z))
                      ==> (H f x = H g x) /\ S x (H f x))
             ==> ?f:A->B. !x. (f x = H f x)`,
  let lemma = prove_inductive_relations_exist
    `!f:A->B x. (!z. z << x ==> R z (f z)) ==> R x (H f x)` in
  REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
  X_CHOOSE_THEN `R:A->B->bool` STRIP_ASSUME_TAC lemma THEN
  SUBGOAL_THEN `!x:A. ?!y:B. R x y` (fun th -> ASM_MESON_TAC[th]) THEN
  FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT STRIP_TAC THEN
  FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC BINDER_CONV [th]) THEN
  SUBGOAL_THEN `!x:A y:B. R x y ==> S x y` MP_TAC THEN ASM_MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Equivalent to just *existence* part of recursion.                         *)
(* ------------------------------------------------------------------------- *)

let WF_REC = prove
 (`WF(<<)
   ==> !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
           ==> ?f:A->B. !x. f x = H f x`,
  REPEAT STRIP_TAC THEN
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC_INVARIANT) THEN
  EXISTS_TAC `\x:A y:B. T` THEN ASM_REWRITE_TAC[]);;

let WF_REC_WF = prove
 (`(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
                 ==> ?f:A->num. !x. f x = H f x)
   ==> WF(<<)`,
  DISCH_TAC THEN REWRITE_TAC[WF_DCHAIN] THEN
  DISCH_THEN(X_CHOOSE_TAC `x:num->A`) THEN
  SUBGOAL_THEN `!n. (x:num->A)(@m. x(m) << x(n)) << x(n)` ASSUME_TAC THENL
   [CONV_TAC(BINDER_CONV SELECT_CONV) THEN ASM_MESON_TAC[]; ALL_TAC] THEN
  FIRST_ASSUM(MP_TAC o SPEC
   `\f:A->num. \y:A. if ?p:num. y = x(p)
                     then SUC(f(x(@m. x(m) << y)))
                     else 0`) THEN
  REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
   [REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
    FIRST_ASSUM(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
    AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
    FIRST_ASSUM MATCH_ACCEPT_TAC; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `f:A->num` MP_TAC) THEN
  DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `(x:num->A) n`) THEN
  SUBGOAL_THEN `!n. ?p. (x:num->A) n = x p` (fun th -> REWRITE_TAC[th]) THENL
   [MESON_TAC[]; DISCH_TAC] THEN
  SUBGOAL_THEN `!n:num. ?k. f(x(k):A) < f(x(n))` ASSUME_TAC THENL
   [GEN_TAC THEN EXISTS_TAC `@m:num. x(m):A << x(n)` THEN
    FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [th]) THEN REWRITE_TAC[LT];
    MP_TAC(SPEC `\n:num. ?i:num. n = f(x(i):A)` num_WOP) THEN
    REWRITE_TAC[] THEN ASM_MESON_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Combine the two versions of the recursion theorem.                        *)
(* ------------------------------------------------------------------------- *)

let WF_EREC = prove
 (`WF(<<) ==>
       !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
            ==> ?!f:A->B. !x. f x = H f x`,
  MESON_TAC[WF_REC; WF_UREC]);;

(* ------------------------------------------------------------------------- *)
(* Some preservation theorems for wellfoundedness.                           *)
(* ------------------------------------------------------------------------- *)

parse_as_infix("<<<",(12,"right"));;

let WF_SUBSET = prove
 (`(!(x:A) y. x << y ==> x <<< y) /\ WF(<<<) ==> WF(<<)`,
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[WF] THEN
  DISCH_TAC THEN GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
  UNDISCH_TAC `!(x:A) (y:A). x << y ==> x <<< y` THEN MESON_TAC[]);;

let WF_MEASURE_GEN = prove
 (`!m:A->B. WF(<<) ==> WF(\x x'. m x << m x')`,
  GEN_TAC THEN REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC `\y:B. !x:A. (m(x) = y) ==> P x`) THEN
  UNDISCH_TAC `!x. (!y. (m:A->B) y << m x ==> P y) ==> P x` THEN
  REWRITE_TAC[] THEN MESON_TAC[]);;

let WF_LEX_DEPENDENT = prove
 (`!R:A->A->bool S:A->B->B->bool. WF(R) /\ (!a. WF(S a))
         ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S r1 s1 s2)`,
  REPEAT GEN_TAC THEN REWRITE_TAC[WF] THEN STRIP_TAC THEN
  X_GEN_TAC `P:A#B->bool` THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  GEN_REWRITE_TAC I [FORALL_PAIR_THM] THEN
  MAP_EVERY X_GEN_TAC [`a0:A`; `b0:B`] THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `\a:A. ?b:B. P(a,b)`) THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  DISCH_THEN(MP_TAC o SPECL [`a0:A`; `b0:B`]) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `a:A` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
  DISCH_THEN(X_CHOOSE_TAC `b1:B`) THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`a:A`; `\b. (P:A#B->bool) (a,b)`]) THEN
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  DISCH_THEN(MP_TAC o SPEC `b1:B`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `b:B` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
  DISCH_TAC THEN EXISTS_TAC `(a:A,b:B)` THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[FORALL_PAIR_THM] THEN ASM_MESON_TAC[]);;

let WF_LEX = prove
 (`!R:A->A->bool S:B->B->bool. WF(R) /\ WF(S)
         ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S s1 s2)`,
  SIMP_TAC[WF_LEX_DEPENDENT; ETA_AX]);;

let WF_POINTWISE = prove
 (`WF((<<) :A->A->bool) /\ WF((<<<) :B->B->bool)
   ==> WF(\(x1,y1) (x2,y2). x1 << x2 /\ y1 <<< y2)`,
  STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL WF_SUBSET) THEN EXISTS_TAC
   `\(x1,y1) (x2,y2). x1 << x2 \/ (x1:A = x2) /\ (y1:B) <<< (y2:B)` THEN
  CONJ_TAC THENL
   [REWRITE_TAC[FORALL_PAIR_THM] THEN CONV_TAC TAUT;
    MATCH_MP_TAC WF_LEX THEN ASM_REWRITE_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Wellfoundedness properties of natural numbers.                            *)
(* ------------------------------------------------------------------------- *)

let WF_num = prove
 (`WF(<)`,
  REWRITE_TAC[WF_IND; num_WF]);;

let WF_REC_num = prove
 (`!H. (!f g n. (!m. m < n ==> (f m = g m)) ==> (H f n = H g n))
        ==> ?f:num->A. !n. f n = H f n`,
  MATCH_ACCEPT_TAC(MATCH_MP WF_REC WF_num));;

(* ------------------------------------------------------------------------- *)
(* Natural number measures (useful in program verification).                 *)
(* ------------------------------------------------------------------------- *)

let MEASURE = new_definition
  `MEASURE m = \x y. m(x) < m(y)`;;

let WF_MEASURE = prove
 (`!m:A->num. WF(MEASURE m)`,
  REPEAT GEN_TAC THEN REWRITE_TAC[MEASURE] THEN
  MATCH_MP_TAC WF_MEASURE_GEN THEN
  MATCH_ACCEPT_TAC WF_num);;

let MEASURE_LE = prove
 (`(!y. MEASURE m y a ==> MEASURE m y b) <=> m(a) <= m(b)`,
    REWRITE_TAC[MEASURE] THEN MESON_TAC[NOT_LE; LTE_TRANS; LT_REFL]);;

(* ------------------------------------------------------------------------- *)
(* Trivially, a WF relation is irreflexive.                                  *)
(* ------------------------------------------------------------------------- *)

let WF_REFL = prove
 (`!x:A. WF(<<) ==> ~(x << x)`,
  GEN_TAC THEN REWRITE_TAC[WF] THEN
  DISCH_THEN(MP_TAC o SPEC `\y:A. y = x`) THEN
  REWRITE_TAC[] THEN MESON_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Even more trivially, the everywhere-false relation is wellfounded.        *)
(* ------------------------------------------------------------------------- *)

let WF_FALSE = prove
 (`WF(\x y:A. F)`,
  REWRITE_TAC[WF]);;

(* ------------------------------------------------------------------------- *)
(* Tail recursion.                                                           *)
(* ------------------------------------------------------------------------- *)

let WF_REC_TAIL = prove
 (`!P g h. ?f:A->B. !x. f x = if P(x) then f(g x) else h x`,
  let lemma1 = prove
   (`~(P 0) ==> ((?n. P(SUC n)) <=> (?n. P(n)))`,
    MESON_TAC[num_CASES; NOT_SUC])
  and lemma2 = prove
   (`(P 0) ==> ((!m. m < n ==> P(SUC m)) <=> (!m. m < SUC n ==> P(m)))`,
    REPEAT(DISCH_TAC ORELSE EQ_TAC) THEN INDUCT_TAC THEN
    ASM_MESON_TAC[LT_SUC; LT_0]) in
  REPEAT GEN_TAC THEN
  MP_TAC(GEN `x:A` (ISPECL [`x:A`; `\y:A n:num. g(y):A`] num_RECURSION)) THEN
  REWRITE_TAC[SKOLEM_THM; FORALL_AND_THM] THEN
  DISCH_THEN(X_CHOOSE_THEN `s:A->num->A` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `\x:A. if ?n:num. ~P(s x n)
                    then (h:A->B)(@y. ?n. (y = s x n) /\ ~P(s x n) /\
                                          !m. m < n ==> P(s x m))
                    else something_arbitrary:B` THEN
  X_GEN_TAC `x:A` THEN
  SUBGOAL_THEN `!n x:A. s (g x) n :A = s x (SUC n)` ASSUME_TAC THENL
   [INDUCT_TAC THEN ASM_REWRITE_TAC[];
    UNDISCH_THEN `!x:A n. s x (SUC n) :A = g (s x n)` (K ALL_TAC)] THEN
  ASM_CASES_TAC `(P:A->bool) x` THEN ASM_REWRITE_TAC[] THENL
   [ASM_SIMP_TAC[lemma1] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
    CONV_TAC SYM_CONV THEN ASM_SIMP_TAC[lemma2; lemma1];
    COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
    AP_TERM_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN
    REWRITE_TAC[] THEN X_GEN_TAC `y:A` THEN EQ_TAC THENL
     [SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
      INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LT_0];
      ASM_MESON_TAC[LT]]]);;

(* ------------------------------------------------------------------------- *)
(* A more general mix of tail and wellfounded recursion.                     *)
(* ------------------------------------------------------------------------- *)

let WF_REC_TAIL_GENERAL = prove
 (`!P G H. WF(<<) /\
           (!f g x. (!z. z << x ==> (f z = g z))
                    ==> (P f x <=> P g x) /\ G f x = G g x /\ H f x = H g x) /\
           (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x)) /\
           (!f x y. P f x /\ y << G f x ==> y << x)
           ==> ?f:A->B. !x. f x = if P f x then f(G f x) else H f x`,
  REPEAT STRIP_TAC THEN
  CHOOSE_THEN MP_TAC
   (prove_inductive_relations_exist
     `(!x:A. ~(P f x) ==> terminates f x) /\
      (!x. P (f:A->B) x /\ terminates f (G f x) ==> terminates f x)`) THEN
  REWRITE_TAC[FORALL_AND_THM] THEN
  DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
  SUBGOAL_THEN
   `?while. !f:A->B x:A. while f x = if P f x then while f (G f x) else x`
   (STRIP_ASSUME_TAC o GSYM)
  THENL [REWRITE_TAC[GSYM SKOLEM_THM; WF_REC_TAIL]; ALL_TAC] THEN
  SUBGOAL_THEN
   `?f:A->B. !x. f x = if terminates f x then H f (while f x :A) else anything`
  MP_TAC THENL
   [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC) THEN
    REPEAT STRIP_TAC THEN MATCH_MP_TAC(MESON[]
     `(a = b) /\ (a /\ b ==> (x = y) /\ (f x = g x))
      ==> ((if a then f x else d) = (if b then g y else d))`) THEN
    REPEAT STRIP_TAC THENL
     [SUBGOAL_THEN
       `!f g x.
           (!x y. P f x /\ y << G (f:A->B) x ==> y << x) /\
           (!y:A. (!z:A. z << y ==> z << x)
                  ==> (P f y = P g y) /\ (G f y = G g y))
               ==> terminates f x ==> terminates g x`
       (fun th -> EQ_TAC THEN MATCH_MP_TAC th THEN ASM_MESON_TAC[]) THEN
      GEN_TAC THEN GEN_TAC THEN
      REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN DISCH_TAC THEN
      ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b ==> a ==> c`] THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
      SUBGOAL_THEN
       `!x:A. terminates (f:A->B) x /\
              (!y:A. (!z:A. z << y ==> z << x)
                     ==> (P f y <=> P g y) /\ (G f y :A = G g y))
              ==> (while f x :A = while g x)`
       (fun th -> MATCH_MP_TAC th THEN ASM_MESON_TAC[]) THEN
      REWRITE_TAC[IMP_CONJ] THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
      FIRST_X_ASSUM MATCH_MP_TAC THEN
      SUBGOAL_THEN
       `!f:A->B. (!x:A y:A. P f x /\ y << G f x ==> y << x)
         ==> !x. terminates f x ==> !y. y << while f x ==> y << x`
       (fun th -> ASM_MESON_TAC[th]) THEN
      GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_MESON_TAC[]];
    MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
    DISCH_THEN(fun th -> ASSUME_TAC(GSYM th) THEN MP_TAC th) THEN
    MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:A` THEN
    ASM_CASES_TAC `P (f:A->B) (x:A) :bool` THEN ASM_MESON_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* Tactic to apply WF induction on a free "measured" term in the goal.       *)
(* ------------------------------------------------------------------------- *)

let WF_INDUCT_TAC =
  let qqconv =
    let pth = prove
     (`(!x. P x ==> !y. Q x y) <=> !y x. P x ==> Q x y`, MESON_TAC[]) in
    GEN_REWRITE_CONV I [pth]
  and eqconv =
    let pth = prove
     (`(!m. P m ==> (m = e) ==> Q) <=> (P e ==> Q)`, MESON_TAC[]) in
    REWR_CONV pth in
  let rec qqconvs tm =
    try (qqconv THENC BINDER_CONV qqconvs) tm
    with Failure _ -> eqconv tm in
  fun tm (asl,w as gl) ->
    let fvs = frees tm
    and gv = genvar(type_of tm) in
    let pat = list_mk_forall(gv::fvs,mk_imp(mk_eq(gv,tm),w)) in
    let th0 = UNDISCH(PART_MATCH rand num_WF pat) in
    let th1 = MP (SPECL (tm::fvs) th0) (REFL tm) in
    let th2 = CONV_RULE(LAND_CONV qqconvs) (DISCH_ALL th1) in
    (MATCH_MP_TAC th2 THEN MAP_EVERY X_GEN_TAC fvs THEN
     CONV_TAC(LAND_CONV qqconvs) THEN DISCH_THEN ASSUME_TAC) gl;;