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

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

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: Sep 25 2021 at 09:17 UTC