TFL/tfl.sig
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
signature TFL_sig =
paulson@2112
     2
sig
paulson@2112
     3
   structure Rules: Rules_sig
paulson@2112
     4
   structure Thms : Thms_sig
paulson@2112
     5
   structure Thry : Thry_sig
paulson@2112
     6
   structure USyntax : USyntax_sig
paulson@2112
     7
paulson@2112
     8
   type Preterm
paulson@2112
     9
   type Term
paulson@2112
    10
   type Thm
paulson@2112
    11
   type Thry
paulson@2112
    12
   type Tactic
paulson@2112
    13
   
paulson@2112
    14
   datatype pattern = GIVEN of Preterm * int
paulson@2112
    15
                    | OMITTED of Preterm * int
paulson@2112
    16
paulson@2112
    17
   val mk_functional : Thry -> Preterm
paulson@2112
    18
                       -> {functional:Preterm,
paulson@2112
    19
                           pats: pattern list}
paulson@2112
    20
paulson@2112
    21
   val prim_wfrec_definition : Thry 
paulson@2112
    22
                                -> {R:Preterm, functional:Preterm}
paulson@2112
    23
                                -> {def:Thm, corollary:Thm, theory:Thry}
paulson@2112
    24
paulson@2112
    25
   val wfrec_eqns : Thry -> Preterm
paulson@2112
    26
                     -> {WFR : Preterm, 
paulson@2112
    27
                         proto_def : Preterm,
paulson@2112
    28
                         extracta :(Thm * Preterm list) list,
paulson@2112
    29
                         pats  : pattern list}
paulson@2112
    30
paulson@2112
    31
paulson@2112
    32
   val gen_wfrec_definition : Thry 
paulson@2112
    33
                               -> {R:Preterm, eqs:Preterm}
paulson@2112
    34
                               -> {theory:Thry,
paulson@2112
    35
                                   rules :Thm, 
paulson@2112
    36
                                     TCs : Preterm list list,
paulson@2112
    37
                           full_pats_TCs :(Preterm * Preterm list) list, 
paulson@2112
    38
                                   patterns : pattern list}
paulson@2112
    39
paulson@2112
    40
   val lazyR_def : Thry
paulson@2112
    41
                   -> Preterm
paulson@2112
    42
                   -> {theory:Thry,
paulson@2112
    43
                       rules :Thm,
paulson@2112
    44
                           R :Preterm,
paulson@2112
    45
                       full_pats_TCs :(Preterm * Preterm list) list, 
paulson@2112
    46
                       patterns: pattern list}
paulson@2112
    47
paulson@2112
    48
   val mk_induction : Thry 
paulson@2112
    49
                       -> Preterm -> Preterm 
paulson@2112
    50
                         -> (Preterm * Preterm list) list
paulson@2112
    51
                           -> Thm
paulson@2112
    52
paulson@2112
    53
   val postprocess: {WFtac:Tactic, terminator:Tactic, simplifier:Term -> Thm}
paulson@2112
    54
                     -> Thry 
paulson@2112
    55
                      -> {rules:Thm, induction:Thm, TCs:Preterm list list}
paulson@2112
    56
                       -> {rules:Thm, induction:Thm, nested_tcs:Thm list}
paulson@2112
    57
paulson@2112
    58
   val termination_goals : Thm -> Preterm list
paulson@2112
    59
paulson@2112
    60
   structure Context
paulson@2112
    61
     : sig
paulson@2112
    62
         val read : unit -> Thm list
paulson@2112
    63
         val write : Thm list -> unit
paulson@2112
    64
       end
paulson@2112
    65
end;