src/Provers/ind.ML
author wenzelm
Wed Apr 04 00:11:03 2007 +0200 (2007-04-04)
changeset 22578 b0eb5652f210
parent 20854 f9cf9e62d11c
permissions -rw-r--r--
removed obsolete sign_of/sign_of_thm;
clasohm@0
     1
(*  Title: 	Provers/ind
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Tobias Nipkow
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Generic induction package -- for use with simplifier
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
signature IND_DATA =
clasohm@0
    10
  sig
clasohm@0
    11
  val spec: thm (* All(?P) ==> ?P(?a) *)
clasohm@0
    12
  end;
clasohm@0
    13
clasohm@0
    14
clasohm@0
    15
signature IND =
clasohm@0
    16
  sig
clasohm@0
    17
  val all_frees_tac: string -> int -> tactic
clasohm@0
    18
  val ALL_IND_TAC: thm -> (int -> tactic) -> (int -> tactic)
clasohm@0
    19
  val IND_TAC: thm -> (int -> tactic) -> string -> (int -> tactic)
clasohm@0
    20
  end;
clasohm@0
    21
clasohm@0
    22
clasohm@0
    23
functor InductionFun(Ind_Data: IND_DATA):IND =
clasohm@0
    24
struct
clasohm@0
    25
local open Ind_Data in
clasohm@0
    26
clasohm@0
    27
val _$(_$Var(a_ixname,aT)) = concl_of spec;
clasohm@0
    28
wenzelm@20344
    29
fun add_term_frees thy =
clasohm@0
    30
let fun add(tm, vars) = case tm of
haftmann@20854
    31
	Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars
clasohm@0
    32
		     else vars
clasohm@0
    33
      | Abs (_,_,body) => add(body,vars)
clasohm@0
    34
      | rator$rand => add(rator, add(rand, vars))
clasohm@0
    35
      | _ => vars
clasohm@0
    36
in add end;
clasohm@0
    37
clasohm@0
    38
berghofe@15462
    39
fun qnt_tac i = fn (tac,var) => tac THEN Tactic.res_inst_tac' [(a_ixname,var)] spec i;
clasohm@0
    40
clasohm@0
    41
(*Generalizes over all free variables, with the named var outermost.*)
paulson@1512
    42
fun all_frees_tac (var:string) i thm = 
wenzelm@20344
    43
    let val frees = add_term_frees (Thm.theory_of_thm thm) (List.nth(prems_of thm,i-1),[var]);
wenzelm@19299
    44
        val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
skalberg@15570
    45
    in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
clasohm@0
    46
clasohm@0
    47
fun REPEAT_SIMP_TAC simp_tac n i =
paulson@1512
    48
let fun repeat thm = 
paulson@1512
    49
        (COND (has_fewer_prems n) all_tac
paulson@1512
    50
	 let val k = nprems_of thm
paulson@1512
    51
	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
paulson@1512
    52
	thm
paulson@1512
    53
in repeat end;
clasohm@0
    54
paulson@1512
    55
fun ALL_IND_TAC sch simp_tac i thm = 
paulson@1512
    56
	(resolve_tac [sch] i THEN
paulson@1512
    57
	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
clasohm@0
    58
clasohm@0
    59
fun IND_TAC sch simp_tac var =
clasohm@0
    60
	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
clasohm@0
    61
clasohm@0
    62
clasohm@0
    63
end
clasohm@0
    64
end;