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.thm list * int * Thm.thm
25 (* low level substitution functions *)
26 val apply_subst_in_asm :
30 (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
31 val apply_subst_in_concl :
34 Thm.cterm list * Thm.thm ->
35 Thm.thm -> match -> Thm.thm Seq.seq
37 (* matching/unification within zippers *)
39 Context.theory -> Term.term -> Zipper.T -> match option
41 Context.theory -> int -> Term.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.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
61 val eqsubst_asm_tac' :
63 (searchinfo -> int -> Term.term -> match skipseq) ->
64 int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
67 int list -> (* list of occurences to rewrite, use [0] for any *)
68 Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
70 Proof.context -> (* proof context *)
71 (searchinfo -> Term.term -> match Seq.seq) (* search function *)
72 -> Thm.thm (* equation theorem to rewrite with *)
73 -> int (* subgoal number in goal theorem *)
74 -> Thm.thm (* goal theorem *)
75 -> Thm.thm Seq.seq (* rewritten goal theorem *)
78 val fakefree_badbounds :
79 (string * Term.typ) list ->
81 (string * Term.typ) list * (string * Term.typ) list * Term.term
84 (Term.term -> Term.term) ->
85 ('a * Term.typ) list -> Term.term -> Term.term
87 (* preparing substitution *)
88 val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
89 val prep_concl_subst :
90 int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
91 val prep_subst_in_asm :
92 int -> Thm.thm -> int ->
93 (Thm.cterm list * int * int * Thm.thm) * searchinfo
94 val prep_subst_in_asms :
96 ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
97 val prep_zipper_match :
98 Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.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.term -> match Seq.seq Seq.seq
106 val searchf_lr_unify_valid :
107 searchinfo -> Term.term -> match Seq.seq Seq.seq
108 val searchf_bt_unify_valid :
109 searchinfo -> Term.term -> match Seq.seq Seq.seq
112 val ith_syntax : Args.T list -> int list * Args.T list
113 val options_syntax : Args.T list -> bool * Args.T list
115 (* Isar level hooks *)
116 val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
117 val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
118 val subst_meth : Method.src -> Proof.context -> Proof.method
119 val setup : theory -> theory
127 structure Z = Zipper;
129 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
130 fun prep_meta_eq ctxt =
131 let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
132 in mk #> map Drule.zero_var_indexes end;
135 (* a type abriviation for match information *)
137 ((indexname * (sort * typ)) list (* type instantiations *)
138 * (indexname * (typ * term)) list) (* term instantiations *)
139 * (string * typ) list (* fake named type abs env *)
140 * (string * typ) list (* type abs env *)
141 * term (* outer term *)
146 * Zipper.T (* focusterm to search under *)
149 (* skipping non-empty sub-sequences but when we reach the end
150 of the seq, remembering how much we have left to skip. *)
151 datatype 'a skipseq = SkipMore of int
152 | SkipSeq of 'a Seq.seq Seq.seq;
153 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
154 fun skipto_skipseq m s =
160 (case Seq.pull h of NONE => skip_occs n t
161 | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
162 else skip_occs (n - 1) t)
163 in (skip_occs m s) end;
165 (* note: outerterm is the taget with the match replaced by a bound
166 variable : ie: "P lhs" beocmes "%x. P x"
167 insts is the types of instantiations of vars in lhs
168 and typinsts is the type instantiations of types in the lhs
169 Note: Final rule is the rule lifted into the ontext of the
171 fun mk_foo_match mkuptermfunc Ts t =
173 val ty = Term.type_of t
174 val bigtype = (rev (map snd Ts)) ---> ty
176 | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
177 val num_of_bnds = (length Ts)
178 (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
179 val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
180 in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
182 (* T is outer bound vars, n is number of locally bound vars *)
183 (* THINK: is order of Ts correct...? or reversed? *)
184 fun fakefree_badbounds Ts t =
185 let val (FakeTs,Ts,newnames) =
186 List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
187 let val newname = Name.variant usednames n
188 in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
190 newname::usednames) end)
193 in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
195 (* before matching we need to fake the bound vars that are missing an
196 abstraction. In this function we additionally construct the
197 abstraction environment, and an outer context term (with the focus
198 abstracted out) for use in rewriting with RWInst.rw *)
199 fun prep_zipper_match z =
203 val Ts = Z.C.nty_ctxt c
204 val (FakeTs', Ts', t') = fakefree_badbounds Ts t
205 val absterm = mk_foo_match (Z.C.apply c) Ts' t'
207 (t', (FakeTs', Ts', absterm))
210 (* Matching and Unification with exception handled *)
211 fun clean_match thy (a as (pat, t)) =
212 let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
213 in SOME (Vartab.dest tyenv, Vartab.dest tenv)
214 end handle Pattern.MATCH => NONE;
216 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
217 fun clean_unify thry ix (a as (pat, tgt)) =
219 (* type info will be re-derived, maybe this can be cached
221 val pat_ty = Term.type_of pat;
222 val tgt_ty = Term.type_of tgt;
223 (* is it OK to ignore the type instantiation info?
224 or should I be using it? *)
226 SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
227 handle Type.TUNIFY => NONE;
230 SOME (typinsttab, ix2) =>
232 (* is it right to throw away the flexes?
233 or should I be using them somehow? *)
235 (Vartab.dest (Envir.type_env env),
237 val initenv = Envir.Envir {asol = Vartab.empty,
238 iTs = typinsttab, maxidx = ix2};
239 val useq = Unify.smash_unifiers thry [a] initenv
240 handle UnequalLengths => Seq.empty
241 | Term.TERM _ => Seq.empty;
242 fun clean_unify' useq () =
243 (case (Seq.pull useq) of
245 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
246 handle UnequalLengths => NONE
247 | Term.TERM _ => NONE
249 (Seq.make (clean_unify' useq))
254 (* Matching and Unification for zippers *)
255 (* Note: Ts is a modified version of the original names of the outer
256 bound variables. New names have been introduced to make sure they are
257 unique w.r.t all names in the term and each other. usednames' is
258 oldnames + new names. *)
259 fun clean_match_z thy pat z =
260 let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
261 case clean_match thy (pat, t) of
263 | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
264 (* ix = max var index *)
265 fun clean_unify_z sgn ix pat z =
266 let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
267 Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
268 (clean_unify sgn ix (t, pat)) end;
272 type trace_subst_errT = int (* subgoal *)
273 * thm (* thm with all goals *)
274 * (Thm.cterm list (* certified free var placeholders for vars *)
275 * thm) (* trivial thm of goal concl *)
276 (* possible matches/unifiers *)
278 * (((indexname * typ) list (* type instantiations *)
279 * (indexname * term) list ) (* term instantiations *)
280 * (string * typ) list (* Type abs env *)
281 * term) (* outer term *);
283 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
284 val trace_subst_search = ref false;
285 exception trace_subst_exp of trace_subst_errT;
289 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
290 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
291 | bot_left_leaf_of x = x;
293 (* Avoid considering replacing terms which have a var at the head as
294 they always succeed trivially, and uninterestingly. *)
295 fun valid_match_start z =
296 (case bot_left_leaf_of (Z.trm z) of
300 (* search from top, left to right, then down *)
301 val search_lr_all = ZipperSearch.all_bl_ur;
303 (* search from top, left to right, then down *)
304 fun search_lr_valid validf =
306 fun sf_valid_td_lr z =
307 let val here = if validf z then [Z.Here z] else [] in
309 of _ $ _ => [Z.LookIn (Z.move_down_left z)]
311 @ [Z.LookIn (Z.move_down_right z)]
312 | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
315 in Z.lzy_search sf_valid_td_lr end;
317 (* search from bottom to top, left to right *)
319 fun search_bt_valid validf =
321 fun sf_valid_td_lr z =
322 let val here = if validf z then [Z.Here z] else [] in
324 of _ $ _ => [Z.LookIn (Z.move_down_left z),
325 Z.LookIn (Z.move_down_right z)] @ here
326 | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
329 in Z.lzy_search sf_valid_td_lr end;
331 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
332 Seq.map (clean_unify_z sgn maxidx lhs)
335 (* search all unifications *)
336 val searchf_lr_unify_all =
337 searchf_unify_gen search_lr_all;
339 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
340 val searchf_lr_unify_valid =
341 searchf_unify_gen (search_lr_valid valid_match_start);
343 val searchf_bt_unify_valid =
344 searchf_unify_gen (search_bt_valid valid_match_start);
346 (* apply a substitution in the conclusion of the theorem th *)
347 (* cfvs are certified free var placeholders for goal params *)
348 (* conclthm is a theorem of for just the conclusion *)
349 (* m is instantiation/match information *)
350 (* rule is the equation for substitution *)
351 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
352 (RWInst.rw m rule conclthm)
353 |> IsaND.unfix_frees cfvs
354 |> RWInst.beta_eta_contract
355 |> (fn r => Tactic.rtac r i th);
357 (* substitute within the conclusion of goal i of gth, using a meta
358 equation rule. Note that we assume rule has var indicies zero'd *)
359 fun prep_concl_subst i gth =
361 val th = Thm.incr_indexes 1 gth;
362 val tgt_term = Thm.prop_of th;
364 val sgn = Thm.theory_of_thm th;
365 val ctermify = Thm.cterm_of sgn;
366 val trivify = Thm.trivial o ctermify;
368 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
369 val cfvs = rev (map ctermify fvs);
371 val conclterm = Logic.strip_imp_concl fixedbody;
372 val conclthm = trivify conclterm;
373 val maxidx = Thm.maxidx_of th;
374 val ft = ((Z.move_down_right (* ==> *)
375 o Z.move_down_left (* Trueprop *)
377 o Thm.prop_of) conclthm)
379 ((cfvs, conclthm), (sgn, maxidx, ft))
382 (* substitute using an object or meta level equality *)
383 fun eqsubst_tac' ctxt searchf instepthm i th =
385 val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
386 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
387 fun rewrite_with_thm r =
388 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
389 in searchf searchinfo lhs
390 |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
391 in stepthms |> Seq.maps rewrite_with_thm end;
394 (* distinct subgoals *)
395 fun distinct_subgoals th =
396 the_default th (SINGLE distinct_subgoals_tac th);
398 (* General substitution of multiple occurances using one of
402 exception eqsubst_occL_exp of
403 string * (int list) * (thm list) * int * thm;
404 fun skip_first_occs_search occ srchf sinfo lhs =
405 case (skipto_skipseq occ (srchf sinfo lhs)) of
406 SkipMore _ => Seq.empty
407 | SkipSeq ss => Seq.flat ss;
409 (* The occL is a list of integers indicating which occurence
410 w.r.t. the search order, to rewrite. Backtracking will also find later
411 occurences, but all earlier ones are skipped. Thus you can use [0] to
412 just find all rewrites. *)
414 fun eqsubst_tac ctxt occL thms i th =
415 let val nprems = Thm.nprems_of th in
416 if nprems < i then Seq.empty else
417 let val thmseq = (Seq.of_list thms)
418 fun apply_occ occ th =
420 (fn r => eqsubst_tac'
422 (skip_first_occs_search
423 occ searchf_lr_unify_valid) r
424 (i + ((Thm.nprems_of th) - nprems))
427 Library.sort (Library.rev_order o Library.int_ord) occL;
429 Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
432 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
435 (* inthms are the given arguments in Isar, and treated as eqstep with
436 the first one, then the second etc *)
437 fun eqsubst_meth ctxt occL inthms =
438 Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
440 (* apply a substitution inside assumption j, keeps asm in the same place *)
441 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
443 val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
445 (RWInst.rw m rule pth)
446 |> (Seq.hd o prune_params_tac)
447 |> Thm.permute_prems 0 ~1 (* put old asm first *)
448 |> IsaND.unfix_frees cfvs (* unfix any global params *)
449 |> RWInst.beta_eta_contract; (* normal form *)
452 |> Tactic.make_elim (* make into elim rule *)
453 |> Thm.lift_rule (th2, i); (* lift into context *)
456 (* ~j because new asm starts at back, thus we subtract 1 *)
457 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
458 (Tactic.dtac preelimrule i th2)
461 false (* use unification *)
462 (true, (* elim resolution *)
463 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
468 (* prepare to substitute within the j'th premise of subgoal i of gth,
469 using a meta-level equation. Note that we assume rule has var indicies
470 zero'd. Note that we also assume that premt is the j'th premice of
471 subgoal i of gth. Note the repetition of work done for each
472 assumption, i.e. this can be made more efficient for search over
473 multiple assumptions. *)
474 fun prep_subst_in_asm i gth j =
476 val th = Thm.incr_indexes 1 gth;
477 val tgt_term = Thm.prop_of th;
479 val sgn = Thm.theory_of_thm th;
480 val ctermify = Thm.cterm_of sgn;
481 val trivify = Thm.trivial o ctermify;
483 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
484 val cfvs = rev (map ctermify fvs);
486 val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
487 val asm_nprems = length (Logic.strip_imp_prems asmt);
489 val pth = trivify asmt;
490 val maxidx = Thm.maxidx_of th;
492 val ft = ((Z.move_down_right (* trueprop *)
495 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
497 (* prepare subst in every possible assumption *)
498 fun prep_subst_in_asms i gth =
499 map (prep_subst_in_asm i gth)
500 ((fn l => Library.upto (1, length l))
501 (Logic.prems_of_goal (Thm.prop_of gth) i));
504 (* substitute in an assumption using an object or meta level equality *)
505 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
507 val asmpreps = prep_subst_in_asms i th;
508 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
509 fun rewrite_with_thm r =
510 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
511 fun occ_search occ [] = Seq.empty
512 | occ_search occ ((asminfo, searchinfo)::moreasms) =
513 (case searchf searchinfo occ lhs of
514 SkipMore i => occ_search i moreasms
516 Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
517 (occ_search 1 moreasms))
518 (* find later substs also *)
520 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
522 in stepthms |> Seq.maps rewrite_with_thm end;
525 fun skip_first_asm_occs_search searchf sinfo occ lhs =
526 skipto_skipseq occ (searchf sinfo lhs);
528 fun eqsubst_asm_tac ctxt occL thms i th =
529 let val nprems = Thm.nprems_of th
531 if nprems < i then Seq.empty else
532 let val thmseq = (Seq.of_list thms)
533 fun apply_occ occK th =
536 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
537 searchf_lr_unify_valid) occK r
538 (i + ((Thm.nprems_of th) - nprems))
541 Library.sort (Library.rev_order o Library.int_ord) occL
543 Seq.map distinct_subgoals
544 (Seq.EVERY (map apply_occ sortedoccs) th)
547 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
549 (* inthms are the given arguments in Isar, and treated as eqstep with
550 the first one, then the second etc *)
551 fun eqsubst_asm_meth ctxt occL inthms =
552 Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
554 (* syntax for options, given "(asm)" will give back true, without
557 (Args.parens (Args.$$$ "asm") >> (K true)) ||
558 (Scan.succeed false);
561 Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
563 (* combination method that takes a flag (true indicates that subst
564 should be done to an assumption, false = apply to the conclusion of
565 the goal) as well as the theorems to use *)
567 Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
568 #> (fn (((asmflag, occL), inthms), ctxt) =>
569 (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
573 Method.add_method ("subst", subst_meth, "single-step substitution");