[isabelle-dev] Referring to unfolded chained facts
makarius at sketis.net
Thu Sep 1 14:51:06 CEST 2011
On Thu, 1 Sep 2011, Jasmin Blanchette wrote:
> Isar generally lets users refer to unnamed local facts using the backtick notation. For example,
> lemma "hd [x] = x"
> using hd.simps[where xs = ""]
> thm `!!x. hd [x] = x`
> works fine. However, the same mechanism doesn't understand unfolding:
> definition "null xs = (xs = )"
> lemma "null xs ⟹ tl xs = xs"
> proof -
> assume "null xs"
> show "tl xs = xs"
> using `null xs`
> unfolding null_def
> thm `xs = ` -- FAILS
> This is an issue in Sledgehammer. Sledgehammer and Metis obviously honor
> "unfolding", but sometimes they need to refer to the chained facts
> explicitly (e.g., if a structured Isar proof is generated).
> 1. Is the above behavior a bug or a feature?
> 2. If it's a feature, could we provide an alternative way of referring to chained facts, e.g. an auto-bound "chained" fact list, so that "chained(1)" would retrieve "xs = " in the above example?
> 3. If it's a bug, can we fix it?
It is neither a bug or a feature, but one of the principles that make the
Isar proof language work: there is a distinction between the static proof
context and the dynamic proof state, and text elements may only refer to
things from the context, not the state. (Otherwise one would get a
variation of tactic language, such as Ltac or SSReflect, with implicit
poking in hidden goal states.)
The 'unfolding' element refers to the dynamic state, so there is no way to
refert to such hidden results later. The notation for literal facts `...`
is even more restrictive in limiting the scope to the "visible" part of
the context, i.e. things that are produced in the proof directly, not
indirectly via imports (locale context, local interpretation etc.).
Anyway, your application is not about extending the scope of `...` but to
refer to the 'using' part in a reaonable (and robust) way. (Generated
`...` is subject to the usual concrete syntax instabilities, like
If you can point me to some examples of generated Isar texts by
Sledgehammer, and also the current code to generate the `...` bits, I can
say more what could be done here.
More information about the isabelle-dev