*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] proving a class instantiation.*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 9 Nov 2010 07:38:59 -0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.1.10.1011091455540.16473@atbroy100.informatik.tu-muenchen.de>*References*: <4CD93BE1.1080609@abo.fi> <AANLkTimoW5NDiPYez+RavGKXEHokjRHJMF35OwQfy5aV@mail.gmail.com> <alpine.LNX.1.10.1011091455540.16473@atbroy100.informatik.tu-muenchen.de>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] proving a class instantiation.***From:*Tobias Nipkow

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

**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

- Previous by Date: [isabelle] CfP TAP
- Next by Date: Re: [isabelle] proving a class instantiation.
- 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