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



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



On 12.10.20 23:27, Peter Gammie wrote:
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







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.