lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
2 (* Title: Provers/eqsubst.ML
3 Author: Lucas Dixon, University of Edinburgh
5 Modified: 18 Feb 2005 - Lucas -
8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
11 A Tactic to perform a substiution using an equation.
14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
16 (* Logic specific data stub *)
17 signature EQRULE_DATA =
20 (* to make a meta equality theorem in the current logic *)
21 val prep_meta_eq : thm -> thm list
26 (* the signature of an instance of the SQSUBST tactic *)
27 signature EQSUBST_TAC =
31 ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
32 * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
33 * (string * Term.typ) list (* fake named type abs env *)
34 * (string * Term.typ) list (* type abs env *)
35 * Term.term (* outer term *)
37 val prep_subst_in_asm :
38 (Sign.sg (* sign for matching *)
40 -> 'a (* input object kind *)
41 -> BasicIsaFTerm.FcTerm (* focusterm to search under *)
42 -> 'b) (* result type *)
43 -> int (* subgoal to subst in *)
44 -> Thm.thm (* target theorem with subgoals *)
45 -> int (* premise to subst in *)
46 -> (Thm.cterm list (* certified free var placeholders for vars *)
47 * int (* premice no. to subst *)
48 * int (* number of assumptions of premice *)
49 * Thm.thm) (* premice as a new theorem for forward reasoning *)
50 * ('a -> 'b) (* matchf *)
52 val prep_subst_in_asms :
53 (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b)
54 -> int (* subgoal to subst in *)
55 -> Thm.thm (* target theorem with subgoals *)
56 -> ((Thm.cterm list (* certified free var placeholders for vars *)
57 * int (* premice no. to subst *)
58 * int (* number of assumptions of premice *)
59 * Thm.thm) (* premice as a new theorem for forward reasoning *)
60 * ('a -> 'b)) (* matchf *)
63 val apply_subst_in_asm :
65 -> Thm.thm (* overall theorem *)
66 -> (Thm.cterm list (* certified free var placeholders for vars *)
67 * int (* assump no being subst *)
68 * int (* num of premises of asm *)
69 * Thm.thm) (* premthm *)
74 val prep_concl_subst :
75 (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *)
77 -> Thm.thm (* overall goal theorem *)
78 -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *)
80 val apply_subst_in_concl :
82 -> Thm.thm (* thm with all goals *)
83 -> Thm.cterm list (* certified free var placeholders for vars *)
84 * Thm.thm (* trivial thm of goal concl *)
85 (* possible matches/unifiers *)
88 -> Thm.thm Seq.seq (* substituted goal *)
90 val searchf_tlr_unify_all :
93 BasicIsaFTerm.FcTerm ->
94 match Seq.seq Seq.seq)
95 val searchf_tlr_unify_valid :
98 BasicIsaFTerm.FcTerm ->
99 match Seq.seq Seq.seq)
101 val eqsubst_asm_meth : int list -> Thm.thm list -> Proof.method
102 val eqsubst_asm_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
103 val eqsubst_asm_tac' :
106 BasicIsaFTerm.FcTerm ->
107 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
109 val eqsubst_meth : int list -> Thm.thm list -> Proof.method
110 val eqsubst_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
114 BasicIsaFTerm.FcTerm ->
115 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
117 val meth : (bool * int list) * Thm.thm list -> Proof.context -> Proof.method
118 val setup : (Theory.theory -> Theory.theory) list
121 functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA)
125 (* a type abriviation for match information *)
127 ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
128 * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
129 * (string * Term.typ) list (* fake named type abs env *)
130 * (string * Term.typ) list (* type abs env *)
131 * Term.term (* outer term *)
135 type trace_subst_errT = int (* subgoal *)
136 * Thm.thm (* thm with all goals *)
137 * (Thm.cterm list (* certified free var placeholders for vars *)
138 * Thm.thm) (* trivial thm of goal concl *)
139 (* possible matches/unifiers *)
141 * (((Term.indexname * Term.typ) list (* type instantiations *)
142 * (Term.indexname * Term.term) list ) (* term instantiations *)
143 * (string * Term.typ) list (* Type abs env *)
144 * Term.term) (* outer term *);
146 val trace_subst_err = (ref NONE : trace_subst_errT option ref);
147 val trace_subst_search = ref false;
148 exception trace_subst_exp of trace_subst_errT;
151 (* also defined in /HOL/Tools/inductive_codegen.ML,
152 maybe move this to seq.ML ? *)
154 fun s :-> f = Seq.flat (Seq.map f s);
156 (* search from top, left to right, then down *)
157 fun search_tlr_all_f f ft =
160 let val t' = (IsaFTerm.focus_of_fcterm ft)
162 if !trace_subst_search then
163 (writeln ("Examining: " ^ (TermLib.string_of_term t'));
164 TermLib.writeterm t'; ())
168 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
170 maux (IsaFTerm.focus_right ft)))
171 | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
172 | leaf => Seq.single (f ft)) end
175 (* search from top, left to right, then down *)
176 fun search_tlr_valid_f f ft =
180 val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
182 (case (IsaFTerm.focus_of_fcterm ft) of
183 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
185 maux (IsaFTerm.focus_right ft)))
186 | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
187 | leaf => Seq.single (hereseq))
191 (* search all unifications *)
192 fun searchf_tlr_unify_all sgn maxidx lhs =
193 IsaFTerm.find_fcterm_matches
195 (IsaFTerm.clean_unify_ft sgn maxidx lhs);
197 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
198 fun searchf_tlr_unify_valid sgn maxidx lhs =
199 IsaFTerm.find_fcterm_matches
201 (IsaFTerm.clean_unify_ft sgn maxidx lhs);
203 (* special tactic to skip the first "occ" occurances - ie start at the nth match *)
204 fun skip_first_occs_search occ searchf sgn i t ft =
209 (case (Seq.pull sq) of NONE => Seq.empty
211 (case Seq.pull h of NONE => skip_occs n t
212 | SOME _ => skip_occs (n - 1) t))
213 in Seq.flat (skip_occs occ (searchf sgn i t ft)) end;
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);
229 |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
233 (* substitute within the conclusion of goal i of gth, using a meta
234 equation rule. Note that we assume rule has var indicies zero'd *)
235 fun prep_concl_subst searchf i gth =
237 val th = Thm.incr_indexes 1 gth;
238 val tgt_term = Thm.prop_of th;
240 val sgn = Thm.sign_of_thm th;
241 val ctermify = Thm.cterm_of sgn;
242 val trivify = Thm.trivial o ctermify;
244 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
245 val cfvs = rev (map ctermify fvs);
247 val conclterm = Logic.strip_imp_concl fixedbody;
248 val conclthm = trivify conclterm;
249 val maxidx = Term.maxidx_of_term conclterm;
252 (fn lhs => searchf sgn maxidx lhs
253 ((IsaFTerm.focus_right
254 o IsaFTerm.focus_left
255 o IsaFTerm.fcterm_of_term
256 o Thm.prop_of) conclthm)))
259 (* substitute using an object or meta level equality *)
260 fun eqsubst_tac' searchf instepthm i th =
262 val (cvfsconclthm, findmatchf) =
263 prep_concl_subst searchf i th;
266 Seq.map Drule.zero_var_indexes
267 (Seq.of_list (EqRuleData.prep_meta_eq instepthm));
269 fun rewrite_with_thm r =
270 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
272 :-> (apply_subst_in_concl i th cvfsconclthm r) end;
274 in (stepthms :-> rewrite_with_thm) end;
277 (* General substiuttion of multiple occurances using one of
279 fun eqsubst_occL tac 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 => tac (skip_first_occs_search
286 occ searchf_tlr_unify_valid) r
287 (i + ((Thm.nprems_of th) - nprems))
290 Seq.EVERY (map apply_occ (Library.sort (Library.rev_order o Library.int_ord) occL))
295 (* implicit argus: occL thms i th *)
296 val eqsubst_tac = eqsubst_occL eqsubst_tac';
299 (* inthms are the given arguments in Isar, and treated as eqstep with
300 the first one, then the second etc *)
301 fun eqsubst_meth occL inthms =
304 HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms ));
307 fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m =
308 (RWInst.rw m rule pth)
309 |> Thm.permute_prems 0 ~1
310 |> IsaND.unfix_frees cfvs
311 |> RWInst.beta_eta_contract
312 |> (fn r => Tactic.dtac r i th);
315 ? should I be using bicompose what if we match more than one
316 assumption, even after instantiation ? (back will work, but it would
317 be nice to avoid the redudent search)
320 |> Thm.lift_rule (th, i)
321 |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r - nprems) i th)
326 (* prepare to substitute within the j'th premise of subgoal i of gth,
327 using a meta-level equation. Note that we assume rule has var indicies
328 zero'd. Note that we also assume that premt is the j'th premice of
329 subgoal i of gth. Note the repetition of work done for each
330 assumption, i.e. this can be made more efficient for search over
331 multiple assumptions. *)
332 fun prep_subst_in_asm searchf i gth j =
334 val th = Thm.incr_indexes 1 gth;
335 val tgt_term = Thm.prop_of th;
337 val sgn = Thm.sign_of_thm th;
338 val ctermify = Thm.cterm_of sgn;
339 val trivify = Thm.trivial o ctermify;
341 val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
342 val cfvs = rev (map ctermify fvs);
344 val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
345 val asm_nprems = length (Logic.strip_imp_prems asmt);
347 val pth = trivify asmt;
348 val maxidx = Term.maxidx_of_term asmt;
351 ((cfvs, j, asm_nprems, pth),
352 (fn lhs => (searchf sgn maxidx lhs
353 ((IsaFTerm.focus_right
354 o IsaFTerm.fcterm_of_term
355 o Thm.prop_of) pth))))
358 (* prepare subst in every possible assumption *)
359 fun prep_subst_in_asms searchf i gth =
361 (prep_subst_in_asm searchf i gth)
362 (Seq.of_list (IsaPLib.mk_num_list
363 (length (Logic.prems_of_goal (Thm.prop_of gth) i))));
366 (* substitute in an assumption using an object or meta level equality *)
367 fun eqsubst_asm_tac' searchf instepthm i th =
369 val asmpreps = prep_subst_in_asms searchf i th;
371 Seq.map Drule.zero_var_indexes
372 (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
374 fun rewrite_with_thm (asminfo, findmatchf) r =
375 let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
377 :-> (apply_subst_in_asm i th asminfo r) end;
379 (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a))
382 (* substitute using one of the given theorems in an assumption.
383 Implicit args: occL thms i th *)
384 val eqsubst_asm_tac = eqsubst_occL eqsubst_asm_tac';
387 (* inthms are the given arguments in Isar, and treated as eqstep with
388 the first one, then the second etc *)
389 fun eqsubst_asm_meth occL inthms =
392 HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occL inthms ));
394 (* combination method that takes a flag (true indicates that subst
395 should be done to an assumption, false = apply to the conclusion of
396 the goal) as well as the theorems to use *)
397 fun meth ((asmflag, occL), inthms) ctxt =
398 if asmflag then eqsubst_asm_meth occL inthms else eqsubst_meth occL inthms;
400 (* syntax for options, given "(asm)" will give back true, without
403 (Args.parens (Args.$$$ "asm") >> (K true)) ||
404 (Scan.succeed false);
407 (Args.parens (Scan.repeat Args.nat))
408 || (Scan.succeed [0]);
410 (* method syntax, first take options, then theorems *)
411 fun meth_syntax meth src ctxt =
412 meth (snd (Method.syntax ((Scan.lift options_syntax)
413 -- (Scan.lift ith_syntax)
414 -- Attrib.local_thms) src ctxt))
417 (* setup function for adding method to theory. *)
419 [Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")];