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(i-1,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;
|