Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Discrepancy between "by (metis XXX ...)" and "...


view this post on Zulip Email Gateway (May 26 2022 at 12:53):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I ran into a situation in which Sledgehammer suggested:

by (metis XXX ...)

but that looped. However, if I instead try

using XXX ... by metis

it succeeds.

Is there supposed to be any difference between what can be done with "by (metis XXX ...)"
versus "using XXX ... by metis"? It seems, at least, that Sledgehammer is failing here due
to the difference between these two cases.

It is always difficult to extract an example of a failure like this from a large theory text,
but for the above example, I might be able to do it if that would be helpful to someone.

On a related note, I have encountered some other situations in which Sledgehammer suggests
"by (metis XXX ...)", which does not work, but "by (metis (no_types) XXX ...)" does work.
Here I would not expect these commands to be equivalent, but this kind of discrepancy seems
to be a common failure mode of the suggestions made by Sledgehammer. I don't currently
have any examples of this that I can extract, though.


Last updated: Jul 15 2022 at 23:21 UTC