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

[Lawrence Paulson]

This sort of thing is well-known but very rare these days. I guess it could trap an unwary user. It just isn't easy to fix, given the old strategy of using assumptions, discarding them, and repeating.
Larry

On 5 Aug 2010, at 06:33, John Matthews wrote:

> 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.