src/Provers/ind.ML
changeset 0 a5a9c433f639
child 1512 ce37c64244c0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Provers/ind.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +(*  Title: 	Provers/ind
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Tobias Nipkow
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Generic induction package -- for use with simplifier
    1.10 +*)
    1.11 +
    1.12 +signature IND_DATA =
    1.13 +  sig
    1.14 +  val spec: thm (* All(?P) ==> ?P(?a) *)
    1.15 +  end;
    1.16 +
    1.17 +
    1.18 +signature IND =
    1.19 +  sig
    1.20 +  val all_frees_tac: string -> int -> tactic
    1.21 +  val ALL_IND_TAC: thm -> (int -> tactic) -> (int -> tactic)
    1.22 +  val IND_TAC: thm -> (int -> tactic) -> string -> (int -> tactic)
    1.23 +  end;
    1.24 +
    1.25 +
    1.26 +functor InductionFun(Ind_Data: IND_DATA):IND =
    1.27 +struct
    1.28 +local open Ind_Data in
    1.29 +
    1.30 +val _$(_$Var(a_ixname,aT)) = concl_of spec;
    1.31 +val a_name = implode(tl(explode(Syntax.string_of_vname a_ixname)));
    1.32 +
    1.33 +fun add_term_frees tsig =
    1.34 +let fun add(tm, vars) = case tm of
    1.35 +	Free(v,T) => if Type.typ_instance(tsig,T,aT) then v ins vars
    1.36 +		     else vars
    1.37 +      | Abs (_,_,body) => add(body,vars)
    1.38 +      | rator$rand => add(rator, add(rand, vars))
    1.39 +      | _ => vars
    1.40 +in add end;
    1.41 +
    1.42 +
    1.43 +fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
    1.44 +
    1.45 +(*Generalizes over all free variables, with the named var outermost.*)
    1.46 +fun all_frees_tac (var:string) i = Tactic(fn thm =>
    1.47 +    let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
    1.48 +        val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
    1.49 +        val frees' = sort(op>)(frees \ var) @ [var]
    1.50 +    in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);
    1.51 +
    1.52 +fun REPEAT_SIMP_TAC simp_tac n i =
    1.53 +let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac
    1.54 +	let val k = length(prems_of thm)
    1.55 +	in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac
    1.56 +	end, thm)
    1.57 +in Tactic repeat end;
    1.58 +
    1.59 +fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(
    1.60 +	resolve_tac [sch] i THEN
    1.61 +	REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));
    1.62 +
    1.63 +fun IND_TAC sch simp_tac var =
    1.64 +	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
    1.65 +
    1.66 +
    1.67 +end
    1.68 +end;