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
  intro!: ext
- 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 method invocation.

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 "prems" confusion.


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.)


	Makarius






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