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