1 (* Title: Provers/eqsubst.ML
3 Author: Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
5 A proof method to perform a substiution using an equation.
10 (* a type abriviation for match information *)
12 ((indexname * (sort * typ)) list (* type instantiations *)
13 * (indexname * (typ * term)) list) (* term instantiations *)
14 * (string * typ) list (* fake named type abs env *)
15 * (string * typ) list (* type abs env *)
16 * term (* outer term *)
21 * Zipper.T (* focusterm to search under *)
23 exception eqsubst_occL_exp of
24 string * int list * Thm.thm list * int * Thm.thm
26 (* low level substitution functions *)
27 val apply_subst_in_asm :
31 (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
32 val apply_subst_in_concl :
35 Thm.cterm list * Thm.thm ->
36 Thm.thm -> match -> Thm.thm Seq.seq
38 (* matching/unification within zippers *)
40 Context.theory -> Term.term -> Zipper.T -> match option
42 Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
44 (* skipping things in seq seq's *)
46 (* skipping non-empty sub-sequences but when we reach the end
47 of the seq, remembering how much we have left to skip. *)
48 datatype 'a skipseq = SkipMore of int
49 | SkipSeq of 'a Seq.seq Seq.seq;
51 val skip_first_asm_occs_search :
52 ('a -> 'b -> 'c Seq.seq Seq.seq) ->
53 'a -> int -> 'b -> 'c skipseq
54 val skip_first_occs_search :
55 int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
56 val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
61 int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
62 val eqsubst_asm_tac' :
64 (searchinfo -> int -> Term.term -> match skipseq) ->
65 int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
68 int list -> (* list of occurences to rewrite, use [0] for any *)
69 Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
71 Proof.context -> (* proof context *)
72 (searchinfo -> Term.term -> match Seq.seq) (* search function *)
73 -> Thm.thm (* equation theorem to rewrite with *)
74 -> int (* subgoal number in goal theorem *)
75 -> Thm.thm (* goal theorem *)
76 -> Thm.thm Seq.seq (* rewritten goal theorem *)
79 val fakefree_badbounds :
80 (string * Term.typ) list ->
82 (string * Term.typ) list * (string * Term.typ) list * Term.term
85 (Term.term -> Term.term) ->
86 ('a * Term.typ) list -> Term.term -> Term.term
88 (* preparing substitution *)
89 val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
90 val prep_concl_subst :
91 int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
92 val prep_subst_in_asm :
93 int -> Thm.thm -> int ->
94 (Thm.cterm list * int * int * Thm.thm) * searchinfo
95 val prep_subst_in_asms :
97 ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
98 val prep_zipper_match :
99 Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
101 (* search for substitutions *)
102 val valid_match_start : Zipper.T -> bool
103 val search_lr_all : Zipper.T -> Zipper.T Seq.seq
104 val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
105 val searchf_lr_unify_all :
106 searchinfo -> Term.term -> match Seq.seq Seq.seq
107 val searchf_lr_unify_valid :
108 searchinfo -> Term.term -> match Seq.seq Seq.seq
109 val searchf_bt_unify_valid :
110 searchinfo -> Term.term -> match Seq.seq Seq.seq
113 val ith_syntax : Args.T list -> int list * Args.T list
114 val options_syntax : Args.T list -> bool * Args.T list
116 (* Isar level hooks *)
117 val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
118 val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
119 val subst_meth : Method.src -> Proof.context -> Proof.method
120 val setup : theory -> theory
128 structure Z = Zipper;
130 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
131 fun prep_meta_eq ctxt =
132 let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
133 in mk #> map Drule.zero_var_indexes end;
136 (* a type abriviation for match information *)
138 ((indexname * (sort * typ)) list (* type instantiations *)
139 * (indexname * (typ * term)) list) (* term instantiations *)
140 * (string * typ) list (* fake named type abs env *)
141 * (string * typ) list (* type abs env *)
142 * term (* outer term *)
147 * Zipper.T (* focusterm to search under *)
150 (* skipping non-empty sub-sequences but when we reach the end
151 of the seq, remembering how much we have left to skip. *)
152 datatype 'a skipseq = SkipMore of int
153 | SkipSeq of 'a Seq.seq Seq.seq;
154 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
155 fun skipto_skipseq m s =
161 (case Seq.pull h of NONE => skip_occs n t
162 | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
163 else skip_occs (n - 1) t)
164 in (skip_occs m s) end;
166 (* note: outerterm is the taget with the match replaced by a bound
167 variable : ie: "P lhs" beocmes "%x. P x"
168 insts is the types of instantiations of vars in lhs
169 and typinsts is the type instantiations of types in the lhs
170 Note: Final rule is the rule lifted into the ontext of the
172 fun mk_foo_match mkuptermfunc Ts t =
174 val ty = Term.type_of t
175 val bigtype = (rev (map snd Ts)) ---> ty
177 | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
178 val num_of_bnds = (length Ts)
179 (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
180 val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
181 in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
183 (* T is outer bound vars, n is number of locally bound vars *)
184 (* THINK: is order of Ts correct...? or reversed? *)
185 fun fakefree_badbounds Ts t =
186 let val (FakeTs,Ts,newnames) =
187 List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
188 let val newname = Name.variant usednames n
189 in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
191 newname::usednames) end)
194 in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
196 (* before matching we need to fake the bound vars that are missing an
197 abstraction. In this function we additionally construct the
198 abstraction environment, and an outer context term (with the focus
199 abstracted out) for use in rewriting with RWInst.rw *)
200 fun prep_zipper_match z =
204 val Ts = Z.C.nty_ctxt c
205 val (FakeTs', Ts', t') = fakefree_badbounds Ts t
206 val absterm = mk_foo_match (Z.C.apply c) Ts' t'
208 (t', (FakeTs', Ts', absterm))
211 (* Matching and Unification with exception handled *)
212 fun clean_match thy (a as (pat, t)) =
213 let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
214 in SOME (Vartab.dest tyenv, Vartab.dest tenv)
215 end handle Pattern.MATCH => NONE;
217 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
218 fun clean_unify thry ix (a as (pat, tgt)) =
220 (* type info will be re-derived, maybe this can be cached
222 val pat_ty = Term.type_of pat;
223 val tgt_ty = Term.type_of tgt;
224 (* is it OK to ignore the type instantiation info?
225 or should I be using it? *)
227 SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
228 handle Type.TUNIFY => NONE;
231 SOME (typinsttab, ix2) =>
233 (* is it right to throw away the flexes?
234 or should I be using them somehow? *)
236 (Vartab.dest (Envir.type_env env),
238 val initenv = Envir.Envir {asol = Vartab.empty,
239 iTs = typinsttab, maxidx = ix2};
240 val useq = Unify.smash_unifiers thry [a] initenv
241 handle UnequalLengths => Seq.empty
242 | Term.TERM _ => Seq.empty;
243 fun clean_unify' useq () =
244 (case (Seq.pull useq) of
246 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
247 handle UnequalLengths => NONE
248 | Term.TERM _ => NONE
250 (Seq.make (clean_unify' useq))
255 (* Matching and Unification for zippers *)
256 (* Note: Ts is a modified version of the original names of the outer
257 bound variables. New names have been introduced to make sure they are
258 unique w.r.t all names in the term and each other. usednames' is
259 oldnames + new names. *)
260 fun clean_match_z thy pat z =
261 let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
262 case clean_match thy (pat, t) of
264 | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
265 (* ix = max var index *)
266 fun clean_unify_z sgn ix pat z =
267 let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
268 Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
269 (clean_unify sgn ix (t, pat)) end;
273 type trace_subst_errT = int (* subgoal *)
274 * thm (* thm with all goals *)
275 * (Thm.cterm list (* certified free var placeholders for vars *)
276 * thm) (* trivial thm of goal concl *)
277 (* possible matches/unifiers *)
279 * (((indexname * typ) list (* type instantiations *)
280 * (indexname * term) list ) (* term instantiations *)
281 * (string * typ) list (* Type abs env *)
282 * term) (* outer term *);
284 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
285 val trace_subst_search = ref false;
286 exception trace_subst_exp of trace_subst_errT;
290 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
291 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
292 | bot_left_leaf_of x = x;
294 (* Avoid considering replacing terms which have a var at the head as
295 they always succeed trivially, and uninterestingly. *)
296 fun valid_match_start z =
297 (case bot_left_leaf_of (Z.trm z) of
301 (* search from top, left to right, then down *)
302 val search_lr_all = ZipperSearch.all_bl_ur;
304 (* search from top, left to right, then down *)
305 fun search_lr_valid validf =
307 fun sf_valid_td_lr z =
308 let val here = if validf z then [Z.Here z] else [] in
310 of _ $ _ => [Z.LookIn (Z.move_down_left z)]
312 @ [Z.LookIn (Z.move_down_right z)]
313 | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
316 in Z.lzy_search sf_valid_td_lr end;
318 (* search from bottom to top, left to right *)
320 fun search_bt_valid validf =
322 fun sf_valid_td_lr z =
323 let val here = if validf z then [Z.Here z] else [] in
325 of _ $ _ => [Z.LookIn (Z.move_down_left z),
326 Z.LookIn (Z.move_down_right z)] @ here
327 | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
330 in Z.lzy_search sf_valid_td_lr end;
332 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
333 Seq.map (clean_unify_z sgn maxidx lhs)
336 (* search all unifications *)
337 val searchf_lr_unify_all =
338 searchf_unify_gen search_lr_all;
340 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
341 val searchf_lr_unify_valid =
342 searchf_unify_gen (search_lr_valid valid_match_start);
344 val searchf_bt_unify_valid =
345 searchf_unify_gen (search_bt_valid valid_match_start);
347 (* apply a substitution in the conclusion of the theorem th *)
348 (* cfvs are certified free var placeholders for goal params *)
349 (* conclthm is a theorem of for just the conclusion *)
350 (* m is instantiation/match information *)
351 (* rule is the equation for substitution *)
352 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
353 (RWInst.rw m rule conclthm)
354 |> IsaND.unfix_frees cfvs
355 |> RWInst.beta_eta_contract
356 |> (fn r => Tactic.rtac r i th);
358 (* substitute within the conclusion of goal i of gth, using a meta
359 equation rule. Note that we assume rule has var indicies zero'd *)
360 fun prep_concl_subst i gth =
362 val th = Thm.incr_indexes 1 gth;
363 val tgt_term = Thm.prop_of th;
365 val sgn = Thm.theory_of_thm th;
366 val ctermify = Thm.cterm_of sgn;
367 val trivify = Thm.trivial o ctermify;
369 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
370 val cfvs = rev (map ctermify fvs);
372 val conclterm = Logic.strip_imp_concl fixedbody;
373 val conclthm = trivify conclterm;
374 val maxidx = Thm.maxidx_of th;
375 val ft = ((Z.move_down_right (* ==> *)
376 o Z.move_down_left (* Trueprop *)
378 o Thm.prop_of) conclthm)
380 ((cfvs, conclthm), (sgn, maxidx, ft))
383 (* substitute using an object or meta level equality *)
384 fun eqsubst_tac' ctxt searchf instepthm i th =
386 val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
387 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
388 fun rewrite_with_thm r =
389 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
390 in searchf searchinfo lhs
391 |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
392 in stepthms |> Seq.maps rewrite_with_thm end;
395 (* distinct subgoals *)
396 fun distinct_subgoals th =
397 the_default th (SINGLE distinct_subgoals_tac th);
399 (* General substitution of multiple occurances using one of
403 exception eqsubst_occL_exp of
404 string * (int list) * (thm list) * int * thm;
405 fun skip_first_occs_search occ srchf sinfo lhs =
406 case (skipto_skipseq occ (srchf sinfo lhs)) of
407 SkipMore _ => Seq.empty
408 | SkipSeq ss => Seq.flat ss;
410 (* The occL is a list of integers indicating which occurence
411 w.r.t. the search order, to rewrite. Backtracking will also find later
412 occurences, but all earlier ones are skipped. Thus you can use [0] to
413 just find all rewrites. *)
415 fun eqsubst_tac ctxt occL thms i th =
416 let val nprems = Thm.nprems_of th in
417 if nprems < i then Seq.empty else
418 let val thmseq = (Seq.of_list thms)
419 fun apply_occ occ th =
421 (fn r => eqsubst_tac'
423 (skip_first_occs_search
424 occ searchf_lr_unify_valid) r
425 (i + ((Thm.nprems_of th) - nprems))
428 Library.sort (Library.rev_order o Library.int_ord) occL;
430 Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
433 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
436 (* inthms are the given arguments in Isar, and treated as eqstep with
437 the first one, then the second etc *)
438 fun eqsubst_meth ctxt occL inthms =
439 Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
441 (* apply a substitution inside assumption j, keeps asm in the same place *)
442 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
444 val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
446 (RWInst.rw m rule pth)
447 |> (Seq.hd o prune_params_tac)
448 |> Thm.permute_prems 0 ~1 (* put old asm first *)
449 |> IsaND.unfix_frees cfvs (* unfix any global params *)
450 |> RWInst.beta_eta_contract; (* normal form *)
453 |> Tactic.make_elim (* make into elim rule *)
454 |> Thm.lift_rule (th2, i); (* lift into context *)
457 (* ~j because new asm starts at back, thus we subtract 1 *)
458 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
459 (Tactic.dtac preelimrule i th2)
462 false (* use unification *)
463 (true, (* elim resolution *)
464 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
469 (* prepare to substitute within the j'th premise of subgoal i of gth,
470 using a meta-level equation. Note that we assume rule has var indicies
471 zero'd. Note that we also assume that premt is the j'th premice of
472 subgoal i of gth. Note the repetition of work done for each
473 assumption, i.e. this can be made more efficient for search over
474 multiple assumptions. *)
475 fun prep_subst_in_asm i gth j =
477 val th = Thm.incr_indexes 1 gth;
478 val tgt_term = Thm.prop_of th;
480 val sgn = Thm.theory_of_thm th;
481 val ctermify = Thm.cterm_of sgn;
482 val trivify = Thm.trivial o ctermify;
484 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
485 val cfvs = rev (map ctermify fvs);
487 val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
488 val asm_nprems = length (Logic.strip_imp_prems asmt);
490 val pth = trivify asmt;
491 val maxidx = Thm.maxidx_of th;
493 val ft = ((Z.move_down_right (* trueprop *)
496 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
498 (* prepare subst in every possible assumption *)
499 fun prep_subst_in_asms i gth =
500 map (prep_subst_in_asm i gth)
501 ((fn l => Library.upto (1, length l))
502 (Logic.prems_of_goal (Thm.prop_of gth) i));
505 (* substitute in an assumption using an object or meta level equality *)
506 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
508 val asmpreps = prep_subst_in_asms i th;
509 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
510 fun rewrite_with_thm r =
511 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
512 fun occ_search occ [] = Seq.empty
513 | occ_search occ ((asminfo, searchinfo)::moreasms) =
514 (case searchf searchinfo occ lhs of
515 SkipMore i => occ_search i moreasms
517 Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
518 (occ_search 1 moreasms))
519 (* find later substs also *)
521 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
523 in stepthms |> Seq.maps rewrite_with_thm end;
526 fun skip_first_asm_occs_search searchf sinfo occ lhs =
527 skipto_skipseq occ (searchf sinfo lhs);
529 fun eqsubst_asm_tac ctxt occL thms i th =
530 let val nprems = Thm.nprems_of th
532 if nprems < i then Seq.empty else
533 let val thmseq = (Seq.of_list thms)
534 fun apply_occ occK th =
537 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
538 searchf_lr_unify_valid) occK r
539 (i + ((Thm.nprems_of th) - nprems))
542 Library.sort (Library.rev_order o Library.int_ord) occL
544 Seq.map distinct_subgoals
545 (Seq.EVERY (map apply_occ sortedoccs) th)
548 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
550 (* inthms are the given arguments in Isar, and treated as eqstep with
551 the first one, then the second etc *)
552 fun eqsubst_asm_meth ctxt occL inthms =
553 Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
555 (* syntax for options, given "(asm)" will give back true, without
558 (Args.parens (Args.$$$ "asm") >> (K true)) ||
559 (Scan.succeed false);
562 Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
564 (* combination method that takes a flag (true indicates that subst
565 should be done to an assumption, false = apply to the conclusion of
566 the goal) as well as the theorems to use *)
568 Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
569 #> (fn (((asmflag, occL), inthms), ctxt) =>
570 (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
574 Method.add_method ("subst", subst_meth, "single-step substitution");