TFL/rules.sig
author paulson
Fri Oct 18 12:41:04 1996 +0200 (1996-10-18)
changeset 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
Konrad Slind's TFL
paulson@2112
     1
signature Rules_sig =
paulson@2112
     2
sig
paulson@2112
     3
(*  structure USyntax : USyntax_sig *)
paulson@2112
     4
  type Type
paulson@2112
     5
  type Preterm
paulson@2112
     6
  type Term
paulson@2112
     7
  type Thm
paulson@2112
     8
  type Tactic
paulson@2112
     9
  type 'a binding
paulson@2112
    10
paulson@2112
    11
  val dest_thm : Thm -> Preterm list * Preterm
paulson@2112
    12
paulson@2112
    13
  (* Inference rules *)
paulson@2112
    14
  val REFL      :Term -> Thm
paulson@2112
    15
  val ASSUME    :Term -> Thm
paulson@2112
    16
  val MP        :Thm -> Thm -> Thm
paulson@2112
    17
  val MATCH_MP  :Thm -> Thm -> Thm
paulson@2112
    18
  val CONJUNCT1 :Thm -> Thm
paulson@2112
    19
  val CONJUNCT2 :Thm -> Thm
paulson@2112
    20
  val CONJUNCTS :Thm -> Thm list
paulson@2112
    21
  val DISCH     :Term -> Thm -> Thm
paulson@2112
    22
  val UNDISCH   :Thm  -> Thm
paulson@2112
    23
  val INST_TYPE :Type binding list -> Thm -> Thm
paulson@2112
    24
  val SPEC      :Term -> Thm -> Thm
paulson@2112
    25
  val ISPEC     :Term -> Thm -> Thm
paulson@2112
    26
  val ISPECL    :Term list -> Thm -> Thm
paulson@2112
    27
  val GEN       :Term -> Thm -> Thm
paulson@2112
    28
  val GENL      :Term list -> Thm -> Thm
paulson@2112
    29
  val BETA_RULE :Thm -> Thm
paulson@2112
    30
  val LIST_CONJ :Thm list -> Thm
paulson@2112
    31
paulson@2112
    32
  val SYM : Thm -> Thm
paulson@2112
    33
  val DISCH_ALL : Thm -> Thm
paulson@2112
    34
  val FILTER_DISCH_ALL : (Preterm -> bool) -> Thm -> Thm
paulson@2112
    35
  val SPEC_ALL  : Thm -> Thm
paulson@2112
    36
  val GEN_ALL   : Thm -> Thm
paulson@2112
    37
  val IMP_TRANS : Thm -> Thm -> Thm
paulson@2112
    38
  val PROVE_HYP : Thm -> Thm -> Thm
paulson@2112
    39
paulson@2112
    40
  val CHOOSE : Term * Thm -> Thm -> Thm
paulson@2112
    41
  val EXISTS : Term * Term -> Thm -> Thm
paulson@2112
    42
  val EXISTL : Term list -> Thm -> Thm
paulson@2112
    43
  val IT_EXISTS : Term binding list -> Thm -> Thm
paulson@2112
    44
paulson@2112
    45
  val EVEN_ORS : Thm list -> Thm list
paulson@2112
    46
  val DISJ_CASESL : Thm -> Thm list -> Thm
paulson@2112
    47
paulson@2112
    48
  val SUBS : Thm list -> Thm -> Thm
paulson@2112
    49
  val simplify : Thm list -> Thm -> Thm
paulson@2112
    50
  val simpl_conv : Thm list -> Term -> Thm
paulson@2112
    51
paulson@2112
    52
(* For debugging my isabelle solver in the conditional rewriter *)
paulson@2112
    53
(*
paulson@2112
    54
  val term_ref : Preterm list ref
paulson@2112
    55
  val thm_ref : Thm list ref
paulson@2112
    56
  val mss_ref : meta_simpset list ref
paulson@2112
    57
  val tracing :bool ref
paulson@2112
    58
*)
paulson@2112
    59
  val CONTEXT_REWRITE_RULE : Preterm * Preterm
paulson@2112
    60
                             -> {thms:Thm list,congs: Thm list, th:Thm} 
paulson@2112
    61
                             -> Thm * Preterm list
paulson@2112
    62
  val RIGHT_ASSOC : Thm -> Thm 
paulson@2112
    63
paulson@2112
    64
  val prove : Term * Tactic -> Thm
paulson@2112
    65
end;