src/Provers/ind.ML
author haftmann
Wed Oct 04 14:17:38 2006 +0200 (2006-10-04)
changeset 20854 f9cf9e62d11c
parent 20344 d02b43ea722e
permissions -rw-r--r--
insert replacing ins ins_int ins_string
     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 
    29 fun add_term_frees thy =
    30 let fun add(tm, vars) = case tm of
    31 	Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars
    32 		     else vars
    33       | Abs (_,_,body) => add(body,vars)
    34       | rator$rand => add(rator, add(rand, vars))
    35       | _ => vars
    36 in add end;
    37 
    38 
    39 fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i;
    40 
    41 (*Generalizes over all free variables, with the named var outermost.*)
    42 fun all_frees_tac (var:string) i thm = 
    43     let val frees = add_term_frees (Thm.theory_of_thm thm) (List.nth(prems_of thm,i-1),[var]);
    44         val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
    45     in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
    46 
    47 fun REPEAT_SIMP_TAC simp_tac n i =
    48 let fun repeat thm = 
    49         (COND (has_fewer_prems n) all_tac
    50 	 let val k = nprems_of thm
    51 	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
    52 	thm
    53 in repeat end;
    54 
    55 fun ALL_IND_TAC sch simp_tac i thm = 
    56 	(resolve_tac [sch] i THEN
    57 	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
    58 
    59 fun IND_TAC sch simp_tac var =
    60 	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
    61 
    62 
    63 end
    64 end;