diff -r 000000000000 -r a5a9c433f639 src/Provers/ind.ML
--- /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;