[isabelle-dev] Referring to unfolded chained facts

[Jasmin Blanchette]

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, but it was wrong. Regarding "null", I had forgotten to include this definition in my email:

    definition "null xs = (xs = [])"

I wasn't aware of "List.null".

Now, the only other conceptual issue I have to lift is the communication between Sledgehammer and its own minimizer, which goes through Isar for technical reasons. E.g. if you add the lines

    using [[sledgehammer_auto_min_max_time = 0]]
    sledgehammer

right after the "unfolding null_def", you'll get this suggestion:

    To minimize: sledgehammer min (tl.simps(1) `xs = []`).

Sledgehammer likes to track precisely which chained fact took part in the proof (to reduce the search space and because it's somewhat tricky to obtain the name of a chained 'thm'). But since these commands are only transient, it's probably acceptable if I catch the exception when resolving `...` and look it up myself in the chained facts.

Thanks for your help. I don't promise a speedy implementation of these ideas, but when the time will come to attack these issues I'll know how to proceed.

Jasmin