TFL/rules.sig
author nipkow
Fri Oct 09 14:19:13 1998 +0200 (1998-10-09)
changeset 5633 fb7fa1b154c4
parent 3405 2cccd0e3e9ea
child 6498 1ebbe18fe236
permissions -rw-r--r--
Added a few breaks in error text.
     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 simpl_conv : simpset -> thm list -> cterm -> thm
    50 
    51 (* For debugging my isabelle solver in the conditional rewriter *)
    52   val term_ref : term list ref
    53   val thm_ref : thm list ref
    54   val mss_ref : meta_simpset list ref
    55   val tracing :bool ref
    56   val CONTEXT_REWRITE_RULE : simpset * term * term * thm * thm list 
    57                              -> thm -> thm * term list
    58   val RIGHT_ASSOC : thm -> thm 
    59 
    60   val prove : cterm * tactic -> thm
    61 end;