src/Provers/ind.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 0 a5a9c433f639
child 4452 b2ee34200dab
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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 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 foldl (qnt_tac i) (all_tac,frees') thm end;
    48 
    49 fun REPEAT_SIMP_TAC simp_tac n i =
    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;
    56 
    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;
    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;