0

1 
(* Title: Provers/ind


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1991 University of Cambridge


5 


6 
Generic induction package  for use with simplifier


7 
*)


8 


9 
signature IND_DATA =


10 
sig


11 
val spec: thm (* All(?P) ==> ?P(?a) *)


12 
end;


13 


14 


15 
signature IND =


16 
sig


17 
val all_frees_tac: string > int > tactic


18 
val ALL_IND_TAC: thm > (int > tactic) > (int > tactic)


19 
val IND_TAC: thm > (int > tactic) > string > (int > tactic)


20 
end;


21 


22 


23 
functor InductionFun(Ind_Data: IND_DATA):IND =


24 
struct


25 
local open Ind_Data in


26 


27 
val _$(_$Var(a_ixname,aT)) = concl_of spec;


28 
val a_name = implode(tl(explode(Syntax.string_of_vname a_ixname)));


29 


30 
fun add_term_frees tsig =


31 
let fun add(tm, vars) = case tm of


32 
Free(v,T) => if Type.typ_instance(tsig,T,aT) then v ins vars


33 
else vars


34 
 Abs (_,_,body) => add(body,vars)


35 
 rator$rand => add(rator, add(rand, vars))


36 
 _ => vars


37 
in add end;


38 


39 


40 
fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;


41 


42 
(*Generalizes over all free variables, with the named var outermost.*)


43 
fun all_frees_tac (var:string) i = Tactic(fn thm =>


44 
let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));


45 
val frees = add_term_frees tsig (nth_elem(i1,prems_of thm),[var]);


46 
val frees' = sort(op>)(frees \ var) @ [var]


47 
in tapply(foldl (qnt_tac i) (all_tac,frees'), thm) end);


48 


49 
fun REPEAT_SIMP_TAC simp_tac n i =


50 
let fun repeat thm = tapply(COND (has_fewer_prems n) all_tac


51 
let val k = length(prems_of thm)


52 
in simp_tac i THEN COND (has_fewer_prems k) (Tactic repeat) all_tac


53 
end, thm)


54 
in Tactic repeat end;


55 


56 
fun ALL_IND_TAC sch simp_tac i = Tactic(fn thm => tapply(


57 
resolve_tac [sch] i THEN


58 
REPEAT_SIMP_TAC simp_tac (length(prems_of thm)) i, thm));


59 


60 
fun IND_TAC sch simp_tac var =


61 
all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;


62 


63 


64 
end


65 
end;
