[isabelle-dev] HOL-Decision_Procs FAILED
makarius at sketis.net
Wed Mar 19 16:47:44 CET 2014
On Wed, 19 Mar 2014, Gerwin Klein wrote:
> On 18 Mar 2014, at 10:23 pm, Makarius <makarius at sketis.net> wrote:
>> Maybe I should try to improve the implicit "rule" method to reveal the rule that was applied --- via a form of semantic completion. It is a bit more difficult than the other completions so far, because there is also the lazy enumeration of rules and rule instantiations involved.
> I think beginners would like that, although it does sound like potential
> for a fairly deep rabbit hole.
Just for informative purposes it might be not so difficult to turn the
existing Method.rule_trace facility into something that is PIDE compliant
-- also with some filtering of successful rules instead of all candidates.
What is more difficult is to produce text (fact names) that can be
understood by the system again in a robust manner. But I am not quite
up-to-date what the Sledgehammer + Isar output can do already, it might
actually solve that problem.
We have a similar situation with Simplifier trace: the system prints funny
"name hints" (often just "??.unknown"), without clear reference to the
fact name space.
I already know a simple trick to make this into authentic entity
references (with hyperlinks in the output), without requiring proper fact
names (simp rules do not have a name in general.)
More information about the isabelle-dev