TFL/tfl.sig
changeset 3245 241838c01caf
parent 3191 14bd6e5985f1
child 3302 404fe31fd8d2
equal deleted inserted replaced
3244:71b760618f30 3245:241838c01caf
     3    structure Rules: Rules_sig
     3    structure Rules: Rules_sig
     4    structure Thms : Thms_sig
     4    structure Thms : Thms_sig
     5    structure Thry : Thry_sig
     5    structure Thry : Thry_sig
     6    structure USyntax : USyntax_sig
     6    structure USyntax : USyntax_sig
     7 
     7 
     8    type Preterm
     8    datatype pattern = GIVEN of term * int
     9    type Term
     9                     | OMITTED of term * int
    10    type Thm
       
    11    type Thry
       
    12    type Tactic
       
    13    
       
    14    datatype pattern = GIVEN of Preterm * int
       
    15                     | OMITTED of Preterm * int
       
    16 
    10 
    17    val mk_functional : Thry -> Preterm
    11    val mk_functional : theory -> term
    18                        -> {functional:Preterm,
    12                        -> {functional:term,
    19                            pats: pattern list}
    13                            pats: pattern list}
    20 
    14 
    21    val wfrec_definition0 : Thry -> Preterm -> Preterm -> Thm * Thry
    15    val wfrec_definition0 : theory -> term -> term -> thm * theory
    22 
    16 
    23    val post_definition : Thry * (Thm * pattern list)
    17    val post_definition : theory * (thm * pattern list)
    24                               -> {theory : Thry,
    18                               -> {theory : theory,
    25                                   rules  : Thm, 
    19                                   rules  : thm, 
    26                                     TCs  : Preterm list list,
    20                                     TCs  : term list list,
    27                           full_pats_TCs  : (Preterm * Preterm list) list, 
    21                           full_pats_TCs  : (term * term list) list, 
    28                                patterns  : pattern list}
    22                                patterns  : pattern list}
    29 
    23 
    30 
    24 
    31    val wfrec_eqns : Thry -> Preterm
    25    val wfrec_eqns : theory -> term
    32                      -> {WFR : Preterm, 
    26                      -> {WFR : term, 
    33                          proto_def : Preterm,
    27                          proto_def : term,
    34                          extracta :(Thm * Preterm list) list,
    28                          extracta :(thm * term list) list,
    35                          pats  : pattern list}
    29                          pats  : pattern list}
    36 
    30 
    37 
    31 
    38    val lazyR_def : Thry
    32    val lazyR_def : theory
    39                    -> Preterm
    33                    -> term
    40                    -> {theory:Thry,
    34                    -> {theory:theory,
    41                        rules :Thm,
    35                        rules :thm,
    42                            R :Preterm,
    36                            R :term,
    43                        full_pats_TCs :(Preterm * Preterm list) list, 
    37                        full_pats_TCs :(term * term list) list, 
    44                        patterns: pattern list}
    38                        patterns: pattern list}
    45 
    39 
    46    val mk_induction : Thry 
    40    val mk_induction : theory 
    47                        -> Preterm -> Preterm 
    41                        -> term -> term 
    48                          -> (Preterm * Preterm list) list
    42                          -> (term * term list) list
    49                            -> Thm
    43                            -> thm
    50 
    44 
    51    val postprocess: {WFtac:Tactic, terminator:Tactic, simplifier:Term -> Thm}
    45    val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
    52                      -> Thry 
    46                      -> theory 
    53                       -> {rules:Thm, induction:Thm, TCs:Preterm list list}
    47                       -> {rules:thm, induction:thm, TCs:term list list}
    54                        -> {rules:Thm, induction:Thm, nested_tcs:Thm list}
    48                        -> {rules:thm, induction:thm, nested_tcs:thm list}
    55 
    49 
    56    structure Context
    50    structure Context
    57      : sig
    51      : sig
    58          val read : unit -> Thm list
    52          val read : unit -> thm list
    59          val write : Thm list -> unit
    53          val write : thm list -> unit
    60        end
    54        end
    61 end;
    55 end;