--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/ind.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,65 @@
+(* Title: Provers/ind
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1991 University of Cambridge
+
+Generic induction package -- for use with simplifier
+*)
+
+signature IND_DATA =
+ sig
+ val spec: thm (* All(?P) ==> ?P(?a) *)
+ end;
+
+
+signature IND =
+ sig
+ val all_frees_tac: string -> int -> tactic
+ val ALL_IND_TAC: thm -> (int -> tactic) -> (int -> tactic)
+ val IND_TAC: thm -> (int -> tactic) -> string -> (int -> tactic)
+ end;
+
+
+functor InductionFun(Ind_Data: IND_DATA):IND =
+struct
+local open Ind_Data in
+
+val _$(_$Var(a_ixname,aT)) = concl_of spec;
+val a_name = implode(tl(explode(Syntax.string_of_vname a_ixname)));
+
+fun add_term_frees tsig =
+let fun add(tm, vars) = case tm of
+ Free(v,T) => if Type.typ_instance(tsig,T,aT) then v ins vars
+ else vars
+ | Abs (_,_,body) => add(body,vars)
+ | rator$rand => add(rator, add(rand, vars))
+ | _ => vars
+in add end;
+
+
+fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
+
+(*Generalizes over all free variables, with the named var outermost.*)
+fun all_frees_tac (var:string) i = Tactic(fn thm =>
+ let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
+ val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
+ val frees' = sort(op>)(frees \ var) @ [var]
+ in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);
+
+fun REPEAT_SIMP_TAC simp_tac n i =
+let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac
+ let val k = length(prems_of thm)
+ in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac
+ end, thm)
+in Tactic repeat end;
+
+fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(
+ resolve_tac [sch] i THEN
+ REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));
+
+fun IND_TAC sch simp_tac var =
+ all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
+
+
+end
+end;