23171
|
1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
|
|
2 |
(* Title: Pure/IsaPlanner/rw_inst.ML
|
|
3 |
ID: $Id$
|
|
4 |
Author: Lucas Dixon, University of Edinburgh
|
|
5 |
lucas.dixon@ed.ac.uk
|
|
6 |
Created: 25 Aug 2004
|
|
7 |
*)
|
|
8 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
|
|
9 |
(* DESCRIPTION:
|
|
10 |
|
|
11 |
rewriting using a conditional meta-equality theorem which supports
|
|
12 |
schematic variable instantiation.
|
|
13 |
|
|
14 |
*)
|
|
15 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
|
|
16 |
signature RW_INST =
|
|
17 |
sig
|
|
18 |
|
|
19 |
(* Rewrite: give it instantiation infromation, a rule, and the
|
|
20 |
target thm, and it will return the rewritten target thm *)
|
|
21 |
val rw :
|
|
22 |
((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *)
|
|
23 |
(Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *)
|
|
24 |
* (string * Term.typ) list (* Fake named bounds + types *)
|
|
25 |
* (string * Term.typ) list (* names of bound + types *)
|
|
26 |
* Term.term -> (* outer term for instantiation *)
|
|
27 |
Thm.thm -> (* rule with indexies lifted *)
|
|
28 |
Thm.thm -> (* target thm *)
|
|
29 |
Thm.thm (* rewritten theorem possibly
|
|
30 |
with additional premises for
|
|
31 |
rule conditions *)
|
|
32 |
|
|
33 |
(* used tools *)
|
|
34 |
val mk_abstractedrule :
|
|
35 |
(string * Term.typ) list (* faked outer bound *)
|
|
36 |
-> (string * Term.typ) list (* hopeful name of outer bounds *)
|
|
37 |
-> Thm.thm -> Thm.cterm list * Thm.thm
|
|
38 |
val mk_fixtvar_tyinsts :
|
|
39 |
(Term.indexname * (Term.sort * Term.typ)) list ->
|
|
40 |
Term.term list -> ((string * int) * (Term.sort * Term.typ)) list
|
|
41 |
* (string * Term.sort) list
|
|
42 |
val mk_renamings :
|
|
43 |
Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
|
|
44 |
val new_tfree :
|
|
45 |
((string * int) * Term.sort) *
|
|
46 |
(((string * int) * (Term.sort * Term.typ)) list * string list) ->
|
|
47 |
((string * int) * (Term.sort * Term.typ)) list * string list
|
|
48 |
val cross_inst : (Term.indexname * (Term.typ * Term.term)) list
|
|
49 |
-> (Term.indexname *(Term.typ * Term.term)) list
|
|
50 |
val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list
|
|
51 |
-> (Term.indexname * (Term.sort * Term.typ)) list
|
|
52 |
|
|
53 |
val beta_contract : Thm.thm -> Thm.thm
|
|
54 |
val beta_eta_contract : Thm.thm -> Thm.thm
|
|
55 |
|
|
56 |
end;
|
|
57 |
|
|
58 |
structure RWInst
|
|
59 |
: RW_INST
|
|
60 |
= struct
|
|
61 |
|
|
62 |
|
|
63 |
(* beta contract the theorem *)
|
|
64 |
fun beta_contract thm =
|
|
65 |
equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
|
|
66 |
|
|
67 |
(* beta-eta contract the theorem *)
|
|
68 |
fun beta_eta_contract thm =
|
|
69 |
let
|
|
70 |
val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
|
|
71 |
val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
|
|
72 |
in thm3 end;
|
|
73 |
|
|
74 |
|
|
75 |
(* to get the free names of a theorem (including hyps and flexes) *)
|
|
76 |
fun usednames_of_thm th =
|
|
77 |
let val rep = Thm.rep_thm th
|
|
78 |
val hyps = #hyps rep
|
|
79 |
val (tpairl,tpairr) = Library.split_list (#tpairs rep)
|
|
80 |
val prop = #prop rep
|
|
81 |
in
|
|
82 |
List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
|
|
83 |
end;
|
|
84 |
|
|
85 |
(* Given a list of variables that were bound, and a that has been
|
|
86 |
instantiated with free variable placeholders for the bound vars, it
|
|
87 |
creates an abstracted version of the theorem, with local bound vars as
|
|
88 |
lambda-params:
|
|
89 |
|
|
90 |
Ts:
|
|
91 |
("x", ty)
|
|
92 |
|
|
93 |
rule::
|
|
94 |
C :x ==> P :x = Q :x
|
|
95 |
|
|
96 |
results in:
|
|
97 |
("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
|
|
98 |
|
|
99 |
note: assumes rule is instantiated
|
|
100 |
*)
|
|
101 |
(* Note, we take abstraction in the order of last abstraction first *)
|
|
102 |
fun mk_abstractedrule TsFake Ts rule =
|
|
103 |
let
|
|
104 |
val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
|
|
105 |
|
|
106 |
(* now we change the names of temporary free vars that represent
|
|
107 |
bound vars with binders outside the redex *)
|
|
108 |
val prop = Thm.prop_of rule;
|
|
109 |
val names = usednames_of_thm rule;
|
|
110 |
val (fromnames,tonames,names2,Ts') =
|
|
111 |
Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
|
|
112 |
let val n2 = Name.variant names n in
|
|
113 |
(ctermify (Free(faken,ty)) :: rnf,
|
|
114 |
ctermify (Free(n2,ty)) :: rnt,
|
|
115 |
n2 :: names,
|
|
116 |
(n2,ty) :: Ts'')
|
|
117 |
end)
|
|
118 |
(([],[],names, []), TsFake~~Ts);
|
|
119 |
|
|
120 |
(* rename conflicting free's in the rule to avoid cconflicts
|
|
121 |
with introduced vars from bounds outside in redex *)
|
|
122 |
val rule' = rule |> Drule.forall_intr_list fromnames
|
|
123 |
|> Drule.forall_elim_list tonames;
|
|
124 |
|
|
125 |
(* make unconditional rule and prems *)
|
|
126 |
val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
|
|
127 |
rule';
|
|
128 |
|
|
129 |
(* using these names create lambda-abstracted version of the rule *)
|
|
130 |
val abstractions = rev (Ts' ~~ tonames);
|
|
131 |
val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
|
|
132 |
Thm.abstract_rule n ct th)
|
|
133 |
(uncond_rule, abstractions);
|
|
134 |
in (cprems, abstract_rule) end;
|
|
135 |
|
|
136 |
|
|
137 |
(* given names to avoid, and vars that need to be fixed, it gives
|
|
138 |
unique new names to the vars so that they can be fixed as free
|
|
139 |
variables *)
|
|
140 |
(* make fixed unique free variable instantiations for non-ground vars *)
|
|
141 |
(* Create a table of vars to be renamed after instantiation - ie
|
|
142 |
other uninstantiated vars in the hyps of the rule
|
|
143 |
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
|
|
144 |
fun mk_renamings tgt rule_inst =
|
|
145 |
let
|
|
146 |
val rule_conds = Thm.prems_of rule_inst
|
|
147 |
val names = foldr Term.add_term_names [] (tgt :: rule_conds);
|
|
148 |
val (conds_tyvs,cond_vs) =
|
|
149 |
Library.foldl (fn ((tyvs, vs), t) =>
|
|
150 |
(Library.union
|
|
151 |
(Term.term_tvars t, tyvs),
|
|
152 |
Library.union
|
|
153 |
(map Term.dest_Var (Term.term_vars t), vs)))
|
|
154 |
(([],[]), rule_conds);
|
|
155 |
val termvars = map Term.dest_Var (Term.term_vars tgt);
|
|
156 |
val vars_to_fix = Library.union (termvars, cond_vs);
|
|
157 |
val (renamings, names2) =
|
|
158 |
foldr (fn (((n,i),ty), (vs, names')) =>
|
|
159 |
let val n' = Name.variant names' n in
|
|
160 |
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
|
|
161 |
end)
|
|
162 |
([], names) vars_to_fix;
|
|
163 |
in renamings end;
|
|
164 |
|
|
165 |
(* make a new fresh typefree instantiation for the given tvar *)
|
|
166 |
fun new_tfree (tv as (ix,sort), (pairs,used)) =
|
|
167 |
let val v = Name.variant used (string_of_indexname ix)
|
|
168 |
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
|
|
169 |
|
|
170 |
|
|
171 |
(* make instantiations to fix type variables that are not
|
|
172 |
already instantiated (in ignore_ixs) from the list of terms. *)
|
|
173 |
fun mk_fixtvar_tyinsts ignore_insts ts =
|
|
174 |
let
|
|
175 |
val ignore_ixs = map fst ignore_insts;
|
|
176 |
val (tvars, tfrees) =
|
|
177 |
foldr (fn (t, (varixs, tfrees)) =>
|
|
178 |
(Term.add_term_tvars (t,varixs),
|
|
179 |
Term.add_term_tfrees (t,tfrees)))
|
|
180 |
([],[]) ts;
|
|
181 |
val unfixed_tvars =
|
|
182 |
List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
|
|
183 |
val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
|
|
184 |
in (fixtyinsts, tfrees) end;
|
|
185 |
|
|
186 |
|
|
187 |
(* cross-instantiate the instantiations - ie for each instantiation
|
|
188 |
replace all occurances in other instantiations - no loops are possible
|
|
189 |
and thus only one-parsing of the instantiations is necessary. *)
|
|
190 |
fun cross_inst insts =
|
|
191 |
let
|
|
192 |
fun instL (ix, (ty,t)) =
|
|
193 |
map (fn (ix2,(ty2,t2)) =>
|
|
194 |
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
|
|
195 |
|
|
196 |
fun cross_instL ([], l) = rev l
|
|
197 |
| cross_instL ((ix, t) :: insts, l) =
|
|
198 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
|
|
199 |
|
|
200 |
in cross_instL (insts, []) end;
|
|
201 |
|
|
202 |
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
|
|
203 |
fun cross_inst_typs insts =
|
|
204 |
let
|
|
205 |
fun instL (ix, (srt,ty)) =
|
|
206 |
map (fn (ix2,(srt2,ty2)) =>
|
|
207 |
(ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
|
|
208 |
|
|
209 |
fun cross_instL ([], l) = rev l
|
|
210 |
| cross_instL ((ix, t) :: insts, l) =
|
|
211 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
|
|
212 |
|
|
213 |
in cross_instL (insts, []) end;
|
|
214 |
|
|
215 |
|
|
216 |
(* assume that rule and target_thm have distinct var names. THINK:
|
|
217 |
efficient version with tables for vars for: target vars, introduced
|
|
218 |
vars, and rule vars, for quicker instantiation? The outerterm defines
|
|
219 |
which part of the target_thm was modified. Note: we take Ts in the
|
|
220 |
upterm order, ie last abstraction first., and with an outeterm where
|
|
221 |
the abstracted subterm has the arguments in the revered order, ie
|
|
222 |
first abstraction first. FakeTs has abstractions using the fake name
|
|
223 |
- ie the name distinct from all other abstractions. *)
|
|
224 |
|
|
225 |
fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
|
|
226 |
let
|
|
227 |
(* general signature info *)
|
|
228 |
val target_sign = (Thm.theory_of_thm target_thm);
|
|
229 |
val ctermify = Thm.cterm_of target_sign;
|
|
230 |
val ctypeify = Thm.ctyp_of target_sign;
|
|
231 |
|
|
232 |
(* fix all non-instantiated tvars *)
|
|
233 |
val (fixtyinsts, othertfrees) =
|
|
234 |
mk_fixtvar_tyinsts nonfixed_typinsts
|
|
235 |
[Thm.prop_of rule, Thm.prop_of target_thm];
|
|
236 |
val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
|
|
237 |
fixtyinsts;
|
|
238 |
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
|
|
239 |
|
|
240 |
(* certified instantiations for types *)
|
|
241 |
val ctyp_insts =
|
|
242 |
map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
|
|
243 |
typinsts;
|
|
244 |
|
|
245 |
(* type instantiated versions *)
|
|
246 |
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
|
|
247 |
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule;
|
|
248 |
|
|
249 |
val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
|
|
250 |
(* type instanitated outer term *)
|
|
251 |
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
|
|
252 |
|
|
253 |
val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
|
|
254 |
FakeTs;
|
|
255 |
val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
|
|
256 |
Ts;
|
|
257 |
|
|
258 |
(* type-instantiate the var instantiations *)
|
|
259 |
val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) =>
|
|
260 |
(ix, (Term.typ_subst_TVars term_typ_inst ty,
|
|
261 |
Term.subst_TVars term_typ_inst t))
|
|
262 |
:: insts_tyinst)
|
|
263 |
[] unprepinsts;
|
|
264 |
|
|
265 |
(* cross-instantiate *)
|
|
266 |
val insts_tyinst_inst = cross_inst insts_tyinst;
|
|
267 |
|
|
268 |
(* create certms of instantiations *)
|
|
269 |
val cinsts_tyinst =
|
|
270 |
map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
|
|
271 |
ctermify t)) insts_tyinst_inst;
|
|
272 |
|
|
273 |
(* The instantiated rule *)
|
|
274 |
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
|
|
275 |
|
|
276 |
(* Create a table of vars to be renamed after instantiation - ie
|
|
277 |
other uninstantiated vars in the hyps the *instantiated* rule
|
|
278 |
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
|
|
279 |
val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
|
|
280 |
rule_inst;
|
|
281 |
val cterm_renamings =
|
|
282 |
map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
|
|
283 |
|
|
284 |
(* Create the specific version of the rule for this target application *)
|
|
285 |
val outerterm_inst =
|
|
286 |
outerterm_tyinst
|
|
287 |
|> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
|
|
288 |
|> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
|
|
289 |
val couter_inst = Thm.reflexive (ctermify outerterm_inst);
|
|
290 |
val (cprems, abstract_rule_inst) =
|
|
291 |
rule_inst |> Thm.instantiate ([], cterm_renamings)
|
|
292 |
|> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
|
|
293 |
val specific_tgt_rule =
|
|
294 |
beta_eta_contract
|
|
295 |
(Thm.combination couter_inst abstract_rule_inst);
|
|
296 |
|
|
297 |
(* create an instantiated version of the target thm *)
|
|
298 |
val tgt_th_inst =
|
|
299 |
tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
|
|
300 |
|> Thm.instantiate ([], cterm_renamings);
|
|
301 |
|
|
302 |
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
|
|
303 |
|
|
304 |
in
|
|
305 |
(beta_eta_contract tgt_th_inst)
|
|
306 |
|> Thm.equal_elim specific_tgt_rule
|
|
307 |
|> Drule.implies_intr_list cprems
|
|
308 |
|> Drule.forall_intr_list frees_of_fixed_vars
|
|
309 |
|> Drule.forall_elim_list vars
|
|
310 |
|> Thm.varifyT' othertfrees
|
|
311 |
|-> K Drule.zero_var_indexes
|
|
312 |
end;
|
|
313 |
|
|
314 |
|
|
315 |
end; (* struct *)
|