[isabelle-dev] Referring to unfolded chained facts

[Jasmin Blanchette]

Hi Makarius,

> 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.)

Indeed.

> 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.

Here's an example. After "unfolding null_def", the user invoked Sledgehammer and asked for an Isar proof. The "proof - ... qed" block after that is generated by Sledgehammer:

    lemma "null xs ==> tl xs = xs"
    proof -
      assume nx: "null xs"
      show "tl xs = xs"
      using `null xs`
      unfolding null_def
      proof -
        have "tl xs = []" by (metis `xs = []` tl.simps(1))
        thus "tl xs = xs" by (metis `xs = []`)
      qed

Thanks for any help.

Jasmin