[isabelle] confusing metis message



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}"
apply(metis)



(Adding in apply(simp add:Domain_def add:Range_def) suffices).

Peter


ps Where should I look for good reference documentation of common
methods?  The "The Isabelle/Isar Reference Manual" doesn't mention
metis in its index, for example.





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