1(* ========================================================================= *)
2(* FIRST ORDER LOGIC FORMULAS                                                *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Formula =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* A type of first order logic formulas.                                     *)
11(* ------------------------------------------------------------------------- *)
12
13datatype formula =
14    True
15  | False
16  | Atom of Atom.atom
17  | Not of formula
18  | And of formula * formula
19  | Or of formula * formula
20  | Imp of formula * formula
21  | Iff of formula * formula
22  | Forall of Term.var * formula
23  | Exists of Term.var * formula
24
25(* ------------------------------------------------------------------------- *)
26(* Constructors and destructors.                                             *)
27(* ------------------------------------------------------------------------- *)
28
29(* Booleans *)
30
31val mkBoolean : bool -> formula
32
33val destBoolean : formula -> bool
34
35val isBoolean : formula -> bool
36
37val isTrue : formula -> bool
38
39val isFalse : formula -> bool
40
41(* Functions *)
42
43val functions : formula -> NameAritySet.set
44
45val functionNames : formula -> NameSet.set
46
47(* Relations *)
48
49val relations : formula -> NameAritySet.set
50
51val relationNames : formula -> NameSet.set
52
53(* Atoms *)
54
55val destAtom : formula -> Atom.atom
56
57val isAtom : formula -> bool
58
59(* Negations *)
60
61val destNeg : formula -> formula
62
63val isNeg : formula -> bool
64
65val stripNeg : formula -> int * formula
66
67(* Conjunctions *)
68
69val listMkConj : formula list -> formula
70
71val stripConj : formula -> formula list
72
73val flattenConj : formula -> formula list
74
75(* Disjunctions *)
76
77val listMkDisj : formula list -> formula
78
79val stripDisj : formula -> formula list
80
81val flattenDisj : formula -> formula list
82
83(* Equivalences *)
84
85val listMkEquiv : formula list -> formula
86
87val stripEquiv : formula -> formula list
88
89val flattenEquiv : formula -> formula list
90
91(* Universal quantification *)
92
93val destForall : formula -> Term.var * formula
94
95val isForall : formula -> bool
96
97val listMkForall : Term.var list * formula -> formula
98
99val setMkForall : NameSet.set * formula -> formula
100
101val stripForall : formula -> Term.var list * formula
102
103(* Existential quantification *)
104
105val destExists : formula -> Term.var * formula
106
107val isExists : formula -> bool
108
109val listMkExists : Term.var list * formula -> formula
110
111val setMkExists : NameSet.set * formula -> formula
112
113val stripExists : formula -> Term.var list * formula
114
115(* ------------------------------------------------------------------------- *)
116(* The size of a formula in symbols.                                         *)
117(* ------------------------------------------------------------------------- *)
118
119val symbols : formula -> int
120
121(* ------------------------------------------------------------------------- *)
122(* A total comparison function for formulas.                                 *)
123(* ------------------------------------------------------------------------- *)
124
125val compare : formula * formula -> order
126
127val equal : formula -> formula -> bool
128
129(* ------------------------------------------------------------------------- *)
130(* Free variables.                                                           *)
131(* ------------------------------------------------------------------------- *)
132
133val freeIn : Term.var -> formula -> bool
134
135val freeVars : formula -> NameSet.set
136
137val freeVarsList : formula list -> NameSet.set
138
139val specialize : formula -> formula
140
141val generalize : formula -> formula
142
143(* ------------------------------------------------------------------------- *)
144(* Substitutions.                                                            *)
145(* ------------------------------------------------------------------------- *)
146
147val subst : Subst.subst -> formula -> formula
148
149(* ------------------------------------------------------------------------- *)
150(* The equality relation.                                                    *)
151(* ------------------------------------------------------------------------- *)
152
153val mkEq : Term.term * Term.term -> formula
154
155val destEq : formula -> Term.term * Term.term
156
157val isEq : formula -> bool
158
159val mkNeq : Term.term * Term.term -> formula
160
161val destNeq : formula -> Term.term * Term.term
162
163val isNeq : formula -> bool
164
165val mkRefl : Term.term -> formula
166
167val destRefl : formula -> Term.term
168
169val isRefl : formula -> bool
170
171val sym : formula -> formula  (* raises Error if given a refl *)
172
173val lhs : formula -> Term.term
174
175val rhs : formula -> Term.term
176
177(* ------------------------------------------------------------------------- *)
178(* Splitting goals.                                                          *)
179(* ------------------------------------------------------------------------- *)
180
181val splitGoal : formula -> formula list
182
183(* ------------------------------------------------------------------------- *)
184(* Parsing and pretty-printing.                                              *)
185(* ------------------------------------------------------------------------- *)
186
187type quotation = formula Parse.quotation
188
189val pp : formula Print.pp
190
191val toString : formula -> string
192
193val fromString : string -> formula
194
195val parse : quotation -> formula
196
197end
198