Re: [isabelle] subst translated to ML-level ?



Quoting Peter Lammich <peter.lammich at uni-muenster.de>:

Hi all,

I cannot figure out how to write
 apply (subst theorem)
in the form:
 apply (tactic {* ... *})

Hi Peter,

Here is a silly example:

lemma "(x = y) = (a = b)"
apply (subst (1 3) eq_commute)
-- New subgoal is "(y = x) = (b = a)"

Note that there are three places that the eq_commute rule could apply to this subgoal; the optional (1 3) argument to "subst" says to apply the rule to the first and third, but not the second.

You can get the same result with:
apply (tactic {* EqSubst.eqsubst_tac @{context} [1,3] [ at {thm eq_commute}] 1 *})

(The "1" at the end just says that the tactic should be applied to the first subgoal.)

If you use [0] as the occL argument, this corresponds to the default behavior of subst where the optional argument is omitted. (There is a comment in eqsubst.ML to this effect.) So the following are equivalent:

apply (subst eq_commute)
apply (tactic {* EqSubst.eqsubst_tac @{context} [0] [ at {thm eq_commute}] 1 *})

Hope this helps.

- Brian

The file Provers/eqsubst.thy seems to define this method, but it lacks
documentation in the isabelle reference manual, the chapter on
substitution there describes "stac" instead, which is not quite the
same.

Maybe my question reduces to the stupid question: What to fill in for
the parameters of "fun eqsubst_tac ctxt occL thms i th", when I want to
use it inside an:
 apply (tactic {* ... *}) ?

Regards and thanks in advance for any help,
 Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.