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
112 val ith_syntax : int list parser
113 val options_syntax : bool parser
115 (* Isar level hooks *)
116 val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
117 val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
118 val setup : theory -> theory
122 structure EqSubst: EQSUBST =
125 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
126 fun prep_meta_eq ctxt =
127 Simplifier.mksimps (simpset_of ctxt) #> map Drule.zero_var_indexes;
130 (* a type abriviation for match information *)
132 ((indexname * (sort * typ)) list (* type instantiations *)
133 * (indexname * (typ * term)) list) (* term instantiations *)
134 * (string * typ) list (* fake named type abs env *)
135 * (string * typ) list (* type abs env *)
136 * term (* outer term *)
141 * Zipper.T (* focusterm to search under *)
144 (* skipping non-empty sub-sequences but when we reach the end
145 of the seq, remembering how much we have left to skip. *)
146 datatype 'a skipseq = SkipMore of int
147 | SkipSeq of 'a Seq.seq Seq.seq;
148 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
149 fun skipto_skipseq m s =
155 (case Seq.pull h of NONE => skip_occs n t
156 | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
157 else skip_occs (n - 1) t)
158 in (skip_occs m s) end;
160 (* note: outerterm is the taget with the match replaced by a bound
161 variable : ie: "P lhs" beocmes "%x. P x"
162 insts is the types of instantiations of vars in lhs
163 and typinsts is the type instantiations of types in the lhs
164 Note: Final rule is the rule lifted into the ontext of the
166 fun mk_foo_match mkuptermfunc Ts t =
168 val ty = Term.type_of t
169 val bigtype = (rev (map snd Ts)) ---> ty
171 | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
172 val num_of_bnds = (length Ts)
173 (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
174 val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
175 in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
177 (* T is outer bound vars, n is number of locally bound vars *)
178 (* THINK: is order of Ts correct...? or reversed? *)
179 fun fakefree_badbounds Ts t =
180 let val (FakeTs,Ts,newnames) =
181 List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
182 let val newname = Name.variant usednames n
183 in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
185 newname::usednames) end)
188 in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
190 (* before matching we need to fake the bound vars that are missing an
191 abstraction. In this function we additionally construct the
192 abstraction environment, and an outer context term (with the focus
193 abstracted out) for use in rewriting with RWInst.rw *)
194 fun prep_zipper_match z =
197 val c = Zipper.ctxt z
198 val Ts = Zipper.C.nty_ctxt c
199 val (FakeTs', Ts', t') = fakefree_badbounds Ts t
200 val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
202 (t', (FakeTs', Ts', absterm))
205 (* Matching and Unification with exception handled *)
206 fun clean_match thy (a as (pat, t)) =
207 let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
208 in SOME (Vartab.dest tyenv, Vartab.dest tenv)
209 end handle Pattern.MATCH => NONE;
211 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
212 fun clean_unify thry ix (a as (pat, tgt)) =
214 (* type info will be re-derived, maybe this can be cached
216 val pat_ty = Term.type_of pat;
217 val tgt_ty = Term.type_of tgt;
218 (* is it OK to ignore the type instantiation info?
219 or should I be using it? *)
221 SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
222 handle Type.TUNIFY => NONE;
225 SOME (typinsttab, ix2) =>
227 (* is it right to throw away the flexes?
228 or should I be using them somehow? *)
230 (Vartab.dest (Envir.type_env env),
231 Vartab.dest (Envir.term_env env));
233 Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
234 val useq = Unify.smash_unifiers thry [a] initenv
235 handle ListPair.UnequalLengths => Seq.empty
236 | Term.TERM _ => Seq.empty;
237 fun clean_unify' useq () =
238 (case (Seq.pull useq) of
240 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
241 handle ListPair.UnequalLengths => NONE
242 | Term.TERM _ => NONE
244 (Seq.make (clean_unify' useq))
249 (* Matching and Unification for zippers *)
250 (* Note: Ts is a modified version of the original names of the outer
251 bound variables. New names have been introduced to make sure they are
252 unique w.r.t all names in the term and each other. usednames' is
253 oldnames + new names. *)
254 fun clean_match_z thy pat z =
255 let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
256 case clean_match thy (pat, t) of
258 | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
259 (* ix = max var index *)
260 fun clean_unify_z sgn ix pat z =
261 let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
262 Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
263 (clean_unify sgn ix (t, pat)) end;
267 type trace_subst_errT = int (* subgoal *)
268 * thm (* thm with all goals *)
269 * (cterm list (* certified free var placeholders for vars *)
270 * thm) (* trivial thm of goal concl *)
271 (* possible matches/unifiers *)
273 * (((indexname * typ) list (* type instantiations *)
274 * (indexname * term) list ) (* term instantiations *)
275 * (string * typ) list (* Type abs env *)
276 * term) (* outer term *);
278 val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
279 val trace_subst_search = Unsynchronized.ref false;
280 exception trace_subst_exp of trace_subst_errT;
284 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
285 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
286 | bot_left_leaf_of x = x;
288 (* Avoid considering replacing terms which have a var at the head as
289 they always succeed trivially, and uninterestingly. *)
290 fun valid_match_start z =
291 (case bot_left_leaf_of (Zipper.trm z) of
295 (* search from top, left to right, then down *)
296 val search_lr_all = ZipperSearch.all_bl_ur;
298 (* search from top, left to right, then down *)
299 fun search_lr_valid validf =
301 fun sf_valid_td_lr z =
302 let val here = if validf z then [Zipper.Here z] else [] in
304 of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
306 @ [Zipper.LookIn (Zipper.move_down_right z)]
307 | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
310 in Zipper.lzy_search sf_valid_td_lr end;
312 (* search from bottom to top, left to right *)
314 fun search_bt_valid validf =
316 fun sf_valid_td_lr z =
317 let val here = if validf z then [Zipper.Here z] else [] in
319 of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
320 Zipper.LookIn (Zipper.move_down_right z)] @ here
321 | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
324 in Zipper.lzy_search sf_valid_td_lr end;
326 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
327 Seq.map (clean_unify_z sgn maxidx lhs)
328 (Zipper.limit_apply f z);
330 (* search all unifications *)
331 val searchf_lr_unify_all =
332 searchf_unify_gen search_lr_all;
334 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
335 val searchf_lr_unify_valid =
336 searchf_unify_gen (search_lr_valid valid_match_start);
338 val searchf_bt_unify_valid =
339 searchf_unify_gen (search_bt_valid valid_match_start);
341 (* apply a substitution in the conclusion of the theorem th *)
342 (* cfvs are certified free var placeholders for goal params *)
343 (* conclthm is a theorem of for just the conclusion *)
344 (* m is instantiation/match information *)
345 (* rule is the equation for substitution *)
346 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
347 (RWInst.rw m rule conclthm)
348 |> IsaND.unfix_frees cfvs
349 |> RWInst.beta_eta_contract
350 |> (fn r => Tactic.rtac r i th);
352 (* substitute within the conclusion of goal i of gth, using a meta
353 equation rule. Note that we assume rule has var indicies zero'd *)
354 fun prep_concl_subst i gth =
356 val th = Thm.incr_indexes 1 gth;
357 val tgt_term = Thm.prop_of th;
359 val sgn = Thm.theory_of_thm th;
360 val ctermify = Thm.cterm_of sgn;
361 val trivify = Thm.trivial o ctermify;
363 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
364 val cfvs = rev (map ctermify fvs);
366 val conclterm = Logic.strip_imp_concl fixedbody;
367 val conclthm = trivify conclterm;
368 val maxidx = Thm.maxidx_of th;
369 val ft = ((Zipper.move_down_right (* ==> *)
370 o Zipper.move_down_left (* Trueprop *)
372 o Thm.prop_of) conclthm)
374 ((cfvs, conclthm), (sgn, maxidx, ft))
377 (* substitute using an object or meta level equality *)
378 fun eqsubst_tac' ctxt searchf instepthm i th =
380 val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
381 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
382 fun rewrite_with_thm r =
383 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
384 in searchf searchinfo lhs
385 |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
386 in stepthms |> Seq.maps rewrite_with_thm end;
389 (* distinct subgoals *)
390 fun distinct_subgoals th =
391 the_default th (SINGLE distinct_subgoals_tac th);
393 (* General substitution of multiple occurances using one of
397 exception eqsubst_occL_exp of
398 string * (int list) * (thm list) * int * thm;
399 fun skip_first_occs_search occ srchf sinfo lhs =
400 case (skipto_skipseq occ (srchf sinfo lhs)) of
401 SkipMore _ => Seq.empty
402 | SkipSeq ss => Seq.flat ss;
404 (* The occL is a list of integers indicating which occurence
405 w.r.t. the search order, to rewrite. Backtracking will also find later
406 occurences, but all earlier ones are skipped. Thus you can use [0] to
407 just find all rewrites. *)
409 fun eqsubst_tac ctxt occL thms i th =
410 let val nprems = Thm.nprems_of th in
411 if nprems < i then Seq.empty else
412 let val thmseq = (Seq.of_list thms)
413 fun apply_occ occ th =
415 (fn r => eqsubst_tac'
417 (skip_first_occs_search
418 occ searchf_lr_unify_valid) r
419 (i + ((Thm.nprems_of th) - nprems))
422 Library.sort (Library.rev_order o Library.int_ord) occL;
424 Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
427 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
430 (* inthms are the given arguments in Isar, and treated as eqstep with
431 the first one, then the second etc *)
432 fun eqsubst_meth ctxt occL inthms =
433 SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
435 (* apply a substitution inside assumption j, keeps asm in the same place *)
436 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
438 val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
440 (RWInst.rw m rule pth)
441 |> (Seq.hd o prune_params_tac)
442 |> Thm.permute_prems 0 ~1 (* put old asm first *)
443 |> IsaND.unfix_frees cfvs (* unfix any global params *)
444 |> RWInst.beta_eta_contract; (* normal form *)
447 |> Tactic.make_elim (* make into elim rule *)
448 |> Thm.lift_rule (th2, i); (* lift into context *)
451 (* ~j because new asm starts at back, thus we subtract 1 *)
452 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
453 (Tactic.dtac preelimrule i th2)
456 false (* use unification *)
457 (true, (* elim resolution *)
458 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
463 (* prepare to substitute within the j'th premise of subgoal i of gth,
464 using a meta-level equation. Note that we assume rule has var indicies
465 zero'd. Note that we also assume that premt is the j'th premice of
466 subgoal i of gth. Note the repetition of work done for each
467 assumption, i.e. this can be made more efficient for search over
468 multiple assumptions. *)
469 fun prep_subst_in_asm i gth j =
471 val th = Thm.incr_indexes 1 gth;
472 val tgt_term = Thm.prop_of th;
474 val sgn = Thm.theory_of_thm th;
475 val ctermify = Thm.cterm_of sgn;
476 val trivify = Thm.trivial o ctermify;
478 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
479 val cfvs = rev (map ctermify fvs);
481 val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
482 val asm_nprems = length (Logic.strip_imp_prems asmt);
484 val pth = trivify asmt;
485 val maxidx = Thm.maxidx_of th;
487 val ft = ((Zipper.move_down_right (* trueprop *)
490 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
492 (* prepare subst in every possible assumption *)
493 fun prep_subst_in_asms i gth =
494 map (prep_subst_in_asm i gth)
495 ((fn l => Library.upto (1, length l))
496 (Logic.prems_of_goal (Thm.prop_of gth) i));
499 (* substitute in an assumption using an object or meta level equality *)
500 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
502 val asmpreps = prep_subst_in_asms i th;
503 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
504 fun rewrite_with_thm r =
505 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
506 fun occ_search occ [] = Seq.empty
507 | occ_search occ ((asminfo, searchinfo)::moreasms) =
508 (case searchf searchinfo occ lhs of
509 SkipMore i => occ_search i moreasms
511 Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
512 (occ_search 1 moreasms))
513 (* find later substs also *)
515 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
517 in stepthms |> Seq.maps rewrite_with_thm end;
520 fun skip_first_asm_occs_search searchf sinfo occ lhs =
521 skipto_skipseq occ (searchf sinfo lhs);
523 fun eqsubst_asm_tac ctxt occL thms i th =
524 let val nprems = Thm.nprems_of th
526 if nprems < i then Seq.empty else
527 let val thmseq = (Seq.of_list thms)
528 fun apply_occ occK th =
531 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
532 searchf_lr_unify_valid) occK r
533 (i + ((Thm.nprems_of th) - nprems))
536 Library.sort (Library.rev_order o Library.int_ord) occL
538 Seq.map distinct_subgoals
539 (Seq.EVERY (map apply_occ sortedoccs) th)
542 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
544 (* inthms are the given arguments in Isar, and treated as eqstep with
545 the first one, then the second etc *)
546 fun eqsubst_asm_meth ctxt occL inthms =
547 SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
549 (* syntax for options, given "(asm)" will give back true, without
552 (Args.parens (Args.$$$ "asm") >> (K true)) ||
553 (Scan.succeed false);
556 Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
558 (* combination method that takes a flag (true indicates that subst
559 should be done to an assumption, false = apply to the conclusion of
560 the goal) as well as the theorems to use *)
562 Method.setup @{binding subst}
563 (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
564 (fn ((asmflag, occL), inthms) => fn ctxt =>
565 (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
566 "single-step substitution";