author | blanchet |
Fri, 17 Sep 2010 01:56:19 +0200 | |
changeset 39501 | aaa7078fff55 |
parent 39444 | beabb8443ee4 |
child 39502 | cffceed8e7fa |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39444
diff
changeset
|
3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *) |
39348 | 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 Print.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 reflexivityRule : Term.term -> Thm.thm |
|
147 |
||
148 |
val reflexivity : Thm.thm |
|
149 |
||
150 |
(* ------------------------------------------------------------------------- *) |
|
151 |
(* *) |
|
152 |
(* --------------------- symmetry *) |
|
153 |
(* ~(x = y) \/ y = x *) |
|
154 |
(* ------------------------------------------------------------------------- *) |
|
155 |
||
156 |
val symmetryRule : Term.term -> Term.term -> Thm.thm |
|
157 |
||
158 |
val symmetry : Thm.thm |
|
159 |
||
160 |
(* ------------------------------------------------------------------------- *) |
|
161 |
(* *) |
|
162 |
(* --------------------------------- transitivity *) |
|
163 |
(* ~(x = y) \/ ~(y = z) \/ x = z *) |
|
164 |
(* ------------------------------------------------------------------------- *) |
|
165 |
||
166 |
val 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 |
||
175 |
val 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 |
||
184 |
val relationCongruence : Atom.relation -> Thm.thm |
|
185 |
||
186 |
(* ------------------------------------------------------------------------- *) |
|
187 |
(* x = y \/ C *) |
|
188 |
(* -------------- symEq (x = y) *) |
|
189 |
(* y = x \/ C *) |
|
190 |
(* ------------------------------------------------------------------------- *) |
|
191 |
||
192 |
val symEq : Literal.literal -> rule |
|
193 |
||
194 |
(* ------------------------------------------------------------------------- *) |
|
195 |
(* ~(x = y) \/ C *) |
|
196 |
(* ----------------- symNeq ~(x = y) *) |
|
197 |
(* ~(y = x) \/ C *) |
|
198 |
(* ------------------------------------------------------------------------- *) |
|
199 |
||
200 |
val symNeq : Literal.literal -> rule |
|
201 |
||
202 |
(* ------------------------------------------------------------------------- *) |
|
203 |
(* sym (x = y) = symEq (x = y) /\ sym ~(x = y) = symNeq ~(x = y) *) |
|
204 |
(* ------------------------------------------------------------------------- *) |
|
205 |
||
206 |
val sym : Literal.literal -> rule |
|
207 |
||
208 |
(* ------------------------------------------------------------------------- *) |
|
209 |
(* ~(x = x) \/ C *) |
|
210 |
(* ----------------- removeIrrefl *) |
|
211 |
(* C *) |
|
212 |
(* *) |
|
213 |
(* where all irreflexive equalities. *) |
|
214 |
(* ------------------------------------------------------------------------- *) |
|
215 |
||
216 |
val 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 |
||
226 |
val 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 |
||
236 |
val expandAbbrevs : rule |
|
237 |
||
238 |
(* ------------------------------------------------------------------------- *) |
|
239 |
(* simplify = isTautology + expandAbbrevs + removeSym *) |
|
240 |
(* ------------------------------------------------------------------------- *) |
|
241 |
||
242 |
val 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 |
||
253 |
val 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 |
||
270 |
val factor' : Thm.clause -> Subst.subst list |
|
271 |
||
272 |
val factor : Thm.thm -> Thm.thm list |
|
273 |
||
274 |
end |