Email Gateway (Jan 25 2021 at 17:01): Email Gateway (Jan 25 2021 at 17:01):From: Makarius <makarius@sketis.net>
There is nothing wrong with it: you are 'using' the fact P three time, in
the three parts of the one proof method.
If you want something different, e.g. see the NEWS entry for Isabelle2016-1
(December 2016):
Proof method "use" allows to modify the main facts of a given method
expression, e.g.
(use facts in simp)
(use facts in ‹simp add: ...›)
Also note that the name "nothing" refers to the empty fact.
There are various possibilities to proceed.
Makarius
Email Gateway (Jan 25 2021 at 18:51):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Makarius Wenzel/All,
Please accept my apologies for the noise. The question was slightly rushed,
especially given that this behavior is not unique to subst/rewrite.
Somehow, it did not seem to be immediately apparent from the documentation
that "using" and sequential (also structural) composition would interact in
this manner:
Email Gateway (Jan 25 2021 at 19:58):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Makarius Wenzel,
Once again, I apologize for the rushed reply. I can now see that it is
possible to use "use nothing" to force individual methods to ignore the
facts provided by the proof state like so:
method abcdef' =
(unfold abcdef(1), use nothing in ‹unfold abcdef(2)›, use nothing in
‹unfold abcdef(3)›)
Is this considered to be a canonical methodology for the use of the
sequential composition of methods in Eisbach?
Kind Regards,
Mikhail Chekhov
Email Gateway (Jan 25 2021 at 20:07):From: Makarius <makarius@sketis.net>
Yes.
Makarius
Last updated: Apr 18 2024 at 20:16 UTC