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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
