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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
