96 (Sign.sg -> int -> |
96 (Sign.sg -> int -> |
97 Term.term -> |
97 Term.term -> |
98 BasicIsaFTerm.FcTerm -> |
98 BasicIsaFTerm.FcTerm -> |
99 match Seq.seq Seq.seq) |
99 match Seq.seq Seq.seq) |
100 |
100 |
101 val eqsubst_asm_meth : int -> Thm.thm list -> Proof.method |
101 val eqsubst_asm_meth : int list -> Thm.thm list -> Proof.method |
102 val eqsubst_asm_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq |
102 val eqsubst_asm_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq |
103 val eqsubst_asm_tac' : |
103 val eqsubst_asm_tac' : |
104 (Sign.sg -> int -> |
104 (Sign.sg -> int -> |
105 Term.term -> |
105 Term.term -> |
106 BasicIsaFTerm.FcTerm -> |
106 BasicIsaFTerm.FcTerm -> |
107 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq |
107 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq |
108 |
108 |
109 val eqsubst_meth : int -> Thm.thm list -> Proof.method |
109 val eqsubst_meth : int list -> Thm.thm list -> Proof.method |
110 val eqsubst_tac : int -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq |
110 val eqsubst_tac : int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq |
111 val eqsubst_tac' : |
111 val eqsubst_tac' : |
112 (Sign.sg -> int -> |
112 (Sign.sg -> int -> |
113 Term.term -> |
113 Term.term -> |
114 BasicIsaFTerm.FcTerm -> |
114 BasicIsaFTerm.FcTerm -> |
115 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq |
115 match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq |
116 |
116 |
117 val meth : (bool * int) * Thm.thm list -> Proof.context -> Proof.method |
117 val meth : (bool * int list) * Thm.thm list -> Proof.context -> Proof.method |
118 val setup : (Theory.theory -> Theory.theory) list |
118 val setup : (Theory.theory -> Theory.theory) list |
119 end; |
119 end; |
120 |
120 |
121 functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) |
121 functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) |
122 : EQSUBST_TAC |
122 : EQSUBST_TAC |
254 o IsaFTerm.focus_left |
254 o IsaFTerm.focus_left |
255 o IsaFTerm.fcterm_of_term |
255 o IsaFTerm.fcterm_of_term |
256 o Thm.prop_of) conclthm))) |
256 o Thm.prop_of) conclthm))) |
257 end; |
257 end; |
258 |
258 |
259 |
|
260 (* substitute using an object or meta level equality *) |
259 (* substitute using an object or meta level equality *) |
261 fun eqsubst_tac' searchf instepthm i th = |
260 fun eqsubst_tac' searchf instepthm i th = |
262 let |
261 let |
263 val (cvfsconclthm, findmatchf) = |
262 val (cvfsconclthm, findmatchf) = |
264 prep_concl_subst searchf i th; |
263 prep_concl_subst searchf i th; |
273 :-> (apply_subst_in_concl i th cvfsconclthm r) end; |
272 :-> (apply_subst_in_concl i th cvfsconclthm r) end; |
274 |
273 |
275 in (stepthms :-> rewrite_with_thm) end; |
274 in (stepthms :-> rewrite_with_thm) end; |
276 |
275 |
277 |
276 |
278 (* substitute using one of the given theorems *) |
277 (* General substiuttion of multiple occurances using one of |
279 fun eqsubst_tac occ instepthms i th = |
278 the given theorems*) |
280 if Thm.nprems_of th < i then Seq.empty else |
279 fun eqsubst_occL tac occL thms i th = |
281 (Seq.of_list instepthms) |
280 let val nprems = Thm.nprems_of th in |
282 :-> (fn r => eqsubst_tac' (skip_first_occs_search |
281 if nprems < i then Seq.empty else |
283 occ searchf_tlr_unify_valid) r i th); |
282 let val thmseq = (Seq.of_list thms) |
|
283 fun apply_occ occ th = |
|
284 thmseq :-> |
|
285 (fn r => tac (skip_first_occs_search |
|
286 occ searchf_tlr_unify_valid) r |
|
287 (i + ((Thm.nprems_of th) - nprems)) |
|
288 th); |
|
289 in |
|
290 Seq.EVERY (map apply_occ (Library.sort (Library.rev_order o Library.int_ord) occL)) |
|
291 th |
|
292 end |
|
293 end; |
|
294 |
|
295 (* implicit argus: occL thms i th *) |
|
296 val eqsubst_tac = eqsubst_occL eqsubst_tac'; |
|
297 |
284 |
298 |
285 (* inthms are the given arguments in Isar, and treated as eqstep with |
299 (* inthms are the given arguments in Isar, and treated as eqstep with |
286 the first one, then the second etc *) |
300 the first one, then the second etc *) |
287 fun eqsubst_meth occ inthms = |
301 fun eqsubst_meth occL inthms = |
288 Method.METHOD |
302 Method.METHOD |
289 (fn facts => |
303 (fn facts => |
290 HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occ inthms )); |
304 HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms )); |
291 |
305 |
292 |
306 |
293 fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = |
307 fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m = |
294 (RWInst.rw m rule pth) |
308 (RWInst.rw m rule pth) |
295 |> Thm.permute_prems 0 ~1 |
309 |> Thm.permute_prems 0 ~1 |
363 :-> (apply_subst_in_asm i th asminfo r) end; |
377 :-> (apply_subst_in_asm i th asminfo r) end; |
364 in |
378 in |
365 (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a)) |
379 (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a)) |
366 end; |
380 end; |
367 |
381 |
368 (* substitute using one of the given theorems *) |
382 (* substitute using one of the given theorems in an assumption. |
369 fun eqsubst_asm_tac occ instepthms i th = |
383 Implicit args: occL thms i th *) |
370 if Thm.nprems_of th < i then Seq.empty else |
384 val eqsubst_asm_tac = eqsubst_occL eqsubst_asm_tac'; |
371 (Seq.of_list instepthms) |
385 |
372 :-> (fn r => eqsubst_asm_tac' (skip_first_occs_search |
|
373 occ searchf_tlr_unify_valid) r i th); |
|
374 |
386 |
375 (* inthms are the given arguments in Isar, and treated as eqstep with |
387 (* inthms are the given arguments in Isar, and treated as eqstep with |
376 the first one, then the second etc *) |
388 the first one, then the second etc *) |
377 fun eqsubst_asm_meth occ inthms = |
389 fun eqsubst_asm_meth occL inthms = |
378 Method.METHOD |
390 Method.METHOD |
379 (fn facts => |
391 (fn facts => |
380 HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occ inthms )); |
392 HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occL inthms )); |
381 |
393 |
382 (* combination method that takes a flag (true indicates that subst |
394 (* combination method that takes a flag (true indicates that subst |
383 should be done to an assumption, false = apply to the conclusion of |
395 should be done to an assumption, false = apply to the conclusion of |
384 the goal) as well as the theorems to use *) |
396 the goal) as well as the theorems to use *) |
385 fun meth ((asmflag, occ), inthms) ctxt = |
397 fun meth ((asmflag, occL), inthms) ctxt = |
386 if asmflag then eqsubst_asm_meth occ inthms else eqsubst_meth occ inthms; |
398 if asmflag then eqsubst_asm_meth occL inthms else eqsubst_meth occL inthms; |
387 |
399 |
388 (* syntax for options, given "(asm)" will give back true, without |
400 (* syntax for options, given "(asm)" will give back true, without |
389 gives back false *) |
401 gives back false *) |
390 val options_syntax = |
402 val options_syntax = |
391 (Args.parens (Args.$$$ "asm") >> (K true)) || |
403 (Args.parens (Args.$$$ "asm") >> (K true)) || |
392 (Scan.succeed false); |
404 (Scan.succeed false); |
|
405 |
393 val ith_syntax = |
406 val ith_syntax = |
394 (Args.parens ((Args.$$$ "occ") |-- Args.nat)) |
407 (Args.parens (Scan.repeat Args.nat)) |
395 || (Scan.succeed 0); |
408 || (Scan.succeed [0]); |
396 |
409 |
397 (* method syntax, first take options, then theorems *) |
410 (* method syntax, first take options, then theorems *) |
398 fun meth_syntax meth src ctxt = |
411 fun meth_syntax meth src ctxt = |
399 meth (snd (Method.syntax ((Scan.lift options_syntax) |
412 meth (snd (Method.syntax ((Scan.lift options_syntax) |
400 -- (Scan.lift ith_syntax) |
413 -- (Scan.lift ith_syntax) |