*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] proving a class instantiation.*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 09 Nov 2010 17:58:39 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <AANLkTimMcLoOfSwK3SkdaJVcpAZ3bdGj-aeMemeTngyR@mail.gmail.com>*References*: <4CD93BE1.1080609@abo.fi> <AANLkTimoW5NDiPYez+RavGKXEHokjRHJMF35OwQfy5aV@mail.gmail.com> <alpine.LNX.1.10.1011091455540.16473@atbroy100.informatik.tu-muenchen.de> <AANLkTimMcLoOfSwK3SkdaJVcpAZ3bdGj-aeMemeTngyR@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

There is one frequent situation where stating a goal in the wysiwyg style (i.e. with ==>) works very well, namely inductions. Tobias Brian Huffman schrieb: > On Tue, Nov 9, 2010 at 6:02 AM, Makarius <makarius at sketis.net> wrote: >> On Tue, 9 Nov 2010, Brian Huffman wrote: >>> because using 'show' with meta-implications is useful sometimes >> Can you give an example for that? I.e. where show "!!x. A x ==> B x" >> is needed as such > > I've used the show "!!x. A x ==> B x" pattern most often in class > instance or locale interpretation proofs, where I have several goals, > and maybe one or two of them have fixes or assumptions. Often I need > to prove a few facts (using have "...") that will be used in multiple > places. > > instance > proof > have lemma1: "..." > show "... first class assumption ..." > by (... lemma1 ...) > show "!!x. A x ==> ... second class assumption ..." > by (... lemma1 ...) > show "!!x. B x ==> ... third class assumption ..." > by (... lemma1 ...) > qed > > I can't use "next", since that erases all of my local facts along with > the local assumptions: > > instance > proof > have lemma1: "..." > show "... first class assumption ..." > by (... lemma1 ...) > next > fix x assume "A x" thus "... second class assumption ..." > by (... lemma1 ...) > (* error: lemma1 is no longer in scope! *) > > The only alternative that I knew about before now was to add another > level of nesting, and restate the goal again. For large locale > interpretations this is quite verbose, compared to the original > solution. (Recall that show ?thesis doesn't work for locale > interpretations!) > > instance > proof - > have lemma1: "..." > show "OFCLASS('a, foo_class)" > proof > show "... first class assumption ..." > by (... lemma1 ...) > next > fix x assume "A x" thus "... second class assumption ..." > by (... lemma1 ...) > next > fix x assume "B x" thus "... third class assumption ..." > by (... lemma1 ...) > qed > qed > >> instead of something that is equivalent to >> { fix x assume "A x" then show "B x" ... } ? > > Until now I didn't know that using 'show' inside a proof block { .. } > would even work to discharge a goal. Where is this documented? In the > Isar tutorial, proof blocks are only ever used with 'have'. > > Indeed, it seems like this would work well in the situation I > described, and it is only a bit more verbose than the show "!!x. A x > ==> B x" approach. > > Even though it seems that show "!!x. A x ==> B x" is never strictly > necessary, I think that the handling of it should be changed: It > should have exactly the same effect on the goal state as {fix x assume > "A x" thus "B x" }, which is what most users expect. The only other > design choice that makes sense to me is to have show "!!x. A x ==> B > x" cause an error message. The current behavior is just weird. > > - Brian

**References**:**[isabelle] proving a class instantiation.***From:*Viorel Preoteasa

**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

**Re: [isabelle] proving a class instantiation.***From:*Makarius

**Re: [isabelle] proving a class instantiation.***From:*Brian Huffman

- Previous by Date: Re: [isabelle] proving a class instantiation.
- Next by Date: Re: [isabelle] statespace
- Previous by Thread: Re: [isabelle] proving a class instantiation.
- Next by Thread: Re: [isabelle] proving a class instantiation.
- Cl-isabelle-users November 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