# 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.*