|
2112
|
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;
|