Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Resolution with non-atomic conclusion

Email Gateway (Aug 22 2022 at 20:39):

From: Joshua Chen <josh@joshchen.io>
Dear all,

I have a situation where I need to perform resolution over a goal state
of the form !!x. P ==> Q ==> R, but consider Q ==> R as the
conclusion and only lift my rule over P and x. More generally, I need to
do resolution, but over non-atomic conclusions.

The implementation manual describes compose_tac, which lets me choose
the number of premises I want but doesn't perform lifting. Deep-diving
into the ML leads me to Thm.bicompose_aux, which seems to have a flag
for turning lifting on. But this is private to the Thm structure, and
Thm.bicompose has no corresponding flag.

Is there any way to achieve what I want?

Thanks and best,
Josh

Email Gateway (Aug 22 2022 at 20:40):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m sorry but this combination isn’t supported.

Larry Paulson

Email Gateway (Aug 22 2022 at 20:40):

From: Makarius <makarius@sketis.net>
On 26/09/2019 22:04, Joshua Chen wrote:

I have a situation where I need to perform resolution over a goal state
of the form !!x. P ==> Q ==> R, but consider Q ==> R as the
conclusion and only lift my rule over P and x. More generally, I need to
do resolution, but over non-atomic conclusions.

The implementation manual describes compose_tac, which lets me choose
the number of premises I want but doesn't perform lifting. Deep-diving
into the ML leads me to Thm.bicompose_aux, which seems to have a flag
for turning lifting on. But this is private to the Thm structure, and
Thm.bicompose has no corresponding flag.

The "compose" family of functions is in some sense a historical
accident, not to say legacy. The "implementation" manual has this
cryptic warning at the bottom of section 4.2.4:

These low-level operations are stepping outside the structure imposed by
regular rule resolution. Used without understanding of the consequences,
they may produce results that cause problems with standard rules and
tactics
later on.

Note that the canonical way to work with subgoal structure is via
Logic.protect, Drule.protect etc.

Is there any way to achieve what I want?

Quite often, what you want is in conflict what you really need. In
such a situation it usually helps to reconsider what you are trying to
do, by re-emerging from the deep-dive and looking at the big picture
from a distance.

You did not say anything about that, so I cannot make this advice more
concrete.

Makarius

Last updated: Apr 19 2024 at 08:19 UTC