*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?*From*: Makarius <makarius at sketis.net>*Date*: Tue, 9 Feb 2010 12:25:57 +0100 (CET)*In-reply-to*: <4B7009A5.7030303@cse.unsw.edu.au>*References*: <4B6F1CA6.3080906@cse.unsw.edu.au> <4B6FE929.8060809@informatik.tu-muenchen.de> <4B7009A5.7030303@cse.unsw.edu.au>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

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

Regarding "-" and fact chaining issues, it turns out that the pre-2009Isabelle 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 proofinstead, what the "sanctioned" way is.So it's not like there's bugs to report, really, just two proof methodssuddenly getting weaker, and a legacy feature I found so intuitive I forgotit was a legacy feature. I'm just curious about the "why" of it.

* 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

**References**:**[isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Rafal Kolanski

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

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

- Previous by Date: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Next by Date: [isabelle] Structured induction with custom tactics
- Previous by Thread: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Next by Thread: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list