author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 53168  d998de7f0efc 
child 54742  7a86358a3c0b 
permissions  rwrr 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
29269
diff
changeset

1 
(* Title: Tools/eqsubst.ML 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
27809
diff
changeset

2 
Author: Lucas Dixon, University of Edinburgh 
15481  3 

52235  4 
Perform a substitution using an equation. 
18598  5 
*) 
15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

6 

18591  7 
signature EQSUBST = 
15481  8 
sig 
19871  9 
type match = 
52234  10 
((indexname * (sort * typ)) list (* type instantiations *) 
11 
* (indexname * (typ * term)) list) (* term instantiations *) 

12 
* (string * typ) list (* fake named type abs env *) 

13 
* (string * typ) list (* type abs env *) 

14 
* term (* outer term *) 

19871  15 

16 
type searchinfo = 

52234  17 
theory 
18 
* int (* maxidx *) 

19 
* Zipper.T (* focusterm to search under *) 

19871  20 

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

21 
datatype 'a skipseq = SkipMore of int  SkipSeq of 'a Seq.seq Seq.seq 
19871  22 

52234  23 
val skip_first_asm_occs_search: ('a > 'b > 'c Seq.seq Seq.seq) > 'a > int > 'b > 'c skipseq 
24 
val skip_first_occs_search: int > ('a > 'b > 'c Seq.seq Seq.seq) > 'a > 'b > 'c Seq.seq 

25 
val skipto_skipseq: int > 'a Seq.seq Seq.seq > 'a skipseq 

19871  26 

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

27 
(* tactics *) 
52234  28 
val eqsubst_asm_tac: Proof.context > int list > thm list > int > tactic 
29 
val eqsubst_asm_tac': Proof.context > 

30 
(searchinfo > int > term > match skipseq) > int > thm > int > tactic 

31 
val eqsubst_tac: Proof.context > 

32 
int list > (* list of occurences to rewrite, use [0] for any *) 

33 
thm list > int > tactic 

34 
val eqsubst_tac': Proof.context > 

35 
(searchinfo > term > match Seq.seq) (* search function *) 

36 
> thm (* equation theorem to rewrite with *) 

37 
> int (* subgoal number in goal theorem *) 

38 
> thm (* goal theorem *) 

39 
> thm Seq.seq (* rewritten goal theorem *) 

19871  40 

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

41 
(* search for substitutions *) 
52234  42 
val valid_match_start: Zipper.T > bool 
43 
val search_lr_all: Zipper.T > Zipper.T Seq.seq 

44 
val search_lr_valid: (Zipper.T > bool) > Zipper.T > Zipper.T Seq.seq 

45 
val searchf_lr_unify_all: searchinfo > term > match Seq.seq Seq.seq 

46 
val searchf_lr_unify_valid: searchinfo > term > match Seq.seq Seq.seq 

47 
val searchf_bt_unify_valid: searchinfo > term > match Seq.seq Seq.seq 

19871  48 

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

49 
val setup : theory > theory 
15481  50 
end; 
51 

41164
6854e9a40edc
avoid ML structure aliases (especially singleletter abbreviations);
wenzelm
parents:
40722
diff
changeset

52 
structure EqSubst: EQSUBST = 
6854e9a40edc
avoid ML structure aliases (especially singleletter abbreviations);
wenzelm
parents:
40722
diff
changeset

53 
struct 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

54 

81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

55 
(* changes object "=" to meta "==" which prepares a given rewrite rule *) 
18598  56 
fun prep_meta_eq ctxt = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49340
diff
changeset

57 
Simplifier.mksimps ctxt #> map Drule.zero_var_indexes; 
18598  58 

52246  59 
(* make free vars into schematic vars with index zero *) 
60 
fun unfix_frees frees = 

61 
fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees; 

62 

15481  63 

52234  64 
type match = 
52235  65 
((indexname * (sort * typ)) list (* type instantiations *) 
66 
* (indexname * (typ * term)) list) (* term instantiations *) 

67 
* (string * typ) list (* fake named type abs env *) 

68 
* (string * typ) list (* type abs env *) 

69 
* term; (* outer term *) 

15550
806214035275
lucas  added more comments and an extra type to clarify the code.
dixon
parents:
15538
diff
changeset

70 

52234  71 
type searchinfo = 
52235  72 
theory 
73 
* int (* maxidx *) 

74 
* Zipper.T; (* focusterm to search under *) 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

75 

81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

76 

81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

77 
(* skipping nonempty subsequences but when we reach the end 
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

78 
of the seq, remembering how much we have left to skip. *) 
52234  79 
datatype 'a skipseq = 
80 
SkipMore of int  

81 
SkipSeq of 'a Seq.seq Seq.seq; 

82 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

83 
(* given a seqseq, skip the first m nonempty seq's, note deficit *) 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44095
diff
changeset

84 
fun skipto_skipseq m s = 
52234  85 
let 
86 
fun skip_occs n sq = 

87 
(case Seq.pull sq of 

88 
NONE => SkipMore n 

52237  89 
 SOME (h, t) => 
52234  90 
(case Seq.pull h of 
91 
NONE => skip_occs n t 

92 
 SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n  1) t)) 

93 
in skip_occs m s end; 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

94 

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

95 
(* note: outerterm is the taget with the match replaced by a bound 
52234  96 
variable : ie: "P lhs" beocmes "%x. P x" 
97 
insts is the types of instantiations of vars in lhs 

98 
and typinsts is the type instantiations of types in the lhs 

99 
Note: Final rule is the rule lifted into the ontext of the 

100 
taget thm. *) 

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

101 
fun mk_foo_match mkuptermfunc Ts t = 
52234  102 
let 
103 
val ty = Term.type_of t 

52235  104 
val bigtype = rev (map snd Ts) > ty 
52234  105 
fun mk_foo 0 t = t 
106 
 mk_foo i t = mk_foo (i  1) (t $ (Bound (i  1))) 

52235  107 
val num_of_bnds = length Ts 
52234  108 
(* foo_term = "fooabs y0 ... yn" where y's are local bounds *) 
109 
val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) 

110 
in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end; 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

111 

81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

112 
(* T is outer bound vars, n is number of locally bound vars *) 
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

113 
(* THINK: is order of Ts correct...? or reversed? *) 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44095
diff
changeset

114 
fun mk_fake_bound_name n = ":b_" ^ n; 
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44095
diff
changeset

115 
fun fakefree_badbounds Ts t = 
52234  116 
let val (FakeTs, Ts, newnames) = 
52242  117 
fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) => 
52234  118 
let 
119 
val newname = singleton (Name.variant_list usednames) n 

120 
in 

121 
((mk_fake_bound_name newname, ty) :: FakeTs, 

122 
(newname, ty) :: Ts, 

123 
newname :: usednames) 

52242  124 
end) Ts ([], [], []) 
52234  125 
in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

