I often use let expressions in Isar proofs to make things more readable, but Isabelle automatically unfolds these in the output, which makes reading it very cumbersome sometimes. Is it possible to disable this?
Use define instead
Syntax:
define x y where "x = foo" and "y = bar"
You get definition theorems x_def
and y_def
from this, similar to the definition
command.
For functions, you have to explicitly use lambda expressions (unlike with the definition
command):
define f where "f = (λx. …)"
I am still unsure if I prefer the λ or the for
version (the latter feels more regular in the Isar syntax):
define f where ‹f x = (x ∧ True)› for x
thm f_def (*f ?x = (?x ∧ True)*)
have ‹¬f False›
unfolding f_def by fast
I keep forgetting this even exists.
Manuel Eberl said:
I keep forgetting this even exists.
Me too...
Last updated: Jul 15 2022 at 23:21 UTC