Email Gateway (Aug 18 2022 at 12:23): Email Gateway (Aug 18 2022 at 12:23):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all, I encounter the following problem with the metis-method and the
+-combinator:
lemma "a#b ~= b" "a#b ~= b" "a#b ~= b" "a#b ~= a#x#b"
apply -
apply (metis not_Cons_self)+
apply (auto)
The second apply-step will fail with the error message
*** Metis: No first-order proof with the lemmas supplied
*** At command "apply".
However, I would have expected the meaning of + to be: Apply argument
method(ical) repeatedly until it fails, at least once.
Hence "apply (metis not_Cons_self)+" should solve the first 3 subgoals.
Regards,
Peter
Email Gateway (Aug 18 2022 at 12:24):From: Makarius <makarius@sketis.net>
This is indeed slightly non-standard behaviour for a proof method. The
reason is that the internal meson tactic does not fail cleanly (by
returning an empty result sequence), but emits spurious errors.
Here is an adhoc version of the tactic that turns all ERROR exeptions
into a failed state (we do this by somewhat unusual operations on the
result sequence):
ML {*
fun my_metis_tac ctxt ths i st =
Seq.of_list (Seq.list_of (MetisTools.metis_tac ctxt ths i st)
handle ERROR _ => [])
*}
(For a production-quality version, instead of handling all kinds of errors
blindly, one would have to go through the Meson/Isabelle linkup carefully
and refrain emitting errors in certain cases.)
The above ML tactic may be turned into an Isar method like this:
method_setup my_metis = {*
Method.thms_ctxt_args (fn ths => fn ctxt =>
Method.SIMPLE_METHOD' (CHANGED_PROP o metis_tac ctxt ths))
*} "METIS"
Example:
lemma "a#b ~= b" "a#b ~= b" "a#b ~= b" "a#b ~= a#x#b"
apply (my_metis not_Cons_self)+
Now only the last goal remains.
Makarius
Email Gateway (Aug 18 2022 at 12:24):From: Peter Lammich <peter.lammich@uni-muenster.de>
Makarius wrote:
Thank you very much!
I removed an obvious typo (replacing metis_tac by my_metis_tac, as
declared in the ML-code above) and now it seems to work:
ML {*
fun my_metis_tac ctxt ths i st =
Seq.of_list (Seq.list_of (MetisTools.metis_tac ctxt ths i st)
handle ERROR _ => [])
*}
method_setup my_metis = {*
Method.thms_ctxt_args (fn ths => fn ctxt =>
Method.SIMPLE_METHOD' (CHANGED_PROP o my_metis_tac ctxt ths))
*} "METIS"
Regards,
Peter
Last updated: May 03 2024 at 08:18 UTC