Stream: Beginner Questions

Topic: Abs_filter


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (May 10 2021 at 10:21):

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

view this post on Zulip Mathias Fleury (May 10 2021 at 10:22):

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

view this post on Zulip Mathias Fleury (May 10 2021 at 10:22):

that Abs_filter F is a filter?

view this post on Zulip Robert Soeldner (May 12 2021 at 17:38):

Can someone explain the difference between notation and syntax?

view this post on Zulip 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.

view this post on Zulip Robert Soeldner (May 12 2021 at 18:01):

thanks Manuel

view this post on Zulip 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.

view this post on Zulip 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