Email Gateway (Aug 18 2022 at 10:15): Email Gateway (Aug 18 2022 at 10:15):From: "Janney, Mark-P26816" <Mark.Janney@gdc4s.com>
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
Email Gateway (Aug 18 2022 at 10:15):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Last updated: Nov 21 2024 at 12:39 UTC