126 

81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

127 
(* before matching we need to fake the bound vars that are missing an 
52235  128 
abstraction. In this function we additionally construct the 
129 
abstraction environment, and an outer context term (with the focus 

52240  130 
abstracted out) for use in rewriting with RW_Inst.rw *) 
49339
d1fcb4de8349
eliminated some old material that is unused in the visible universe;
wenzelm
parents:
44095
diff
changeset

131 
fun prep_zipper_match z = 
52234  132 
let 
133 
val t = Zipper.trm z 

134 
val c = Zipper.ctxt z 

135 
val Ts = Zipper.C.nty_ctxt c 

136 
val (FakeTs', Ts', t') = fakefree_badbounds Ts t 

137 
val absterm = mk_foo_match (Zipper.C.apply c) Ts' t' 

138 
in 

139 
(t', (FakeTs', Ts', absterm)) 

140 
end; 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

141 

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

142 
(* Unification with exception handled *) 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

143 
(* given theory, max var index, pat, tgt; returns Seq of instantiations *) 
52235  144 
fun clean_unify thy ix (a as (pat, tgt)) = 
52234  145 
let 
146 
(* type info will be rederived, maybe this can be cached 

147 
for efficiency? *) 

148 
val pat_ty = Term.type_of pat; 

149 
val tgt_ty = Term.type_of tgt; 

52235  150 
(* FIXME is it OK to ignore the type instantiation info? 
52234  151 
or should I be using it? *) 
152 
val typs_unify = 

52235  153 
SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix)) 
52234  154 
handle Type.TUNIFY => NONE; 
155 
in 

156 
(case typs_unify of 

157 
SOME (typinsttab, ix2) => 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

158 
let 
52234  159 
(* FIXME is it right to throw away the flexes? 
160 
or should I be using them somehow? *) 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

161 
fun mk_insts env = 
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

162 
(Vartab.dest (Envir.type_env env), 
32032  163 
Vartab.dest (Envir.term_env env)); 
164 
val initenv = 

165 
Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab}; 

