*To*: Chris Capel <pdf23ds at gmail.com>*Subject*: Re: [isabelle] problem with opening proof*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 22 May 2009 13:01:59 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <737b61f30905212054n968f86di25c0c6e0bcb9308@mail.gmail.com>*References*: <737b61f30905212054n968f86di25c0c6e0bcb9308@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

On Thu, May 21, 2009 at 8:54 PM, Chris Capel <pdf23ds at gmail.com> wrote: > On a completely different note, it would be cool if abbreviations > could be made that are local to proofs. Often I have expressions > repeated several times throughout a goal that make it quite large, > when it would be manageable with some abbreviations. Let statements > are nice, but they're expanded in the goal display. Such a command > might not semantically differ from the let command. Hi Chris, I have often used local definitions to help manage the size of large subgoals. There are two ways to use them. First, you can use "defines" in the theorem statement: lemma foo: fixes x and y ... assumes ... defines wibble_def: "wibble == ... x ... y ..." shows "... wibble ..." Note that if the rhs of the definition mentions any free variables, they must be previously declared using "fixes". Once you finish the proof, the local definitions are unfolded, and the locally-defined constants do not appear in the resulting theorem. The other method is to use the "def" command. Note the unusual placement of the quote marks---only the rhs is quoted. lemma foo: ... proof - fix x and y def wibble == "... x .. y ..." show ... Local definitions are not abbreviations; you will still need to fold/unfold the definitions manually within the proofs. But if your subgoal terms are really big, this is an advantage: Not only do your goals look smaller, they really are smaller---which makes simplification and other proof tactics run faster. On the other hand, it would be nice to have both local definitions and local abbreviations. I'm sure that it would be possible to implement an "abbrev" command that works much like "def", but I'm just not sure how to do it. - Brian

**References**:**[isabelle] problem with opening proof***From:*Chris Capel

- Previous by Date: [isabelle] Tableaux 2009: Call for Participation
- Next by Date: Re: [isabelle] problem with opening proof
- Previous by Thread: Re: [isabelle] problem with opening proof
- Next by Thread: [isabelle] Reminder: Deadline for Special Issue of IMLA approaching (31st May 2009)
- Cl-isabelle-users May 2009 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