TFL/rules.sig
changeset 2112 3902e9af752f
child 3245 241838c01caf
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/rules.sig	Fri Oct 18 12:41:04 1996 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +signature Rules_sig =
     1.5 +sig
     1.6 +(*  structure USyntax : USyntax_sig *)
     1.7 +  type Type
     1.8 +  type Preterm
     1.9 +  type Term
    1.10 +  type Thm
    1.11 +  type Tactic
    1.12 +  type 'a binding
    1.13 +
    1.14 +  val dest_thm : Thm -> Preterm list * Preterm
    1.15 +
    1.16 +  (* Inference rules *)
    1.17 +  val REFL      :Term -> Thm
    1.18 +  val ASSUME    :Term -> Thm
    1.19 +  val MP        :Thm -> Thm -> Thm
    1.20 +  val MATCH_MP  :Thm -> Thm -> Thm
    1.21 +  val CONJUNCT1 :Thm -> Thm
    1.22 +  val CONJUNCT2 :Thm -> Thm
    1.23 +  val CONJUNCTS :Thm -> Thm list
    1.24 +  val DISCH     :Term -> Thm -> Thm
    1.25 +  val UNDISCH   :Thm  -> Thm
    1.26 +  val INST_TYPE :Type binding list -> Thm -> Thm
    1.27 +  val SPEC      :Term -> Thm -> Thm
    1.28 +  val ISPEC     :Term -> Thm -> Thm
    1.29 +  val ISPECL    :Term list -> Thm -> Thm
    1.30 +  val GEN       :Term -> Thm -> Thm
    1.31 +  val GENL      :Term list -> Thm -> Thm
    1.32 +  val BETA_RULE :Thm -> Thm
    1.33 +  val LIST_CONJ :Thm list -> Thm
    1.34 +
    1.35 +  val SYM : Thm -> Thm
    1.36 +  val DISCH_ALL : Thm -> Thm
    1.37 +  val FILTER_DISCH_ALL : (Preterm -> bool) -> Thm -> Thm
    1.38 +  val SPEC_ALL  : Thm -> Thm
    1.39 +  val GEN_ALL   : Thm -> Thm
    1.40 +  val IMP_TRANS : Thm -> Thm -> Thm
    1.41 +  val PROVE_HYP : Thm -> Thm -> Thm
    1.42 +
    1.43 +  val CHOOSE : Term * Thm -> Thm -> Thm
    1.44 +  val EXISTS : Term * Term -> Thm -> Thm
    1.45 +  val EXISTL : Term list -> Thm -> Thm
    1.46 +  val IT_EXISTS : Term binding list -> Thm -> Thm
    1.47 +
    1.48 +  val EVEN_ORS : Thm list -> Thm list
    1.49 +  val DISJ_CASESL : Thm -> Thm list -> Thm
    1.50 +
    1.51 +  val SUBS : Thm list -> Thm -> Thm
    1.52 +  val simplify : Thm list -> Thm -> Thm
    1.53 +  val simpl_conv : Thm list -> Term -> Thm
    1.54 +
    1.55 +(* For debugging my isabelle solver in the conditional rewriter *)
    1.56 +(*
    1.57 +  val term_ref : Preterm list ref
    1.58 +  val thm_ref : Thm list ref
    1.59 +  val mss_ref : meta_simpset list ref
    1.60 +  val tracing :bool ref
    1.61 +*)
    1.62 +  val CONTEXT_REWRITE_RULE : Preterm * Preterm
    1.63 +                             -> {thms:Thm list,congs: Thm list, th:Thm} 
    1.64 +                             -> Thm * Preterm list
    1.65 +  val RIGHT_ASSOC : Thm -> Thm 
    1.66 +
    1.67 +  val prove : Term * Tactic -> Thm
    1.68 +end;