Theory Jacobson_Basic_Algebra.Set_Theory

(*
  Copyright (c) 2014-2019 by Clemens Ballarin
  This file is licensed under the 3-clause BSD license.
*)

theory Set_Theory imports "HOL-Library.FuncSet" begin

hide_const map
hide_const partition

no_notation divide (infixl "'/" 70)
no_notation inverse_divide (infixl "'/" 70)

text ‹
  Each statement in the formal text is annotated with the location of the originating statement
  in Jacobson's text citeJacobson1985.  Each fact that Jacobson states explicitly is marked
  as @{command theorem} unless it is translated to a @{command sublocale} declaration.
  Literal quotations from Jacobson's text are reproduced in double quotes.

  Auxiliary results needed for the formalisation that cannot be found in Jacobson's text are marked
  as @{command lemma} or are @{command interpretation}s.  Such results are annotated with the
  location of a related statement.  For example, the introduction rule of a constant is annotated
  with the location of the definition of the corresponding operation.
›


section ‹Concepts from Set Theory.  The Integers›

subsection ‹The Cartesian Product Set.  Maps›

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"

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 ‹
  Exploit existing knowledge about @{term bij_betw} rather than extending @{locale surjective_map}
  and @{locale injective_map}.
›
text ‹p 7, ll 9--10›
locale bijective_map = map + bijective 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
  by unfold_locales (simp add: inv_into_into surjective)

text ‹p 9, ll 12--13›
sublocale inverse: bijective "restrict (inv_into S α) T" T S
  by unfold_locales (simp add: bij_betw_inv_into surjective)

end (* bijective_map *)

text ‹p 8, ll 14--15›
abbreviation "identity S  (λx  S. x)"

context map begin

text ‹p 8, ll 18--20; p 9, ll 1--8›
theorem bij_betw_iff_has_inverse:
  "bij_betw α S T  (β  T E S. compose S β α = identity S  compose T α β = identity T)"
    (is "_  (β  T E S. ?INV β)")
proof
  let ?inv = "restrict (inv_into S α) T"
  assume "bij_betw α S T"
  then have "?INV ?inv" and "?inv  T E S"
    by (simp_all add: compose_inv_into_id bij_betw_imp_surj_on compose_id_inv_into bij_betw_imp_funcset bij_betw_inv_into)
  then show "β  T E S. ?INV β" ..
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 PiE_restrict compose_eq graph restrict_PiE restrict_apply)
  then show "bij_betw α S T" by (rule bij_betwI) 
qed

end (* map *)


subsection ‹Equivalence Relations.  Factoring a Map Through an Equivalence Relation›

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 (* equivalence *)

text ‹p 11, ll 16--20›
locale partition =
  fixes S and P
  assumes subset: "P  Pow S"
    and non_vacuous: "{}  P"
    and complete: "P = S"
    and disjoint: " A  P; B  P; A  B   A  B = {}"

context equivalence begin

text ‹p 11, ll 24--26›
definition "Class = (λa  S. {b  S. (b, a)  E})"

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"
  unfolding Class_def by (simp add: left_closed 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"
  unfolding Class_def by simp

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]:
  "(aS. 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 not_disjoint: "Class a  Class b  {}"
  assumes closed: "a  S" "b  S"
  shows "Class a = Class b"
proof -
  from not_disjoint and closed obtain c where witness: "c  Class a  Class b" by fast
  with closed have "(a, c)  E" by (blast intro: symmetric)
  also from witness and closed have "(c, b)  E" by fast
  finally show ?thesis by (rule Class_eq)
qed

text ‹p 12, ll 7--8›
definition "Partition = Class ` S"

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 S Partition"
proof
  fix A and B
  assume closed: "A  Partition" "B  Partition"
  then obtain a and b where eq: "A = Class a" "B = Class b" and ab: "a  S" "b  S"
  unfolding Partition_def by auto
  assume distinct: "A  B"
  then show "A  B = {}"
  proof (rule contrapos_np)
    assume not_disjoint: "A  B  {}"
    then show "A = B" by (simp add: eq) (metis not_disjoint_implies_equal ab)
  qed
qed (auto simp: Partition_def)

end (* equivalence *)

context partition begin

text ‹p 12, ll 9--10›
theorem block_exists:
  "a  S  A. a  A  A  P"
  using complete by blast

text ‹p 12, ll 9--10›
theorem block_unique:
  " a  A; A  P; a  B; B  P   A = B"
  using disjoint by blast

text ‹p 12, ll 9--10›
lemma block_closed [intro]: (* inefficient as a simp rule *)
  " a  A; A  P   a  S"
  using complete by blast

