[isabelle-dev] HOL-Decision_Procs FAILED

[Makarius]

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.)


 	Makarius