# 3 Set theory

The very basics of set theory have already been covered. The definition of `set`

was in 2.6.1,
`undefined`

in 2.6.3, equivalence classes in 2.11.2, order in 2.12.1.2,
lattices in 2.12.2.3, Boolean algebra in 2.12.4 and some basic properties of `set`

in 2.12.5.

Here we extend these ideas to fully leverage locales.

TODO: Follow a proper set theory textbook and extend this chapter.

## 3.1 Maps

The extensional functions `S →⇩E T`

are a vital tool that allows treating
normal Isabelle functions `S → T`

as if they were sets. Many objects in
set-theory (and beyond) are functions `S →⇩E T`

with certain additional
assumptions and constraints. The ideal mechanism to express those assumptions
are locales. Therefore as the very foundation we need to turn `S →⇩E T`

into a locale

```
text ‹Maps as extensional HOL functions›
text ‹p 5, ll 21--25›
locale map =
fixes α and S and T
assumes graph [intro, simp]: "α ∈ S →⇩E T"
```

##
Some obvious properties necessary for `auto`

to work.

```
context map begin
text ‹p 5, ll 21--25›
lemma map_closed [intro, simp]:
"a ∈ S ⟹ α a ∈ T"
using graph by fast
text ‹p 5, ll 21--25›
lemma map_undefined [intro]:
"a ∉ S ⟹ α a = undefined"
using graph by fast
end (* map *)
```

Now we can extend the `map`

locale and
turn the definitions of surjective, injective and bijective functions
from 2.12.5.3 into their own locales.

```
text ‹p 7, ll 7--8›
locale surjective_map = map + assumes surjective [intro]: "α ` S = T"
text ‹p 7, ll 8--9›
locale injective_map = map + assumes injective [intro, simp]: "inj_on α S"
text ‹Enables locale reasoning about the inverse @{term "restrict (inv_into S α) T"} of @{term α}.›
text ‹p 7, ll 9--10›
locale bijective =
fixes α and S and T
assumes bijective [intro, simp]: "bij_betw α S T"
text ‹p 7, ll 9--10›
locale bijective_map = map + bijective begin
```

Every bijective map is both surjective and injective.

```
begin context bijective_map
text ‹p 7, ll 9--10›
sublocale surjective_map by unfold_locales (simp add: bij_betw_imp_surj_on)
text ‹p 7, ll 9--10›
sublocale injective_map using bij_betw_def by unfold_locales fast
end (* bijective_map *)
```

## 3.2 Equivalence classes

TODO

```
text ‹p 11, ll 6--11›
locale equivalence =
fixes S and E
assumes closed [intro, simp]: "E ⊆ S × S"
and reflexive [intro, simp]: "a ∈ S ⟹ (a, a) ∈ E"
and symmetric [sym]: "(a, b) ∈ E ⟹ (b, a) ∈ E"
and transitive [trans]: "⟦ (a, b) ∈ E; (b, c) ∈ E ⟧ ⟹ (a, c) ∈ E"
begin
text ‹p 11, ll 6--11›
lemma left_closed [intro]: (* inefficient as a simp rule *)
"(a, b) ∈ E ⟹ a ∈ S"
using closed by blast
text ‹p 11, ll 6--11›
lemma right_closed [intro]: (* inefficient as a simp rule *)
"(a, b) ∈ E ⟹ b ∈ S"
using closed by blast
end
```