text ‹p 12, ll 9--10›
lemma element_exists:
  "A  P  a  S. a  A"
  by (metis non_vacuous block_closed all_not_in_conv)

text ‹p 12, ll 9--10›
definition "Block = (λa  S. THE A. a  A  A  P)"

text ‹p 12, ll 9--10›
lemma Block_closed [intro, simp]:
  assumes [intro]: "a  S" shows "Block a  P"
proof -
  obtain A where "a  A" "A  P" using block_exists by blast
  then show ?thesis
    apply (auto simp: Block_def)
    apply (rule theI2)
      apply (auto dest: block_unique)
    done
qed
  
text ‹p 12, ll 9--10›
lemma Block_undefined [intro, simp]:
  "a  S  Block a = undefined"
  unfolding Block_def by simp

text ‹p 12, ll 9--10›
lemma Block_self:
  " a  A; A  P   Block a = A"
  apply (simp add: Block_def block_closed)
  apply (rule the_equality)
   apply (auto dest: block_unique)
  done

text ‹p 12, ll 10--11›
definition "Equivalence = {(a, b) . A  P. a  A  b  A}"

text ‹p 12, ll 11--12›
theorem equivalence: "equivalence S Equivalence"
proof
  show "Equivalence  S × S" unfolding Equivalence_def using subset by auto
next
  fix a
  assume "a  S"
  then show "(a, a)  Equivalence" unfolding Equivalence_def using complete by auto
next
  fix a and b
  assume "(a, b)  Equivalence"
  then show "(b, a)  Equivalence" unfolding Equivalence_def by auto
next
  fix a and b and c
  assume "(a, b)  Equivalence" "(b, c)  Equivalence"
  then show "(a, c)  Equivalence" unfolding Equivalence_def using disjoint by auto
qed

text ‹Temporarily introduce equivalence associated to partition.›
text ‹p 12, ll 12--14›
interpretation equivalence S Equivalence by (rule equivalence)

text ‹p 12, ll 12--14›
theorem Class_is_Block:
  assumes "a  S" shows "Class a = Block a"
proof -
  from a  S and block_exists obtain A where block: "a  A  A  P" by blast
  show ?thesis
    apply (simp add: Block_def Class_def)
    apply (rule theI2)
      apply (rule block)
     apply (metis block block_unique)
    apply (auto dest: block_unique simp: Equivalence_def)
    done
qed

text ‹p 12, l 14›
lemma Class_equals_Block:
  "Class = Block"
proof
  fix x show "Class x = Block x"
  by (cases "x  S") (auto simp: Class_is_Block)
qed

text ‹p 12, l 14›
theorem partition_of_equivalence:
  "Partition = P"
  by (auto simp add: Partition_def Class_equals_Block image_iff) (metis Block_self element_exists)

end (* partition *)

context equivalence begin

text ‹p 12, ll 14--17›
interpretation partition S Partition by (rule partition)

text ‹p 12, ll 14--17›
theorem equivalence_of_partition:
  "Equivalence = E"
  unfolding Equivalence_def unfolding Partition_def by auto (metis ClassD Class_closed Class_eq)

end (* equivalence *)

text ‹p 12, l 14›
sublocale partition  equivalence S Equivalence
  rewrites "equivalence.Partition S Equivalence = P" and "equivalence.Class S Equivalence = Block"
    apply (rule equivalence)
   apply (rule partition_of_equivalence)
  apply (rule Class_equals_Block)
  done

text ‹p 12, ll 14--17›
sublocale equivalence  partition S Partition
  rewrites "partition.Equivalence Partition = E" and "partition.Block S Partition = Class"
    apply (rule partition)
   apply (rule equivalence_of_partition)
  apply (metis equivalence_of_partition partition partition.Class_equals_Block)
  done

text ‹Unfortunately only effective on input›
text ‹p 12, ll 18--20›
notation equivalence.Partition (infixl "'/" 75)

context equivalence begin

text ‹p 12, ll 18--20›
lemma representant_exists [dest]: "A  S / E  aS. a  A  A = Class a"
  by (metis Block_self element_exists)

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

end (* equivalence *)

text ‹p 12, ll 21--23›
sublocale equivalence  natural: surjective_map Class S "S / E"
  by unfold_locales force+

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 unfold_locales auto

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 "(THE b. aClass a. b = α a) = α a"
    by (rule the_equality) (auto simp: Fiber_equality [symmetric] Block_self block_closed)
  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 element_exists by auto
  have "(THE b. aA. b = α a)  T"
    apply (rule theI2)
    using a apply (auto simp: Fiber_equality [symmetric] Block_self block_closed)
    done
  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 Block_self element_exists induced_Fiber_simp)
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" by fast
    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 *)

end