52235  166 
val useq = Unify.smash_unifiers thy [a] initenv 
52234  167 
handle ListPair.UnequalLengths => Seq.empty 
168 
 Term.TERM _ => Seq.empty; 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

169 
fun clean_unify' useq () = 
52234  170 
(case (Seq.pull useq) of 
171 
NONE => NONE 

172 
 SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t))) 

173 
handle ListPair.UnequalLengths => NONE 

174 
 Term.TERM _ => NONE; 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

175 
in 
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

176 
(Seq.make (clean_unify' useq)) 
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

177 
end 
52234  178 
 NONE => Seq.empty) 
179 
end; 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

180 

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

181 
(* Unification for zippers *) 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

182 
(* Note: Ts is a modified version of the original names of the outer 
52235  183 
bound variables. New names have been introduced to make sure they are 
184 
unique w.r.t all names in the term and each other. usednames' is 

185 
oldnames + new names. *) 

186 
fun clean_unify_z thy maxidx pat z = 

187 
let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in 

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

188 
Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
52235  189 
(clean_unify thy maxidx (t, pat)) 
52234  190 
end; 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

191 

15550
806214035275
lucas  added more comments and an extra type to clarify the code.
dixon
parents:
15538
diff
changeset

192 

52234  193 
fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l 
194 
 bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t 

19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

195 
 bot_left_leaf_of x = x; 
15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

196 

19975
ecd684d62808
fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents:
19871
diff
changeset

197 
(* Avoid considering replacing terms which have a var at the head as 
ecd684d62808
fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents:
19871
diff
changeset

198 
they always succeed trivially, and uninterestingly. *) 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

199 
fun valid_match_start z = 
52234  200 
(case bot_left_leaf_of (Zipper.trm z) of 
201 
Var _ => false 

202 
 _ => true); 

19975
ecd684d62808
fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents:
19871
diff
changeset

203 

15814
d65f461c8672
lucas  fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset

204 
(* search from top, left to right, then down *) 
19871  205 
val search_lr_all = ZipperSearch.all_bl_ur; 
15481  206 

15814
d65f461c8672
lucas  fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset

207 
(* search from top, left to right, then down *) 
19871  208 
fun search_lr_valid validf = 
52234  209 
let 
210 
fun sf_valid_td_lr z = 

211 
let val here = if validf z then [Zipper.Here z] else [] in 

212 
(case Zipper.trm z of 

213 
_ $ _ => 

214 
[Zipper.LookIn (Zipper.move_down_left z)] @ here @ 

215 
[Zipper.LookIn (Zipper.move_down_right z)] 

216 
 Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)] 

217 
 _ => here) 

218 
end; 

219 
in Zipper.lzy_search sf_valid_td_lr end; 

15814
d65f461c8672
lucas  fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset

220 

23064  221 
(* search from bottom to top, left to right *) 
222 
fun search_bt_valid validf = 

52234  223 
let 
224 
fun sf_valid_td_lr z = 

225 
let val here = if validf z then [Zipper.Here z] else [] in 

226 
(case Zipper.trm z of 

227 
_ $ _ => 

228 
[Zipper.LookIn (Zipper.move_down_left z), 

229 
Zipper.LookIn (Zipper.move_down_right z)] @ here 

230 
 Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here 

231 
 _ => here) 

232 
end; 

233 
in Zipper.lzy_search sf_valid_td_lr end; 

23064  234 

52235  235 
fun searchf_unify_gen f (thy, maxidx, z) lhs = 
236 
Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z); 

23064  237 

15814
d65f461c8672
lucas  fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset

238 
(* search all unifications *) 
52234  239 
val searchf_lr_unify_all = searchf_unify_gen search_lr_all; 
15481  240 

15814
d65f461c8672
lucas  fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset

241 
(* search only for 'valid' unifiers (non abs subterms and non vars) *) 
52234  242 
val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start); 
15929
68bd1e16552a
lucas  added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset

243 

52234  244 
val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start); 
15814
d65f461c8672
lucas  fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset

245 

52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

246 
(* apply a substitution in the conclusion of the theorem *) 
15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

247 
(* cfvs are certified free var placeholders for goal params *) 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

248 
(* conclthm is a theorem of for just the conclusion *) 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

249 
(* m is instantiation/match information *) 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

250 
(* rule is the equation for substitution *) 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

