Theory Jacobson_Basic_Algebra.Set_Theory
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 \<^cite>‹Jacobson1985›. 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
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
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
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]:
"(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
end
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]:
"(⋃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 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
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]:
"⟦ 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
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
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 ⟹ ∃a∈S. 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
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
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. ∃a∈Class 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. ∃a∈A. 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
end