Stream: Beginner Questions

Topic: ✔ Disable unfolding of let expressions


view this post on Zulip Ujkan Sulejmani (Nov 08 2021 at 16:57):

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?

view this post on Zulip Lukas Stevens (Nov 08 2021 at 18:00):

Use define instead

view this post on Zulip Manuel Eberl (Nov 09 2021 at 08:16):

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. …)"

view this post on Zulip Mathias Fleury (Nov 09 2021 at 08:22):

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

view this post on Zulip Manuel Eberl (Nov 09 2021 at 08:23):

I keep forgetting this even exists.

view this post on Zulip Wenda Li (Nov 09 2021 at 10:05):

Manuel Eberl said:

I keep forgetting this even exists.

Me too...

view this post on Zulip Notification Bot (Nov 09 2021 at 20:51):

Ujkan Sulejmani has marked this topic as resolved.


Last updated: Aug 13 2022 at 05:18 UTC