TFL/rules.sig
author paulson
Fri May 30 15:55:27 1997 +0200 (1997-05-30)
changeset 3379 7091ffa99c93
parent 3353 9112a2efb9a3
child 3405 2cccd0e3e9ea
permissions -rw-r--r--
Simplified the calling sequence of CONTEXT_REWRITE_RULE
Eliminated get_rhs, which was calling dest_Trueprop too many times
     1 (*  Title:      TFL/rules
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Emulation of HOL inference rules for TFL
     7 *)
     8 
     9 signature Rules_sig =
    10 sig
    11 (*  structure USyntax : USyntax_sig *)
    12   val dest_thm : thm -> term list * term
    13 
    14   (* Inference rules *)
    15   val REFL      :cterm -> thm
    16   val ASSUME    :cterm -> thm
    17   val MP        :thm -> thm -> thm
    18   val MATCH_MP  :thm -> thm -> thm
    19   val CONJUNCT1 :thm -> thm
    20   val CONJUNCT2 :thm -> thm
    21   val CONJUNCTS :thm -> thm list
    22   val DISCH     :cterm -> thm -> thm
    23   val UNDISCH   :thm  -> thm
    24   val INST_TYPE :(typ*typ)list -> thm -> thm
    25   val SPEC      :cterm -> thm -> thm
    26   val ISPEC     :cterm -> thm -> thm
    27   val ISPECL    :cterm list -> thm -> thm
    28   val GEN       :cterm -> thm -> thm
    29   val GENL      :cterm list -> thm -> thm
    30   val LIST_CONJ :thm list -> thm
    31 
    32   val SYM : thm -> thm
    33   val DISCH_ALL : thm -> thm
    34   val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
    35   val SPEC_ALL  : thm -> thm
    36   val GEN_ALL   : thm -> thm
    37   val IMP_TRANS : thm -> thm -> thm
    38   val PROVE_HYP : thm -> thm -> thm
    39 
    40   val CHOOSE : cterm * thm -> thm -> thm
    41   val EXISTS : cterm * cterm -> thm -> thm
    42   val EXISTL : cterm list -> thm -> thm
    43   val IT_EXISTS : (cterm*cterm) list -> thm -> thm
    44 
    45   val EVEN_ORS : thm list -> thm list
    46   val DISJ_CASESL : thm -> thm list -> thm
    47 
    48   val SUBS : thm list -> thm -> thm
    49   val simplify : thm list -> thm -> thm
    50   val simpl_conv : thm list -> cterm -> thm
    51 
    52 (* For debugging my isabelle solver in the conditional rewriter *)
    53   val term_ref : term list ref
    54   val thm_ref : thm list ref
    55   val mss_ref : meta_simpset list ref
    56   val tracing :bool ref
    57   val CONTEXT_REWRITE_RULE : term * term
    58                              -> {cut_lemma:thm, congs: thm list, th:thm} 
    59                              -> thm * term list
    60   val RIGHT_ASSOC : thm -> thm 
    61 
    62   val prove : cterm * tactic -> thm
    63 end;