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