251 
fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m = 
52240  252 
RW_Inst.rw ctxt m rule conclthm 
52246  253 
> unfix_frees cfvs 
52239  254 
> Conv.fconv_rule Drule.beta_eta_conversion 
52732  255 
> (fn r => rtac r i st); 
15481  256 

257 
(* substitute within the conclusion of goal i of gth, using a meta 

15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

258 
equation rule. Note that we assume rule has var indicies zero'd *) 
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

259 
fun prep_concl_subst ctxt i gth = 
52234  260 
let 
261 
val th = Thm.incr_indexes 1 gth; 

262 
val tgt_term = Thm.prop_of th; 

15481  263 

52235  264 
val thy = Thm.theory_of_thm th; 
265 
val cert = Thm.cterm_of thy; 

15481  266 

52234  267 
val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; 
52235  268 
val cfvs = rev (map cert fvs); 
15481  269 

52234  270 
val conclterm = Logic.strip_imp_concl fixedbody; 
52235  271 
val conclthm = Thm.trivial (cert conclterm); 
52234  272 
val maxidx = Thm.maxidx_of th; 
273 
val ft = 

274 
(Zipper.move_down_right (* ==> *) 

275 
o Zipper.move_down_left (* Trueprop *) 

276 
o Zipper.mktop 

277 
o Thm.prop_of) conclthm 

278 
in 

52235  279 
((cfvs, conclthm), (thy, maxidx, ft)) 
52234  280 
end; 
15481  281 

282 
(* substitute using an object or meta level equality *) 

52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

283 
fun eqsubst_tac' ctxt searchf instepthm i st = 
52234  284 
let 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

285 
val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st; 
52234  286 
val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); 
287 
fun rewrite_with_thm r = 

288 
let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in 

289 
searchf searchinfo lhs 

52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

290 
> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r) 
52234  291 
end; 
292 
in stepthms > Seq.maps rewrite_with_thm end; 

15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

293 

d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

294 

19047  295 
(* General substitution of multiple occurances using one of 
52235  296 
the given theorems *) 
19835
81d6dc597559
added updated version of IsaPlanner and substitution.
dixon
parents:
19473
diff
changeset

297 

16978  298 
fun skip_first_occs_search occ srchf sinfo lhs = 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

299 
(case skipto_skipseq occ (srchf sinfo lhs) of 
52234  300 
SkipMore _ => Seq.empty 
301 
 SkipSeq ss => Seq.flat ss); 

16004
031f56012483
lucas  fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset

302 

52238  303 
(* The "occs" argument is a list of integers indicating which occurence 
22727  304 
w.r.t. the search order, to rewrite. Backtracking will also find later 
305 
occurences, but all earlier ones are skipped. Thus you can use [0] to 

306 
just find all rewrites. *) 

307 

52238  308 
fun eqsubst_tac ctxt occs thms i st = 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

309 
let val nprems = Thm.nprems_of st in 
52234  310 
if nprems < i then Seq.empty else 
311 
let 

52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

312 
val thmseq = Seq.of_list thms; 
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

313 
fun apply_occ occ st = 
52234  314 
thmseq > Seq.maps (fn r => 
315 
eqsubst_tac' ctxt 

316 
(skip_first_occs_search occ searchf_lr_unify_valid) r 

52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

317 
(i + (Thm.nprems_of st  nprems)) st); 
52238  318 
val sorted_occs = Library.sort (rev_order o int_ord) occs; 
52234  319 
in 
52238  320 
Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st) 
52234  321 
end 
322 
end; 

15959
366d39e95d3c
lucas  fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flexflex constraints)
dixon
parents:
15936
diff
changeset

323 

15481  324 

16004
031f56012483
lucas  fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset

325 
(* apply a substitution inside assumption j, keeps asm in the same place *) 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

326 
fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) = 
52234  327 
let 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

328 
val st2 = Thm.rotate_rule (j  1) i st; (* put premice first *) 
52234  329 
val preelimrule = 
52240  330 
RW_Inst.rw ctxt m rule pth 
52234  331 
> (Seq.hd o prune_params_tac) 
332 
> Thm.permute_prems 0 ~1 (* put old asm first *) 

52246  333 
> unfix_frees cfvs (* unfix any global params *) 
52239  334 
> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *) 
52234  335 
in 
336 
(* ~j because new asm starts at back, thus we subtract 1 *) 

52732  337 
Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2) 
52234  338 
end; 
15481  339 

340 

15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

