author  wenzelm 
Thu, 07 Apr 2016 20:51:52 +0200  
changeset 62908  d7009a515733 
parent 60642  48dd1cefb4ae 
child 74233  9eff7c673b42 
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 
*) 

60358  33 
fun allify_conditions ctxt Ts th = 
52245  34 
let 
35 
fun allify (x, T) t = 

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

37 

60358  38 
val cTs = map (Thm.cterm_of ctxt o Free) Ts; 
39 
val cterm_asms = map (Thm.cterm_of ctxt o fold_rev allify Ts) (Thm.prems_of th); 

52245  40 
val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms; 
41 
in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end; 

42 

43 

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

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

47 
lambdaparams: 

48 

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

49 
Ts: 
23171  50 
("x", ty) 
51 

52 
rule:: 

53 
C :x ==> P :x = Q :x 

54 

55 
results in: 

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

57 

58 
note: assumes rule is instantiated 

59 
*) 

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

61 
fun mk_abstractedrule ctxt TsFake Ts rule = 
52240  62 
let 
63 
(* now we change the names of temporary free vars that represent 

64 
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

65 

52240  66 
val ns = 
67 
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

68 

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

59641  71 
(Thm.cterm_of ctxt (Free(faken,ty)) :: rnf, 
72 
Thm.cterm_of ctxt (Free(n2,ty)) :: rnt, 

52240  73 
(n2,ty) :: Ts'')) 
74 
(TsFake ~~ Ts ~~ ns) ([], [], []); 

23171  75 

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

78 
val rule' = rule 

79 
> Drule.forall_intr_list fromnames 

80 
> Drule.forall_elim_list tonames; 

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

81 

52240  82 
(* make unconditional rule and prems *) 
60358  83 
val (uncond_rule, cprems) = allify_conditions ctxt (rev Ts') rule'; 
23171  84 

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

87 
val abstract_rule = 

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

52240  90 
in (cprems, abstract_rule) end; 
23171  91 

92 

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

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

95 
variables *) 

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

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

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

100 
fun mk_renamings ctxt tgt rule_inst = 
52240  101 
let 
102 
val rule_conds = Thm.prems_of rule_inst; 

103 
val (_, cond_vs) = 

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

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

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

109 
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

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

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

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

23171  116 

117 

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

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

120 
fun mk_fixtvar_tyinsts ignore_insts ts = 
52240  121 
let 
122 
val ignore_ixs = map fst ignore_insts; 

123 
val (tvars, tfrees) = 

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

131 

132 
(* crossinstantiate the instantiations  ie for each instantiation 

58318  133 
replace all occurrences in other instantiations  no loops are possible 
23171  134 
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

135 
fun cross_inst insts = 
52240  136 
let 
137 
fun instL (ix, (ty,t)) = map (fn (ix2,(ty2,t2)) => 

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

23171  139 

52240  140 
fun cross_instL ([], l) = rev l 
141 
 cross_instL ((ix, t) :: insts, l) = 

23171  142 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
143 

52240  144 
in cross_instL (insts, []) end; 
23171  145 

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

147 
fun cross_inst_typs insts = 
52240  148 
let 
149 
fun instL (ix, (srt,ty)) = 

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

23171  151 

52240  152 
fun cross_instL ([], l) = rev l 
153 
 cross_instL ((ix, t) :: insts, l) = 

23171  154 
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l)); 
155 

52240  156 
in cross_instL (insts, []) end; 
23171  157 

158 

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

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

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

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

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

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

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

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

167 

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

168 
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
52240  169 
let 
170 
(* fix all noninstantiated tvars *) 

171 
val (fixtyinsts, othertfrees) = (* FIXME proper context!? *) 

172 
mk_fixtvar_tyinsts nonfixed_typinsts 

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

174 
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); 

23171  175 

52240  176 
(* certified instantiations for types *) 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset

177 
val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; 
52240  178 

179 
(* type instantiated versions *) 

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

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

23171  182 

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

185 
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; 

23171  186 

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

23171  189 

52240  190 
(* typeinstantiate the var instantiations *) 
191 
val insts_tyinst = 

52242  192 
fold_rev (fn (ix, (ty, t)) => fn insts_tyinst => 
52240  193 
(ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) 
52242  194 
:: insts_tyinst) unprepinsts []; 
23171  195 

52240  196 
(* crossinstantiate *) 
197 
val insts_tyinst_inst = cross_inst insts_tyinst; 

23171  198 

52240  199 
(* create certms of instantiations *) 
200 
val cinsts_tyinst = 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset

201 
map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; 
23171  202 

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

23171  205 

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

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

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

59641  210 
val cterm_renamings = map (fn (x, y) => apply2 (Thm.cterm_of ctxt) (Var x, y)) renamings; 
23171  211 

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

214 
outerterm_tyinst 

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

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

59641  217 
val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); 
52240  218 
val (cprems, abstract_rule_inst) = 
219 
rule_inst 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset

220 
> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) 
52240  221 
> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; 
222 
val specific_tgt_rule = 

223 
Conv.fconv_rule Drule.beta_eta_conversion 

224 
(Thm.combination couter_inst abstract_rule_inst); 

23171  225 

52240  226 
(* create an instantiated version of the target thm *) 
227 
val tgt_th_inst = 

228 
tgt_th_tyinst 

229 
> Thm.instantiate ([], cinsts_tyinst) 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60358
diff
changeset

230 
> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); 
23171  231 

52240  232 
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; 
233 
in 

234 
Conv.fconv_rule Drule.beta_eta_conversion tgt_th_inst 

235 
> Thm.equal_elim specific_tgt_rule 

236 
> Drule.implies_intr_list cprems 

237 
> Drule.forall_intr_list frees_of_fixed_vars 

238 
> Drule.forall_elim_list vars 

239 
> Thm.varifyT_global' othertfrees 

240 
> K Drule.zero_var_indexes 

241 
end; 

23171  242 

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

243 
end; 