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.*)

1512

43 
fun all_frees_tac (var:string) i thm =

0

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]

1512

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

0

48 


49 
fun REPEAT_SIMP_TAC simp_tac n i =

1512

50 
let fun repeat thm =


51 
(COND (has_fewer_prems n) all_tac


52 
let val k = nprems_of thm


53 
in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)


54 
thm


55 
in repeat end;

0

56 

1512

57 
fun ALL_IND_TAC sch simp_tac i thm =


58 
(resolve_tac [sch] i THEN


59 
REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;

0

60 


61 
fun IND_TAC sch simp_tac var =


62 
all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;


63 


64 


65 
end


66 
end;
