TFL/tfl.sig
changeset 6498 1ebbe18fe236
parent 3459 112cbb8301dc
child 8622 870a58dd0ddd
equal deleted inserted replaced
6497:120ca2bb27e1 6498:1ebbe18fe236
     6 Main module
     6 Main module
     7 *)
     7 *)
     8 
     8 
     9 signature TFL_sig =
     9 signature TFL_sig =
    10 sig
    10 sig
       
    11 
       
    12    val trace : bool ref
       
    13 
       
    14    val default_simps : thm list      (*simprules used for deriving rules...*)
       
    15 
       
    16    val congs : thm list -> thm list  (*fn to make congruent rules*)
       
    17 
    11    datatype pattern = GIVEN of term * int
    18    datatype pattern = GIVEN of term * int
    12                     | OMITTED of term * int
    19                     | OMITTED of term * int
    13 
    20 
    14    val mk_functional : theory -> term list
    21    val mk_functional : theory -> term list
    15                        -> {functional:term,
    22                        -> {functional:term,
    16                            pats: pattern list}
    23                            pats: pattern list}
    17 
    24 
    18    val wfrec_definition0 : theory -> string -> term -> term -> theory
    25    val wfrec_definition0 : theory -> string -> term -> term -> theory
    19 
    26 
    20    val post_definition : simpset * thm list -> theory * (thm * pattern list)
    27    val post_definition : thm list -> theory * (thm * pattern list)
    21 				 -> {theory : theory,
    28 				  -> {theory : theory,
    22 				     rules  : thm, 
    29 				     rules  : thm, 
    23 				       TCs  : term list list,
    30 				       TCs  : term list list,
    24 			     full_pats_TCs  : (term * term list) list, 
    31 			     full_pats_TCs  : (term * term list) list, 
    25 				  patterns  : pattern list}
    32 				  patterns  : pattern list}
    26 
    33 
    27 (*CURRENTLY UNUSED
    34    val wfrec_eqns : theory -> xstring
    28    val wfrec_eqns : simpset * thm list -> theory -> term list
    35 	             -> thm list (* congruence rules *)
    29                      -> {WFR : term, 
    36                      -> term list
       
    37                      -> {WFR : term,  SV : term list,
    30                          proto_def : term,
    38                          proto_def : term,
    31                          extracta :(thm * term list) list,
    39                          extracta :(thm * term list) list,
    32                          pats  : pattern list}
    40                          pats  : pattern list}
    33 
    41 
    34    val lazyR_def : theory
    42    val lazyR_def : theory -> xstring
       
    43 	           -> thm list (* congruence rules *)
    35                    -> term list
    44                    -> term list
    36                    -> {theory:theory,
    45                    -> {theory : theory,
    37                        rules :thm,
    46                        rules : thm,
    38                            R :term,
    47                        R : term, 
    39                        full_pats_TCs :(term * term list) list, 
    48                        SV : term list,
    40                        patterns: pattern list}
    49                        full_pats_TCs : (term * term list) list, 
    41 ---------------------*)
    50                        patterns : pattern list}
    42 
    51 
    43    val mk_induction : theory -> term -> term -> (term * term list) list -> thm
    52    val mk_induction : theory 
       
    53                        -> {fconst:term,
       
    54                            R : term,
       
    55                            SV : term list,
       
    56                            pat_TCs_list : (term * term list) list}
       
    57                        -> thm
    44 
    58 
    45    val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
    59    val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
    46                      -> theory 
    60                      -> theory 
    47                       -> {rules:thm, induction:thm, TCs:term list list}
    61                       -> {rules:thm, induction:thm, TCs:term list list}
    48                        -> {rules:thm, induction:thm, nested_tcs:thm list}
    62                        -> {rules:thm, induction:thm, nested_tcs:thm list}