author | wenzelm |
Sat, 04 Sep 2021 21:45:43 +0200 | |
changeset 74233 | 9eff7c673b42 |
parent 60642 | 48dd1cefb4ae |
child 74266 | 612b7e0d6721 |
permissions | -rw-r--r-- |
23175 | 1 |
(* Title: Tools/IsaPlanner/rw_inst.ML |
23171 | 2 |
Author: Lucas Dixon, University of Edinburgh |
3 |
||
23175 | 4 |
Rewriting using a conditional meta-equality theorem which supports |
5 |
schematic variable instantiation. |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
6 |
*) |
23171 | 7 |
|
8 |
signature RW_INST = |
|
9 |
sig |
|
52240 | 10 |
val rw: Proof.context -> |
11 |
((indexname * (sort * typ)) list * (* type var instantiations *) |
|
12 |
(indexname * (typ * term)) list) (* schematic var instantiations *) |
|
13 |
* (string * typ) list (* Fake named bounds + types *) |
|
14 |
* (string * typ) list (* names of bound + types *) |
|
15 |
* term -> (* outer term for instantiation *) |
|
16 |
thm -> (* rule with indexes lifted *) |
|
17 |
thm -> (* target thm *) |
|
18 |
thm (* rewritten theorem possibly with additional premises for rule conditions *) |
|
23171 | 19 |
end; |
20 |
||
52240 | 21 |
structure RW_Inst: RW_INST = |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
22 |
struct |
23171 | 23 |
|
52245 | 24 |
(* Given (string,type) pairs capturing the free vars that need to be |
25 |
allified in the assumption, and a theorem with assumptions possibly |
|
26 |
containing the free vars, then we give back the assumptions allified |
|
27 |
as hidden hyps. |
|
28 |
||
29 |
Given: x |
|
30 |
th: A vs ==> B vs |
|
31 |
Results in: "B vs" [!!x. A x] |
|
32 |
*) |
|
60358 | 33 |
fun allify_conditions ctxt Ts th = |
52245 | 34 |
let |
35 |
fun allify (x, T) t = |
|
36 |
Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t)); |
|
37 |
||
60358 | 38 |
val cTs = map (Thm.cterm_of ctxt o Free) Ts; |
39 |
val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th); |
|
52245 | 40 |
val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; |
41 |
in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; |
|
42 |
||
43 |
||
23171 | 44 |
(* Given a list of variables that were bound, and a that has been |
45 |
instantiated with free variable placeholders for the bound vars, it |
|
46 |
creates an abstracted version of the theorem, with local bound vars as |
|
47 |
lambda-params: |
|
48 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
49 |
Ts: |
23171 | 50 |
("x", ty) |
51 |
||
52 |
rule:: |
|
53 |
C :x ==> P :x = Q :x |
|
54 |
||
55 |
results in: |
|
56 |
("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) |
|
57 |
||
58 |
note: assumes rule is instantiated |
|
59 |
*) |
|
60 |
(* Note, we take abstraction in the order of last abstraction first *) |
|
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset
|
61 |
fun mk_abstractedrule ctxt TsFake Ts rule = |
52240 | 62 |
let |
63 |
(* now we change the names of temporary free vars that represent |
|
64 |
bound vars with binders outside the redex *) |
|
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset
|
65 |
|
52240 | 66 |
val ns = |
67 |
IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); |
|
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset
|
68 |
|
52240 | 69 |
val (fromnames, tonames, Ts') = |
70 |
fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => |
|
59641 | 71 |
(Thm.cterm_of ctxt (Free(faken,ty)) :: rnf, |
72 |
Thm.cterm_of ctxt (Free(n2,ty)) :: rnt, |
|
52240 | 73 |
(n2,ty) :: Ts'')) |
74 |
(TsFake ~~ Ts ~~ ns) ([], [], []); |
|
23171 | 75 |
|
52240 | 76 |
(* rename conflicting free's in the rule to avoid cconflicts |
77 |
with introduced vars from bounds outside in redex *) |
|
78 |
val rule' = rule |
|
79 |
|> Drule.forall_intr_list fromnames |
|
80 |
|> Drule.forall_elim_list tonames; |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
81 |
|
52240 | 82 |
(* make unconditional rule and prems *) |
60358 | 83 |
val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule'; |
23171 | 84 |
|
52240 | 85 |
(* using these names create lambda-abstracted version of the rule *) |
86 |
val abstractions = rev (Ts' ~~ tonames); |
|
87 |
val abstract_rule = |
|
52242 | 88 |
fold (fn ((n, ty), ct) => Thm.abstract_rule n ct) |
89 |
abstractions uncond_rule; |
|
52240 | 90 |
in (cprems, abstract_rule) end; |
23171 | 91 |
|
92 |
||
93 |
(* given names to avoid, and vars that need to be fixed, it gives |
|
94 |
unique new names to the vars so that they can be fixed as free |
|
95 |
variables *) |
|
96 |
(* make fixed unique free variable instantiations for non-ground vars *) |
|
97 |
(* Create a table of vars to be renamed after instantiation - ie |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
98 |
other uninstantiated vars in the hyps of the rule |
23171 | 99 |
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) |
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset
|
100 |
fun mk_renamings ctxt tgt rule_inst = |
52240 | 101 |
let |
102 |
val rule_conds = Thm.prems_of rule_inst; |
|
103 |
val (_, cond_vs) = |
|
52242 | 104 |
fold (fn t => fn (tyvs, vs) => |
105 |
(union (op =) (Misc_Legacy.term_tvars t) tyvs, |
|
106 |
union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []); |
|
52240 | 107 |
val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); |
108 |
val vars_to_fix = union (op =) termvars cond_vs; |
|
109 |
val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); |
|
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset
|
110 |
in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; |
23171 | 111 |
|
112 |
(* make a new fresh typefree instantiation for the given tvar *) |
|
52242 | 113 |
fun new_tfree (tv as (ix,sort)) (pairs, used) = |
52240 | 114 |
let val v = singleton (Name.variant_list used) (string_of_indexname ix) |
115 |
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
|
23171 | 116 |
|
117 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
118 |
(* make instantiations to fix type variables that are not |
23171 | 119 |
already instantiated (in ignore_ixs) from the list of terms. *) |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
120 |
fun mk_fixtvar_tyinsts ignore_insts ts = |
52240 | 121 |
let |
122 |
val ignore_ixs = map fst ignore_insts; |
|
123 |
val (tvars, tfrees) = |
|
52242 | 124 |
fold_rev (fn t => fn (varixs, tfrees) => |
52240 | 125 |
(Misc_Legacy.add_term_tvars (t,varixs), |
52242 | 126 |
Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); |
52240 | 127 |
val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; |
52242 | 128 |
val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) |
52240 | 129 |
in (fixtyinsts, tfrees) end; |
23171 | 130 |
|
131 |
||
132 |
(* cross-instantiate the instantiations - ie for each instantiation |
|
58318 | 133 |
replace all occurrences in other instantiations - no loops are possible |
23171 | 134 |
and thus only one-parsing of the instantiations is necessary. *) |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
135 |
fun cross_inst insts = |
52240 | 136 |
let |
137 |
fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => |
|
138 |
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); |
|
23171 | 139 |
|
52240 | 140 |
fun cross_instL ([], l) = rev l |
141 |
| cross_instL ((ix, t) :: insts, l) = |
|
23171 | 142 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); |
143 |
||
52240 | 144 |
in cross_instL (insts, []) end; |
23171 | 145 |
|
146 |
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
147 |
fun cross_inst_typs insts = |
52240 | 148 |
let |
149 |
fun instL (ix, (srt,ty)) = |
|
150 |
map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); |
|
23171 | 151 |
|
52240 | 152 |
fun cross_instL ([], l) = rev l |
153 |
| cross_instL ((ix, t) :: insts, l) = |
|
23171 | 154 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); |
155 |
||
52240 | 156 |
in cross_instL (insts, []) end; |
23171 | 157 |
|
158 |
||
159 |
(* assume that rule and target_thm have distinct var names. THINK: |
|
160 |
efficient version with tables for vars for: target vars, introduced |
|
161 |
vars, and rule vars, for quicker instantiation? The outerterm defines |
|
162 |
which part of the target_thm was modified. Note: we take Ts in the |
|
163 |
upterm order, ie last abstraction first., and with an outeterm where |
|
164 |
the abstracted subterm has the arguments in the revered order, ie |
|
165 |
first abstraction first. FakeTs has abstractions using the fake name |
|
166 |
- ie the name distinct from all other abstractions. *) |
|
167 |
||
49340
25fc6e0da459
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents:
49339
diff
changeset
|
168 |
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = |
52240 | 169 |
let |
170 |
(* fix all non-instantiated tvars *) |
|
171 |
val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) |
|
172 |
mk_fixtvar_tyinsts nonfixed_typinsts |
|
173 |
[Thm.prop_of rule, Thm.prop_of target_thm]; |
|
174 |
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); |
|
23171 | 175 |
|
52240 | 176 |
(* certified instantiations for types *) |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset
|
177 |
val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; |
52240 | 178 |
|
179 |
(* type instantiated versions *) |
|
180 |
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; |
|
181 |
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; |
|
23171 | 182 |
|
52240 | 183 |
val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; |
184 |
(* type instanitated outer term *) |
|
185 |
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; |
|
23171 | 186 |
|
52240 | 187 |
val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs; |
188 |
val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts; |
|
23171 | 189 |
|
52240 | 190 |
(* type-instantiate the var instantiations *) |
191 |
val insts_tyinst = |
|
52242 | 192 |
fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => |
52240 | 193 |
(ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) |
52242 | 194 |
:: insts_tyinst) unprepinsts []; |
23171 | 195 |
|
52240 | 196 |
(* cross-instantiate *) |
197 |
val insts_tyinst_inst = cross_inst insts_tyinst; |
|
23171 | 198 |
|
52240 | 199 |
(* create certms of instantiations *) |
200 |
val cinsts_tyinst = |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset
|
201 |
map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; |
23171 | 202 |
|
52240 | 203 |
(* The instantiated rule *) |
204 |
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); |
|
23171 | 205 |
|
52240 | 206 |
(* Create a table of vars to be renamed after instantiation - ie |
207 |
other uninstantiated vars in the hyps the *instantiated* rule |
|
208 |
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) |
|
209 |
val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; |
|
59641 | 210 |
val cterm_renamings = map (fn (x, y) => apply2 (Thm.cterm_of ctxt) (Var x, y)) renamings; |
23171 | 211 |
|
52240 | 212 |
(* Create the specific version of the rule for this target application *) |
213 |
val outerterm_inst = |
|
214 |
outerterm_tyinst |
|
215 |
|> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst) |
|
216 |
|> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings); |
|
59641 | 217 |
val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); |
52240 | 218 |
val (cprems, abstract_rule_inst) = |
219 |
rule_inst |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset
|
220 |
|> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) |
52240 | 221 |
|> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; |
222 |
val specific_tgt_rule = |
|
223 |
Conv.fconv_rule Drule.beta_eta_conversion |
|
224 |
(Thm.combination couter_inst abstract_rule_inst); |
|
23171 | 225 |
|
52240 | 226 |
(* create an instantiated version of the target thm *) |
227 |
val tgt_th_inst = |
|
228 |
tgt_th_tyinst |
|
229 |
|> Thm.instantiate ([], cinsts_tyinst) |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset
|
230 |
|> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); |
23171 | 231 |
|
52240 | 232 |
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; |
233 |
in |
|
234 |
Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst |
|
235 |
|> Thm.equal_elim specific_tgt_rule |
|
236 |
|> Drule.implies_intr_list cprems |
|
237 |
|> Drule.forall_intr_list frees_of_fixed_vars |
|
238 |
|> Drule.forall_elim_list vars |
|
74233 | 239 |
|> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees) |
52240 | 240 |
|-> K Drule.zero_var_indexes |
241 |
end; |
|
23171 | 242 |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
243 |
end; |