Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] scope of facts arising from `subgoal`


view this post on Zulip Email Gateway (Oct 12 2020 at 21:27):

From: Peter Gammie <peteg42@gmail.com>
Hi,

I’m a bit surprised that the cartouches don’t seem to know about facts arising from the subgoal construct. Here’s an example:

lemma "mono id"
apply (rule monoI)
subgoal for x y
using arg_cong[OF ‹x ≤ y›]

Using a recent (unmentionable on this mailing list) version of Isabelle, I get:

Failed to retrieve literal fact⌂:
x ≤ y

The motivation for this is that a tool I’m using wants to have such facts passed in explicitly, i.e. it wants

apply (method ‹x ≤ y›)

I think this is the right UI for it; like subst it is a precise and low-level method, and so shouldn’t pick up arbitrary hypotheses from the goal or other contexts.

Can we change the behavior of subgoal or log this behavior somewhere?

cheers,
peter

view this post on Zulip Email Gateway (Oct 13 2020 at 05:35):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Peter,

subgoal for x y only brings the universal quantifiers into the context, but it leaves
the premises in the goal state. Therefore, they're not available as facts to be referenced
from Isar. However, if you use subgoal premises prems for x y then all premises of the
goal state are assumed and you can retrieve them with cartouches. Accordingly, they
disappear from the goal state. If you still need them for your method calls to be there,
you can re-insert them with using prems as usual.

Best,
Andreas

view this post on Zulip Email Gateway (Oct 17 2020 at 22:19):

From: Peter Gammie <peteg42@gmail.com>
Thanks Andreas. I see now that it’s well documented in Sec 7.2 of the Isar reference manual. Sorry for the noise.

cheers,
peter


Last updated: Jul 15 2022 at 23:21 UTC