author  wenzelm 
Thu, 30 May 2013 16:53:32 +0200  
changeset 52242  2d634bfa1bbf 
parent 52240  066c2ff17f7c 
child 52245  f76fb8858e0b 
permissions  rwrr 
23175  1 
(* Title: Tools/IsaPlanner/rw_inst.ML 
23171  2 
Author: Lucas Dixon, University of Edinburgh 
3 

23175  4 
Rewriting using a conditional metaequality 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 

24 
(* Given a list of variables that were bound, and a that has been 

25 
instantiated with free variable placeholders for the bound vars, it 

26 
creates an abstracted version of the theorem, with local bound vars as 

27 
lambdaparams: 

28 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

29 
Ts: 
23171  30 
("x", ty) 
31 

32 
rule:: 

33 
C :x ==> P :x = Q :x 

34 

35 
results in: 

36 
("!! x. C x", (%x. p x = %y. p y) [!! x. C x]) 

37 

38 
note: assumes rule is instantiated 

39 
*) 

40 
(* 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

41 
fun mk_abstractedrule ctxt TsFake Ts rule = 
52240  42 
let 
43 
val cert = Thm.cterm_of (Thm.theory_of_thm rule); 

23171  44 

52240  45 
(* now we change the names of temporary free vars that represent 
46 
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

47 

52240  48 
val ns = 
49 
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

50 

52240  51 
val (fromnames, tonames, Ts') = 
52 
fold (fn (((faken, _), (n, ty)), n2) => fn (rnf, rnt, Ts'') => 

53 
(cert (Free(faken,ty)) :: rnf, 

54 
cert (Free(n2,ty)) :: rnt, 

55 
(n2,ty) :: Ts'')) 

56 
(TsFake ~~ Ts ~~ ns) ([], [], []); 

23171  57 

52240  58 
(* rename conflicting free's in the rule to avoid cconflicts 
59 
with introduced vars from bounds outside in redex *) 

60 
val rule' = rule 

61 
> Drule.forall_intr_list fromnames 

62 
> Drule.forall_elim_list tonames; 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

63 

52240  64 
(* make unconditional rule and prems *) 
65 
val (uncond_rule, cprems) = IsaND.allify_conditions cert (rev Ts') rule'; 

23171  66 

52240  67 
(* using these names create lambdaabstracted version of the rule *) 
68 
val abstractions = rev (Ts' ~~ tonames); 

69 
val abstract_rule = 

52242  70 
fold (fn ((n, ty), ct) => Thm.abstract_rule n ct) 
71 
abstractions uncond_rule; 

52240  72 
in (cprems, abstract_rule) end; 
23171  73 

74 

75 
(* given names to avoid, and vars that need to be fixed, it gives 

76 
unique new names to the vars so that they can be fixed as free 

77 
variables *) 

78 
(* make fixed unique free variable instantiations for nonground vars *) 

79 
(* 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

80 
other uninstantiated vars in the hyps of the rule 
23171  81 
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

82 
fun mk_renamings ctxt tgt rule_inst = 
52240  83 
let 
84 
val rule_conds = Thm.prems_of rule_inst; 

85 
val (_, cond_vs) = 

52242  86 
fold (fn t => fn (tyvs, vs) => 
87 
(union (op =) (Misc_Legacy.term_tvars t) tyvs, 

88 
union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []); 

52240  89 
val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); 
90 
val vars_to_fix = union (op =) termvars cond_vs; 

91 
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

92 
in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end; 
23171  93 

94 
(* make a new fresh typefree instantiation for the given tvar *) 

52242  95 
fun new_tfree (tv as (ix,sort)) (pairs, used) = 
52240  96 
let val v = singleton (Name.variant_list used) (string_of_indexname ix) 
97 
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; 

23171  98 

99 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

100 
(* make instantiations to fix type variables that are not 
23171  101 
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

102 
fun mk_fixtvar_tyinsts ignore_insts ts = 
52240  103 
let 
104 
val ignore_ixs = map fst ignore_insts; 

105 
val (tvars, tfrees) = 

52242  106 
fold_rev (fn t => fn (varixs, tfrees) => 
52240  107 
(Misc_Legacy.add_term_tvars (t,varixs), 
52242  108 
Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); 
52240  109 
val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; 
52242  110 
val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) 
52240  111 
in (fixtyinsts, tfrees) end; 
23171  112 

113 

114 
(* crossinstantiate the instantiations  ie for each instantiation 

115 
replace all occurances in other instantiations  no loops are possible 

116 
and thus only oneparsing of the instantiations is necessary. *) 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

117 
fun cross_inst insts = 
52240  118 
let 
119 
fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => 

120 
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); 

23171  121 

52240  122 
fun cross_instL ([], l) = rev l 
123 
 cross_instL ((ix, t) :: insts, l) = 

23171  124 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
125 

52240  126 
in cross_instL (insts, []) end; 
23171  127 

128 
(* 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

129 
fun cross_inst_typs insts = 
52240  130 
let 
131 
fun instL (ix, (srt,ty)) = 

132 
map (fn (ix2,(srt2,ty2)) => (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); 

23171  133 

52240  134 
fun cross_instL ([], l) = rev l 
135 
 cross_instL ((ix, t) :: insts, l) = 

23171  136 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
137 

52240  138 
in cross_instL (insts, []) end; 
23171  139 

140 

141 
(* assume that rule and target_thm have distinct var names. THINK: 

142 
efficient version with tables for vars for: target vars, introduced 

143 
vars, and rule vars, for quicker instantiation? The outerterm defines 

144 
which part of the target_thm was modified. Note: we take Ts in the 

145 
upterm order, ie last abstraction first., and with an outeterm where 

146 
the abstracted subterm has the arguments in the revered order, ie 

147 
first abstraction first. FakeTs has abstractions using the fake name 

148 
 ie the name distinct from all other abstractions. *) 

149 

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

150 
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
52240  151 
let 
152 
val thy = Thm.theory_of_thm target_thm; 

153 
val cert = Thm.cterm_of thy; 

154 
val certT = Thm.ctyp_of thy; 

23171  155 

52240  156 
(* fix all noninstantiated tvars *) 
157 
val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) 

158 
mk_fixtvar_tyinsts nonfixed_typinsts 

159 
[Thm.prop_of rule, Thm.prop_of target_thm]; 

160 
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); 

23171  161 

52240  162 
(* certified instantiations for types *) 
163 
val ctyp_insts = map (fn (ix, (s, ty)) => (certT (TVar (ix, s)), certT ty)) typinsts; 

164 

165 
(* type instantiated versions *) 

166 
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; 

167 
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; 

23171  168 

52240  169 
val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; 
170 
(* type instanitated outer term *) 

171 
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; 

23171  172 

52240  173 
val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) FakeTs; 
174 
val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) Ts; 

23171  175 

52240  176 
(* typeinstantiate the var instantiations *) 
177 
val insts_tyinst = 

52242  178 
fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => 
52240  179 
(ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) 
52242  180 
:: insts_tyinst) unprepinsts []; 
23171  181 

52240  182 
(* crossinstantiate *) 
183 
val insts_tyinst_inst = cross_inst insts_tyinst; 

23171  184 

52240  185 
(* create certms of instantiations *) 
186 
val cinsts_tyinst = 

187 
map (fn (ix, (ty, t)) => (cert (Var (ix, ty)), cert t)) insts_tyinst_inst; 

23171  188 

52240  189 
(* The instantiated rule *) 
190 
val rule_inst = rule_tyinst > Thm.instantiate ([], cinsts_tyinst); 

23171  191 

52240  192 
(* Create a table of vars to be renamed after instantiation  ie 
193 
other uninstantiated vars in the hyps the *instantiated* rule 

194 
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) 

195 
val renamings = mk_renamings ctxt (Thm.prop_of tgt_th_tyinst) rule_inst; 

196 
val cterm_renamings = map (fn (x, y) => (cert (Var x), cert y)) renamings; 

23171  197 

52240  198 
(* Create the specific version of the rule for this target application *) 
199 
val outerterm_inst = 

200 
outerterm_tyinst 

201 
> Term.subst_Vars (map (fn (ix, (ty, t)) => (ix, t)) insts_tyinst_inst) 

202 
> Term.subst_Vars (map (fn ((ix, ty), t) => (ix, t)) renamings); 

203 
val couter_inst = Thm.reflexive (cert outerterm_inst); 

204 
val (cprems, abstract_rule_inst) = 

205 
rule_inst 

206 
> Thm.instantiate ([], cterm_renamings) 

207 
> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; 

208 
val specific_tgt_rule = 

209 
Conv.fconv_rule Drule.beta_eta_conversion 

210 
(Thm.combination couter_inst abstract_rule_inst); 

23171  211 

52240  212 
(* create an instantiated version of the target thm *) 
213 
val tgt_th_inst = 

214 
tgt_th_tyinst 

215 
> Thm.instantiate ([], cinsts_tyinst) 

216 
> Thm.instantiate ([], cterm_renamings); 

23171  217 

52240  218 
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; 
219 
in 

220 
Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst 

221 
> Thm.equal_elim specific_tgt_rule 

222 
> Drule.implies_intr_list cprems 

223 
> Drule.forall_intr_list frees_of_fixed_vars 

224 
> Drule.forall_elim_list vars 

225 
> Thm.varifyT_global' othertfrees 

226 
> K Drule.zero_var_indexes 

227 
end; 

23171  228 

49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

229 
end; 