ETCSprover/drule.sig at master · u5943321/ETCSprover · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
signature drule =
sig
type form = form.form
type term = term.term
type sort = term.sort
type menv = form.menv
type thm = logic.thm

val simple_exists: (string * sort) -> thm -> thm
val prove_hyp: thm -> thm -> thm
val imp_trans: thm -> thm -> thm
val frefl: form -> thm
val dimpl2r: thm -> thm
val dimpr2l: thm -> thm
val iff_trans: thm -> thm -> thm
val iff_swap: thm -> thm
val equivT: thm -> thm

val eqT_intro: thm -> thm
val eqF_intro: thm -> thm

val dimp_mp_l2r: thm -> thm -> thm
val dimp_mp_r2l: thm -> thm -> thm


val abstl: (string * sort) list -> thm -> thm
val spec_all: thm -> thm
val specl: term list -> thm -> thm

val gen_all: thm -> thm
val genl: (string * sort) list -> thm -> thm

val undisch: thm -> thm
val add_assum: form -> thm -> thm


val conj_iff: thm -> thm -> thm
val disj_iff: thm -> thm -> thm
val imp_iff: thm -> thm -> thm
val dimp_iff: thm -> thm -> thm
val neg_iff: thm -> thm

val forall_iff: string * sort -> thm -> thm
val exists_iff: string * sort -> thm -> thm


val T_conj_1: thm
val T_conj_2: thm
val F_conj_1: thm
val F_conj_2: thm

val T_disj_1: thm
val T_disj_2: thm
val F_disj_1: thm
val F_disj_2: thm

val T_imp_1: thm
val T_imp_2: thm
val F_imp_1: thm
val F_imp_2: thm

val T_dimp_1: thm
val T_dimp_2: thm
val F_dimp_1: thm
val F_dimp_2: thm

val forall_true_ob: thm
val forall_true_ar: thm

val forall_false_ob: thm
val forall_false_ar: thm

val exists_true_ar: thm
val exists_true_ob: thm
val exists_false_ar: thm
val exists_false_ob: thm

val disch_all: thm -> thm
val dischl: form list -> thm -> thm
val conj_assum: form -> form -> thm -> thm

val F_imp: form -> thm
val F2f: form -> thm
val contr: form -> thm -> thm

val double_neg: form -> thm
val undisch_all: thm -> thm
val elim_double_neg:thm -> thm
val strip_neg: thm -> thm
val exists_forall: (string * sort) -> thm
val forall_exists: (string * sort) -> thm
val conj_all_assum: thm -> thm

val nF2T: thm
val nT2F: thm
val double_neg_elim: thm


val strip_all_and_imp: thm -> thm
val F_imp2: form -> thm
val contrapos: thm -> thm
val split_assum: thm -> thm

val gen_dischl: form list -> thm -> thm
val gen_disch_all: thm -> thm

val pe_ob_clauses: thm
val pe_ar_clauses: thm
val PULL_EXISTS: thm

val neg_disch: form -> thm -> thm

end