Re: [isabelle] Unfolding constant defintiions
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)"
note zot_def [where a="x" and b="y" and c="z"]
which should have the same effect. Hope this helps.
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