src/Provers/ind.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 0 a5a9c433f639
child 4452 b2ee34200dab
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
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
val a_name = implode(tl(explode(Syntax.string_of_vname a_ixname)));
clasohm@0
    29
clasohm@0
    30
fun add_term_frees tsig =
clasohm@0
    31
let fun add(tm, vars) = case tm of
clasohm@0
    32
	Free(v,T) => if Type.typ_instance(tsig,T,aT) then v ins vars
clasohm@0
    33
		     else vars
clasohm@0
    34
      | Abs (_,_,body) => add(body,vars)
clasohm@0
    35
      | rator$rand => add(rator, add(rand, vars))
clasohm@0
    36
      | _ => vars
clasohm@0
    37
in add end;
clasohm@0
    38
clasohm@0
    39
clasohm@0
    40
fun qnt_tac i = fn (tac,var) => tac THEN res_inst_tac [(a_name,var)] spec i;
clasohm@0
    41
clasohm@0
    42
(*Generalizes over all free variables, with the named var outermost.*)
paulson@1512
    43
fun all_frees_tac (var:string) i thm = 
clasohm@0
    44
    let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
clasohm@0
    45
        val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
clasohm@0
    46
        val frees' = sort(op>)(frees \ var) @ [var]
paulson@1512
    47
    in foldl (qnt_tac i) (all_tac,frees') thm end;
clasohm@0
    48
clasohm@0
    49
fun REPEAT_SIMP_TAC simp_tac n i =
paulson@1512
    50
let fun repeat thm = 
paulson@1512
    51
        (COND (has_fewer_prems n) all_tac
paulson@1512
    52
	 let val k = nprems_of thm
paulson@1512
    53
	 in simp_tac i THEN COND (has_fewer_prems k) repeat all_tac end)
paulson@1512
    54
	thm
paulson@1512
    55
in repeat end;
clasohm@0
    56
paulson@1512
    57
fun ALL_IND_TAC sch simp_tac i thm = 
paulson@1512
    58
	(resolve_tac [sch] i THEN
paulson@1512
    59
	 REPEAT_SIMP_TAC simp_tac (nprems_of thm) i) thm;
clasohm@0
    60
clasohm@0
    61
fun IND_TAC sch simp_tac var =
clasohm@0
    62
	all_frees_tac var THEN' ALL_IND_TAC sch simp_tac;
clasohm@0
    63
clasohm@0
    64
clasohm@0
    65
end
clasohm@0
    66
end;