Theory Quotient_Type
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