zibo yang (May 10 2021 at 10:07): 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.
Robert Soeldner (May 12 2021 at 18:01):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: Apr 24 2024 at 20:16 UTC