Email Gateway (Aug 18 2022 at 12:25): Email Gateway (Aug 18 2022 at 12:25):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I cannot figure out how to write
apply (subst theorem)
in the form:
apply (tactic {* ... *})
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
Email Gateway (Aug 18 2022 at 12:25):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Peter Lammich <peter.lammich@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] [@{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] [@{thm eq_commute}] 1 *})
Hope this helps.
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
Last updated: May 03 2024 at 04:19 UTC