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"
  by (simp add: vimage_inter_cong)

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