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 |
let open Attrib
|
|
11 |
in
|
|
12 |
struct
|
|
13 |
|
|
14 |
(**************************************************************)
|
|
15 |
(* extra functions necessary for factoring and paramodulation *)
|
|
16 |
(**************************************************************)
|
|
17 |
|
|
18 |
fun mksubstlist [] sublist = sublist
|
|
19 |
| mksubstlist ((a,b)::rest) sublist =
|
|
20 |
let val vartype = type_of b
|
|
21 |
val avar = Var(a,vartype)
|
|
22 |
val newlist = ((avar,b)::sublist)
|
|
23 |
in mksubstlist rest newlist end;
|
|
24 |
|
|
25 |
|
|
26 |
fun get_unif_comb t eqterm =
|
|
27 |
if ((type_of t) = (type_of eqterm))
|
|
28 |
then t
|
|
29 |
else
|
|
30 |
let val _ $ rand = t
|
|
31 |
in get_unif_comb rand eqterm end;
|
|
32 |
|
|
33 |
fun get_unif_lit t eqterm =
|
|
34 |
if (can HOLogic.dest_eq t)
|
|
35 |
then
|
|
36 |
let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
|
|
37 |
in lhs end
|
|
38 |
else
|
|
39 |
get_unif_comb t eqterm;
|
|
40 |
|
|
41 |
|
|
42 |
|
|
43 |
(**** attributes ****)
|
|
44 |
|
|
45 |
(** Binary resolution **)
|
|
46 |
|
|
47 |
fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
|
|
48 |
select_literal (lit1 + 1) cl1
|
|
49 |
RSN ((lit2 + 1), cl2);
|
|
50 |
|
|
51 |
fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
|
|
52 |
|
|
53 |
fun gen_BINARY thm = syntax
|
|
54 |
((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
|
|
55 |
val BINARY_global = gen_BINARY global_thm;
|
|
56 |
val BINARY_local = gen_BINARY local_thm;
|
|
57 |
|
|
58 |
(*I have not done the MRR rule because it seems to be identifical to
|
|
59 |
BINARY*)
|
|
60 |
|
|
61 |
|
|
62 |
fun inst_single sign t1 t2 cl =
|
|
63 |
let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
|
|
64 |
in hd (Seq.list_of(distinct_subgoals_tac
|
|
65 |
(cterm_instantiate [(ct1,ct2)] cl)))
|
|
66 |
end;
|
|
67 |
|
|
68 |
fun inst_subst sign substs cl =
|
|
69 |
if (is_Var (fst(hd(substs))))
|
|
70 |
then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
|
|
71 |
else if (is_Var (snd(hd(substs))))
|
|
72 |
then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
|
|
73 |
else raise THM ("inst_subst", 0, [cl]);
|
|
74 |
|
|
75 |
(*Grabs the environment from the result of Unify.unifiers*)
|
|
76 |
fun getnewenv thisseq = fst (hd (Seq.list_of thisseq));
|
|
77 |
|
|
78 |
(** Factoring **)
|
|
79 |
|
|
80 |
fun factor_rule (cl, lit1, lit2) =
|
|
81 |
let
|
|
82 |
val prems = prems_of cl
|
|
83 |
val fac1 = List.nth (prems,lit1)
|
|
84 |
val fac2 = List.nth (prems,lit2)
|
|
85 |
val sign = sign_of_thm cl
|
|
86 |
val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
|
|
87 |
val newenv = getnewenv unif_env
|
|
88 |
val envlist = Envir.alist_of newenv
|
|
89 |
in
|
|
90 |
inst_subst sign (mksubstlist envlist []) cl
|
|
91 |
end;
|
|
92 |
|
|
93 |
fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
|
|
94 |
|
|
95 |
fun FACTOR x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
|
|
96 |
|
|
97 |
|
|
98 |
(** Paramodulation **)
|
|
99 |
|
|
100 |
(*Get rid of a Not if it is present*)
|
|
101 |
fun maybe_dest_not (Const ("Not", _) $ t) = t
|
|
102 |
| maybe_dest_not t = t;
|
|
103 |
|
|
104 |
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
|
|
105 |
let val prems1 = prems_of cl1
|
|
106 |
val prems2 = prems_of cl2
|
|
107 |
val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2)
|
|
108 |
(* want to get first element of equality *)
|
|
109 |
|
|
110 |
val fac1 = List.nth (prems1,lit1)
|
|
111 |
val (lhs, rhs) = HOLogic.dest_eq(maybe_dest_not
|
|
112 |
(HOLogic.dest_Trueprop fac1))
|
|
113 |
(* get other literal involved in the paramodulation *)
|
|
114 |
val fac2 = List.nth (prems2,lit2)
|
|
115 |
|
|
116 |
(* get bit of th2 to unify with lhs of cl1 *)
|
|
117 |
val unif_lit = get_unif_lit (HOLogic.dest_Trueprop fac2) lhs
|
|
118 |
val unif_env = Unify.unifiers (sign, Envir.empty 0, [(unif_lit, lhs)])
|
|
119 |
val newenv = getnewenv unif_env
|
|
120 |
val envlist = Envir.alist_of newenv
|
|
121 |
(* instantiate cl2 with unifiers *)
|
|
122 |
|
|
123 |
val newth1 = inst_subst sign (mksubstlist envlist []) cl1
|
|
124 |
(*rewrite cl2 with the equality bit of cl2 i.e. lit2 *)
|
|
125 |
val facthm' = select_literal (lit1 + 1) newth1
|
|
126 |
val equal_lit = concl_of facthm'
|
|
127 |
val cterm_eq = cterm_of sign equal_lit
|
|
128 |
val eq_thm = assume cterm_eq
|
|
129 |
val meta_eq_thm = mk_meta_eq eq_thm
|
|
130 |
val newth2= rewrite_rule [meta_eq_thm] cl2
|
|
131 |
(*thin lit2 from cl2 *)
|
|
132 |
(* get cl1 with lit1 as concl, then resolve with thin_rl *)
|
|
133 |
val thm' = facthm' RS thin_rl
|
|
134 |
(* now resolve cl2 with last premise of thm' *)
|
|
135 |
val newthm = newth2 RSN ((length prems1), thm')
|
|
136 |
in newthm end
|
|
137 |
|
|
138 |
|
|
139 |
fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
|
|
140 |
|
|
141 |
fun gen_PARAMOD thm = syntax
|
|
142 |
((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
|
|
143 |
val PARAMOD_global = gen_PARAMOD global_thm;
|
|
144 |
val PARAMOD_local = gen_PARAMOD local_thm;
|
|
145 |
|
|
146 |
|
|
147 |
(** Demodulation, i.e. rewriting **)
|
|
148 |
|
|
149 |
fun demod_rule (cl1,lit1,cl2) =
|
|
150 |
let val eq_lit_th = select_literal (lit1+1) cl1
|
|
151 |
val equal_lit = concl_of eq_lit_th
|
|
152 |
val sign = Sign.merge (sign_of_thm cl1, sign_of_thm cl2)
|
|
153 |
val cterm_eq = cterm_of sign equal_lit
|
|
154 |
val eq_thm = assume cterm_eq
|
|
155 |
val meta_eq_thm = mk_meta_eq eq_thm
|
|
156 |
val newth2= rewrite_rule [meta_eq_thm] cl2
|
|
157 |
in newth2 end;
|
|
158 |
|
|
159 |
fun demod_syntax (i, B) (x, A) = (x, demod_rule (A,i,B));
|
|
160 |
|
|
161 |
fun gen_DEMOD thm = syntax ((Scan.lift Args.nat -- thm) >> demod_syntax);
|
|
162 |
val DEMOD_global = gen_DEMOD global_thm;
|
|
163 |
val DEMOD_local = gen_DEMOD local_thm;
|
|
164 |
|
|
165 |
|
|
166 |
(** theory setup **)
|
|
167 |
|
|
168 |
val setup =
|
|
169 |
[Attrib.add_attributes
|
|
170 |
[("BINARY", (BINARY_global, BINARY_local), "binary resolution"),
|
|
171 |
("PARAMOD", (PARAMOD_global, PARAMOD_local), "paramodulation"),
|
|
172 |
("DEMOD", (DEMOD_global, DEMOD_local), "demodulation"),
|
|
173 |
("FACTOR", (FACTOR, FACTOR), "factoring")]];
|
|
174 |
|
|
175 |
end
|
|
176 |
end
|
|
177 |
|
|
178 |
|