[isabelle-dev] Referring to unfolded chained facts

Jasmin Blanchette jasmin.blanchette at gmail.com
Fri Sep 2 16:46:54 CEST 2011

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

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.


More information about the isabelle-dev mailing list