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