Re: [isabelle] metis method and +-combinator



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.