TFL/tfl.sig
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3459 112cbb8301dc
child 6498 1ebbe18fe236
permissions -rw-r--r--
tidying
     1 (*  Title:      TFL/tfl
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Main module
     7 *)
     8 
     9 signature TFL_sig =
    10 sig
    11    datatype pattern = GIVEN of term * int
    12                     | OMITTED of term * int
    13 
    14    val mk_functional : theory -> term list
    15                        -> {functional:term,
    16                            pats: pattern list}
    17 
    18    val wfrec_definition0 : theory -> string -> term -> term -> theory
    19 
    20    val post_definition : simpset * thm list -> theory * (thm * pattern list)
    21 				 -> {theory : theory,
    22 				     rules  : thm, 
    23 				       TCs  : term list list,
    24 			     full_pats_TCs  : (term * term list) list, 
    25 				  patterns  : pattern list}
    26 
    27 (*CURRENTLY UNUSED
    28    val wfrec_eqns : simpset * thm list -> theory -> term list
    29                      -> {WFR : term, 
    30                          proto_def : term,
    31                          extracta :(thm * term list) list,
    32                          pats  : pattern list}
    33 
    34    val lazyR_def : theory
    35                    -> term list
    36                    -> {theory:theory,
    37                        rules :thm,
    38                            R :term,
    39                        full_pats_TCs :(term * term list) list, 
    40                        patterns: pattern list}
    41 ---------------------*)
    42 
    43    val mk_induction : theory -> term -> term -> (term * term list) list -> thm
    44 
    45    val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
    46                      -> theory 
    47                       -> {rules:thm, induction:thm, TCs:term list list}
    48                        -> {rules:thm, induction:thm, nested_tcs:thm list}
    49 end;