[isabelle-dev] [isabelle] safe for boolean equality
matthews at galois.com
Thu Aug 5 07:33:42 CEST 2010
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:
"ALL (x::nat). x = y ==> False"
apply (erule allE)
After the first step in the proof the subgoal remains provable, but
then after the call to auto the subgoal becomes False.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2205 bytes
Desc: not available
More information about the isabelle-dev