author  ballarin 
Wed, 19 Jul 2006 19:25:58 +0200  
changeset 20168  ed7bced29e1b 
parent 19299  5f0610aafc48 
child 20344  d02b43ea722e 
permissions  rwrr 
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 

29 
fun add_term_frees tsig = 

30 
let fun add(tm, vars) = case tm of 

14772  31 
Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars 
0  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 

15462
b4208fbf9439
Eliminated hack for deleting leading question mark from induction
berghofe
parents:
14772
diff
changeset

39 
fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i; 
0  40 

41 
(*Generalizes over all free variables, with the named var outermost.*) 

1512  42 
fun all_frees_tac (var:string) i thm = 
14643  43 
let val tsig = Sign.tsig_of (Thm.sign_of_thm thm); 
15570  44 
val frees = add_term_frees tsig (List.nth(prems_of thm,i1),[var]); 
19299  45 
val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var] 
15570  46 
in Library.foldl (qnt_tac i) (all_tac,frees') thm end; 
0  47 

48 
fun REPEAT_SIMP_TAC simp_tac n i = 

1512  49 
let fun repeat thm = 
50 
(COND (has_fewer_prems n) all_tac 

51 
let val k = nprems_of thm 

52 
in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end) 

53 
thm 

54 
in repeat end; 

0  55 

1512  56 
fun ALL_IND_TAC sch simp_tac i thm = 
57 
(resolve_tac [sch] i THEN 

58 
REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm; 

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