Theory Quotient_Type

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