Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] adding chained facts to a method


view this post on Zulip Email Gateway (Dec 03 2021 at 14:26):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear all,

this is likely a repeated question, but I cannot find what is the
current canonical way of adding chained facts into a method.
So that I can write
by my_method
instead of
by - my_method.

Thanks

Stepan

view this post on Zulip Email Gateway (Dec 03 2021 at 15:10):

From: Manuel Eberl <manuel@pruvisto.org>
I always use the SIMPLE_METHOD/SIMPLE_METHOD' combinators to turn a
tactic into a method. They take care of this.

Or are you talking about an already existing method like "rule" that you
want to wrap?

Manuel

view this post on Zulip Email Gateway (Dec 03 2021 at 18:32):

From: Makarius <makarius@sketis.net>
Maybe the "use" method is what you want, see also isar-ref manual. There is
also the dynamic fact "method_facts". Some examples are in the vicinity of
Eisbach.

The most basic applications are like this:

from a have B by (use nothing in rule r, simp)

have A
proof ...
...
qed (use a in method)

Makarius

view this post on Zulip Email Gateway (Dec 05 2021 at 21:51):

From: Martin Raška <RaskaMartin@seznam.cz>
Hi,

thanks for the answers. I would like to be more specific about Stepan's
question and write how we solved the problem.

'my_method' is defined using Eisbach by method combinators. This method
assumes that all chained facts have been moved to the premises of the goal,
since leaving theorems in chained facts would for instance lead to
repetitive insertion in the goal in sequential compositions.

This has been achieved by

using assms by - my_method

where insertion of facts to the goal is done by '-' method while removal
from chained facts is done by 'by' command after initial proof method.

Question is how to modify Eisbach definition to my_method1 which starts by
moving chained facts to the goal, so that we could write 

by my_method1

instead of

by - my_method.

We solved it by:

method my_method1 = (-, use nothing in ‹my_method›)

or more explicitly

method my_method2 = (insert method_facts, use nothing in ‹my_method›)

(Although 'use nothing in' does not remove chained facts, it hides them for
my_method.)

Martin Raška

---------- Původní e-mail ----------
Od: Makarius <makarius@sketis.net>
Komu: Stepan Holub <holub@karlin.mff.cuni.cz>, isabelle-users <cl-isabelle-
users@lists.cam.ac.uk>
Datum: 3. 12. 2021 19:42:57
Předmět: Re: [isabelle] adding chained facts to a method
"
Maybe the "use" method is what you want, see also isar-ref manual. There is
also the dynamic fact "method_facts". Some examples are in the vicinity of
Eisbach.

The most basic applications are like this:

from a have B by (use nothing in rule r, simp)

have A
proof ...
...
qed (use a in method)

Makarius

"

view this post on Zulip Email Gateway (Dec 06 2021 at 10:31):

From: Makarius <makarius@sketis.net>
On 05/12/2021 22:51, Martin Raška wrote:

'my_method' is defined using Eisbach by method combinators. This method
assumes that all chained facts have been moved to the premises of the goal,
since leaving theorems in chained facts would for instance lead to repetitive
insertion in the goal in sequential compositions.

Note that this is how the Isar proof language works: proof methods get exposed
to certain chained facts, but cannot "consume" them. Subsequent methods in the
same expression will get them as well.

We solved it by:
method my_method1 = (-, use nothing in ‹my_method›)
or more explicitly
method my_method2 = (insert method_facts, use nothing in ‹my_method›)

This looks fine. The second form looks very canonical to me.

Makarius


Last updated: Jul 15 2022 at 23:21 UTC