|
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; |