Stream: Beginner Questions

Topic: Abs_filter

zibo yang (May 10 2021 at 10:07):

when I ctrl + click on Abs_filter :: "(('a ⇒ bool) ⇒ bool) ⇒ 'a filter" I get:

``````locale is_filter =
fixes F :: "('a ⇒ bool) ⇒ bool"
assumes True: "F (λx. True)"
assumes conj: "F (λx. P x) ⟹ F (λx. Q x) ⟹ F (λx. P x ∧ Q x)"
assumes mono: "∀x. P x ⟶ Q x ⟹ F (λx. P x) ⟹ F (λx. Q x)"

typedef 'a filter = "{F :: ('a ⇒ bool) ⇒ bool. is_filter F}"
proof
show "(λx. True) ∈ ?filter" by (auto intro: is_filter.intro)
qed
``````

I am confused about how to map F::"('a ⇒ bool) ⇒ bool" into 'a filter?

Mathias Fleury (May 10 2021 at 10:21):

Query panel > find constants > `‹(_ ⇒ bool) ⇒ _ filter›`

Mathias Fleury (May 10 2021 at 10:22):

but I am confused by your question: what don't you understand?

Mathias Fleury (May 10 2021 at 10:22):

that `Abs_filter F` is a filter?

Robert Soeldner (May 12 2021 at 17:38):

Can someone explain the difference between `notation` and `syntax`?

Manuel Eberl (May 12 2021 at 17:57):

`notation` only allows relatively simple infix/mixfix syntax for constants; `syntax` allows introducing more complex syntactic features. For more details, look at Chapter 8 of the Isabelle/Isar reference manual.

thanks Manuel

Manuel Eberl (May 12 2021 at 18:29):

I wouldn't worry too much about it though; I've been using Isabelle for 10 years and I still don't really understand `syntax` and `translation`. If there's anything concrete that you want to achieve and you can't figure it out by looking e.g. at other stuff in the library, maybe ask the concrete question here.

Manuel Eberl (May 12 2021 at 18:30):

As a regular Isabelle user, I think it's not too fruitful to invest time and effort into learning how these work

Last updated: Aug 13 2022 at 06:26 UTC