Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?



Here is a follow-up on the discussion.  Refal agreed that it is of general
interest to the list.


	Makarius

---------- Forwarded message ----------
Date: Tue, 9 Feb 2010 13:38:47 +0100 (CET)
From: Makarius <makarius at sketis.net>
To: Rafal Kolanski <rafalk at cse.unsw.edu.au>
Subject: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?

On Tue, 9 Feb 2010, Rafal Kolanski wrote:

now the system says:

proof (prove): step 14

using this: (everything that came out of the Cons x xs)

goal: (IH &&& in')

so I thought I already explicitly stated which prems I want in the proof. Somehow auto can deal with this without any problems, but simp and blast will not.

OK so far, but note your simultaneous goal (&&&), which is the main reason for this mystery (see below).


What is more, I can't say:
       by (simp add: prems)
     or
       by (force intro: prems)

Here the evil "prems" refers again to that global list of physical premises that happen to be around in the context. The notion of premises within an old-style goal is different from this -- it simulates the effect of having local facts within a tactical proof. (Back to field 1 of the game.)


as that will not solve the pending goal. These, though, will:
       by auto
       by - assumption
       by - simp
       by - blast
So auto is somehow special. However, simp and blast don't do this, thought they used to, because that feature is deprecated. What's the reasoning behind this? How come auto gets to chain without error or a legacy feature warning, but the other proof methods do not?

There are 3 different kinds of methods here:

  * assumption is a single-step method (like "rule", "this") and is very
    picky about the "using" part -- it will try to use these facts
    simultaneously, which practically only works for 0 or 1 such facts.

    "by - assumption" should hardly ever be useful in a proof; the
    implicit ending of 'by' already includes "assumption" for all
    remaining subgoals.

  * auto: "simple method" that addresses multiple goals.  This means the
    using part is first inserted into all subgoals and the internal
    auto_tac operates on all of that.

  * simp/blast: "simple method" that addresses the first goal.  The using
    part is only inserted into the single subgoal where the internal
    tactic operates.

Since you have multiple subgoals initially, plain "simp" and "blast" only ever operate on the first one. (There is some chance that the old-style implicit use of prems happened to solve the second one without further notice -- Now call this "intuitive".)

BTW, the "-" method inserts used facts into all goals as well, which is the reason why the "by - method" form sometimes does a bit more than "by method". (I do not recommend to use "-" in this form, though.)


I reckon the following will work in your case:

  by simp_all  -- "solve all goals uniformly (last to first)"
  by blast+    -- "solve all goals iteratively (first to last)"

In general simp+ will *not* work as expected, because simp does not need to solve the subgoal it is applied to; blast/fast/force are all the same in solve-or-fail behaviour, so plain iteration does the job. (This is the deeper reason why there is "simp_all" but no "blast_all" etc.)

The "auto" method is always in this "all" mode, but the [] method combinator explained in the isar-ref manual allows to restrict its effect on a selection of subgoals as well.


	Makarius





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