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