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 val setup : theory -> theory
19 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
20 fun prep_meta_eq ctxt =
21 let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
22 in mk #> map Drule.zero_var_indexes end;
25 (* a type abriviation for match information *)
27 ((indexname * (sort * typ)) list (* type instantiations *)
28 * (indexname * (typ * term)) list) (* term instantiations *)
29 * (string * typ) list (* fake named type abs env *)
30 * (string * typ) list (* type abs env *)
31 * term (* outer term *)
36 * Zipper.T (* focusterm to search under *)
39 (* skipping non-empty sub-sequences but when we reach the end
40 of the seq, remembering how much we have left to skip. *)
41 datatype 'a skipseq = SkipMore of int
42 | SkipSeq of 'a Seq.seq Seq.seq;
43 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
44 fun skipto_skipseq m s =
50 (case Seq.pull h of NONE => skip_occs n t
51 | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
52 else skip_occs (n - 1) t)
53 in (skip_occs m s) end;
55 (* note: outerterm is the taget with the match replaced by a bound
56 variable : ie: "P lhs" beocmes "%x. P x"
57 insts is the types of instantiations of vars in lhs
58 and typinsts is the type instantiations of types in the lhs
59 Note: Final rule is the rule lifted into the ontext of the
61 fun mk_foo_match mkuptermfunc Ts t =
63 val ty = Term.type_of t
64 val bigtype = (rev (map snd Ts)) ---> ty
66 | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
67 val num_of_bnds = (length Ts)
68 (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
69 val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
70 in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
72 (* T is outer bound vars, n is number of locally bound vars *)
73 (* THINK: is order of Ts correct...? or reversed? *)
74 fun fakefree_badbounds Ts t =
75 let val (FakeTs,Ts,newnames) =
76 List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
77 let val newname = Term.variant usednames n
78 in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
80 newname::usednames) end)
83 in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
85 (* before matching we need to fake the bound vars that are missing an
86 abstraction. In this function we additionally construct the
87 abstraction environment, and an outer context term (with the focus
88 abstracted out) for use in rewriting with RWInst.rw *)
89 fun prep_zipper_match z =
93 val Ts = Z.C.nty_ctxt c
94 val (FakeTs', Ts', t') = fakefree_badbounds Ts t
95 val absterm = mk_foo_match (Z.C.apply c) Ts' t'
97 (t', (FakeTs', Ts', absterm))
100 (* Matching and Unification with exception handled *)
101 fun clean_match thy (a as (pat, t)) =
102 let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
103 in SOME (Vartab.dest tyenv, Vartab.dest tenv)
104 end handle Pattern.MATCH => NONE;
105 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
106 fun clean_unify sgn ix (a as (pat, tgt)) =
108 (* type info will be re-derived, maybe this can be cached
110 val pat_ty = Term.type_of pat;
111 val tgt_ty = Term.type_of tgt;
112 (* is it OK to ignore the type instantiation info?
113 or should I be using it? *)
115 SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
116 handle Type.TUNIFY => NONE;
119 SOME (typinsttab, ix2) =>
121 (* is it right to throw away the flexes?
122 or should I be using them somehow? *)
124 (Vartab.dest (Envir.type_env env),
126 val initenv = Envir.Envir {asol = Vartab.empty,
127 iTs = typinsttab, maxidx = ix2};
128 val useq = Unify.smash_unifiers sgn [a] initenv
129 handle UnequalLengths => Seq.empty
130 | Term.TERM _ => Seq.empty;
131 fun clean_unify' useq () =
132 (case (Seq.pull useq) of
134 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
135 handle UnequalLengths => NONE
136 | Term.TERM _ => NONE;
138 (Seq.make (clean_unify' useq))
143 (* Matching and Unification for zippers *)
144 (* Note: Ts is a modified version of the original names of the outer
145 bound variables. New names have been introduced to make sure they are
146 unique w.r.t all names in the term and each other. usednames' is
147 oldnames + new names. *)
148 fun clean_match_z thy pat z =
149 let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
150 case clean_match thy (pat, t) of
152 | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
153 (* ix = max var index *)
154 fun clean_unify_z sgn ix pat z =
155 let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
156 Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
157 (clean_unify sgn ix (t, pat)) end;
161 type trace_subst_errT = int (* subgoal *)
162 * thm (* thm with all goals *)
163 * (Thm.cterm list (* certified free var placeholders for vars *)
164 * thm) (* trivial thm of goal concl *)
165 (* possible matches/unifiers *)
167 * (((indexname * typ) list (* type instantiations *)
168 * (indexname * term) list ) (* term instantiations *)
169 * (string * typ) list (* Type abs env *)
170 * term) (* outer term *);
172 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
173 val trace_subst_search = ref false;
174 exception trace_subst_exp of trace_subst_errT;
178 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
179 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
180 | bot_left_leaf_of x = x;
182 fun valid_match_start z =
183 (case bot_left_leaf_of (Z.trm z) of
186 | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
187 | _ => false); (* avoid vars - always suceeds uninterestingly. *)
189 (* search from top, left to right, then down *)
190 val search_tlr_all = ZipperSearch.all_td_lr;
192 (* search from top, left to right, then down *)
193 fun search_tlr_valid validf =
195 fun sf_valid_td_lr z =
196 let val here = if validf z then [Z.Here z] else [] in
198 of _ $ _ => here @ [Z.LookIn (Z.move_down_left z),
199 Z.LookIn (Z.move_down_right z)]
200 | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
203 in Z.lzy_search sf_valid_td_lr end;
205 (* search all unifications *)
206 fun searchf_tlr_unify_all (sgn, maxidx, z) lhs =
207 Seq.map (clean_unify_z sgn maxidx lhs)
208 (Z.limit_apply search_tlr_all z);
210 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
211 fun searchf_tlr_unify_valid (sgn, maxidx, z) lhs =
212 Seq.map (clean_unify_z sgn maxidx lhs)
213 (Z.limit_apply (search_tlr_valid valid_match_start) z);
216 (* apply a substitution in the conclusion of the theorem th *)
217 (* cfvs are certified free var placeholders for goal params *)
218 (* conclthm is a theorem of for just the conclusion *)
219 (* m is instantiation/match information *)
220 (* rule is the equation for substitution *)
221 fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
222 (RWInst.rw m rule conclthm)
223 |> IsaND.unfix_frees cfvs
224 |> RWInst.beta_eta_contract
225 |> (fn r => Tactic.rtac r i th);
227 (* substitute within the conclusion of goal i of gth, using a meta
228 equation rule. Note that we assume rule has var indicies zero'd *)
229 fun prep_concl_subst i gth =
231 val th = Thm.incr_indexes 1 gth;
232 val tgt_term = Thm.prop_of th;
234 val sgn = Thm.sign_of_thm th;
235 val ctermify = Thm.cterm_of sgn;
236 val trivify = Thm.trivial o ctermify;
238 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
239 val cfvs = rev (map ctermify fvs);
241 val conclterm = Logic.strip_imp_concl fixedbody;
242 val conclthm = trivify conclterm;
243 val maxidx = Term.maxidx_of_term conclterm;
244 val ft = ((Z.move_down_right (* ==> *)
245 o Z.move_down_left (* Trueprop *)
247 o Thm.prop_of) conclthm)
249 ((cfvs, conclthm), (sgn, maxidx, ft))
252 (* substitute using an object or meta level equality *)
253 fun eqsubst_tac' ctxt searchf instepthm i th =
255 val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
256 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
257 fun rewrite_with_thm r =
258 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
259 in searchf searchinfo lhs
260 |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
261 in stepthms |> Seq.maps rewrite_with_thm end;
264 (* distinct subgoals *)
265 fun distinct_subgoals th =
266 the_default th (SINGLE distinct_subgoals_tac th);
268 (* General substitution of multiple occurances using one of
272 exception eqsubst_occL_exp of
273 string * (int list) * (thm list) * int * thm;
274 fun skip_first_occs_search occ srchf sinfo lhs =
275 case (skipto_skipseq occ (srchf sinfo lhs)) of
276 SkipMore _ => Seq.empty
277 | SkipSeq ss => Seq.flat ss;
279 fun eqsubst_tac ctxt occL thms i th =
280 let val nprems = Thm.nprems_of th in
281 if nprems < i then Seq.empty else
282 let val thmseq = (Seq.of_list thms)
283 fun apply_occ occ th =
285 (fn r => eqsubst_tac'
287 (skip_first_occs_search
288 occ searchf_tlr_unify_valid) r
289 (i + ((Thm.nprems_of th) - nprems))
292 Library.sort (Library.rev_order o Library.int_ord) occL;
294 Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
297 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
300 (* inthms are the given arguments in Isar, and treated as eqstep with
301 the first one, then the second etc *)
302 fun eqsubst_meth ctxt occL inthms =
305 HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
307 (* apply a substitution inside assumption j, keeps asm in the same place *)
308 fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
310 val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
312 (RWInst.rw m rule pth)
313 |> (Seq.hd o Tactic.prune_params_tac)
314 |> Thm.permute_prems 0 ~1 (* put old asm first *)
315 |> IsaND.unfix_frees cfvs (* unfix any global params *)
316 |> RWInst.beta_eta_contract; (* normal form *)
319 |> Tactic.make_elim (* make into elim rule *)
320 |> Thm.lift_rule (th2, i); (* lift into context *)
323 (* ~j because new asm starts at back, thus we subtract 1 *)
324 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
325 (Tactic.dtac preelimrule i th2)
328 false (* use unification *)
329 (true, (* elim resolution *)
330 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
335 (* prepare to substitute within the j'th premise of subgoal i of gth,
336 using a meta-level equation. Note that we assume rule has var indicies
337 zero'd. Note that we also assume that premt is the j'th premice of
338 subgoal i of gth. Note the repetition of work done for each
339 assumption, i.e. this can be made more efficient for search over
340 multiple assumptions. *)
341 fun prep_subst_in_asm i gth j =
343 val th = Thm.incr_indexes 1 gth;
344 val tgt_term = Thm.prop_of th;
346 val sgn = Thm.sign_of_thm th;
347 val ctermify = Thm.cterm_of sgn;
348 val trivify = Thm.trivial o ctermify;
350 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
351 val cfvs = rev (map ctermify fvs);
353 val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
354 val asm_nprems = length (Logic.strip_imp_prems asmt);
356 val pth = trivify asmt;
357 val maxidx = Term.maxidx_of_term asmt;
359 val ft = ((Z.move_down_right (* trueprop *)
362 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
364 (* prepare subst in every possible assumption *)
365 fun prep_subst_in_asms i gth =
366 map (prep_subst_in_asm i gth)
367 ((fn l => Library.upto (1, length l))
368 (Logic.prems_of_goal (Thm.prop_of gth) i));
371 (* substitute in an assumption using an object or meta level equality *)
372 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
374 val asmpreps = prep_subst_in_asms i th;
375 val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
376 fun rewrite_with_thm r =
377 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
378 fun occ_search occ [] = Seq.empty
379 | occ_search occ ((asminfo, searchinfo)::moreasms) =
380 (case searchf searchinfo occ lhs of
381 SkipMore i => occ_search i moreasms
383 Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
384 (occ_search 1 moreasms))
385 (* find later substs also *)
387 occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
389 in stepthms |> Seq.maps rewrite_with_thm end;
392 fun skip_first_asm_occs_search searchf sinfo occ lhs =
393 skipto_skipseq occ (searchf sinfo lhs);
395 fun eqsubst_asm_tac ctxt occL thms i th =
396 let val nprems = Thm.nprems_of th
398 if nprems < i then Seq.empty else
399 let val thmseq = (Seq.of_list thms)
400 fun apply_occ occK th =
403 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
404 searchf_tlr_unify_valid) occK r
405 (i + ((Thm.nprems_of th) - nprems))
408 Library.sort (Library.rev_order o Library.int_ord) occL
410 Seq.map distinct_subgoals
411 (Seq.EVERY (map apply_occ sortedoccs) th)
414 handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
416 (* inthms are the given arguments in Isar, and treated as eqstep with
417 the first one, then the second etc *)
418 fun eqsubst_asm_meth ctxt occL inthms =
421 HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
423 (* syntax for options, given "(asm)" will give back true, without
426 (Args.parens (Args.$$$ "asm") >> (K true)) ||
427 (Scan.succeed false);
430 (Args.parens (Scan.repeat Args.nat))
431 || (Scan.succeed [0]);
433 (* combination method that takes a flag (true indicates that subst
434 should be done to an assumption, false = apply to the conclusion of
435 the goal) as well as the theorems to use *)
437 Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
438 #> (fn (ctxt, ((asmflag, occL), inthms)) =>
439 (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
443 Method.add_method ("subst", subst_meth, "single-step substitution");