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