author | wenzelm |
Wed, 12 Sep 2012 23:18:26 +0200 | |
changeset 49340 | 25fc6e0da459 |
parent 49339 | d1fcb4de8349 |
child 52239 | 6a6033fa507c |
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 |
|
10 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
11 |
val beta_eta_contract : thm -> thm |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
12 |
|
23171 | 13 |
(* Rewrite: give it instantiation infromation, a rule, and the |
14 |
target thm, and it will return the rewritten target thm *) |
|
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
|
15 |
val rw : Proof.context -> |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
16 |
((indexname * (sort * typ)) list * (* type var instantiations *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
17 |
(indexname * (typ * term)) list) (* schematic var instantiations *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
18 |
* (string * typ) list (* Fake named bounds + types *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
19 |
* (string * typ) list (* names of bound + types *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
20 |
* term -> (* outer term for instantiation *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
21 |
thm -> (* rule with indexies lifted *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
22 |
thm -> (* target thm *) |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
23 |
thm (* rewritten theorem possibly |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
24 |
with additional premises for |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
25 |
rule conditions *) |
23171 | 26 |
end; |
27 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
28 |
structure RWInst : RW_INST = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
29 |
struct |
23171 | 30 |
|
31 |
||
32 |
(* beta-eta contract the theorem *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
33 |
fun beta_eta_contract thm = |
23171 | 34 |
let |
36945 | 35 |
val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm |
36 |
val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 |
|
23171 | 37 |
in thm3 end; |
38 |
||
39 |
||
40 |
(* Given a list of variables that were bound, and a that has been |
|
41 |
instantiated with free variable placeholders for the bound vars, it |
|
42 |
creates an abstracted version of the theorem, with local bound vars as |
|
43 |
lambda-params: |
|
44 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
45 |
Ts: |
23171 | 46 |
("x", ty) |
47 |
||
48 |
rule:: |
|
49 |
C :x ==> P :x = Q :x |
|
50 |
||
51 |
results in: |
|
52 |
("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) |
|
53 |
||
54 |
note: assumes rule is instantiated |
|
55 |
*) |
|
56 |
(* 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
|
57 |
fun mk_abstractedrule ctxt TsFake Ts rule = |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
58 |
let |
23171 | 59 |
val ctermify = Thm.cterm_of (Thm.theory_of_thm rule); |
60 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
61 |
(* now we change the names of temporary free vars that represent |
23171 | 62 |
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
|
63 |
|
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
|
64 |
val ns = |
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 |
IsaND.variant_names ctxt (Thm.full_prop_of rule :: Thm.hyps_of rule) (map fst Ts); |
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
|
66 |
|
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
|
67 |
val (fromnames, tonames, Ts') = |
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 |
fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => |
23171 | 69 |
(ctermify (Free(faken,ty)) :: rnf, |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
70 |
ctermify (Free(n2,ty)) :: rnt, |
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
|
71 |
(n2,ty) :: Ts'')) |
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
|
72 |
(TsFake ~~ Ts ~~ ns) ([], [], []); |
23171 | 73 |
|
74 |
(* rename conflicting free's in the rule to avoid cconflicts |
|
75 |
with introduced vars from bounds outside in redex *) |
|
76 |
val rule' = rule |> Drule.forall_intr_list fromnames |
|
77 |
|> Drule.forall_elim_list tonames; |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
78 |
|
23171 | 79 |
(* make unconditional rule and prems *) |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
80 |
val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') |
23171 | 81 |
rule'; |
82 |
||
83 |
(* using these names create lambda-abstracted version of the rule *) |
|
84 |
val abstractions = rev (Ts' ~~ tonames); |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
85 |
val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => |
23171 | 86 |
Thm.abstract_rule n ct th) |
87 |
(uncond_rule, abstractions); |
|
88 |
in (cprems, abstract_rule) end; |
|
89 |
||
90 |
||
91 |
(* given names to avoid, and vars that need to be fixed, it gives |
|
92 |
unique new names to the vars so that they can be fixed as free |
|
93 |
variables *) |
|
94 |
(* make fixed unique free variable instantiations for non-ground vars *) |
|
95 |
(* 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
|
96 |
other uninstantiated vars in the hyps of the rule |
23171 | 97 |
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
|
98 |
fun mk_renamings ctxt tgt rule_inst = |
23171 | 99 |
let |
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 |
val rule_conds = Thm.prems_of rule_inst; |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
101 |
val (_, cond_vs) = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
102 |
Library.foldl (fn ((tyvs, vs), t) => |
44121 | 103 |
(union (op =) (Misc_Legacy.term_tvars t) tyvs, |
104 |
union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) |
|
23171 | 105 |
(([],[]), rule_conds); |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
106 |
val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); |
33042 | 107 |
val vars_to_fix = union (op =) termvars cond_vs; |
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
|
108 |
val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix); |
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
|
109 |
in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; |
23171 | 110 |
|
111 |
(* make a new fresh typefree instantiation for the given tvar *) |
|
112 |
fun new_tfree (tv as (ix,sort), (pairs,used)) = |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
36945
diff
changeset
|
113 |
let val v = singleton (Name.variant_list used) (string_of_indexname ix) |
23171 | 114 |
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
115 |
||
116 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
117 |
(* make instantiations to fix type variables that are not |
23171 | 118 |
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
|
119 |
fun mk_fixtvar_tyinsts ignore_insts ts = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
120 |
let |
23171 | 121 |
val ignore_ixs = map fst ignore_insts; |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
122 |
val (tvars, tfrees) = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
123 |
List.foldr (fn (t, (varixs, tfrees)) => |
44121 | 124 |
(Misc_Legacy.add_term_tvars (t,varixs), |
125 |
Misc_Legacy.add_term_tfrees (t,tfrees))) |
|
23171 | 126 |
([],[]) ts; |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
127 |
val unfixed_tvars = |
33317 | 128 |
filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; |
30190 | 129 |
val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars |
23171 | 130 |
in (fixtyinsts, tfrees) end; |
131 |
||
132 |
||
133 |
(* cross-instantiate the instantiations - ie for each instantiation |
|
134 |
replace all occurances in other instantiations - no loops are possible |
|
135 |
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
|
136 |
fun cross_inst insts = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
137 |
let |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
138 |
fun instL (ix, (ty,t)) = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
139 |
map (fn (ix2,(ty2,t2)) => |
23171 | 140 |
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); |
141 |
||
142 |
fun cross_instL ([], l) = rev l |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
143 |
| cross_instL ((ix, t) :: insts, l) = |
23171 | 144 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); |
145 |
||
146 |
in cross_instL (insts, []) end; |
|
147 |
||
148 |
(* 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
|
149 |
fun cross_inst_typs insts = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
150 |
let |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
151 |
fun instL (ix, (srt,ty)) = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
152 |
map (fn (ix2,(srt2,ty2)) => |
23171 | 153 |
(ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); |
154 |
||
155 |
fun cross_instL ([], l) = rev l |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
156 |
| cross_instL ((ix, t) :: insts, l) = |
23171 | 157 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); |
158 |
||
159 |
in cross_instL (insts, []) end; |
|
160 |
||
161 |
||
162 |
(* assume that rule and target_thm have distinct var names. THINK: |
|
163 |
efficient version with tables for vars for: target vars, introduced |
|
164 |
vars, and rule vars, for quicker instantiation? The outerterm defines |
|
165 |
which part of the target_thm was modified. Note: we take Ts in the |
|
166 |
upterm order, ie last abstraction first., and with an outeterm where |
|
167 |
the abstracted subterm has the arguments in the revered order, ie |
|
168 |
first abstraction first. FakeTs has abstractions using the fake name |
|
169 |
- ie the name distinct from all other abstractions. *) |
|
170 |
||
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
|
171 |
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
172 |
let |
23171 | 173 |
(* general signature info *) |
174 |
val target_sign = (Thm.theory_of_thm target_thm); |
|
175 |
val ctermify = Thm.cterm_of target_sign; |
|
176 |
val ctypeify = Thm.ctyp_of target_sign; |
|
177 |
||
178 |
(* fix all non-instantiated tvars *) |
|
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
|
179 |
val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) |
23171 | 180 |
mk_fixtvar_tyinsts nonfixed_typinsts |
181 |
[Thm.prop_of rule, Thm.prop_of target_thm]; |
|
182 |
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); |
|
183 |
||
184 |
(* certified instantiations for types *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
185 |
val ctyp_insts = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
186 |
map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) |
23171 | 187 |
typinsts; |
188 |
||
189 |
(* type instantiated versions *) |
|
190 |
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; |
|
191 |
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; |
|
192 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
193 |
val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; |
23171 | 194 |
(* type instanitated outer term *) |
195 |
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; |
|
196 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
197 |
val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) |
23171 | 198 |
FakeTs; |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
199 |
val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) |
23171 | 200 |
Ts; |
201 |
||
202 |
(* type-instantiate the var instantiations *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
203 |
val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) => |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
204 |
(ix, (Term.typ_subst_TVars term_typ_inst ty, |
23171 | 205 |
Term.subst_TVars term_typ_inst t)) |
206 |
:: insts_tyinst) |
|
207 |
[] unprepinsts; |
|
208 |
||
209 |
(* cross-instantiate *) |
|
210 |
val insts_tyinst_inst = cross_inst insts_tyinst; |
|
211 |
||
212 |
(* create certms of instantiations *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
213 |
val cinsts_tyinst = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
214 |
map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), |
23171 | 215 |
ctermify t)) insts_tyinst_inst; |
216 |
||
217 |
(* The instantiated rule *) |
|
218 |
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); |
|
219 |
||
220 |
(* 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
|
221 |
other uninstantiated vars in the hyps the *instantiated* rule |
23171 | 222 |
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
|
223 |
val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
224 |
val cterm_renamings = |
23171 | 225 |
map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings; |
226 |
||
227 |
(* Create the specific version of the rule for this target application *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
228 |
val outerterm_inst = |
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
229 |
outerterm_tyinst |
23171 | 230 |
|> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst) |
231 |
|> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings); |
|
232 |
val couter_inst = Thm.reflexive (ctermify outerterm_inst); |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
233 |
val (cprems, abstract_rule_inst) = |
23171 | 234 |
rule_inst |> Thm.instantiate ([], cterm_renamings) |
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
|
235 |
|> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; |
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
236 |
val specific_tgt_rule = |
23171 | 237 |
beta_eta_contract |
238 |
(Thm.combination couter_inst abstract_rule_inst); |
|
239 |
||
240 |
(* create an instantiated version of the target thm *) |
|
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
241 |
val tgt_th_inst = |
23171 | 242 |
tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) |
243 |
|> Thm.instantiate ([], cterm_renamings); |
|
244 |
||
245 |
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; |
|
246 |
||
247 |
in |
|
248 |
(beta_eta_contract tgt_th_inst) |
|
249 |
|> Thm.equal_elim specific_tgt_rule |
|
250 |
|> Drule.implies_intr_list cprems |
|
251 |
|> Drule.forall_intr_list frees_of_fixed_vars |
|
252 |
|> Drule.forall_elim_list vars |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
33317
diff
changeset
|
253 |
|> Thm.varifyT_global' othertfrees |
23171 | 254 |
|-> K Drule.zero_var_indexes |
255 |
end; |
|
256 |
||
257 |
||
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset
|
258 |
end; |