src/Provers/ind.ML
changeset 0 a5a9c433f639
child 1512 ce37c64244c0
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     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(i-1,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;