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

[Alexander Krauss]

Hi Lars,

You are mis-reading the schematic goal below:

>> lemma
>> "ALL (x::nat). x = y ==> False"
>> apply (erule allE)
> 
> After this step, the subgoal "?x = y ==> False" remains, which cannot be 
> proven. Else, we could prove:
> 
> schematic_lemma foo: "?x = y ==> False"
>   sorry
> 
> lemma "False" by (auto intro: foo[of 1 1, simplified])

Schematic vars in a goal state are "morally existentially quantified": 
they can be instantiated during the proof, that is, it is sufficient to 
prove any instance. Thus, the subgoal is provable, e.g. by substituting 
"Suc y" for x.

When you sorry the schematic lemma, then your sorry doesn't instantiate 
the ?x. In the result, the ?x is morally universally quantified. This 
shows that in schematic lemma statements, unlike normal ones, the proof 
matters.

To the original question: My experience is that auto is unsafe in a few 
corner cases, but that this does not happen too often. It seems 
eliminating equations where one variable does not occur in the rest of 
the goal is "often safe", but not always, and in the presence of 
locales, these situations tend to occur more often. Probably this should 
be rethought at some point (which involves fixing many proofs, if auto 
should be changed).

Alex