author  wenzelm 
Wed, 12 Sep 2012 22:00:29 +0200  
changeset 49339  d1fcb4de8349 
parent 44121  44adaa6db327 
child 49340  25fc6e0da459 
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 

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

15 
val rw : 

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 
(* betaeta 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 
(* to get the free names of a theorem (including hyps and flexes) *) 

41 
fun usednames_of_thm th = 

42 
let val rep = Thm.rep_thm th 

43 
val hyps = #hyps rep 

44 
val (tpairl,tpairr) = Library.split_list (#tpairs rep) 

45 
val prop = #prop rep 

46 
in 

44121  47 
List.foldr Misc_Legacy.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps))) 
23171  48 
end; 
49 

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

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

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

53 
lambdaparams: 

54 

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

55 
Ts: 
23171  56 
("x", ty) 
57 

58 
rule:: 

59 
C :x ==> P :x = Q :x 

60 

61 
results in: 

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

63 

64 
note: assumes rule is instantiated 

65 
*) 

66 
(* Note, we take abstraction in the order of last abstraction first *) 

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

67 
fun mk_abstractedrule TsFake Ts rule = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

68 
let 
23171  69 
val ctermify = Thm.cterm_of (Thm.theory_of_thm rule); 
70 

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

71 
(* now we change the names of temporary free vars that represent 
23171  72 
bound vars with binders outside the redex *) 
73 
val names = usednames_of_thm rule; 

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

74 
val (fromnames,tonames,_,Ts') = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

75 
Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
36945
diff
changeset

76 
let val n2 = singleton (Name.variant_list names) n in 
23171  77 
(ctermify (Free(faken,ty)) :: rnf, 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

78 
ctermify (Free(n2,ty)) :: rnt, 
23171  79 
n2 :: names, 
80 
(n2,ty) :: Ts'') 

81 
end) 

82 
(([],[],names, []), TsFake~~Ts); 

83 

84 
(* rename conflicting free's in the rule to avoid cconflicts 

85 
with introduced vars from bounds outside in redex *) 

86 
val rule' = rule > Drule.forall_intr_list fromnames 

87 
> Drule.forall_elim_list tonames; 

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

88 

23171  89 
(* make unconditional rule and prems *) 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

90 
val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
23171  91 
rule'; 
92 

93 
(* using these names create lambdaabstracted version of the rule *) 

94 
val abstractions = rev (Ts' ~~ tonames); 

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

95 
val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
23171  96 
Thm.abstract_rule n ct th) 
97 
(uncond_rule, abstractions); 

98 
in (cprems, abstract_rule) end; 

99 

100 

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

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

103 
variables *) 

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

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

106 
other uninstantiated vars in the hyps of the rule 
23171  107 
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

108 
fun mk_renamings tgt rule_inst = 
23171  109 
let 
110 
val rule_conds = Thm.prems_of rule_inst 

44121  111 
val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds); 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

112 
val (_, cond_vs) = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

113 
Library.foldl (fn ((tyvs, vs), t) => 
44121  114 
(union (op =) (Misc_Legacy.term_tvars t) tyvs, 
115 
union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) 

23171  116 
(([],[]), rule_conds); 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

117 
val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); 
33042  118 
val vars_to_fix = union (op =) termvars cond_vs; 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

119 
val (renamings, _) = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

