Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
On Mon, 8 Feb 2010, Rafal Kolanski wrote:
I'm attaching my explorations in the area.
Regarding more "!":
- my memory was faulty with auto, it works pretty much how it used to
- force is weaker, needs help with intro and dest more, especially
- fast is weaker, needs ! with intro: ext
First of all, we need to be careful about different roles of "!". IIRC,
your examples were all about intro! elim! etc., but at some point I've
thought it would be force! auto! etc. as a method argument. The latter is
an ancient abbreviation for something like (insert prems) just before the
There might be reasons in the main HOL setup why some extra intro! elim!
is required in your examples, but this is probably independent of the
Regarding "-" and fact chaining issues, it turns out that the pre-2009
Isabelle does warn me that this is a legacy feature:
"Legacy feature! Implicit use of prems in assumption proof"
I just don't really get why this is, and how I should be writing my proof
instead, what the "sanctioned" way is.
So it's not like there's bugs to report, really, just two proof methods
suddenly getting weaker, and a legacy feature I found so intuitive I forgot
it was a legacy feature. I'm just curious about the "why" of it.
Everything around "prems" causes lots misunderstanding, this mail thread
already proves it (and there are older threads related to the same issue).
When you see "Legacy feature! Implicit use of prems in assumption proof"
(in Isabelle2008) it means that "by auto" (or similar) has left over some
pending subgoals, but these were closed by applying some arbitrary facts
that happen to be connected to low-level assumptions for foundational
reasons. This is not really intuitive for two main reasons:
* Foundation via assimptions is an implementation detail, nothing the
user should care about. For example, assume / presume / obtain /
guess / case / def produce such prems right now, but have / show do
not. Moreover, 'assumes' in locale expressions produce prems in
certain intermediate situations, but later it changes into a predicate
that is assumed and the rest is derived. Various local theory targets
also have their own idea of introducing prems intermediately.
* Structurally, it is unclear which facts actually solve the
situation. Referring to "prems" is somehow non-local. You just need
to inspect the situations were the system emits the above "Legacy
feature! ..." message, and replace "by method" by "apply method" and
then look at the remaining goal state. Usually it will take quite
some time to figure out how the goal was actually solved, but
information this is then easily added to the 'from' or 'using' part of
the invocation. (I've done these cleanups many times, and often there
were even some errors in the proof text which facts really contribute
to the result.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and