Stream: Beginner Questions

Topic: Use of Not in definition

Philipp Theyssen (Sep 29 2022 at 09:39):

Hi, I am currently confused why the definition of is_zero is not valid, I get
an Inner syntax error, it seems like I am not allowed to use ¬ in that
way but why?

fun not_zero :: "nat ⇒ bool" where
  "not_zero 0 = False"
| "not_zero n = True"

definition is_zero :: "nat ⇒ bool" where
"is_zero n = ¬(not_zero n)"

Mathias Fleury (Sep 29 2022 at 09:44):

Isabelle has a global issue with the priority of bindings, but that will never get fixed

Mathias Fleury (Sep 29 2022 at 09:45):

Here = binds too strongly.

Lukas Stevens (Sep 29 2022 at 09:45):

You can use $\longleftrightarrow$ which has weaker binding priority.

Robert Soeldner (Sep 29 2022 at 09:46):

Or ≡

Philipp Theyssen (Sep 29 2022 at 09:48):

Thanks :+1:

Manuel Eberl (Sep 29 2022 at 09:56):

Mathias Fleury said:

Isabelle has a global issue with the priority of bindings, but that will never get fixed

In most cases, you actually do want = to bind more weakly than logical connectives. It's only the Boolean = where one often wants it to bind more weakly, and that's why ⟷ exists for Boolean equality, as Lukas mentioned.

Mathias Fleury (Sep 29 2022 at 10:00):

I kind of agree, but then why does A ⟶ ∃x. P x not parse either? (⟶ exists only for bools)

Mathias Fleury (Sep 29 2022 at 10:01):

(I am just mentioning it because I wrote about a "global issue")

Last updated: Apr 19 2024 at 08:19 UTC