Re: [isabelle] Difference between "apply(auto)" and "apply(force)"



The intention of auto is to do all possible obvious steps to all goals, and return whatever is left over. And auto is supposed to return fairly quickly.

The intention of force is to throw everything at the first goal, and never give up until it is proved.

Larry Paulson


On 2 May 2012, at 01:04, Ridgway, John V. E. wrote:

> This seems like a really simple question, but I can't find an answer in the documentation anywhere.  Maybe I'm just looking in the wrong places.  If so, can somebody give me a pointer?
> 
> I am working on a proof, of a fairly complex lemma, and at one point I enter
> 
> apply(auto)
> 
> Isabelle then thinks for a while and gives me back a list of the remaining goals.  I then enter
> 
> apply(force)
> 
> and the first of the remaining goals is discharged.  I was under the impression (apparently incorrect) that apply(auto) was essentially the same as apply(force) except that it was applied to all goals.  Is this wrong?  Furthermore, at another place in the proof, when I try apply(auto) it ends me up with a goal of False, whereas when I try apply(force)+ I don't have the patience to wait for it to finish...






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