-
Notifications
You must be signed in to change notification settings - Fork 6
/
mlproof.mli
136 lines (122 loc) · 6.13 KB
/
mlproof.mli
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
(* Copyright 2003 INRIA *)
(* $Id: mlproof.mli,v 1.10 2009-08-05 14:47:43 doligez Exp $ *)
open Expr;;
type rule =
| Close of expr (* p, -p / (.) [p]*)
| Close_refl of expr * expr (* -r(a,a) / (.) [r a]*)
| Close_sym of expr * expr * expr
(* r(a,b), -r(b,a) / (.) [r a b]*)
| False (* false / (.) []*)
| NotTrue (* -true / (.) []*)
| NotNot of expr (* --p / p [p]*)
| And of expr * expr (* p/\q / p, q [p q]*)
| NotOr of expr * expr (* -(p\/q) / -p, -q [p q]*)
| NotImpl of expr * expr (*-(p=>q) / p, -q [p q]*)
| NotAll of expr (*-A.p / -p(t(-p)) [-A.p]*)
| NotAllEx of expr (*-A.p / -p(t(-p)) [-A.p]*)
| Ex of expr (* E.p / p(t(p)) [E.p]*)
| All of expr * expr (* A.p / p(a) [A.p a]*)
| NotEx of expr * expr (* -E.p / -p(a) [-E.p a]*)
| Or of expr * expr (* p\/q / p | q [p q]*)
| Impl of expr * expr (* p=>q / -p | q [p q]*)
| NotAnd of expr * expr (* -(p/\q) / -p | -q [p q]*)
| Equiv of expr * expr (* p<=>q / -p, -q | p, q [p q]*)
| NotEquiv of expr * expr (* -(p<=>q) / -p, q | p, -q [p q]*)
| P_NotP of expr * expr
(* P(a0, .. an), -P(b0, .. bn) / a0!=b0 | .. an!=bn [P(..) -P(..)]*)
| P_NotP_sym of expr * expr * expr
(* r(a,b), -r(c,d) / b!=c | a!=d [r r(.) -r(.)]*)
| NotEqual of expr * expr
(* F(a0, .. an)!=F(b0, .. bn) / a0!=b0 | .. an!=bn [F(a..) F(b.)]*)
| Definition of definition * expr * expr
(* folded / unfolded [def fld unf]*)
| ConjTree of expr (* p1/\p2/\.. / p1, p2, .. [conj]*)
| DisjTree of expr (* p1\/p2\/.. / p1 | p2 | .. [disj]*)
| AllPartial of expr * expr * int
(* Ax.p(x) / Axyz.p(s(xyz)) [Axpx s ar]*)
| NotExPartial of expr * expr * int
(* -Ex.p(x) / -Exyz.p(s(xyz)) [-Expx s ar]*)
| Refl of expr * expr * expr
(* -r(a,b) / a!=b [r a b]*)
| Trans of expr * expr
(* r(a,b),-r(c,d) / c!=a,-r(c,a) | b!=d,-r(b,d) [rab -rcd]*)
| Trans_sym of expr * expr
(* r(a,b),-r(c,d) / d!=a,-r(d,a) | b!=c,-r(b,c) [rab -rcd]*)
| TransEq of expr * expr * expr
(* a=b,-r(c,d) / c!=a,-r(c,a) | -r(c,a),-r(b,d) | b!=d,-r(b,d)
[a b -rcd]*)
| TransEq2 of expr * expr * expr
(* a=b,-r(c,d) / c!=b,-r(c,b) | -r(c,b),-r(a,d) | a!=d,-r(a,d)
[a b -rcd]*)
| TransEq_sym of expr * expr * expr
(* a=b,-r(c,d) / d!=a,-r(d,a) | -r(d,a),-r(b,c) | b!=c,-r(b,c)
[a b -rcd]*)
| Cut of expr (* / p | -p [p]*)
| CongruenceLR of expr * expr * expr
(* p[a],a=b / p[b] [p a b]*)
| CongruenceRL of expr * expr * expr
(* p[a],b=a / p[b] [p a b]*)
| Miniscope of expr * expr * expr list
(* $scope (f, t, v1, ...) / f[v1] | ... | t != v1, ... , f[t]
[f t v1 ...] *)
| Ext of string * string * expr list
(* ... [extension, rule, arguments]*)
;;
type proof = {
mlconc : expr list; (* conclusion *)
mlrule : rule; (* rule *)
mlhyps : proof array; (* proof branches *)
mutable mlrefc : int; (* reference count *)
};;
val size : proof -> int;;
val iter : (proof -> unit) -> proof -> unit;;
val make_node : expr list -> rule -> expr list list -> proof list -> proof;;
val make_cl : expr -> proof;;
val make_clr : expr -> expr -> proof;;
val make_cls : expr -> expr -> expr -> proof;;
val make_f : proof;;
val make_nt : proof;;
val make_nn : expr -> proof -> proof;;
val make_and : expr -> expr -> proof -> proof;;
val make_nor : expr -> expr -> proof -> proof;;
val make_nimpl : expr -> expr -> proof -> proof;;
val make_nall : expr -> proof -> proof;;
val make_ex : expr -> proof -> proof;;
val make_all : expr -> expr -> proof -> proof;;
val make_nex : expr -> expr -> proof -> proof;;
val make_or : expr -> expr -> proof -> proof -> proof;;
val make_impl : expr -> expr -> proof -> proof -> proof;;
val make_nand : expr -> expr -> proof -> proof -> proof;;
val make_eqv : expr -> expr -> proof -> proof -> proof;;
val make_neqv : expr -> expr -> proof -> proof -> proof;;
val make_pnp : expr -> expr -> proof list -> proof;;
val make_pnps : expr -> expr -> expr -> proof -> proof -> proof;;
val make_neql : expr -> expr -> proof list -> proof;;
val make_conglr : expr -> expr -> expr -> proof -> proof;;
val make_congrl : expr -> expr -> expr -> proof -> proof;;
val make_def : definition -> expr -> expr -> proof -> proof;;
val make_cut : expr -> proof -> proof -> proof;;
val make_open : expr list -> proof;;
val is_open_node : proof -> bool;;
val is_open_proof : proof -> bool;;
(*
These are not provided because they are derived rules
val make_ctree : expr -> expr list -> proof -> proof;;
val make_dtree : expr -> expr list -> proof list -> proof;;
val make_allp : expr -> string -> int -> proof -> proof;;
val make_nexp : expr -> string -> int -> proof -> proof;;
val make_refl : string -> expr -> expr -> proof -> proof;;
val make_trans :
string -> expr -> expr -> expr -> expr -> proof -> proof -> proof
;;
val make_transs :
string -> expr -> expr -> expr -> expr -> proof -> proof -> proof
;;
val make_transeq :
string -> expr -> expr -> expr -> expr -> proof -> proof -> proof
;;
val make_transeqs :
string -> expr -> expr -> expr -> expr -> proof -> proof -> proof
;;
val make_miniscope : expr -> expr -> expr list -> proof list -> proof;;
*)