Email Gateway (Aug 18 2022 at 17:18): Email Gateway (Aug 18 2022 at 17:18):From: Lawrence Paulson <lp15@cam.ac.uk>
The right way is to use a structured proof, where you have elements such as
def a \<equiv> "x+y+z"
and
let ?a = "x+y+z"
The former must be expanded explicitly, while the latter are mere abbreviations and expand automatically.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:28):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
In a proof I need to introduce some local names.
something like: a = x+y+z, b = a + x, ...
apply (subgoal_tac "\<exists> a b: a = x+y+z /\ b = a + x")
but this is simplified away by simp or safe.
Is there a way to achieve this goal?
Best regards,
Viorel
Last updated: Apr 26 2024 at 20:16 UTC