TFL/rules.sig
author paulson
Thu May 22 15:13:16 1997 +0200 (1997-05-22)
changeset 3302 404fe31fd8d2
parent 3245 241838c01caf
child 3353 9112a2efb9a3
permissions -rw-r--r--
New headers and other minor changes
     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   type 'a binding
    13 
    14   val dest_thm : thm -> term list * term
    15 
    16   (* Inference rules *)
    17   val REFL      :cterm -> thm
    18   val ASSUME    :cterm -> thm
    19   val MP        :thm -> thm -> thm
    20   val MATCH_MP  :thm -> thm -> thm
    21   val CONJUNCT1 :thm -> thm
    22   val CONJUNCT2 :thm -> thm
    23   val CONJUNCTS :thm -> thm list
    24   val DISCH     :cterm -> thm -> thm
    25   val UNDISCH   :thm  -> thm
    26   val INST_TYPE :typ binding list -> thm -> thm
    27   val SPEC      :cterm -> thm -> thm
    28   val ISPEC     :cterm -> thm -> thm
    29   val ISPECL    :cterm list -> thm -> thm
    30   val GEN       :cterm -> thm -> thm
    31   val GENL      :cterm list -> thm -> thm
    32   val LIST_CONJ :thm list -> thm
    33 
    34   val SYM : thm -> thm
    35   val DISCH_ALL : thm -> thm
    36   val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
    37   val SPEC_ALL  : thm -> thm
    38   val GEN_ALL   : thm -> thm
    39   val IMP_TRANS : thm -> thm -> thm
    40   val PROVE_HYP : thm -> thm -> thm
    41 
    42   val CHOOSE : cterm * thm -> thm -> thm
    43   val EXISTS : cterm * cterm -> thm -> thm
    44   val EXISTL : cterm list -> thm -> thm
    45   val IT_EXISTS : cterm binding list -> thm -> thm
    46 
    47   val EVEN_ORS : thm list -> thm list
    48   val DISJ_CASESL : thm -> thm list -> thm
    49 
    50   val SUBS : thm list -> thm -> thm
    51   val simplify : thm list -> thm -> thm
    52   val simpl_conv : thm list -> cterm -> thm
    53 
    54 (* For debugging my isabelle solver in the conditional rewriter *)
    55 (*
    56   val term_ref : term list ref
    57   val thm_ref : thm list ref
    58   val mss_ref : meta_simpset list ref
    59   val tracing :bool ref
    60 *)
    61   val CONTEXT_REWRITE_RULE : term * term
    62                              -> {thms:thm list,congs: thm list, th:thm} 
    63                              -> thm * term list
    64   val RIGHT_ASSOC : thm -> thm 
    65 
    66   val prove : cterm * tactic -> thm
    67 end;