[isabelle-dev] [isabelle] safe for boolean equality
lp15 at cam.ac.uk
Thu Aug 5 15:22:42 CEST 2010
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.
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:
> "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.
More information about the isabelle-dev