Stream: Beginner Questions

Topic: ✔ Disable unfolding of let expressions

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?

Lukas Stevens (Nov 08 2021 at 18:00):

Use define instead

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

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

Manuel Eberl (Nov 09 2021 at 08:23):

I keep forgetting this even exists.

Wenda Li (Nov 09 2021 at 10:05):

Manuel Eberl said:

I keep forgetting this even exists.

Me too...

Notification Bot (Nov 09 2021 at 20:51):

Ujkan Sulejmani has marked this topic as resolved.

Last updated: Dec 21 2024 at 12:33 UTC