author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 52245  f76fb8858e0b 
child 58318  f95754ca7082 
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 

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 
*) 

33 
fun allify_conditions Ts th = 

34 
let 

35 
val cert = Thm.cterm_of (Thm.theory_of_thm th); 

36 

37 
fun allify (x, T) t = 

38 
Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t)); 

39 

40 
val cTs = map (cert o Free) Ts; 

41 
val cterm_asms = map (cert o fold_rev allify Ts) (Thm.prems_of th); 

42 
val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; 

43 
in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; 

44 

45 

23171  46 
(* Given a list of variables that were bound, and a that has been 
47 
instantiated with free variable placeholders for the bound vars, it 

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

49 
lambdaparams: 

50 

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

51 
Ts: 
23171  52 
("x", ty) 
53 

54 
rule:: 

55 
C :x ==> P :x = Q :x 

56 

57 
results in: 

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

59 

60 
note: assumes rule is instantiated 

61 
*) 

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

63 
fun mk_abstractedrule ctxt TsFake Ts rule = 
52240  64 
let 
65 
val cert = Thm.cterm_of (Thm.theory_of_thm rule); 

23171  66 

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

69 

52240  70 
val ns = 
71 
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

72 

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

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

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

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

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

23171  79 

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

82 
val rule' = rule 

83 
> Drule.forall_intr_list fromnames 

84 
> Drule.forall_elim_list tonames; 

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

85 

52240  86 
(* make unconditional rule and prems *) 
52245  87 
val (uncond_rule, cprems) = allify_conditions (rev Ts') rule'; 
23171  88 

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

91 
val abstract_rule = 

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

52240  94 
in (cprems, abstract_rule) end; 
23171  95 

96 

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

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

99 
variables *) 

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

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

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

104 
fun mk_renamings ctxt tgt rule_inst = 
52240  105 
let 
106 
val rule_conds = Thm.prems_of rule_inst; 

107 
val (_, cond_vs) = 

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

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

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

113 
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

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

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

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

23171  120 

121 

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

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

124 
fun mk_fixtvar_tyinsts ignore_insts ts = 
52240  125 
let 
126 
val ignore_ixs = map fst ignore_insts; 

127 
val (tvars, tfrees) = 

52242  128 
fold_rev (fn t => fn (varixs, tfrees) => 
52240  129 
(Misc_Legacy.add_term_tvars (t,varixs), 
52242  130 
Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []); 
52240  131 
val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; 
52242  132 
val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees) 
52240  133 
in (fixtyinsts, tfrees) end; 
23171  134 

135 

136 
(* crossinstantiate the instantiations  ie for each instantiation 

137 
replace all occurances in other instantiations  no loops are possible 

138 
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

139 
fun cross_inst insts = 
52240  140 
let 
141 
fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => 

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

23171  143 

52240  144 
fun cross_instL ([], l) = rev l 
145 
 cross_instL ((ix, t) :: insts, l) = 

23171  146 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
147 

52240  148 
in cross_instL (insts, []) end; 
23171  149 

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

151 
fun cross_inst_typs insts = 
52240  152 
let 
153 
fun instL (ix, (srt,ty)) = 

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

23171  155 

52240  156 
fun cross_instL ([], l) = rev l 
157 
 cross_instL ((ix, t) :: insts, l) = 

23171  158 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
159 

52240  160 
in cross_instL (insts, []) end; 
23171  161 

162 

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

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

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

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

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

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

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

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

171 

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

172 
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
52240  173 
let 
174 
val thy = Thm.theory_of_thm target_thm; 

175 
val cert = Thm.cterm_of thy; 

176 
val certT = Thm.ctyp_of thy; 

23171  177 

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

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); 

23171  183 

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

186 

187 
(* type instantiated versions *) 

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

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

23171  190 

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

193 
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; 

23171  194 

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

23171  197 

52240  198 
(* typeinstantiate the var instantiations *) 
199 
val insts_tyinst = 

52242  200 
fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => 
52240  201 
(ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) 
52242  202 
:: insts_tyinst) unprepinsts []; 
23171  203 

52240  204 
(* crossinstantiate *) 
205 
val insts_tyinst_inst = cross_inst insts_tyinst; 

23171  206 

52240  207 
(* create certms of instantiations *) 
208 
val cinsts_tyinst = 

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

23171  210 

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

23171  213 

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

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

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

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

23171  219 

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

222 
outerterm_tyinst 

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

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

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

226 
val (cprems, abstract_rule_inst) = 

227 
rule_inst 

228 
> Thm.instantiate ([], cterm_renamings) 

229 
> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; 

230 
val specific_tgt_rule = 

231 
Conv.fconv_rule Drule.beta_eta_conversion 

232 
(Thm.combination couter_inst abstract_rule_inst); 

23171  233 

52240  234 
(* create an instantiated version of the target thm *) 
235 
val tgt_th_inst = 

236 
tgt_th_tyinst 

237 
> Thm.instantiate ([], cinsts_tyinst) 

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

23171  239 

52240  240 
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; 
241 
in 

242 
Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst 

243 
> Thm.equal_elim specific_tgt_rule 

244 
> Drule.implies_intr_list cprems 

245 
> Drule.forall_intr_list frees_of_fixed_vars 

246 
> Drule.forall_elim_list vars 

247 
> Thm.varifyT_global' othertfrees 

248 
> K Drule.zero_var_indexes 

249 
end; 

23171  250 

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

251 
end; 