(* 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 \<^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 (* 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]: "(⋃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 (* 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 ⟹ ∃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 (* 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. ∃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 (* fiber_relation *) end