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
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 pro
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 unfold
On 08/31/2011 04:21 PM, Andreas Schropp wrote:
On 08/30/2011 08:12 PM, Brian Huffman wrote:
However, the nonemptiness proof does rely on type class assumptions:
Indeed, "{A. ~ finite A}" is actually empty for any finite type 'a.
I think I get your point now: assumptions for type class constra
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
