312 rearr (new + 1) |
312 rearr (new + 1) |
313 (map (fn q => if new <= q andalso q < p then q + 1 else q) ps) |
313 (map (fn q => if new <= q andalso q < p then q + 1 else q) ps) |
314 (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm)) |
314 (Thm.permute_prems (new + 1) (new - p) (Thm.permute_prems new (p - new) thm)) |
315 in rearr 0 end; |
315 in rearr 0 end; |
316 |
316 |
317 (*Resolution: exactly one resolvent must be produced.*) |
317 |
318 fun tha RSN (i,thb) = |
318 (*Resolution: multiple arguments, multiple results*) |
319 case Seq.chop 2 (Thm.biresolution false [(false,tha)] i thb) of |
319 local |
320 ([th],_) => th |
320 fun res th i rule = |
321 | ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) |
321 Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; |
322 | _ => raise THM("RSN: multiple unifiers", i, [tha,thb]); |
322 |
323 |
323 fun multi_res _ [] rule = Seq.single rule |
324 (*resolution: P==>Q, Q==>R gives P==>R. *) |
324 | multi_res i (th :: ths) rule = Seq.maps (res th i) (multi_res (i + 1) ths rule); |
|
325 in |
|
326 val multi_resolve = multi_res 1; |
|
327 fun multi_resolves facts rules = Seq.maps (multi_resolve facts) (Seq.of_list rules); |
|
328 end; |
|
329 |
|
330 (*Resolution: exactly one resolvent must be produced*) |
|
331 fun tha RSN (i, thb) = |
|
332 (case Seq.chop 2 (Thm.biresolution false [(false, tha)] i thb) of |
|
333 ([th], _) => th |
|
334 | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb]) |
|
335 | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb])); |
|
336 |
|
337 (*Resolution: P==>Q, Q==>R gives P==>R*) |
325 fun tha RS thb = tha RSN (1,thb); |
338 fun tha RS thb = tha RSN (1,thb); |
326 |
339 |
327 (*For joining lists of rules*) |
340 (*For joining lists of rules*) |
328 fun thas RLN (i,thbs) = |
341 fun thas RLN (i, thbs) = |
329 let val resolve = Thm.biresolution false (map (pair false) thas) i |
342 let val resolve = Thm.biresolution false (map (pair false) thas) i |
330 fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] |
343 fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] |
331 in maps resb thbs end; |
344 in maps resb thbs end; |
332 |
345 |
333 fun thas RL thbs = thas RLN (1,thbs); |
346 fun thas RL thbs = thas RLN (1, thbs); |
|
347 |
|
348 (*Isar-style multi-resolution*) |
|
349 fun bottom_rl OF rls = |
|
350 (case Seq.chop 2 (multi_resolve rls bottom_rl) of |
|
351 ([th], _) => th |
|
352 | ([], _) => raise THM ("OF: no unifiers", 0, bottom_rl :: rls) |
|
353 | _ => raise THM ("OF: multiple unifiers", 0, bottom_rl :: rls)); |
334 |
354 |
335 (*Resolve a list of rules against bottom_rl from right to left; |
355 (*Resolve a list of rules against bottom_rl from right to left; |
336 makes proof trees*) |
356 makes proof trees*) |
337 fun rls MRS bottom_rl = |
357 fun rls MRS bottom_rl = bottom_rl OF rls; |
338 let fun rs_aux i [] = bottom_rl |
|
339 | rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls) |
|
340 in rs_aux 1 rls end; |
|
341 |
|
342 (*A version of MRS with more appropriate argument order*) |
|
343 fun bottom_rl OF rls = rls MRS bottom_rl; |
|
344 |
358 |
345 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R |
359 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R |
346 with no lifting or renaming! Q may contain ==> or meta-quants |
360 with no lifting or renaming! Q may contain ==> or meta-quants |
347 ALWAYS deletes premise i *) |
361 ALWAYS deletes premise i *) |
348 fun compose(tha,i,thb) = |
362 fun compose(tha,i,thb) = |
349 distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb)); |
363 distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb)); |
350 |
364 |
351 fun compose_single (tha,i,thb) = |
365 fun compose_single (tha,i,thb) = |
352 case compose (tha,i,thb) of |
366 (case compose (tha,i,thb) of |
353 [th] => th |
367 [th] => th |
354 | _ => raise THM ("compose: unique result expected", i, [tha,thb]); |
368 | _ => raise THM ("compose: unique result expected", i, [tha,thb])); |
355 |
369 |
356 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) |
370 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) |
357 fun tha COMP thb = |
371 fun tha COMP thb = |
358 case compose(tha,1,thb) of |
372 (case compose(tha, 1, thb) of |
359 [th] => th |
373 [th] => th |
360 | _ => raise THM("COMP", 1, [tha,thb]); |
374 | _ => raise THM ("COMP", 1, [tha, thb])); |
361 |
375 |
362 |
376 |
363 (** theorem equality **) |
377 (** theorem equality **) |
364 |
378 |
365 (*Useful "distance" function for BEST_FIRST*) |
379 (*Useful "distance" function for BEST_FIRST*) |