Re: [isabelle] metis method and +-combinator



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


On Mon, 15 Sep 2008, Peter Lammich wrote:

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.

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





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