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