[isabelle-dev] [isabelle] safe for boolean equality
Alexander Krauss
krauss at in.tum.de
Thu Aug 5 11:56:10 CEST 2010
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
More information about the isabelle-dev
mailing list