Re: [isabelle] problem with opening proof



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.