[isabelle-dev] Referring to unfolded chained facts

[Makarius]

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).
>
> Hence:
>
> 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 
HOL-Import.)

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.


 	Makarius