[isabelle-dev] Referring to unfolded chained facts
jasmin.blanchette at gmail.com
Fri Sep 2 16:46:54 CEST 2011
> 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