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
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
