author | wenzelm |
Thu, 02 Jun 2005 09:11:32 +0200 | |
changeset 16179 | fa7e70be26b0 |
parent 15959 | 366d39e95d3c |
child 18127 | 9f03d8a9a81b |
permissions | -rw-r--r-- |
15481 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
16179 | 2 |
(* Title: Pure/IsaPlanner/rw_inst.ML |
3 |
ID: $Id$ |
|
15481 | 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 : |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
22 |
((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *) |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
23 |
(Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
24 |
* (string * Term.typ) list (* Fake named bounds + types *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
25 |
* (string * Term.typ) list (* names of bound + types *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
26 |
* Term.term -> (* outer term for instantiation *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
27 |
Thm.thm -> (* rule with indexies lifted *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
28 |
Thm.thm -> (* target thm *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
29 |
Thm.thm (* rewritten theorem possibly |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
30 |
with additional premises for |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
31 |
rule conditions *) |
15481 | 32 |
|
33 |
(* used tools *) |
|
34 |
val mk_abstractedrule : |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
35 |
(string * Term.typ) list (* faked outer bound *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
36 |
-> (string * Term.typ) list (* hopeful name of outer bounds *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
37 |
-> Thm.thm -> Thm.cterm list * Thm.thm |
15481 | 38 |
val mk_fixtvar_tyinsts : |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
39 |
(Term.indexname * (Term.sort * Term.typ)) list -> |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
40 |
Term.term list -> ((string * int) * (Term.sort * Term.typ)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
41 |
* (string * Term.sort) list |
15481 | 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) * |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
46 |
(((string * int) * (Term.sort * Term.typ)) list * string list) -> |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
47 |
((string * int) * (Term.sort * Term.typ)) list * string list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
48 |
val cross_inst : (Term.indexname * (Term.typ * Term.term)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
49 |
-> (Term.indexname *(Term.typ * Term.term)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
50 |
val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
51 |
-> (Term.indexname * (Term.sort * Term.typ)) list |
15481 | 52 |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
53 |
val beta_contract : Thm.thm -> Thm.thm |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
54 |
val beta_eta_contract : Thm.thm -> Thm.thm |
15481 | 55 |
|
56 |
end; |
|
57 |
||
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
58 |
structure RWInst |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
59 |
(* : RW_INST *) |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
60 |
= struct |
15481 | 61 |
|
62 |
||
63 |
(* beta contract the theorem *) |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
64 |
fun beta_contract thm = |
15481 | 65 |
equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; |
66 |
||
67 |
(* beta-eta contract the theorem *) |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
68 |
fun beta_eta_contract thm = |
15481 | 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 |
(* Given a list of variables that were bound, and a that has been |
|
75 |
instantiated with free variable placeholders for the bound vars, it |
|
76 |
creates an abstracted version of the theorem, with local bound vars as |
|
77 |
lambda-params: |
|
78 |
||
79 |
Ts: |
|
80 |
("x", ty) |
|
81 |
||
82 |
rule:: |
|
83 |
C :x ==> P :x = Q :x |
|
84 |
||
85 |
results in: |
|
86 |
("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) |
|
87 |
||
88 |
note: assumes rule is instantiated |
|
89 |
*) |
|
90 |
(* Note, we take abstraction in the order of last abstraction first *) |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
91 |
fun mk_abstractedrule TsFake Ts rule = |
15481 | 92 |
let |
93 |
val ctermify = Thm.cterm_of (Thm.sign_of_thm rule); |
|
94 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
95 |
(* now we change the names of temporary free vars that represent |
15481 | 96 |
bound vars with binders outside the redex *) |
97 |
val prop = Thm.prop_of rule; |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
98 |
val names = TermLib.usednames_of_thm rule; |
15560
c862d556fb18
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon
parents:
15481
diff
changeset
|
99 |
val (fromnames,tonames,names2,Ts') = |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
100 |
Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => |
15481 | 101 |
let val n2 = Term.variant names n in |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
102 |
(ctermify (Free(faken,ty)) :: rnf, |
15481 | 103 |
ctermify (Free(n2,ty)) :: rnt, |
15560
c862d556fb18
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon
parents:
15481
diff
changeset
|
104 |
n2 :: names, |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
105 |
(n2,ty) :: Ts'') |
15481 | 106 |
end) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
107 |
(([],[],names, []), TsFake~~Ts); |
15560
c862d556fb18
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon
parents:
15481
diff
changeset
|
108 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
109 |
(* rename conflicting free's in the rule to avoid cconflicts |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
110 |
with introduced vars from bounds outside in redex *) |
15481 | 111 |
val rule' = rule |> Drule.forall_intr_list fromnames |
112 |
|> Drule.forall_elim_list tonames; |
|
113 |
||
114 |
(* make unconditional rule and prems *) |
|
15560
c862d556fb18
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon
parents:
15481
diff
changeset
|
115 |
val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') |
c862d556fb18
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon
parents:
15481
diff
changeset
|
116 |
rule'; |
15481 | 117 |
|
118 |
(* using these names create lambda-abstracted version of the rule *) |
|
15560
c862d556fb18
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
dixon
parents:
15481
diff
changeset
|
119 |
val abstractions = rev (Ts' ~~ tonames); |
15570 | 120 |
val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => |
15481 | 121 |
Thm.abstract_rule n ct th) |
122 |
(uncond_rule, abstractions); |
|
123 |
in (cprems, abstract_rule) end; |
|
124 |
||
125 |
||
126 |
(* given names to avoid, and vars that need to be fixed, it gives |
|
127 |
unique new names to the vars so that they can be fixed as free |
|
128 |
variables *) |
|
129 |
(* make fixed unique free variable instantiations for non-ground vars *) |
|
130 |
(* Create a table of vars to be renamed after instantiation - ie |
|
131 |
other uninstantiated vars in the hyps of the rule |
|
132 |
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) |
|
133 |
fun mk_renamings tgt rule_inst = |
|
134 |
let |
|
135 |
val rule_conds = Thm.prems_of rule_inst |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
136 |
val names = foldr Term.add_term_names [] (tgt :: rule_conds); |
15481 | 137 |
val (conds_tyvs,cond_vs) = |
15570 | 138 |
Library.foldl (fn ((tyvs, vs), t) => |
15481 | 139 |
(Library.union |
140 |
(Term.term_tvars t, tyvs), |
|
141 |
Library.union |
|
142 |
(map Term.dest_Var (Term.term_vars t), vs))) |
|
143 |
(([],[]), rule_conds); |
|
144 |
val termvars = map Term.dest_Var (Term.term_vars tgt); |
|
145 |
val vars_to_fix = Library.union (termvars, cond_vs); |
|
146 |
val (renamings, names2) = |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
147 |
foldr (fn (((n,i),ty), (vs, names')) => |
15481 | 148 |
let val n' = Term.variant names' n in |
149 |
((((n,i),ty), Free (n', ty)) :: vs, n'::names') |
|
150 |
end) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
151 |
([], names) vars_to_fix; |
15481 | 152 |
in renamings end; |
153 |
||
154 |
(* make a new fresh typefree instantiation for the given tvar *) |
|
155 |
fun new_tfree (tv as (ix,sort), (pairs,used)) = |
|
156 |
let val v = variant used (string_of_indexname ix) |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
157 |
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; |
15481 | 158 |
|
159 |
||
160 |
(* make instantiations to fix type variables that are not |
|
161 |
already instantiated (in ignore_ixs) from the list of terms. *) |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
162 |
fun mk_fixtvar_tyinsts ignore_insts ts = |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
163 |
let |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
164 |
val ignore_ixs = map fst ignore_insts; |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
165 |
val (tvars, tfrees) = |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
166 |
foldr (fn (t, (varixs, tfrees)) => |
15481 | 167 |
(Term.add_term_tvars (t,varixs), |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
168 |
Term.add_term_tfrees (t,tfrees))) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
169 |
([],[]) ts; |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
170 |
val unfixed_tvars = |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
171 |
List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars; |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
172 |
val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
173 |
in (fixtyinsts, tfrees) end; |
15481 | 174 |
|
175 |
||
176 |
(* cross-instantiate the instantiations - ie for each instantiation |
|
177 |
replace all occurances in other instantiations - no loops are possible |
|
178 |
and thus only one-parsing of the instantiations is necessary. *) |
|
179 |
fun cross_inst insts = |
|
180 |
let |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
181 |
fun instL (ix, (ty,t)) = |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
182 |
map (fn (ix2,(ty2,t2)) => |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
183 |
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); |
15481 | 184 |
|
185 |
fun cross_instL ([], l) = rev l |
|
186 |
| cross_instL ((ix, t) :: insts, l) = |
|
187 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); |
|
188 |
||
189 |
in cross_instL (insts, []) end; |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
190 |
|
15481 | 191 |
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *) |
192 |
fun cross_inst_typs insts = |
|
193 |
let |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
194 |
fun instL (ix, (srt,ty)) = |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
195 |
map (fn (ix2,(srt2,ty2)) => |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
196 |
(ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); |
15481 | 197 |
|
198 |
fun cross_instL ([], l) = rev l |
|
199 |
| cross_instL ((ix, t) :: insts, l) = |
|
200 |
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); |
|
201 |
||
202 |
in cross_instL (insts, []) end; |
|
203 |
||
204 |
||
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
205 |
(* assume that rule and target_thm have distinct var names. THINK: |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
206 |
efficient version with tables for vars for: target vars, introduced |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
207 |
vars, and rule vars, for quicker instantiation? The outerterm defines |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
208 |
which part of the target_thm was modified. Note: we take Ts in the |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
209 |
upterm order, ie last abstraction first., and with an outeterm where |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
210 |
the abstracted subterm has the arguments in the revered order, ie |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
211 |
first abstraction first. FakeTs has abstractions using the fake name |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
212 |
- ie the name distinct from all other abstractions. *) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
213 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15798
diff
changeset
|
214 |
fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = |
15481 | 215 |
let |
216 |
(* general signature info *) |
|
217 |
val target_sign = (Thm.sign_of_thm target_thm); |
|
218 |
val ctermify = Thm.cterm_of target_sign; |
|
219 |
val ctypeify = Thm.ctyp_of target_sign; |
|
220 |
||
221 |
(* fix all non-instantiated tvars *) |
|
222 |
val (fixtyinsts, othertfrees) = |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
223 |
mk_fixtvar_tyinsts nonfixed_typinsts |
15481 | 224 |
[Thm.prop_of rule, Thm.prop_of target_thm]; |
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
225 |
val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty)) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
226 |
fixtyinsts; |
15481 | 227 |
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); |
228 |
||
229 |
(* certified instantiations for types *) |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
230 |
val ctyp_insts = |
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
231 |
map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
232 |
typinsts; |
15481 | 233 |
|
234 |
(* type instantiated versions *) |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
235 |
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
236 |
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; |
15481 | 237 |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
238 |
val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts; |
15481 | 239 |
(* type instanitated outer term *) |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
240 |
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; |
15481 | 241 |
|
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
242 |
val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
243 |
FakeTs; |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
244 |
val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
245 |
Ts; |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
246 |
|
15481 | 247 |
(* type-instantiate the var instantiations *) |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
248 |
val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
249 |
(ix, (Term.typ_subst_TVars term_typ_inst ty, |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
250 |
Term.subst_TVars term_typ_inst t)) |
15481 | 251 |
:: insts_tyinst) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
252 |
[] unprepinsts; |
15481 | 253 |
|
254 |
(* cross-instantiate *) |
|
255 |
val insts_tyinst_inst = cross_inst insts_tyinst; |
|
256 |
||
257 |
(* create certms of instantiations *) |
|
258 |
val cinsts_tyinst = |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
259 |
map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
260 |
ctermify t)) insts_tyinst_inst; |
15481 | 261 |
|
262 |
(* The instantiated rule *) |
|
263 |
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); |
|
264 |
||
265 |
(* Create a table of vars to be renamed after instantiation - ie |
|
266 |
other uninstantiated vars in the hyps the *instantiated* rule |
|
267 |
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) |
|
268 |
val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) |
|
269 |
rule_inst; |
|
270 |
val cterm_renamings = |
|
271 |
map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings; |
|
272 |
||
273 |
(* Create the specific version of the rule for this target application *) |
|
274 |
val outerterm_inst = |
|
275 |
outerterm_tyinst |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
276 |
|> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst) |
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
277 |
|> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings); |
15481 | 278 |
val couter_inst = Thm.reflexive (ctermify outerterm_inst); |
279 |
val (cprems, abstract_rule_inst) = |
|
280 |
rule_inst |> Thm.instantiate ([], cterm_renamings) |
|
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15915
diff
changeset
|
281 |
|> mk_abstractedrule FakeTs_tyinst Ts_tyinst; |
15481 | 282 |
val specific_tgt_rule = |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
283 |
beta_eta_contract |
15481 | 284 |
(Thm.combination couter_inst abstract_rule_inst); |
285 |
||
286 |
(* create an instantiated version of the target thm *) |
|
287 |
val tgt_th_inst = |
|
288 |
tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) |
|
289 |
|> Thm.instantiate ([], cterm_renamings); |
|
290 |
||
291 |
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; |
|
292 |
||
293 |
in |
|
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15814
diff
changeset
|
294 |
(beta_eta_contract tgt_th_inst) |
15481 | 295 |
|> Thm.equal_elim specific_tgt_rule |
296 |
|> Drule.implies_intr_list cprems |
|
297 |
|> Drule.forall_intr_list frees_of_fixed_vars |
|
298 |
|> Drule.forall_elim_list vars |
|
299 |
|> fst o Thm.varifyT' othertfrees |
|
300 |
|> Drule.zero_var_indexes |
|
301 |
end; |
|
302 |
||
303 |
||
304 |
end; (* struct *) |