*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] proving a class instantiation.*From*: Makarius <makarius at sketis.net>*Date*: Wed, 10 Nov 2010 16:54:02 +0100 (CET)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*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*: Alpine 1.10 (LNX 962 2008-03-14)

On Tue, 9 Nov 2010, Brian Huffman wrote:

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 sometimesCan you give an example for that? I.e. where show "!!x. A x ==> B x" is needed as suchI'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!)

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 theIsar 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 strictlynecessary, I think that the handling of it should be changed: It shouldhave 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 designchoice that makes sense to me is to have show "!!x. A x ==> B x" causean error message. The current behavior is just weird.

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

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

- Previous by Date: Re: [isabelle] statespace
- 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