120 
List.foldr (fn (((n,i),ty), (vs, names')) => 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
36945
diff
changeset

121 
let val n' = singleton (Name.variant_list names') n in 
23171  122 
((((n,i),ty), Free (n', ty)) :: vs, n'::names') 
123 
end) 

124 
([], names) vars_to_fix; 

125 
in renamings end; 

126 

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

128 
fun new_tfree (tv as (ix,sort), (pairs,used)) = 

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
36945
diff
changeset

129 
let val v = singleton (Name.variant_list used) (string_of_indexname ix) 
23171  130 
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end; 
131 

132 

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

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

135 
fun mk_fixtvar_tyinsts ignore_insts ts = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

136 
let 
23171  137 
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

138 
val (tvars, tfrees) = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

139 
List.foldr (fn (t, (varixs, tfrees)) => 
44121  140 
(Misc_Legacy.add_term_tvars (t,varixs), 
141 
Misc_Legacy.add_term_tfrees (t,tfrees))) 

23171  142 
([],[]) ts; 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

143 
val unfixed_tvars = 
33317  144 
filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; 
30190  145 
val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars 
23171  146 
in (fixtyinsts, tfrees) end; 
147 

148 

149 
(* crossinstantiate the instantiations  ie for each instantiation 

150 
replace all occurances in other instantiations  no loops are possible 

151 
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

152 
fun cross_inst insts = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

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

154 
fun instL (ix, (ty,t)) = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

155 
map (fn (ix2,(ty2,t2)) => 
23171  156 
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2))); 
157 

158 
fun cross_instL ([], l) = rev l 

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

159 
 cross_instL ((ix, t) :: insts, l) = 
23171  160 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
161 

162 
in cross_instL (insts, []) end; 

163 

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

165 
fun cross_inst_typs insts = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

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

167 
fun instL (ix, (srt,ty)) = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

168 
map (fn (ix2,(srt2,ty2)) => 
23171  169 
(ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2))); 
170 

171 
fun cross_instL ([], l) = rev l 

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

172 
 cross_instL ((ix, t) :: insts, l) = 
23171  173 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
174 

175 
in cross_instL (insts, []) end; 

176 

177 

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

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

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

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

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

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

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

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

186 

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

187 
fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

188 
let 
23171  189 
(* general signature info *) 
190 
val target_sign = (Thm.theory_of_thm target_thm); 

191 
val ctermify = Thm.cterm_of target_sign; 

192 
val ctypeify = Thm.ctyp_of target_sign; 

193 

194 
(* fix all noninstantiated tvars *) 

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

195 
val (fixtyinsts, othertfrees) = 
23171  196 
mk_fixtvar_tyinsts nonfixed_typinsts 
197 
[Thm.prop_of rule, Thm.prop_of target_thm]; 

198 
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); 

199 

200 
(* certified instantiations for types *) 

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

201 
val ctyp_insts = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

202 
map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
23171  203 
typinsts; 
204 

205 
(* type instantiated versions *) 

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

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

208 

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

209 
val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; 
23171  210 
(* type instanitated outer term *) 
211 
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; 

212 

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

213 
val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
23171  214 
FakeTs; 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

215 
val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
23171  216 
Ts; 
217 

218 
(* typeinstantiate the var instantiations *) 

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

219 
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

220 
(ix, (Term.typ_subst_TVars term_typ_inst ty, 
23171  221 
Term.subst_TVars term_typ_inst t)) 
222 
:: insts_tyinst) 

223 
[] unprepinsts; 

224 

225 
(* crossinstantiate *) 

226 
val insts_tyinst_inst = cross_inst insts_tyinst; 

227 

228 
(* create certms of instantiations *) 

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

229 
val cinsts_tyinst = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

230 
map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
23171  231 
ctermify t)) insts_tyinst_inst; 
232 

233 
(* The instantiated rule *) 

234 
val rule_inst = rule_tyinst > Thm.instantiate ([], cinsts_tyinst); 

235 

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

237 
other uninstantiated vars in the hyps the *instantiated* rule 
23171  238 
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *) 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

239 
val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
23171  240 
rule_inst; 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

241 
val cterm_renamings = 
23171  242 
map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings; 
243 

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

245 
val outerterm_inst = 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44121
diff
changeset

246 
outerterm_tyinst 
23171  247 
> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst) 
248 
> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings); 

249 
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

250 
val (cprems, abstract_rule_inst) = 
23171  251 
rule_inst > Thm.instantiate ([], cterm_renamings) 
252 
> mk_abstractedrule FakeTs_tyinst Ts_tyinst; 

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

253 
val specific_tgt_rule = 
23171  254 
beta_eta_contract 
255 
(Thm.combination couter_inst abstract_rule_inst); 

256 

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

258 
val tgt_th_inst = 
23171  259 
tgt_th_tyinst > Thm.instantiate ([], cinsts_tyinst) 
260 
> Thm.instantiate ([], cterm_renamings); 

261 

262 
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; 

263 

264 
in 

265 
(beta_eta_contract tgt_th_inst) 

266 
> Thm.equal_elim specific_tgt_rule 

267 
> Drule.implies_intr_list cprems 

268 
> Drule.forall_intr_list frees_of_fixed_vars 

269 
> 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

270 
> Thm.varifyT_global' othertfrees 
23171  271 
> K Drule.zero_var_indexes 
272 
end; 

273 

274 

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

275 
end; 