# Theory Set_Extras

```text ‹Authors: Anthony Bordg and Lawrence Paulson›

theory Set_Extras
imports "Jacobson_Basic_Algebra.Set_Theory"

begin

text ‹Some new notation for built-in primitives›

section ‹Sets›

abbreviation complement_in_of:: "'a set ⇒ 'a set ⇒ 'a set" ("_∖_" [65,65]65)
where "A ∖ B ≡ A-B"

section ‹Functions›

abbreviation preimage:: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ 'a set" ("_ ⇧¯ _ _" [90,90,1000]90)
where "f⇧¯ X V ≡ (vimage f V) ∩ X"

lemma preimage_of_inter:
fixes f::"'a ⇒ 'b" and X::"'a set" and V::"'b set" and V'::"'b set"
shows "f⇧¯ X (V ∩ V') = (f⇧¯ X V) ∩ (f⇧¯ X V')"
by blast

lemma preimage_identity_self: "identity A ⇧¯ A B = B ∩ A"

text ‹Simplification actually replaces the RHS by the LHS›
lemma preimage_vimage_eq: "(f ⇧¯ (f -` U') U) ∩ X = f⇧¯ X (U ∩ U')"
by simp

definition inverse_map:: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ ('b ⇒ 'a)"
where "inverse_map f S T ≡ restrict (inv_into S f) T"

lemma bijective_map_preimage:
assumes "bijective_map f S T"
shows "bijective_map (inverse_map f S T) T S"
proof
show "inverse_map f S T ∈ T →⇩E S"
by (simp add: assms bij_betw_imp_funcset bij_betw_inv_into bijective.bijective bijective_map.axioms(2) inverse_map_def)
show "bij_betw (inverse_map f S T) T S"
using assms by (simp add: bij_betw_inv_into bijective_def bijective_map_def inverse_map_def)
qed

lemma inverse_map_identity [simp]:
"inverse_map (identity S) S S = identity S"
by (metis Id_compose compose_id_inv_into image_ident image_restrict_eq inv_into_funcset inverse_map_def restrict_extensional)

abbreviation composing ("_ ∘ _ ↓ _" [60,0,60]59)
where "g ∘ f ↓ D ≡ compose D g f"

lemma comp_maps:
assumes "Set_Theory.map η A B" and "Set_Theory.map θ B C"
shows "Set_Theory.map (θ ∘ η ↓ A) A C"
proof-
have "(θ ∘ η ↓ A) ∈ A →⇩E C"
using assms by (metis Int_iff PiE_def compose_def funcset_compose map.graph restrict_extensional)
thus ?thesis by (simp add: Set_Theory.map_def)
qed

lemma undefined_is_map_on_empty:
fixes f:: "'a set ⇒ 'b set"
assumes "f = (λx. undefined)"
shows "map f {} {}"
using assms by (simp add: map.intro)

lemma restrict_on_source:
assumes "map f S T"
shows "restrict f S = f"
using assms by (meson PiE_restrict map.graph)

lemma restrict_further:
assumes "map f S T" and "U ⊆ S" and "V ⊆ U"
shows "restrict (restrict f U) V = restrict f V"
using assms by (simp add: inf.absorb_iff2)

lemma map_eq:
assumes "map f S T" and "map g S T" and "⋀x. x ∈ S ⟹ f x = g x"
shows "f = g"
using assms by (metis restrict_ext restrict_on_source)

lemma image_subset_of_target:
assumes "map f S T"
shows "f ` S ⊆ T"
using assms by (meson image_subsetI map.map_closed)

end
```