author | mengj |
Fri, 07 Apr 2006 05:12:51 +0200 | |
changeset 19354 | aebf9dddccd7 |
parent 18729 | 216e31270509 |
child 19963 | 806eaa2a2a5e |
permissions | -rw-r--r-- |
15151 | 1 |
(* Title: HOL/Reconstruction.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson and Claire Quigley |
|
4 |
Copyright 2004 University of Cambridge |
|
5 |
*) |
|
6 |
||
7 |
(*Attributes for reconstructing external resolution proofs*) |
|
8 |
||
9 |
structure Reconstruction = |
|
10 |
struct |
|
11 |
||
12 |
(**************************************************************) |
|
13 |
(* extra functions necessary for factoring and paramodulation *) |
|
14 |
(**************************************************************) |
|
15 |
||
16 |
fun mksubstlist [] sublist = sublist |
|
18729 | 17 |
| mksubstlist ((a, (_, b)) :: rest) sublist = |
15151 | 18 |
let val vartype = type_of b |
19 |
val avar = Var(a,vartype) |
|
18729 | 20 |
val newlist = ((avar,b)::sublist) |
15151 | 21 |
in mksubstlist rest newlist end; |
22 |
||
23 |
||
24 |
(**** attributes ****) |
|
25 |
||
26 |
(** Binary resolution **) |
|
27 |
||
28 |
fun binary_rule ((cl1, lit1), (cl2 , lit2)) = |
|
29 |
select_literal (lit1 + 1) cl1 |
|
30 |
RSN ((lit2 + 1), cl2); |
|
31 |
||
18729 | 32 |
val binary = Attrib.syntax |
33 |
(Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
|
34 |
>> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); |
|
15151 | 35 |
|
36 |
||
37 |
fun inst_single sign t1 t2 cl = |
|
38 |
let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2 |
|
39 |
in hd (Seq.list_of(distinct_subgoals_tac |
|
18729 | 40 |
(cterm_instantiate [(ct1,ct2)] cl))) |
15151 | 41 |
end; |
42 |
||
43 |
fun inst_subst sign substs cl = |
|
44 |
if (is_Var (fst(hd(substs)))) |
|
45 |
then inst_single sign (fst (hd substs)) (snd (hd substs)) cl |
|
46 |
else if (is_Var (snd(hd(substs)))) |
|
47 |
then inst_single sign (snd (hd substs)) (fst (hd substs)) cl |
|
48 |
else raise THM ("inst_subst", 0, [cl]); |
|
49 |
||
50 |
||
51 |
(** Factoring **) |
|
52 |
||
53 |
fun factor_rule (cl, lit1, lit2) = |
|
54 |
let |
|
55 |
val prems = prems_of cl |
|
56 |
val fac1 = List.nth (prems,lit1) |
|
57 |
val fac2 = List.nth (prems,lit2) |
|
58 |
val sign = sign_of_thm cl |
|
59 |
val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)]) |
|
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
15955
diff
changeset
|
60 |
val newenv = ReconTranslateProof.getnewenv unif_env |
15151 | 61 |
val envlist = Envir.alist_of newenv |
62 |
in |
|
63 |
inst_subst sign (mksubstlist envlist []) cl |
|
64 |
end; |
|
65 |
||
18729 | 66 |
val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat) |
67 |
>> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j)))); |
|
15151 | 68 |
|
69 |
||
70 |
(** Paramodulation **) |
|
71 |
||
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
72 |
(*subst with premises exchanged: that way, side literals of the equality will appear |
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
73 |
as the second to last premises of the result.*) |
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
74 |
val rev_subst = rotate_prems 1 subst; |
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
75 |
|
15499 | 76 |
fun paramod_rule ((cl1, lit1), (cl2, lit2)) = |
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
77 |
let val eq_lit_th = select_literal (lit1+1) cl1 |
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
78 |
val mod_lit_th = select_literal (lit2+1) cl2 |
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
79 |
val eqsubst = eq_lit_th RSN (2,rev_subst) |
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
80 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) |
15499 | 81 |
val newth' = Seq.hd (flexflex_rule newth) |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15531
diff
changeset
|
82 |
in Meson.negated_asm_of_head newth' end; |
15151 | 83 |
|
84 |
||
18729 | 85 |
val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
86 |
>> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j))))); |
|
15151 | 87 |
|
88 |
||
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
89 |
(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **) |
15151 | 90 |
|
18729 | 91 |
fun demod_rule ((cl1, lit1), (cl2 , lit2)) = |
15151 | 92 |
let val eq_lit_th = select_literal (lit1+1) cl1 |
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
93 |
val mod_lit_th = select_literal (lit2+1) cl2 |
18729 | 94 |
val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th |
15449
a27c81bd838d
fixed the treatment of demodulation and paramodulation
paulson
parents:
15384
diff
changeset
|
95 |
val eqsubst = eq_lit_th RSN (2,rev_subst) |
15495
50fde6f04e4c
new treatment of demodulation in proof reconstruction
paulson
parents:
15466
diff
changeset
|
96 |
val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst) |
15499 | 97 |
val offset = #maxidx(rep_thm newth) + 1 |
18729 | 98 |
(*ensures "renaming apart" even when Vars are frozen*) |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15531
diff
changeset
|
99 |
in Meson.negated_asm_of_head (thaw offset newth) end; |
15151 | 100 |
|
18729 | 101 |
val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
102 |
>> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j))))); |
|
15151 | 103 |
|
104 |
||
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset
|
105 |
(** Conversion of a theorem into clauses **) |
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset
|
106 |
|
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15794
diff
changeset
|
107 |
(*For efficiency, we rely upon memo-izing in ResAxioms.*) |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15794
diff
changeset
|
108 |
fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i) |
15466 | 109 |
|
18729 | 110 |
val clausify = Attrib.syntax (Scan.lift Args.nat |
111 |
>> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); |
|
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset
|
112 |
|
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15151
diff
changeset
|
113 |
|
15151 | 114 |
(** theory setup **) |
115 |
||
116 |
val setup = |
|
18708 | 117 |
Attrib.add_attributes |
18729 | 118 |
[("binary", binary, "binary resolution"), |
119 |
("paramod", paramod, "paramodulation"), |
|
120 |
("demod", demod, "demodulation"), |
|
121 |
("factor", factor, "factoring"), |
|
122 |
("clausify", clausify, "conversion to clauses")]; |
|
15151 | 123 |
|
124 |
end |