Theory Set_Theory

(*
  Derived from the AFP entry Jacobson_Basic_Algebra, by Clemens Ballarin
*)

theory Set_Theory 
  imports "HOL-Library.FuncSet" "HOL-Library.Disjoint_Sets"

begin

no_notation divide (infixl ‹'/› 70)
no_notation inverse_divide (infixl ‹'/› 70)
no_notation quotient (infixl ‹'/'/› 90)

abbreviation "identity S ≡ (λx ∈ S. x)"

theorem bij_betw_iff_has_inverse:
  assumes "α ∈ S →⇩E T"
  shows "bij_betw α S T ⟷ (∃β ∈ T →⇩E S. compose S β α = identity S ∧ compose T α β = identity T)"
    (is "_ ⟷ (∃β ∈ T →⇩E S. ?INV β)")
proof
  assume "bij_betw α S T"
  then have "?INV (restrict (inv_into S α) T)" 
    by (simp add: bij_betw_imp_surj_on compose_id_inv_into compose_inv_into_id)
  then show "∃β ∈ T →⇩E S. ?INV β"
    by (metis ‹bij_betw α S T› bij_betw_imp_surj_on inv_into_funcset restrict_PiE
        restrict_Pi_cancel) 
next
  assume "∃β ∈ T →⇩E S. ?INV β"
  then obtain β where "α ∈ S → T" "β ∈ T → S" "⋀x. x ∈ S ⟹ β (α x) = x" "⋀y. y ∈ T ⟹ α (β y) = y"
    by (metis Int_iff PiE_def assms compose_eq restrict_apply')
  then show "bij_betw α S T" by (rule bij_betwI) 
qed

subsection ‹Compatibility with Ballarin's original development›

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"
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 *)

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"

locale bijective_map = map + 
  assumes bijective [intro, simp]: "bij_betw α S T"

begin

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

text ‹p 9, ll 12--13›
sublocale inverse: map "restrict (inv_into S α) T" T S
proof qed (simp add: inv_into_into surjective)

text ‹p 9, ll 12--13›
lemma bij_betw_inverse: "bij_betw (restrict (inv_into S α) T) T S"
  by (simp add: bij_betw_inv_into)

end (* bijective_map *)


locale Equivalence =
  fixes S and E
  assumes eqv: "equiv S E"
begin

lemma closed [intro, simp]: "E ⊆ S × S"
  by (simp add: equiv_type eqv)

lemma reflexive [intro, simp]: "a ∈ S ⟹ (a, a) ∈ E"
  by (metis eq_equiv_class_iff2 eqv)

lemma symmetric [sym]: "(a, b) ∈ E ⟹ (b, a) ∈ E"
  by (meson equivE eqv symD)

lemma transitive [trans]: "⟦ (a, b) ∈ E; (b, c) ∈ E ⟧ ⟹ (a, c) ∈ E"
  by (meson equiv_def eqv transE)

lemma left_closed [intro]: 
  "(a, b) ∈ E ⟹ a ∈ S"
  using closed by blast
  
text ‹p 11, ll 6--11›
lemma right_closed [intro]: 
  "(a, b) ∈ E ⟹ b ∈ S"
  using closed by blast

text ‹Equivalence classes›
definition "Class ≡ (λa ∈ S. E``{a})"

text ‹p 11, ll 24--26›
lemma Class_closed [dest]:
  "⟦ a ∈ Class b; b ∈ S ⟧ ⟹ a ∈ S"
  unfolding Class_def by auto

text ‹p 11, ll 24--26›
lemma Class_closed2 [intro, simp]:
  "a ∈ S ⟹ Class a ⊆ S"
  unfolding Class_def by auto

text ‹p 11, ll 24--26›
lemma Class_undefined [intro, simp]:
  "a ∉ S ⟹ Class a = undefined"
  unfolding Class_def by simp

text ‹p 11, ll 24--26›
lemma ClassI [intro, simp]:
  "(a, b) ∈ E ⟹ a ∈ Class b"
  by (simp add: Class_def local.symmetric right_closed)
  
text ‹p 11, ll 24--26›
lemma Class_revI [intro, simp]:
  "(a, b) ∈ E ⟹ b ∈ Class a"
  by (blast intro: symmetric)

text ‹p 11, ll 24--26›
lemma ClassD [dest]:
  "⟦ b ∈ Class a; a ∈ S ⟧ ⟹ (b, a) ∈ E"
  by (simp add: Class_def local.symmetric)

text ‹p 11, ll 30--31›
theorem Class_self [intro, simp]:
  "a ∈ S ⟹ a ∈ Class a"
  unfolding Class_def by simp

text ‹p 11, l 31; p 12, l 1›
theorem Class_Union [simp]:
  "(⋃a∈S. Class a) = S"
  by blast

text ‹p 11, ll 2--3›
theorem Class_subset:
  "(a, b) ∈ E ⟹ Class a ⊆ Class b"
proof
  fix a and b and c
  assume "(a, b) ∈ E" and "c ∈ Class a"
  then have "(c, a) ∈ E" by auto
  also note ‹(a, b) ∈ E›
  finally have "(c, b) ∈ E" by simp
  then show "c ∈ Class b" by auto
qed

text ‹p 11, ll 3--4›
theorem Class_eq:
  "(a, b) ∈ E ⟹ Class a = Class b"
  by (auto intro!: Class_subset intro: symmetric)

text ‹p 12, ll 1--5›
theorem Class_equivalence:
  "⟦ a ∈ S; b ∈ S ⟧ ⟹ Class a = Class b ⟷ (a, b) ∈ E"
proof
  fix a and b
  assume "a ∈ S" "b ∈ S" "Class a = Class b"
  then have "a ∈ Class a" by auto
  also note ‹Class a = Class b›
  finally show "(a, b) ∈ E" by (fast intro: ‹b ∈ S›)
qed (rule Class_eq)

text ‹p 12, ll 5--7›
theorem not_disjoint_implies_equal:
  assumes "Class a ∩ Class b ≠ {}"
  assumes "a ∈ S" "b ∈ S"
  shows "Class a = Class b"
  by (metis ClassD Class_eq assms disjoint_iff_not_equal)

definition "Partition = Class ` S"
notation Equivalence.Partition (infixl ‹'/› 75)

text ‹p 12, ll 7--8›
lemma Class_in_Partition [intro, simp]:
  "a ∈ S ⟹ Class a ∈ Partition"
  unfolding Partition_def by fast

text ‹p 12, ll 7--8›
theorem partition:
  "partition_on S Partition"
proof (intro partition_onI)
  fix p q
  assume "p ∈ Partition" "q ∈ Partition" "p ≠ q"
  with not_disjoint_implies_equal show "disjnt p q"
    by (auto simp: Partition_def disjnt_iff)
qed (force simp add: Partition_def)+

end


context Equivalence
begin

text ‹p 12, ll 18--20›
lemma representant_exists: "A ∈ S / E ⟹ ∃a∈S. a ∈ A ∧ A = Class a"
  using Class_self Partition_def image_iff by auto

text ‹p 12, ll 18--20›
lemma quotient_ClassE: "A ∈ S / E ⟹ (⋀a. a ∈ S ⟹ P (Class a)) ⟹ P A"
  using representant_exists by auto

end (* equivalence *)

lemma equivalenceI:
  assumes closed: "E ⊆ S × S"
    and reflexive: "⋀a. a ∈ S ⟹ (a, a) ∈ E"
    and symmetric: "⋀a b. (a, b) ∈ E ⟹ (b, a) ∈ E"
    and transitive: "⋀a b c. ⟦ (a, b) ∈ E; (b, c) ∈ E ⟧ ⟹ (a, c) ∈ E"
  shows "Equivalence S E"
  using assms Equivalence_def equiv_def refl_on_def sym_def trans_def
  by metis


text ‹p 12, ll 21--23›
sublocale Equivalence ⊆ natural: surjective_map Class S "S / E"
proof qed (auto simp: Partition_def)

text ‹Technical device to achieve Jacobson's syntax; context where @{text α} is not a parameter.›
text ‹p 12, ll 25--26›
locale fiber_relation_notation = fixes S :: "'a set" begin

text ‹p 12, ll 25--26›
definition Fiber_Relation (‹E'(_')›) where "Fiber_Relation α = {(x, y). x ∈ S ∧ y ∈ S ∧ α x = α y}"

end (* fiber_relation_notation *)

text ‹
  Context where classes and the induced map are defined through the fiber relation.
  This will be the case for monoid homomorphisms but not group homomorphisms.
›
text ‹Avoids infinite interpretation chain.›
text ‹p 12, ll 25--26›
locale fiber_relation = map begin

text ‹Install syntax›
text ‹p 12, ll 25--26›
sublocale fiber_relation_notation .

text ‹p 12, ll 26--27›
sublocale Equivalence where E = "E(α)"
  unfolding Fiber_Relation_def
  by (force intro: equivalenceI)

text ‹``define $\bar{\alpha}$ by $\bar{\alpha}(\bar{a}) = \alpha(a)$''›
text ‹p 13, ll 8--9›
definition "induced = (λA ∈ S / E(α). THE b. ∃a ∈ A. b = α a)"

text ‹p 13, l 10›
theorem Fiber_equality:
  "⟦ a ∈ S; b ∈ S ⟧ ⟹ Class a = Class b ⟷ α a = α b"
  unfolding Class_equivalence unfolding Fiber_Relation_def by simp

text ‹p 13, ll 8--9›
theorem induced_Fiber_simp [simp]:
  assumes [intro, simp]: "a ∈ S" 
  shows "induced (Class a) = α a"
proof -
  have "⋀b. ∃x∈Class a. b = α x ⟹ b = α a"
    by (metis ClassD Class_closed Class_eq Fiber_equality assms)
  then have "(THE b. ∃a∈Class a. b = α a) = α a"
    by blast
  then show ?thesis unfolding induced_def by simp
qed

text ‹p 13, ll 10--11›
interpretation induced: map induced "S / E(α)" T
proof (unfold_locales, rule)
  fix A
  assume [intro, simp]: "A ∈ S / E(α)"
  obtain a where a: "a ∈ S" "a ∈ A"
    using representant_exists by blast
  have "(THE b. ∃a∈A. b = α a) ∈ T"
    by (metis (no_types, lifting) ‹A ∈ Partition› induced_Fiber_simp
        induced_def map_closed representant_exists restrict_apply')
  then show "induced A ∈ T" unfolding induced_def by simp
qed (simp add: induced_def)

text ‹p 13, ll 12--13›
sublocale induced: injective_map induced "S / E(α)" T
proof
  show "inj_on induced Partition"
    unfolding inj_on_def
    by (metis Fiber_equality induced_Fiber_simp representant_exists)
qed

text ‹p 13, ll 16--19›
theorem factorization_lemma:
  "a ∈ S ⟹ compose S induced Class a = α a"
  by (simp add: compose_eq)

text ‹p 13, ll 16--19›
theorem factorization [simp]: "compose S induced Class = α"
  by (rule ext) (simp add: compose_def map_undefined)

text ‹p 14, ll 2--4›
theorem uniqueness:
  assumes map: "β ∈ S / E(α) →⇩E T"
    and factorization: "compose S β Class = α"
  shows "β = induced"
proof
  fix A
  show "β A = induced A"
  proof (cases "A ∈ S / E(α)")
    case True
    then obtain a where [simp]: "A = Class a" "a ∈ S"
      using representant_exists by auto
    then have "β (Class a) = α a" by (metis compose_eq factorization)
    also have "… = induced (Class a)" by simp
    finally show ?thesis by simp
  qed (simp add: induced_def PiE_arb [OF map])
qed

end (* fiber_relation *)

hide_const (open) map

end