Re: [isabelle] confusing metis message

A more accurate message might be "This subgoal is not a first-order consequence of the supplied lemmas". But it isn't very clear. Metis is at least complete, so finite failure means no proof exists. Suggestions for a rewording are welcome.


On 1 Apr 2008, at 16:06, Peter Sewell wrote:
Dear Isabelle,

The following true lemma causes metis to say:

*** Metis finds the theorem to be invalid

which is at least confusing to this naive user, if not a more profound
bug (confusing especially when it came up in a more complex situation,
from which this was simplified).

lemma " [|ALL e1 e2.
              e2 : es & (e1,e2):r --> e1 : es;
              e ~: es; e ~: Domain (r) & e ~: Range (r) |]
        ==> ALL e1 e2.
               e2 : es Un {e} & (e1,e2):r -->
               e1 : es Un {e}"

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.