Email Gateway (Aug 18 2022 at 11:39): Email Gateway (Aug 18 2022 at 11:39):From: Lawrence Paulson <lp15@cam.ac.uk>
Metis only uses pure first order logic along with the lemmas supplied.
Larry
Email Gateway (Aug 18 2022 at 11:40):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
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.
Email Gateway (Aug 18 2022 at 11:41):From: Tobias Nipkow <nipkow@in.tum.de>
The message should be the truth when you have given metis all of HOL.
But since one tends to be a bit more selective, I agree that it is
confusing.
Tobias
Peter Sewell schrieb:
Email Gateway (Aug 18 2022 at 11:42):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
Larry
Email Gateway (Aug 18 2022 at 11:43):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
Now I'm more confused - here it seems that it failed due to not
expanding Domain and Range, and so (even given all of HOL) would
similarly fail, and announce invalidity, if the lemma involved some
other user-defined constant?
But, in any case, your remark suggests I've misunderstood what a
typical invocation would be, or what it already knows?
best,
Peter
Email Gateway (Aug 18 2022 at 11:44):From: Tobias Nipkow <nipkow@in.tum.de>
The message should be the truth when you have given metis all of HOL.
But since one tends to be a bit more selective, I agree that it is
confusing.Now I'm more confused - here it seems that it failed due to not
expanding Domain and Range, and so (even given all of HOL) would
similarly fail,
My "all of HOL" was meant to include all your definitions.
But, in any case, your remark suggests I've misunderstood what a
typical invocation would be, or what it already knows?
Metis knows first-order logic. Everything else you have to tell it. In
contrast to blast. Hence metis is primarily useful in connection with
sledgehammer, which figures out the required lemmas for you.
Tobias
Last updated: May 03 2024 at 12:27 UTC