1 (* Title: Tools/eqsubst.ML
2 Author: Lucas Dixon, University of Edinburgh
4 A proof method to perform a substiution using an equation.
9 (* a type abbreviation for match information *)
11 ((indexname * (sort * typ)) list (* type instantiations *)
12 * (indexname * (typ * term)) list) (* term instantiations *)
13 * (string * typ) list (* fake named type abs env *)
14 * (string * typ) list (* type abs env *)
15 * term (* outer term *)
20 * Zipper.T (* focusterm to search under *)
22 exception eqsubst_occL_exp of
23 string * int list * thm list * int * thm
25 (* low level substitution functions *)
26 val apply_subst_in_asm :
30 (cterm list * int * 'a * thm) * match -> thm Seq.seq
31 val apply_subst_in_concl :
35 thm -> match -> thm Seq.seq
37 (* matching/unification within zippers *)
39 theory -> term -> Zipper.T -> match option
41 theory -> int -> term -> Zipper.T -> match Seq.seq
43 (* skipping things in seq seq's *)
45 (* skipping non-empty sub-sequences but when we reach the end
46 of the seq, remembering how much we have left to skip. *)
47 datatype 'a skipseq = SkipMore of int
48 | SkipSeq of 'a Seq.seq Seq.seq;
50 val skip_first_asm_occs_search :
51 ('a -> 'b -> 'c Seq.seq Seq.seq) ->
52 'a -> int -> 'b -> 'c skipseq
53 val skip_first_occs_search :
54 int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
55 val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
60 int list -> thm list -> int -> tactic
61 val eqsubst_asm_tac' :
63 (searchinfo -> int -> term -> match skipseq) ->
64 int -> thm -> int -> tactic
67 int list -> (* list of occurences to rewrite, use [0] for any *)
68 thm list -> int -> tactic
70 Proof.context -> (* proof context *)
71 (searchinfo -> term -> match Seq.seq) (* search function *)
72 -> thm (* equation theorem to rewrite with *)
73 -> int (* subgoal number in goal theorem *)
74 -> thm (* goal theorem *)
75 -> thm Seq.seq (* rewritten goal theorem *)
78 val fakefree_badbounds :
79 (string * typ) list ->
81 (string * typ) list * (string * typ) list * term
85 ('a * typ) list -> term -> term
87 (* preparing substitution *)
88 val prep_meta_eq : Proof.context -> thm -> thm list
89 val prep_concl_subst :
90 int -> thm -> (cterm list * thm) * searchinfo
91 val prep_subst_in_asm :
93 (cterm list * int * int * thm) * searchinfo
94 val prep_subst_in_asms :
96 ((cterm list * int * int * thm) * searchinfo) list
97 val prep_zipper_match :
98 Zipper.T -> term * ((string * typ) list * (string * typ) list * term)
100 (* search for substitutions *)
101 val valid_match_start : Zipper.T -> bool
102 val search_lr_all : Zipper.T -> Zipper.T Seq.seq
103 val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
104 val searchf_lr_unify_all :
105 searchinfo -> term -> match Seq.seq Seq.seq
106 val searchf_lr_unify_valid :
107 searchinfo -> term -> match Seq.seq Seq.seq
108 val searchf_bt_unify_valid :
109 searchinfo -> term -> match Seq.seq Seq.seq
111 (* Isar level hooks *)
112 val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
113 val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
114 val setup : theory -> theory
118 structure EqSubst: EQSUBST =
121 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
122 fun prep_meta_eq ctxt =
123 Simplifier.mksimps (simpset_of ctxt) #> map Drule.zero_var_indexes;
126 (* a type abriviation for match information *)
128 ((indexname * (sort * typ)) list (* type instantiations *)
129 * (indexname * (typ * term)) list) (* term instantiations *)
130 * (string * typ) list (* fake named type abs env *)
131 * (string * typ) list (* type abs env *)
132 * term (* outer term *)
137 * Zipper.T (* focusterm to search under *)
140 (* skipping non-empty sub-sequences but when we reach the end
141 of the seq, remembering how much we have left to skip. *)
142 datatype 'a skipseq = SkipMore of int
143 | SkipSeq of 'a Seq.seq Seq.seq;
144 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
145 fun skipto_skipseq m s =
151 (case Seq.pull h of NONE => skip_occs n t
152 | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
153 else skip_occs (n - 1) t)
154 in (skip_occs m s) end;
156 (* note: outerterm is the taget with the match replaced by a bound
157 variable : ie: "P lhs" beocmes "%x. P x"
158 insts is the types of instantiations of vars in lhs
159 and typinsts is the type instantiations of types in the lhs
160 Note: Final rule is the rule lifted into the ontext of the
162 fun mk_foo_match mkuptermfunc Ts t =
164 val ty = Term.type_of t
165 val bigtype = (rev (map snd Ts)) ---> ty
167 | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
168 val num_of_bnds = (length Ts)
169 (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
170 val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
171 in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
173 (* T is outer bound vars, n is number of locally bound vars *)
174 (* THINK: is order of Ts correct...? or reversed? *)
175 fun fakefree_badbounds Ts t =
176 let val (FakeTs,Ts,newnames) =
177 List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
178 let val newname = singleton (Name.variant_list usednames) n
179 in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
181 newname::usednames) end)
184 in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
186 (* before matching we need to fake the bound vars that are missing an
187 abstraction. In this function we additionally construct the
188 abstraction environment, and an outer context term (with the focus
189 abstracted out) for use in rewriting with RWInst.rw *)
190 fun prep_zipper_match z =
193 val c = Zipper.ctxt z
194 val Ts = Zipper.C.nty_ctxt c
195 val (FakeTs', Ts', t') = fakefree_badbounds Ts t
196 val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
198 (t', (FakeTs', Ts', absterm))
201 (* Matching and Unification with exception handled *)
202 fun clean_match thy (a as (pat, t)) =
203 let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
204 in SOME (Vartab.dest tyenv, Vartab.dest tenv)
205 end handle Pattern.MATCH => NONE;
207 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
208 fun clean_unify thry ix (a as (pat, tgt)) =
210 (* type info will be re-derived, maybe this can be cached
212 val pat_ty = Term.type_of pat;
213 val tgt_ty = Term.type_of tgt;
214 (* is it OK to ignore the type instantiation info?
215 or should I be using it? *)
217 SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
218 handle Type.TUNIFY => NONE;
221 SOME (typinsttab, ix2) =>
223 (* is it right to throw away the flexes?
224 or should I be using them somehow? *)
226 (Vartab.dest (Envir.type_env env),
227 Vartab.dest (Envir.term_env env));
229 Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
230 val useq = Unify.smash_unifiers thry [a] initenv
231 handle ListPair.UnequalLengths => Seq.empty
232 | Term.TERM _ => Seq.empty;
233 fun clean_unify' useq () =
234 (case (Seq.pull useq) of
236 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
237 handle ListPair.UnequalLengths => NONE
238 | Term.TERM _ => NONE
240 (Seq.make (clean_unify' useq))
245 (* Matching and Unification for zippers *)
246 (* Note: Ts is a modified version of the original names of the outer
247 bound variables. New names have been introduced to make sure they are
248 unique w.r.t all names in the term and each other. usednames' is
249 oldnames + new names. *)
250 fun clean_match_z thy pat z =
251 let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
252 case clean_match thy (pat, t) of
254 | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
255 (* ix = max var index *)
256 fun clean_unify_z sgn ix pat z =
257 let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
258 Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
259 (clean_unify sgn ix (t, pat)) end;
263 type trace_subst_errT = int (* subgoal *)
264 * thm (* thm with all goals *)
265 * (cterm list (* certified free var placeholders for vars *)
266 * thm) (* trivial thm of goal concl *)
267 (* possible matches/unifiers *)
269 * (((indexname * typ) list (* type instantiations *)
270 * (indexname * term) list ) (* term instantiations *)
271 * (string * typ) list (* Type abs env *)
272 * term) (* outer term *);
274 val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
275 val trace_subst_search = Unsynchronized.ref false;
276 exception trace_subst_exp of trace_subst_errT;
280 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
281 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
282 | bot_left_leaf_of x = x;
284 (* Avoid considering replacing terms which have a var at the head as
285 they always succeed trivially, and uninterestingly. *)
286 fun valid_match_start z =
287 (case bot_left_leaf_of (Zipper.trm z) of
291 (* search from top, left to right, then down *)
292 val search_lr_all = ZipperSearch.all_bl_ur;
294 (* search from top, left to right, then down *)
295 fun search_lr_valid validf =
297 fun sf_valid_td_lr z =
298 let val here = if validf z then [Zipper.Here z] else [] in
300 of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
302 @ [Zipper.LookIn (Zipper.move_down_right z)]
303 | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
306 in Zipper.lzy_search sf_valid_td_lr end;
308 (* search from bottom to top, left to right *)
310 fun search_bt_valid validf =
312 fun sf_valid_td_lr z =
313 let val here = if validf z then [Zipper.Here z] else [] in
315 of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
316 Zipper.LookIn (Zipper.move_down_right z)] @ here
317 | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
320 in Zipper.lzy_search sf_valid_td_lr end;
322 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
323 Seq.map (clean_unify_z sgn maxidx lhs)
324 (Zipper.limit_apply f z);
326 (* search all unifications *)
327 val searchf_lr_unify_all =
328 searchf_unify_gen search_lr_all;
330 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
331 val searchf_lr_unify_valid =
332 searchf_unify_gen (search_lr_valid valid_match_start);
334 val searchf_bt_unify_valid =
335 searchf_unify_gen (search_bt_valid valid_match_start);
337 (* apply a substitution in the conclusion of the theorem th *)
338 (* cfvs are certified free var placeholders for goal params *)
339 (* conclthm is a theorem of for just the conclusion *)
340 (* m is instantiation/match information *)
341 (* rule is the equation for substitution *)
342 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
343 (RWInst.rw m rule conclthm)
344 |> IsaND.unfix_frees cfvs
345 |> RWInst.beta_eta_contract
346 |> (fn r => Tactic.rtac r i th);
348 (* substitute within the conclusion of goal i of gth, using a meta
349 equation rule. Note that we assume rule has var indicies zero'd *)
350 fun prep_concl_subst i gth =
352 val th = Thm.incr_indexes 1 gth;
353 val tgt_term = Thm.prop_of th;
355 val sgn = Thm.theory_of_thm th;
356 val ctermify = Thm.cterm_of sgn;
357 val trivify = Thm.trivial o ctermify;
359 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
360 val cfvs = rev (map ctermify fvs);
362 val conclterm = Logic.strip_imp_concl fixedbody;
363 val conclthm = trivify conclterm;
364 val maxidx = Thm.maxidx_of th;
365 val ft = ((Zipper.move_down_right (* ==> *)
366 o Zipper.move_down_left (* Trueprop *)
368 o Thm.prop_of) conclthm)
370 ((cfvs, conclthm), (sgn, maxidx, ft))
373 (* substitute using an object or meta level equality *)
374 fun eqsubst_tac' ctxt searchf instepthm i th =
376 val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
377 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
378 fun rewrite_with_thm r =
379 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
380 in searchf searchinfo lhs
381 |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
382 in stepthms |> Seq.maps rewrite_with_thm end;
385 (* distinct subgoals *)
386 fun distinct_subgoals th =
387 the_default th (SINGLE distinct_subgoals_tac th);
389 (* General substitution of multiple occurances using one of
393 exception eqsubst_occL_exp of
394 string * (int list) * (thm list) * int * thm;
395 fun skip_first_occs_search occ srchf sinfo lhs =
396 case (skipto_skipseq occ (srchf sinfo lhs)) of
397 SkipMore _ => Seq.empty
398 | SkipSeq ss => Seq.flat ss;
400 (* The occL is a list of integers indicating which occurence
401 w.r.t. the search order, to rewrite. Backtracking will also find later
402 occurences, but all earlier ones are skipped. Thus you can use [0] to
403 just find all rewrites. *)
405 fun eqsubst_tac ctxt occL thms i th =
406 let val nprems = Thm.nprems_of th in
407 if nprems < i then Seq.empty else
408 let val thmseq = (Seq.of_list thms)
409 fun apply_occ occ th =
411 (fn r => eqsubst_tac'
413 (skip_first_occs_search
414 occ searchf_lr_unify_valid) r
415 (i + ((Thm.nprems_of th) - nprems))
418 Library.sort (Library.rev_order o Library.int_ord) occL;
420 Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
423 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
426 (* inthms are the given arguments in Isar, and treated as eqstep with
427 the first one, then the second etc *)
428 fun eqsubst_meth ctxt occL inthms =
429 SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
431 (* apply a substitution inside assumption j, keeps asm in the same place *)
432 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
434 val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
436 (RWInst.rw m rule pth)
437 |> (Seq.hd o prune_params_tac)
438 |> Thm.permute_prems 0 ~1 (* put old asm first *)
439 |> IsaND.unfix_frees cfvs (* unfix any global params *)
440 |> RWInst.beta_eta_contract; (* normal form *)
443 |> Tactic.make_elim (* make into elim rule *)
444 |> Thm.lift_rule (th2, i); (* lift into context *)
447 (* ~j because new asm starts at back, thus we subtract 1 *)
448 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
449 (Tactic.dtac preelimrule i th2)
452 false (* use unification *)
453 (true, (* elim resolution *)
454 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
459 (* prepare to substitute within the j'th premise of subgoal i of gth,
460 using a meta-level equation. Note that we assume rule has var indicies
461 zero'd. Note that we also assume that premt is the j'th premice of
462 subgoal i of gth. Note the repetition of work done for each
463 assumption, i.e. this can be made more efficient for search over
464 multiple assumptions. *)
465 fun prep_subst_in_asm i gth j =
467 val th = Thm.incr_indexes 1 gth;
468 val tgt_term = Thm.prop_of th;
470 val sgn = Thm.theory_of_thm th;
471 val ctermify = Thm.cterm_of sgn;
472 val trivify = Thm.trivial o ctermify;
474 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
475 val cfvs = rev (map ctermify fvs);
477 val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
478 val asm_nprems = length (Logic.strip_imp_prems asmt);
480 val pth = trivify asmt;
481 val maxidx = Thm.maxidx_of th;
483 val ft = ((Zipper.move_down_right (* trueprop *)
486 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
488 (* prepare subst in every possible assumption *)
489 fun prep_subst_in_asms i gth =
490 map (prep_subst_in_asm i gth)
491 ((fn l => Library.upto (1, length l))
492 (Logic.prems_of_goal (Thm.prop_of gth) i));
495 (* substitute in an assumption using an object or meta level equality *)
496 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
498 val asmpreps = prep_subst_in_asms i th;
499 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
500 fun rewrite_with_thm r =
501 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
502 fun occ_search occ [] = Seq.empty
503 | occ_search occ ((asminfo, searchinfo)::moreasms) =
504 (case searchf searchinfo occ lhs of
505 SkipMore i => occ_search i moreasms
507 Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
508 (occ_search 1 moreasms))
509 (* find later substs also *)
511 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
513 in stepthms |> Seq.maps rewrite_with_thm end;
516 fun skip_first_asm_occs_search searchf sinfo occ lhs =
517 skipto_skipseq occ (searchf sinfo lhs);
519 fun eqsubst_asm_tac ctxt occL thms i th =
520 let val nprems = Thm.nprems_of th
522 if nprems < i then Seq.empty else
523 let val thmseq = (Seq.of_list thms)
524 fun apply_occ occK th =
527 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
528 searchf_lr_unify_valid) occK r
529 (i + ((Thm.nprems_of th) - nprems))
532 Library.sort (Library.rev_order o Library.int_ord) occL
534 Seq.map distinct_subgoals
535 (Seq.EVERY (map apply_occ sortedoccs) th)
538 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
540 (* inthms are the given arguments in Isar, and treated as eqstep with
541 the first one, then the second etc *)
542 fun eqsubst_asm_meth ctxt occL inthms =
543 SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
545 (* combination method that takes a flag (true indicates that subst
546 should be done to an assumption, false = apply to the conclusion of
547 the goal) as well as the theorems to use *)
549 Method.setup @{binding subst}
550 (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
552 (fn ((asm, occL), inthms) => fn ctxt =>
553 (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
554 "single-step substitution";