TFL/rules.sig
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
     1 signature Rules_sig =
     2 sig
     3 (*  structure USyntax : USyntax_sig *)
     4   type Type
     5   type Preterm
     6   type Term
     7   type Thm
     8   type Tactic
     9   type 'a binding
    10 
    11   val dest_thm : Thm -> Preterm list * Preterm
    12 
    13   (* Inference rules *)
    14   val REFL      :Term -> Thm
    15   val ASSUME    :Term -> Thm
    16   val MP        :Thm -> Thm -> Thm
    17   val MATCH_MP  :Thm -> Thm -> Thm
    18   val CONJUNCT1 :Thm -> Thm
    19   val CONJUNCT2 :Thm -> Thm
    20   val CONJUNCTS :Thm -> Thm list
    21   val DISCH     :Term -> Thm -> Thm
    22   val UNDISCH   :Thm  -> Thm
    23   val INST_TYPE :Type binding list -> Thm -> Thm
    24   val SPEC      :Term -> Thm -> Thm
    25   val ISPEC     :Term -> Thm -> Thm
    26   val ISPECL    :Term list -> Thm -> Thm
    27   val GEN       :Term -> Thm -> Thm
    28   val GENL      :Term list -> Thm -> Thm
    29   val BETA_RULE :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 : (Preterm -> 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 : Term * Thm -> Thm -> Thm
    41   val EXISTS : Term * Term -> Thm -> Thm
    42   val EXISTL : Term list -> Thm -> Thm
    43   val IT_EXISTS : Term binding 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 -> Term -> Thm
    51 
    52 (* For debugging my isabelle solver in the conditional rewriter *)
    53 (*
    54   val term_ref : Preterm list ref
    55   val thm_ref : Thm list ref
    56   val mss_ref : meta_simpset list ref
    57   val tracing :bool ref
    58 *)
    59   val CONTEXT_REWRITE_RULE : Preterm * Preterm
    60                              -> {thms:Thm list,congs: Thm list, th:Thm} 
    61                              -> Thm * Preterm list
    62   val RIGHT_ASSOC : Thm -> Thm 
    63 
    64   val prove : Term * Tactic -> Thm
    65 end;