341 
(* prepare to substitute within the j'th premise of subgoal i of gth, 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

342 
using a metalevel equation. Note that we assume rule has var indicies 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

343 
zero'd. Note that we also assume that premt is the j'th premice of 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

344 
subgoal i of gth. Note the repetition of work done for each 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

345 
assumption, i.e. this can be made more efficient for search over 
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

346 
multiple assumptions. *) 
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

347 
fun prep_subst_in_asm ctxt i gth j = 
52234  348 
let 
349 
val th = Thm.incr_indexes 1 gth; 

350 
val tgt_term = Thm.prop_of th; 

15481  351 

52235  352 
val thy = Thm.theory_of_thm th; 
353 
val cert = Thm.cterm_of thy; 

15481  354 

52234  355 
val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; 
52235  356 
val cfvs = rev (map cert fvs); 
15481  357 

52234  358 
val asmt = nth (Logic.strip_imp_prems fixedbody) (j  1); 
359 
val asm_nprems = length (Logic.strip_imp_prems asmt); 

360 

52235  361 
val pth = Thm.trivial (cert asmt); 
52234  362 
val maxidx = Thm.maxidx_of th; 
15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

363 

52234  364 
val ft = 
365 
(Zipper.move_down_right (* trueprop *) 

366 
o Zipper.mktop 

367 
o Thm.prop_of) pth 

52235  368 
in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end; 
15481  369 

15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

370 
(* prepare subst in every possible assumption *) 
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

371 
fun prep_subst_in_asms ctxt i gth = 
52234  372 
map (prep_subst_in_asm ctxt i gth) 
373 
((fn l => Library.upto (1, length l)) 

374 
(Logic.prems_of_goal (Thm.prop_of gth) i)); 

15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

375 

d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

376 

d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

377 
(* substitute in an assumption using an object or meta level equality *) 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

378 
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st = 
52234  379 
let 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

380 
val asmpreps = prep_subst_in_asms ctxt i st; 
52234  381 
val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); 
382 
fun rewrite_with_thm r = 

383 
let 

384 
val (lhs,_) = Logic.dest_equals (Thm.concl_of r); 

385 
fun occ_search occ [] = Seq.empty 

386 
 occ_search occ ((asminfo, searchinfo)::moreasms) = 

387 
(case searchf searchinfo occ lhs of 

388 
SkipMore i => occ_search i moreasms 

389 
 SkipSeq ss => 

390 
Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss)) 

391 
(occ_search 1 moreasms)) (* find later substs also *) 

392 
in 

52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

393 
occ_search skipocc asmpreps > Seq.maps (apply_subst_in_asm ctxt i st r) 
52234  394 
end; 
395 
in stepthms > Seq.maps rewrite_with_thm end; 

15538
d8edf54cc28c
lucas  rearranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset

396 

16004
031f56012483
lucas  fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset

397 

16978  398 
fun skip_first_asm_occs_search searchf sinfo occ lhs = 
52234  399 
skipto_skipseq occ (searchf sinfo lhs); 
16004
031f56012483
lucas  fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset

400 

52238  401 
fun eqsubst_asm_tac ctxt occs thms i st = 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

402 
let val nprems = Thm.nprems_of st in 
52234  403 
if nprems < i then Seq.empty 
404 
else 

405 
let 

406 
val thmseq = Seq.of_list thms; 

52238  407 
fun apply_occ occ st = 
52234  408 
thmseq > Seq.maps (fn r => 
409 
eqsubst_asm_tac' ctxt 

52238  410 
(skip_first_asm_occs_search searchf_lr_unify_valid) occ r 
52236
fb82b42eb498
tuned  prefer terminology of tactic / goal state;
wenzelm
parents:
52235
diff
changeset

411 
(i + (Thm.nprems_of st  nprems)) st); 
52238  412 
val sorted_occs = Library.sort (rev_order o int_ord) occs; 
16004
031f56012483
lucas  fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset

413 
in 
52238  414 
Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st) 
16004
031f56012483
lucas  fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset

415 
end 
52234  416 
end; 
15481  417 

18598  418 
(* combination method that takes a flag (true indicates that subst 
31301  419 
should be done to an assumption, false = apply to the conclusion of 
420 
the goal) as well as the theorems to use *) 

16978  421 
val setup = 
31301  422 
Method.setup @{binding subst} 
53168  423 
(Scan.lift (Args.mode "asm"  Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])  
44095  424 
Attrib.thms >> 
52238  425 
(fn ((asm, occs), inthms) => fn ctxt => 
426 
SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms))) 

31301  427 
"singlestep substitution"; 
15481  428 

16978  429 
end; 