Re: [isabelle] Unfolding constant defintiions



Hi Mark,

You can try instantiating zot_def using the "where" attribute. Let's say the 
theorem zot_def has variables named a, b, and c thus:
zot_def: "zot ?a ?b ?c = ZOT(?a,?b,?c)"

Then zot_def [where a="x" and b="y" and c="z"] instantiates these variables to 
give "zot x y z = ZOT(x,y,z)".

In an Isar-style proof, you can replace the statement
  have "zot x y z = ZOT(x,y,z)"
with
  note zot_def [where a="x" and b="y" and c="z"]
which should have the same effect. Hope this helps.

- Brian

On Thursday 22 February 2007 14:20, Janney, Mark-P26816 wrote:
> Here's a newbie question:
>
> I frequently find that I have some constant, zot, having a fairly
> complex definition, zot_def.
>
> Then in some proof I want to say things like
>     have "zot x y z = ZOT(x,yz)"
> where ZOT(x,yz) the unfolded definition of zot with the actual
> parameters x, y, z, substituted in for the formal parameters.
>
> So far I have done the unfolding manually via cut-n-paste, which is
> tedious and error-prone.
>
> Is there any way to get Isabelle to perform the unfolding for me?
>
> Thanks - Mark Janney





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