On Thu, 1 Sep 2011, Alexander Krauss wrote:
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
Hi Alex,
It works for me (tested with Isabelle2011) when I replace null with
List.null (There is a hide_const (open) in List.thy). Otherwise the
unfolding doesn't actually unfold anything :-)
You're right, it works, also with the latest Isabelle. I don't know what I
tested this morning,
Hi Makarius,
I have also thought again about 'unfolding' as such: it might actually
qualify as preserving textual structure and thus as something that can be
included in the textual scope for `...` -- assuming it will someday really
cease to perform arbitrary simplification by accident.
On Fri, 2 Sep 2011, Jasmin Blanchette wrote:
We should develop some feeling in which direction to move for the
source generation business. Anyway, is this mission critical for the
upcoming release?
No, not at all. It's not mission critical for any release. I've noticed
the problem when
Hi all,
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 =
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
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`
