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.
---------- 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
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)
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 - 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
* 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and