Stream: Beginner Questions

Topic: `'a => bool` vs `'a set`

Yiming Xu (Sep 11 2024 at 08:04):

Hi, all. Here is a new comer from HOL4. In HOL4, 'a set is just by definition the same as 'a => bool, whereas I have discovered that in Isabelle there exists s file called Set.thy. I saw the declaration of the type 'a set there, means they are different. The practical difference which means something for me is that for P :: 'a -> bool, the expression `a \<in> P' (btw, how to type \<in> in Tulip?) does not type check anymore.

So may I please ask what do people conventionally use to jump between 'a -> bool and 'a set? Is there any theorem of form "P a <-> a in Collect P "?

I tried to type

find_theorems "(s a) ↔ (a ∈ Collect s)"

Isabelle complains "Inner lexical error Failed to parse term".

Asta Halkjær From (Sep 11 2024 at 10:12):

You've got CollectI and CollectD in each direction. The Isabelle complaint is because your <-> is a bit too short. It should be <-->. You can find the theorems like this:

find_theorems "(?s ?a) ⟹ (?a ∈ Collect ?s)"
find_theorems "(?a ∈ Collect ?s) ⟹ (?s ?a)"

Yiming Xu (Sep 11 2024 at 11:15):

Thanks! But may I please ask why this pattern matching search fails? Is there any strategy for finding it out?

Yiming Xu (Sep 11 2024 at 11:15):

find_theorems "(_ _) ⟷ (_ ∈ Collect _)"

find_theorems "s a ⟷ (a ∈ Collect s)"

Yiming Xu (Sep 11 2024 at 11:15):

image.png

Asta Halkjær From (Sep 11 2024 at 11:40):

For two reasons. First, there's no lemma using <-->, so that gives no match. Instead there are lemmas for each direction. My strategy was to try each direction instead. Second, when you type s instead of ?s or _, you're searching for that specific term instead of a placeholder.

Yiming Xu (Sep 11 2024 at 11:46):

I see. Many thanks! The simplifier in HOL4 likes "iff"'s because then a rewriting can be applied. I am very curious why Isabelle does not like "<-->" lemma, but that is another topic :-) .

Asta Halkjær From (Sep 11 2024 at 12:09):

I think Isabelle is very happy with <--> (more generally written =), but in this case no one has proven that specific lemma :)

John Park (Sep 11 2024 at 15:01):

You've got the order reversed. Rewriting rules go from complex terms into simpler ones.

See thm mem_Collect_eq

Yiming Xu (Sep 11 2024 at 15:55):

Oh yes! Good point! It would be the other direction. It is good to know Isabelle likes iffs! That makes sense.

Last updated: Dec 21 2024 at 16:20 UTC