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