1(* ========================================================================= *)
2(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Rule =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* An equation consists of two terms (t,u) plus a theorem (stronger than)    *)
11(* t = u \/ C.                                                               *)
12(* ------------------------------------------------------------------------- *)
13
14type equation = (Term.term * Term.term) * Thm.thm
15
16val ppEquation : equation Print.pp
17
18val equationToString : equation -> string
19
20(* Returns t = u if the equation theorem contains this literal *)
21val equationLiteral : equation -> Literal.literal option
22
23val reflEqn : Term.term -> equation
24
25val symEqn : equation -> equation
26
27val transEqn : equation -> equation -> equation
28
29(* ------------------------------------------------------------------------- *)
30(* A conversion takes a term t and either:                                   *)
31(* 1. Returns a term u together with a theorem (stronger than) t = u \/ C.   *)
32(* 2. Raises an Error exception.                                             *)
33(* ------------------------------------------------------------------------- *)
34
35type conv = Term.term -> Term.term * Thm.thm
36
37val allConv : conv
38
39val noConv : conv
40
41val thenConv : conv -> conv -> conv
42
43val orelseConv : conv -> conv -> conv
44
45val tryConv : conv -> conv
46
47val repeatConv : conv -> conv
48
49val firstConv : conv list -> conv
50
51val everyConv : conv list -> conv
52
53val rewrConv : equation -> Term.path -> conv
54
55val pathConv : conv -> Term.path -> conv
56
57val subtermConv : conv -> int -> conv
58
59val subtermsConv : conv -> conv  (* All function arguments *)
60
61(* ------------------------------------------------------------------------- *)
62(* Applying a conversion to every subterm, with some traversal strategy.     *)
63(* ------------------------------------------------------------------------- *)
64
65val bottomUpConv : conv -> conv
66
67val topDownConv : conv -> conv
68
69val repeatTopDownConv : conv -> conv  (* useful for rewriting *)
70
71(* ------------------------------------------------------------------------- *)
72(* A literule (bad pun) takes a literal L and either:                        *)
73(* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C.     *)
74(* 2. Raises an Error exception.                                             *)
75(* ------------------------------------------------------------------------- *)
76
77type literule = Literal.literal -> Literal.literal * Thm.thm
78
79val allLiterule : literule
80
81val noLiterule : literule
82
83val thenLiterule : literule -> literule -> literule
84
85val orelseLiterule : literule -> literule -> literule
86
87val tryLiterule : literule -> literule
88
89val repeatLiterule : literule -> literule
90
91val firstLiterule : literule list -> literule
92
93val everyLiterule : literule list -> literule
94
95val rewrLiterule : equation -> Term.path -> literule
96
97val pathLiterule : conv -> Term.path -> literule
98
99val argumentLiterule : conv -> int -> literule
100
101val allArgumentsLiterule : conv -> literule
102
103(* ------------------------------------------------------------------------- *)
104(* A rule takes one theorem and either deduces another or raises an Error    *)
105(* exception.                                                                *)
106(* ------------------------------------------------------------------------- *)
107
108type rule = Thm.thm -> Thm.thm
109
110val allRule : rule
111
112val noRule : rule
113
114val thenRule : rule -> rule -> rule
115
116val orelseRule : rule -> rule -> rule
117
118val tryRule : rule -> rule
119
120val changedRule : rule -> rule
121
122val repeatRule : rule -> rule
123
124val firstRule : rule list -> rule
125
126val everyRule : rule list -> rule
127
128val literalRule : literule -> Literal.literal -> rule
129
130val rewrRule : equation -> Literal.literal -> Term.path -> rule
131
132val pathRule : conv -> Literal.literal -> Term.path -> rule
133
134val literalsRule : literule -> LiteralSet.set -> rule
135
136val allLiteralsRule : literule -> rule
137
138val convRule : conv -> rule  (* All arguments of all literals *)
139
140(* ------------------------------------------------------------------------- *)
141(*                                                                           *)
142(* --------- reflexivity                                                     *)
143(*   x = x                                                                   *)
144(* ------------------------------------------------------------------------- *)
145
146val reflexivityRule : Term.term -> Thm.thm
147
148val reflexivity : Thm.thm
149
150(* ------------------------------------------------------------------------- *)
151(*                                                                           *)
152(* --------------------- symmetry                                            *)
153(*   ~(x = y) \/ y = x                                                       *)
154(* ------------------------------------------------------------------------- *)
155
156val symmetryRule : Term.term -> Term.term -> Thm.thm
157
158val symmetry : Thm.thm
159
160(* ------------------------------------------------------------------------- *)
161(*                                                                           *)
162(* --------------------------------- transitivity                            *)
163(*   ~(x = y) \/ ~(y = z) \/ x = z                                           *)
164(* ------------------------------------------------------------------------- *)
165
166val transitivity : Thm.thm
167
168(* ------------------------------------------------------------------------- *)
169(*                                                                           *)
170(* ---------------------------------------------- functionCongruence (f,n)   *)
171(*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
172(*   f x0 ... x{n-1} = f y0 ... y{n-1}                                       *)
173(* ------------------------------------------------------------------------- *)
174
175val functionCongruence : Term.function -> Thm.thm
176
177(* ------------------------------------------------------------------------- *)
178(*                                                                           *)
179(* ---------------------------------------------- relationCongruence (R,n)   *)
180(*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
181(*   ~R x0 ... x{n-1} \/ R y0 ... y{n-1}                                     *)
182(* ------------------------------------------------------------------------- *)
183
184val relationCongruence : Atom.relation -> Thm.thm
185
186(* ------------------------------------------------------------------------- *)
187(*   x = y \/ C                                                              *)
188(* -------------- symEq (x = y)                                              *)
189(*   y = x \/ C                                                              *)
190(* ------------------------------------------------------------------------- *)
191
192val symEq : Literal.literal -> rule
193
194(* ------------------------------------------------------------------------- *)
195(*   ~(x = y) \/ C                                                           *)
196(* ----------------- symNeq ~(x = y)                                         *)
197(*   ~(y = x) \/ C                                                           *)
198(* ------------------------------------------------------------------------- *)
199
200val symNeq : Literal.literal -> rule
201
202(* ------------------------------------------------------------------------- *)
203(* sym (x = y) = symEq (x = y)  /\  sym ~(x = y) = symNeq ~(x = y)           *)
204(* ------------------------------------------------------------------------- *)
205
206val sym : Literal.literal -> rule
207
208(* ------------------------------------------------------------------------- *)
209(*   ~(x = x) \/ C                                                           *)
210(* ----------------- removeIrrefl                                            *)
211(*         C                                                                 *)
212(*                                                                           *)
213(* where all irreflexive equalities.                                         *)
214(* ------------------------------------------------------------------------- *)
215
216val removeIrrefl : rule
217
218(* ------------------------------------------------------------------------- *)
219(*   x = y \/ y = x \/ C                                                     *)
220(* ----------------------- removeSym                                         *)
221(*       x = y \/ C                                                          *)
222(*                                                                           *)
223(* where all duplicate copies of equalities and disequalities are removed.   *)
224(* ------------------------------------------------------------------------- *)
225
226val removeSym : rule
227
228(* ------------------------------------------------------------------------- *)
229(*   ~(v = t) \/ C                                                           *)
230(* ----------------- expandAbbrevs                                           *)
231(*      C[t/v]                                                               *)
232(*                                                                           *)
233(* where t must not contain any occurrence of the variable v.                *)
234(* ------------------------------------------------------------------------- *)
235
236val expandAbbrevs : rule
237
238(* ------------------------------------------------------------------------- *)
239(* simplify = isTautology + expandAbbrevs + removeSym                        *)
240(* ------------------------------------------------------------------------- *)
241
242val simplify : Thm.thm -> Thm.thm option
243
244(* ------------------------------------------------------------------------- *)
245(*    C                                                                      *)
246(* -------- freshVars                                                        *)
247(*   C[s]                                                                    *)
248(*                                                                           *)
249(* where s is a renaming substitution chosen so that all of the variables in *)
250(* C are replaced by fresh variables.                                        *)
251(* ------------------------------------------------------------------------- *)
252
253val freshVars : rule
254
255(* ------------------------------------------------------------------------- *)
256(*               C                                                           *)
257(* ---------------------------- factor                                       *)
258(*   C_s_1, C_s_2, ..., C_s_n                                                *)
259(*                                                                           *)
260(* where each s_i is a substitution that factors C, meaning that the theorem *)
261(*                                                                           *)
262(*   C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C                    *)
263(*                                                                           *)
264(* has fewer literals than C.                                                *)
265(*                                                                           *)
266(* Also, if s is any substitution that factors C, then one of the s_i will   *)
267(* result in a theorem C_s_i that strictly subsumes the theorem C_s.         *)
268(* ------------------------------------------------------------------------- *)
269
270val factor' : Thm.clause -> Subst.subst list
271
272val factor : Thm.thm -> Thm.thm list
273
274end
275