(*---------------------------------------------------------------------------*)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)               *)
(* DATE          : 2008                                                      *)
(*---------------------------------------------------------------------------*)


(*---------------------------------------------------------------------------*)
(*       INDUCT_THEN                                                         *)
(*---------------------------------------------------------------------------*)

let INDUCT_THEN th =

(* ---------------------------------------------------------------------*)
(* Internal function: 							*)
(*									*)
(* BETAS "f" tm : returns a conversion that, when applied to a term with*)
(*		 the same structure as the input term tm, will do a	*)
(*		 beta reduction at all top-level subterms of tm which	*)
(*		 are of the form "f <arg>", for some argument <arg>.	*)
(*									*)
(* ---------------------------------------------------------------------*)

let rec BETAS fnn body =
 if (is_var body) or (is_const body) then REFL else
 if (is_abs body) then ABS_CONV (BETAS fnn (snd (dest_abs body)))
 else let (ratorx,randx) = dest_comb body
      in if ratorx = fnn then BETA_CONV
         else let cnv1 = BETAS fnn ratorx
                  and cnv2 = BETAS fnn randx
                  in let f (ratorx,randx) = (cnv1 ratorx, cnv2 randx)
              in MK_COMB o (f o dest_comb)

(* ---------------------------------------------------------------------*)
(* Internal function: GTAC						*)
(*									*)
(*   !x. tm[x]  							*)
(*  ------------  GTAC "y"   (primes the "y" if necessary).		*)
(*     tm[y]								*)
(*									*)
(* NB: the x is always a genvar, so optimized for this case.		*)
(* ---------------------------------------------------------------------*)
and
let GTAC y (A,g) =
   let (bvarx,bodyx) = dest_forall g
       and y' = Term.variant (freesl (g::A)) y
   in ([(A, subst[(bvarx,y')] bodyx)],
   fun [th] -> GEN bvarx (INST [(y', bvarx)] th))

(* ---------------------------------------------------------------------*)
(* Internal function: TACF						*)
(*									*)
(* TACF is used to generate the subgoals for each case in an inductive 	*)
(* proof.  The argument tm is formula which states one generalized	*)
(* case in the induction. For example, the induction theorem for num is:*)
(*									*)
(*   |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n			*)
(*									*)
(* In this case, the argument tm will be one of:			*)
(*									*)
(*   1:  "P 0"   or   2: !n. P n ==> P(SUC n)				*)
(*   									*)
(* TACF applied to each these terms to construct a parameterized tactic *)
(* which will be used to further break these terms into subgoals.  The  *)
(* resulting tactic takes a variable name x and a user supplied theorem *)
(* continuation ttac.  For a base case, like case 1 above, the resulting*)
(* tactic just throws these parameters away and passes the goal on 	*)
(* unchanged (i.e. \x ttac. ALL_TAC).  For a step case, like case 2, the*)
(* tactic applies GTAC x as many times as required.  It then strips off *)
(* the induction hypotheses and applies ttac to each one.  For example, *)
(* if tac is the tactic generated by:					*)
(*									*)
(*    TACF "!n. P n ==> P(SUC n)" "x:num" ASSUME_TAC			*)
(*									*)
(* then applying tac to the goal A,"!n. P[n] ==> P[SUC n] has the same 	*)
(* effect as applying:							*)
(*									*)
(*    GTAC "x:num" THEN DISCH_THEN ASSUME_TAC				*)
(*									*)
(* TACF is a strictly local function, used only to define TACS, below.	*)
(* ---------------------------------------------------------------------*)
and
let rec ctacs tm =
       if (is_conj tm)
       then let tac2 = ctacs (snd(dest_conj tm))
            in fun ttac -> CONJUNCTS_THEN2 ttac (tac2 ttac)
       else I
in
let TACF tm =
 let (vs,body) = strip_forall tm
 in if (is_imp body)
    then (let TTAC = ctacs (fst(dest_imp body))
         in fun x ttac ->
              MAP_EVERY (GTAC o K x) vs THEN DISCH_THEN (TTAC ttac))
    else (fun x ttac -> ALL_TAC)

(* ---------------------------------------------------------------------*)
(* Internal function: TACS						*)
(*									*)
(* TACS uses TACF to generate a parameterized list of tactics, one for  *)
(* each conjunct in the hypothesis of an induction theorem.		*)
(*									*)
(* For example, if tm is the hypothesis of the induction theorem for the*)
(* natural numbers---i.e. if:						*)
(*									*)
(*   tm = "P 0 /\ (!n. P n ==> P(SUC n))"				*)
(*									*)
(* then TACS tm yields the parameterized list of tactics:		*)
(*									*)
(*   \x ttac. [TACF "P 0" x ttac; TACF "!n. P n ==> P(SUC n)" x ttac]   *)
(*									*)
(* TACS is a strictly local function, used only in INDUCT_THEN.		*)
(* ---------------------------------------------------------------------*)

fun f (conj1,conj2) = (TACF conj1, TACS conj2)
and TACS tm =
  let val (cf,csf) = f(dest_conj tm) handle HOL_ERR _ => (TACF tm, K(K[]))
  in fn x => fn ttac => cf x ttac::csf x ttac
  end;

(* ---------------------------------------------------------------------*)
(* Internal function: GOALS						*)
(*									*)
(* GOALS generates the subgoals (and proof functions) for all the cases *)
(* in an induction. The argument A is the common assumption list for all*)
(* the goals, and tacs is a list of tactics used to generate subgoals 	*)
(* from these goals.							*)
(*									*)
(* GOALS is a strictly local function, used only in INDUCT_THEN.	*)
(* ---------------------------------------------------------------------*)

fun GOALS A [] tm = raise ERR "GOALS" "empty list"
  | GOALS A [t] tm = let val (sg,pf) = t (A,tm) in ([sg],[pf]) end
  | GOALS A (h::t) tm =
      let val (conj1,conj2) = dest_conj tm
          val (sgs,pfs) = GOALS A t conj2
          val (sg,pf) = h (A,conj1)
      in (sg::sgs, pf::pfs)
      end;

(* --------------------------------------------------------------------- *)
(* Internal function: GALPH						*)
(* 									*)
(* GALPH "!x1 ... xn. A ==> B":   alpha-converts the x's to genvars.	*)
(* --------------------------------------------------------------------- *)

local fun rule v =
       let val gv = genvar(type_of v)
       in fn eq => let val th = FORALL_EQ v eq
                   in TRANS th (GEN_ALPHA_CONV gv (rhs(concl th)))
                   end
       end
in
fun GALPH tm =
   let val (vs,hy) = strip_forall tm
   in if (is_imp hy) then Lib.itlist rule vs (REFL hy) else REFL tm
   end
end;

(* ---------------------------------------------------------------------*)
(* Internal function: GALPHA						*)
(* 									*)
(* Applies the conversion GALPH to each conjunct in a sequence.		*)
(* ---------------------------------------------------------------------*)

fun f (conj1,conj2) = (GALPH conj1, GALPHA conj2)
and GALPHA tm =
   let val (c,cs) = f(dest_conj tm)
   in MK_COMB(AP_TERM boolSyntax.conjunction c, cs)
   end handle HOL_ERR _ => GALPH tm


(* ---------------------------------------------------------------------*)
(* Internal function: mapshape						*)
(* 									*)
(* Applies the functions in fl to argument lists obtained by splitting  *)
(* the list l into sublists of lengths given by nl.			*)
(* ---------------------------------------------------------------------*)

fun mapshape [] _ _ =  [] |
    mapshape (n1::nums) (f1::funcs) args =
       let val (f1_args,args') = Lib.split_after n1 args
       in f1 f1_args :: mapshape nums funcs args'
       end;

(* --------------------------------------------------------------------- *)
(* INDUCT_THEN : general induction tactic for concrete recursive types.	 *)
(* --------------------------------------------------------------------- *)

local val boolvar = genvar Type.bool
in
fun INDUCT_THEN th =
 let val (Bvar,Body) = dest_forall(concl th)
     val (hy,_) = dest_imp Body
     val bconv = BETAS Bvar hy
     val tacsf = TACS hy
     val v = genvar (type_of Bvar)
     val eta_th = CONV_RULE (RAND_CONV ETA_CONV) (UNDISCH(SPEC v th))
     val ([asm],con) = dest_thm eta_th
     val ind = GEN v (SUBST [boolvar |-> GALPHA asm]
                            (mk_imp(boolvar, con))
                            (DISCH asm eta_th))
 in fn ttac => fn (A,t) =>
     let val lam = snd(dest_comb t)
         val spec = SPEC lam (INST_TYPE (Lib.snd(Term.match_term v lam)) ind)
         val (ant,conseq) = dest_imp(concl spec)
         val beta = SUBST [boolvar |-> bconv ant]
                          (mk_imp(boolvar, conseq)) spec
         val tacs = tacsf (fst(dest_abs lam)) ttac
         val (gll,pl) = GOALS A tacs (fst(dest_imp(concl beta)))
         val pf = ((MP beta) o LIST_CONJ) o mapshape(map length gll)pl
     in
       (Lib.flatten gll, pf)
     end
     handle e => raise wrap_exn "Prim_rec" "INDUCT_THEN" e
 end
 handle e => raise wrap_exn "Prim_rec" "INDUCT_THEN" e
end;
