Re: [isabelle] Search in Isabelle



On Mar 25 at 14:10 +0300, grechukbogdan wrote:
> Suggestion 1. The message like  “The current goal could be solved
> directly with...” should appear not only after I formulate the
> existing result as a lemma, but also when I formulate it inside the
> proof, say after have. Ideally, something like this should work when
> the existing result appears as a subgoal in the proof, etc. 
> 
> The first part of this (about “have”) I have suggested during my
> first visit in June, and the reply was “good point. We will think
> about it”. This is very important because it will help to avoid
> duplicate job. Is it hard for realization?
> 
> Unfortunately, this mechanism is very sensitive for reformulations.
> For example, there exist a lemma “id x = x”, but I have no
> suggestions for lemma “x = id x”. In this and many similar cases
> Sledgehammer can help, but the same question arises: is it possible
> to run it in the background automatically, every time when I
> formulate a lemma or “have” statement? 

Manually running:
    find_theorems solves
or
    C-c C-f solves

should have the desired effect.

You could also make a more specific key binding if you need this
often.

Tim.

Attachment: signature.asc
Description: Digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.