Email Gateway (Aug 23 2022 at 08:18): Email Gateway (Aug 23 2022 at 08:18):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Dear Isabelle users,
While using Isabelle, I often run in a situation where I have an intro rule
of the form:
lemma R_rule:
assumes A1:....
shows ....
proof<>
Then I would like to track "A1" in the local proof context after
application of the intro rule "R_rule". The usual way is to create a dummy
definition and wrap it around the "..." of "A1" and not unfolding it.
This results with a rule of the same rule with the form:
definition "my_wrap ... = ..."
lemma R_rule:
assumes A1:"my_wrap ...."
shows "...."
unfolding my_wrap_def
proof <>
The result will be each time I apply "R_rule" as an intro rule I can get
the verification condition
my_wrap ...., that indicate that this verification condition is coming
from "A1" of "R_rule".
my question is:
Is there a way to use the label "A1" automatically to do the tracking? I
mean without the need of "my_wrap"!
Anyone else is using this kind of trick a lot or it is just me who is using
this trick by ignoring that something better and automatic exist already?
Best wishes,
Yakoub
Email Gateway (Aug 23 2022 at 08:18):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
The example is simplified, I can have more automation by creating a dummy
elim rule for " my_wrap .." and applying it after R_rule, which does what I
want.
However, it is odd to create the dummy def my_wrap and the dummy elim rule
for it to have the effect.
Last updated: Nov 21 2024 at 12:39 UTC