Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] rewrite, subst, uses and sequential compositio...


view this post on Zulip 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):

Also note that the name "nothing" refers to the empty fact.

There are various possibilities to proceed.

Makarius

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Email Gateway (Jan 25 2021 at 20:07):

From: Makarius <makarius@sketis.net>
Yes.

Makarius


Last updated: Dec 08 2021 at 08:24 UTC