[isabelle-dev] [isabelle] safe for boolean equality

[John Matthews]

A while back Larry made this comment:

> I have just remembered that I always advise people to use “auto” prior
> to trying sledgehammer, because it will split up the subgoal into
> manageable parts and simplify them. This is bad advice if “auto” can
> render the problem impossible to prove.

Was it ever resolved whether auto should work this way? I'd always  
assumed that "auto" was a safe tactic, provided I didn't try to spoof  
it by pretending unsafe rules were safe, etc.

I think most other Isabelle users also assume auto is safe.

In any case, here is another example where auto turns a provable  
subgoal into an unprovable one. This example doesn't require locales  
or the assumes..shows form of a lemma statement:

   lemma
     "ALL (x::nat). x = y ==> False"
   apply (erule allE)
   apply auto

After the first step in the proof the subgoal remains provable, but  
then after the call to auto the subgoal becomes False.

-john


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100804/fa79dd99/attachment.bin>