Email Gateway (Oct 12 2020 at 21:27): 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
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
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: Jan 04 2025 at 20:18 UTC