Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Meta-implication as part of a goal

Email Gateway (Apr 22 2024 at 22:26):

From: Roland Lutz <rlutz@hedmen.org>
Hi,

is there a way to apply a rule of the form

A ⟹ B ⟹ C ⟹ D

to a goal of the form

C ⟹ D

to obtain new goals A and B?

"rule" treats D as the goal and C as a premise. "erule" tries to match A
against C and fails (but could work if there is a way to rotate the
premises in the rule, or to specify a different premise to match).

Ideally, what I would be looking for is a way to state that C is to be
considered part of the goal.

Roland

Email Gateway (Apr 22 2024 at 22:37):

From: Jan van Brügge <jan@vanbruegge.de>
You can rotate the premises.

If your rule is called foo, then foo[rotated -1] is C => A => B => D which fits with erule.

Apr 22, 2024 11:26:08 PM Roland Lutz <rlutz@hedmen.org>:

Email Gateway (Apr 23 2024 at 21:27):

From: Roland Lutz <rlutz@hedmen.org>
This works well. Thank you!

Last updated: Jan 04 2025 at 20:18 UTC