author | paulson |
Mon, 11 Apr 2005 16:25:31 +0200 | |
changeset 15697 | 681bcb7f0389 |
parent 15684 | 5ec4d21889d6 |
child 15700 | 970e0293dfb3 |
permissions | -rw-r--r-- |
15642 | 1 |
|
2 |
||
3 |
(*----------------------------------------------*) |
|
4 |
(* Reorder clauses for use in binary resolution *) |
|
5 |
(*----------------------------------------------*) |
|
6 |
||
7 |
fun drop n [] = [] |
|
8 |
| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs) |
|
9 |
||
10 |
fun remove n [] = [] |
|
11 |
| remove n (x::xs) = List.filter (not_equal n) (x::xs); |
|
12 |
||
13 |
fun remove_nth n [] = [] |
|
15697 | 14 |
| remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n)) |
15642 | 15 |
|
16 |
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs)) |
|
17 |
||
18 |
||
19 |
fun literals (Const("Trueprop",_) $ P) = literals P |
|
20 |
| literals (Const("op |",_) $ P $ Q) = literals P @ literals Q |
|
21 |
| literals (Const("Not",_) $ P) = [(false,P)] |
|
22 |
| literals P = [(true,P)]; |
|
23 |
||
24 |
(*number of literals in a term*) |
|
25 |
val nliterals = length o literals; |
|
26 |
||
27 |
exception Not_in_list; |
|
28 |
||
29 |
||
30 |
(* |
|
31 |
(* gives horn clause with kth disj as concl (starting at 1) *) |
|
32 |
fun rots (0,th) = (Meson.make_horn Meson.crules th) |
|
33 |
| rots (k,th) = rots(k-1, assoc_right (th RS disj_comm)) |
|
34 |
||
35 |
||
36 |
||
37 |
Goal " (~~P) == P"; |
|
38 |
by Auto_tac; |
|
39 |
qed "notnotEq"; |
|
40 |
||
41 |
Goal "A | A ==> A"; |
|
42 |
by Auto_tac; |
|
43 |
qed "rem_dup_disj"; |
|
44 |
||
45 |
||
46 |
||
47 |
||
48 |
(* New Meson code Versions of make_neg_rule and make_pos_rule that don't insert new *) |
|
49 |
(* assumptions, for ordinary resolution. *) |
|
50 |
||
51 |
||
52 |
||
53 |
||
54 |
val not_conjD = thm "meson_not_conjD"; |
|
55 |
val not_disjD = thm "meson_not_disjD"; |
|
56 |
val not_notD = thm "meson_not_notD"; |
|
57 |
val not_allD = thm "meson_not_allD"; |
|
58 |
val not_exD = thm "meson_not_exD"; |
|
59 |
val imp_to_disjD = thm "meson_imp_to_disjD"; |
|
60 |
val not_impD = thm "meson_not_impD"; |
|
61 |
val iff_to_disjD = thm "meson_iff_to_disjD"; |
|
62 |
val not_iffD = thm "meson_not_iffD"; |
|
63 |
val conj_exD1 = thm "meson_conj_exD1"; |
|
64 |
val conj_exD2 = thm "meson_conj_exD2"; |
|
65 |
val disj_exD = thm "meson_disj_exD"; |
|
66 |
val disj_exD1 = thm "meson_disj_exD1"; |
|
67 |
val disj_exD2 = thm "meson_disj_exD2"; |
|
68 |
val disj_assoc = thm "meson_disj_assoc"; |
|
69 |
val disj_comm = thm "meson_disj_comm"; |
|
70 |
val disj_FalseD1 = thm "meson_disj_FalseD1"; |
|
71 |
val disj_FalseD2 = thm "meson_disj_FalseD2"; |
|
72 |
||
73 |
||
74 |
fun literals (Const("Trueprop",_) $ P) = literals P |
|
75 |
| literals (Const("op |",_) $ P $ Q) = literals P @ literals Q |
|
76 |
| literals (Const("Not",_) $ P) = [(false,P)] |
|
77 |
| literals P = [(true,P)]; |
|
78 |
||
79 |
(*number of literals in a term*) |
|
80 |
val nliterals = length o literals; |
|
81 |
||
82 |
exception Not_in_list; |
|
83 |
||
84 |
||
85 |
(* get a meta-clause for resolution with correct order of literals *) |
|
86 |
fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th) |
|
87 |
val contra = if lits = 1 |
|
88 |
then |
|
89 |
th |
|
90 |
else |
|
91 |
rots (n,th) |
|
92 |
in |
|
93 |
if lits = 1 |
|
94 |
then |
|
95 |
||
96 |
contra |
|
97 |
else |
|
98 |
rotate_prems (lits - n) contra |
|
99 |
end |
|
100 |
||
101 |
||
102 |
||
103 |
fun zip xs [] = [] |
|
104 |
| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys)) |
|
105 |
||
106 |
||
107 |
fun unzip [] = ([],[]) |
|
108 |
| unzip((x,y)::pairs) = |
|
109 |
let val (xs,ys) = unzip pairs |
|
110 |
in (x::xs, y::ys) end; |
|
111 |
||
112 |
fun numlist 0 = [] |
|
113 |
| numlist n = (numlist (n - 1))@[n] |
|
114 |
||
115 |
||
116 |
||
117 |
||
118 |
fun last(x::xs) = if xs=[] then x else last xs |
|
119 |
fun butlast []= [] |
|
120 |
| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs)) |
|
121 |
||
122 |
||
123 |
fun minus a b = b - a; |
|
124 |
||
125 |
||
126 |
||
127 |
||
128 |
(* gives meta clause with kth disj as concl (starting at 1) *) |
|
129 |
(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules th) |
|
130 |
| rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*) |
|
131 |
||
132 |
||
133 |
(* get a meta-clause for resolution with correct order of literals *) |
|
134 |
fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th) |
|
135 |
val contra = if lits = 1 |
|
136 |
then |
|
137 |
th |
|
138 |
else |
|
139 |
rots (n,th) |
|
140 |
in |
|
141 |
if lits = 1 |
|
142 |
then |
|
143 |
||
144 |
contra |
|
145 |
else |
|
146 |
rotate_prems (lits - n) contra |
|
147 |
end |
|
148 |
*) |
|
149 |
||
150 |
||
151 |
||
152 |
||
153 |
fun zip xs [] = [] |
|
154 |
| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys)) |
|
155 |
||
156 |
||
157 |
fun unzip [] = ([],[]) |
|
158 |
| unzip((x,y)::pairs) = |
|
159 |
let val (xs,ys) = unzip pairs |
|
160 |
in (x::xs, y::ys) end; |
|
161 |
||
162 |
fun numlist 0 = [] |
|
163 |
| numlist n = (numlist (n - 1))@[n] |
|
164 |
||
165 |
||
166 |
||
167 |
||
168 |
fun last(x::xs) = if xs=[] then x else last xs |
|
169 |
fun butlast []= [] |
|
170 |
| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs)) |
|
171 |
||
172 |
||
173 |
fun minus a b = b - a; |
|
174 |
||
175 |
||
176 |
(* code to rearrange clauses so that they're the same as the parsed in SPASS version *) |
|
177 |
||
15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15642
diff
changeset
|
178 |
fun assoc3 a [] = raise Recon_Base.Noassoc |
15642 | 179 |
| assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t; |
180 |
||
181 |
||
182 |
fun third (a,b,c) = c; |
|
183 |
||
184 |
||
185 |
fun takeUntil ch [] res = (res, []) |
|
186 |
| takeUntil ch (x::xs) res = if x = ch |
|
187 |
then |
|
188 |
(res, xs) |
|
189 |
else |
|
190 |
takeUntil ch xs (res@[x]) |
|
191 |
fun contains_eq str = inlist "=" str |
|
192 |
||
193 |
fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str []) |
|
194 |
in |
|
195 |
if ((last uptoeq) = "~") |
|
196 |
then |
|
197 |
false |
|
198 |
else |
|
199 |
true |
|
200 |
end |
|
201 |
||
202 |
||
203 |
||
204 |
||
205 |
fun get_eq_strs str = if eq_not_neq str (*not an inequality *) |
|
206 |
then |
|
207 |
let val (left, right) = takeUntil "=" str [] |
|
208 |
in |
|
209 |
((butlast left), (drop 1 right)) |
|
210 |
end |
|
211 |
else (* is an inequality *) |
|
212 |
let val (left, right) = takeUntil "~" str [] |
|
213 |
in |
|
214 |
((butlast left), (drop 2 right)) |
|
215 |
end |
|
216 |
||
217 |
||
218 |
||
219 |
fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a |
|
220 |
val (x_lhs, x_rhs) = get_eq_strs x |
|
221 |
||
222 |
in |
|
223 |
(a_lhs = x_rhs) andalso (a_rhs = x_lhs) |
|
224 |
end |
|
225 |
||
226 |
fun equal_pair (a,b) = equal a b |
|
227 |
||
228 |
fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars) |
|
229 |
||
230 |
fun var_equiv vars (a,b) = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars) |
|
231 |
||
232 |
fun all_true [] = false |
|
233 |
| all_true xs = let val falselist = List.filter (equal false ) xs |
|
234 |
in |
|
235 |
falselist = [] |
|
236 |
end |
|
237 |
||
238 |
||
239 |
||
240 |
fun var_pos_eq vars x y = let val xs = explode x |
|
241 |
val ys = explode y |
|
242 |
in |
|
243 |
if not_equal (length xs) (length ys) |
|
244 |
then |
|
245 |
false |
|
246 |
else |
|
247 |
let val xsys = zip xs ys |
|
248 |
val are_var_pairs = map (var_equiv vars) xsys |
|
249 |
in |
|
250 |
all_true are_var_pairs |
|
251 |
end |
|
252 |
end |
|
253 |
||
254 |
||
255 |
||
256 |
||
257 |
fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list |
|
258 |
|pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = |
|
259 |
let val y = explode x |
|
260 |
val b = explode a |
|
261 |
in |
|
262 |
if b = y |
|
263 |
then |
|
264 |
(pos_num, symlist, nsymlist) |
|
265 |
else |
|
266 |
if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *) |
|
267 |
then |
|
268 |
(pos_num, symlist, nsymlist) |
|
269 |
else |
|
270 |
if (contains_eq b) andalso (contains_eq y) |
|
271 |
then |
|
272 |
if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*) |
|
273 |
then |
|
274 |
(pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else |
|
275 |
if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *) |
|
276 |
then |
|
277 |
(pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) |
|
278 |
else |
|
279 |
raise Not_in_list |
|
280 |
else |
|
281 |
raise Not_in_list |
|
282 |
||
283 |
end |
|
284 |
||
285 |
| pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = |
|
286 |
let val y = explode x |
|
287 |
val b = explode a |
|
288 |
in |
|
289 |
if b = y |
|
290 |
then |
|
291 |
(pos_num, symlist, nsymlist) |
|
292 |
||
293 |
else |
|
294 |
if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *) |
|
295 |
then |
|
296 |
(pos_num, symlist, nsymlist) |
|
297 |
else |
|
298 |
if (contains_eq b) andalso (contains_eq y) |
|
299 |
then |
|
300 |
if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*) |
|
301 |
then |
|
302 |
(pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else |
|
303 |
if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *) |
|
304 |
then |
|
305 |
(pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) |
|
306 |
else |
|
307 |
pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist) |
|
308 |
else |
|
309 |
pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist) |
|
310 |
||
311 |
end |
|
312 |
||
313 |
||
314 |
||
315 |
||
316 |
||
317 |
||
318 |
||
319 |
(* in |
|
320 |
if b = y |
|
321 |
then |
|
322 |
(pos_num, symlist, nsymlist) |
|
323 |
else if (contains_eq b) andalso (contains_eq y) |
|
324 |
then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*) |
|
325 |
then if (switch_equal b y ) (* if they're equal under sym *) |
|
326 |
then |
|
327 |
(pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) |
|
328 |
else |
|
329 |
pos_in_list a xs ((pos_num + 1), symlist, nsymlist) |
|
330 |
else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *) |
|
331 |
then if (switch_equal b y ) (* if they're equal under not_sym *) |
|
332 |
then |
|
333 |
(pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *) |
|
334 |
else |
|
335 |
pos_in_list a xs ((pos_num + 1), symlist, nsymlist) |
|
336 |
else |
|
337 |
pos_in_list a xs ((pos_num + 1), symlist, nsymlist) |
|
338 |
else |
|
339 |
pos_in_list a xs ((pos_num + 1), symlist, nsymlist) |
|
340 |
else |
|
341 |
pos_in_list a xs ((pos_num + 1), symlist, nsymlist) |
|
342 |
end |
|
343 |
||
344 |
*) |
|
345 |
||
346 |
||
347 |
(* checkorder Spass Isabelle [] *) |
|
348 |
||
349 |
fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist) |
|
350 |
| checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) = |
|
351 |
let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) |
|
352 |
in |
|
353 |
checkorder xs strlist allvars ((numlist@[posnum]), symlist', not_symlist') |
|
354 |
end |
|
355 |
||
356 |
fun is_digit ch = |
|
357 |
( ch >= "0" andalso ch <= "9") |
|
358 |
||
359 |
||
360 |
fun is_alpha ch = |
|
361 |
(ch >= "A" andalso ch <= "Z") orelse |
|
362 |
(ch >= "a" andalso ch <= "z") |
|
363 |
||
364 |
||
365 |
fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") |
|
366 |
||
367 |
fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t |
|
368 |
val exp_term = explode termstr |
|
369 |
in |
|
370 |
implode(List.filter is_alpha_space_or_neg_or_eq exp_term) |
|
371 |
end |
|
372 |
||
373 |
fun get_meta_lits thm = map lit_string (prems_of thm) |
|
374 |
||
375 |
||
376 |
||
377 |
||
378 |
fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")") |
|
379 |
||
380 |
fun lit_string_bracket t = let val termstr = (Sign.string_of_term Mainsign ) t |
|
381 |
val exp_term = explode termstr |
|
382 |
in |
|
383 |
implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term) |
|
384 |
end |
|
385 |
||
386 |
fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm) |
|
387 |
||
388 |
||
389 |
||
390 |
||
391 |
fun apply_rule rule [] thm = thm |
|
392 |
| apply_rule rule (x::xs) thm = let val thm' = rule RSN ((x+1),thm) |
|
393 |
in |
|
394 |
apply_rule rule xs thm' |
|
395 |
end |
|
396 |
||
397 |
||
398 |
||
399 |
(* resulting thm, clause-strs in spass order, vars *) |
|
400 |
||
401 |
fun rearrange_clause thm res_strlist allvars = |
|
402 |
let val isa_strlist = get_meta_lits thm |
|
403 |
val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[]) |
|
404 |
val symmed = apply_rule sym symlist thm |
|
405 |
val not_symmed = apply_rule not_sym not_symlist symmed |
|
406 |
||
407 |
in |
|
408 |
((rearrange_prems posns not_symmed), posns, symlist,not_symlist) |
|
409 |
end |