(* Title: HOL/Library/Quotient_Type.thy Author: Markus Wenzel, TU Muenchen *) section ‹Quotient types› theory Quotient_Type imports Main begin text ‹We introduce the notion of quotient types over equivalence relations via type classes.› subsection ‹Equivalence relations and quotient types› text ‹Type class ‹equiv› models equivalence relations ‹∼ :: 'a ⇒ 'a ⇒ bool›.› class eqv = fixes eqv :: "'a ⇒ 'a ⇒ bool" (infixl "∼" 50) class equiv = eqv + assumes equiv_refl [intro]: "x ∼ x" and equiv_trans [trans]: "x ∼ y ⟹ y ∼ z ⟹ x ∼ z" and equiv_sym [sym]: "x ∼ y ⟹ y ∼ x" begin lemma equiv_not_sym [sym]: "¬ x ∼ y ⟹ ¬ y ∼ x" proof - assume "¬ x ∼ y" then show "¬ y ∼ x" by (rule contrapos_nn) (rule equiv_sym) qed lemma not_equiv_trans1 [trans]: "¬ x ∼ y ⟹ y ∼ z ⟹ ¬ x ∼ z" proof - assume "¬ x ∼ y" and "y ∼ z" show "¬ x ∼ z" proof assume "x ∼ z" also from ‹y ∼ z› have "z ∼ y" .. finally have "x ∼ y" . with ‹¬ x ∼ y› show False by contradiction qed qed lemma not_equiv_trans2 [trans]: "x ∼ y ⟹ ¬ y ∼ z ⟹ ¬ x ∼ z" proof - assume "¬ y ∼ z" then have "¬ z ∼ y" .. also assume "x ∼ y" then have "y ∼ x" .. finally have "¬ z ∼ x" . then show "¬ x ∼ z" .. qed end text ‹The quotient type ‹'a quot› consists of all \emph{equivalence classes} over elements of the base type \<^typ>‹'a›.› definition (in eqv) "quot = {{x. a ∼ x} | a. True}" typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" unfolding quot_def by blast lemma quotI [intro]: "{x. a ∼ x} ∈ quot" unfolding quot_def by blast lemma quotE [elim]: assumes "R ∈ quot" obtains a where "R = {x. a ∼ x}" using assms unfolding quot_def by blast text ‹Abstracted equivalence classes are the canonical representation of elements of a quotient type.› definition "class" :: "'a::equiv ⇒ 'a quot" ("⌊_⌋") where "⌊a⌋ = Abs_quot {x. a ∼ x}" theorem quot_exhaust: "∃a. A = ⌊a⌋" proof (cases A) fix R assume R: "A = Abs_quot R" assume "R ∈ quot" then have "∃a. R = {x. a ∼ x}" by blast with R have "∃a. A = Abs_quot {x. a ∼ x}" by blast then show ?thesis unfolding class_def . qed lemma quot_cases [cases type: quot]: obtains a where "A = ⌊a⌋" using quot_exhaust by blast subsection ‹Equality on quotients› text ‹Equality of canonical quotient elements coincides with the original relation.› theorem quot_equality [iff?]: "⌊a⌋ = ⌊b⌋ ⟷ a ∼ b" proof assume eq: "⌊a⌋ = ⌊b⌋" show "a ∼ b" proof - from eq have "{x. a ∼ x} = {x. b ∼ x}" by (simp only: class_def Abs_quot_inject quotI) moreover have "a ∼ a" .. ultimately have "a ∈ {x. b ∼ x}" by blast then have "b ∼ a" by blast then show ?thesis .. qed next assume ab: "a ∼ b" show "⌊a⌋ = ⌊b⌋" proof - have "{x. a ∼ x} = {x. b ∼ x}" proof (rule Collect_cong) fix x show "(a ∼ x) = (b ∼ x)" proof from ab have "b ∼ a" .. also assume "a ∼ x" finally show "b ∼ x" . next note ab also assume "b ∼ x" finally show "a ∼ x" . qed qed then show ?thesis by (simp only: class_def) qed qed subsection ‹Picking representing elements› definition pick :: "'a::equiv quot ⇒ 'a" where "pick A = (SOME a. A = ⌊a⌋)" theorem pick_equiv [intro]: "pick ⌊a⌋ ∼ a" proof (unfold pick_def) show "(SOME x. ⌊a⌋ = ⌊x⌋) ∼ a" proof (rule someI2) show "⌊a⌋ = ⌊a⌋" .. fix x assume "⌊a⌋ = ⌊x⌋" then have "a ∼ x" .. then show "x ∼ a" .. qed qed theorem pick_inverse [intro]: "⌊pick A⌋ = A" proof (cases A) fix a assume a: "A = ⌊a⌋" then have "pick A ∼ a" by (simp only: pick_equiv) then have "⌊pick A⌋ = ⌊a⌋" .. with a show ?thesis by simp qed text ‹The following rules support canonical function definitions on quotient types (with up to two arguments). Note that the stripped-down version without additional conditions is sufficient most of the time.› theorem quot_cond_function: assumes eq: "⋀X Y. P X Y ⟹ f X Y ≡ g (pick X) (pick Y)" and cong: "⋀x x' y y'. ⌊x⌋ = ⌊x'⌋ ⟹ ⌊y⌋ = ⌊y'⌋ ⟹ P ⌊x⌋ ⌊y⌋ ⟹ P ⌊x'⌋ ⌊y'⌋ ⟹ g x y = g x' y'" and P: "P ⌊a⌋ ⌊b⌋" shows "f ⌊a⌋ ⌊b⌋ = g a b" proof - from eq and P have "f ⌊a⌋ ⌊b⌋ = g (pick ⌊a⌋) (pick ⌊b⌋)" by (simp only:) also have "... = g a b" proof (rule cong) show "⌊pick ⌊a⌋⌋ = ⌊a⌋" .. moreover show "⌊pick ⌊b⌋⌋ = ⌊b⌋" .. moreover show "P ⌊a⌋ ⌊b⌋" by (rule P) ultimately show "P ⌊pick ⌊a⌋⌋ ⌊pick ⌊b⌋⌋" by (simp only:) qed finally show ?thesis . qed theorem quot_function: assumes "⋀X Y. f X Y ≡ g (pick X) (pick Y)" and "⋀x x' y y'. ⌊x⌋ = ⌊x'⌋ ⟹ ⌊y⌋ = ⌊y'⌋ ⟹ g x y = g x' y'" shows "f ⌊a⌋ ⌊b⌋ = g a b" using assms and TrueI by (rule quot_cond_function) theorem quot_function': "(⋀X Y. f X Y ≡ g (pick X) (pick Y)) ⟹ (⋀x x' y y'. x ∼ x' ⟹ y ∼ y' ⟹ g x y = g x' y') ⟹ f ⌊a⌋ ⌊b⌋ = g a b" by (rule quot_function) (simp_all only: quot_equality) end