# Theory Quotient

Up to index of Isabelle/HOL/Library

theory Quotient
imports Main
begin

    (*  Title:      HOL/Library/Quotient.thy
        ID:         $Id: Quotient.thy,v 1.26 2004/08/18 09:10:01 nipkow Exp $
        Author:     Markus Wenzel, TU Muenchen
    *)

    header {* Quotient types *}

    theory Quotient
    imports Main
    begin

    text {*
     We introduce the notion of quotient types over equivalence relations
     via axiomatic type classes.
    *}

    subsection {* Equivalence relations and quotient types *}

    text {*
     \medskip Type class @{text equiv} models equivalence relations @{text
     "∼ :: 'a => 'a => bool"}.
    *}

    axclass eqv ⊆ type
    consts
      eqv :: "('a::eqv) => 'a => bool"    (infixl "∼" 50)

    axclass equiv ⊆ eqv
      equiv_refl [intro]: "x ∼ x"
      equiv_trans [trans]: "x ∼ y ==> y ∼ z ==> x ∼ z"
      equiv_sym [sym]: "x ∼ y ==> y ∼ x"

    lemma equiv_not_sym [sym]: "¬ (x ∼ y) ==> ¬ (y ∼ (x::'a::equiv))"
    proof -
      assume "¬ (x ∼ y)" thus "¬ (y ∼ x)"
        by (rule contrapos_nn) (rule equiv_sym)
    qed

    lemma not_equiv_trans1 [trans]: "¬ (x ∼ y) ==> y ∼ z ==> ¬ (x ∼ (z::'a::equiv))"
    proof -
      assume "¬ (x ∼ y)" and yz: "y ∼ z"
      show "¬ (x ∼ z)"
      proof
        assume "x ∼ z"
        also from yz have "z ∼ y" ..
        finally have "x ∼ y" .
        thus False by contradiction
      qed
    qed

    lemma not_equiv_trans2 [trans]: "x ∼ y ==> ¬ (y ∼ z) ==> ¬ (x ∼ (z::'a::equiv))"
    proof -
      assume "¬ (y ∼ z)" hence "¬ (z ∼ y)" ..
      also assume "x ∼ y" hence "y ∼ x" ..
      finally have "¬ (z ∼ x)" . thus "(¬ x ∼ z)" ..
    qed

    text {*
     \medskip The quotient type @{text "'a quot"} consists of all
     \emph{equivalence classes} over elements of the base type @{typ 'a}.
    *}

    typedef 'a quot = "{{x. a ∼ x} | a::'a::eqv. True}"
      by blast

    lemma quotI [intro]: "{x. a ∼ x} ∈ quot"
      by (unfold quot_def) blast

    lemma quotE [elim]: "R ∈ quot ==> (!!a. R = {x. a ∼ x} ==> C) ==> C"
      by (unfold quot_def) blast

    text {*
     \medskip Abstracted equivalence classes are the canonical
     representation of elements of a quotient type.
    *}

    constdefs
      class :: "'a::equiv => 'a quot"    ("⌊_⌋")
      "⌊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" hence "∃a. R = {x. a ∼ x}" by blast
      with R have "∃a. A = Abs_quot {x. a ∼ x}" by blast
      thus ?thesis by (unfold class_def)
    qed

    lemma quot_cases [cases type: quot]: "(!!a. A = ⌊a⌋ ==> C) ==> C"
      by (insert quot_exhaust) 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
        hence "b ∼ a" by blast
        thus ?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
        thus ?thesis by (simp only: class_def)
      qed
    qed

    subsection {* Picking representing elements *}

    constdefs
      pick :: "'a::equiv quot => 'a"
      "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⌋"
        hence "a ∼ x" .. thus "x ∼ a" ..
      qed
    qed

    theorem pick_inverse [intro]: "⌊pick A⌋ = A"
    proof (cases A)
      fix a assume a: "A = ⌊a⌋"
      hence "pick A ∼ a" by (simp only: pick_equiv)
      hence "⌊pick A⌋ = ⌊a⌋" ..
      with a show ?thesis by simp
    qed

    text {*
     \medskip 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:
      "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
        (!!x x' y y'. ⌊x⌋ = ⌊x'⌋ ==> ⌊y⌋ = ⌊y'⌋
          ==> P ⌊x⌋ ⌊y⌋ ==> P ⌊x'⌋ ⌊y'⌋ ==> g x y = g x' y') ==>
        P ⌊a⌋ ⌊b⌋ ==> f ⌊a⌋ ⌊b⌋ = g a b"
      (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
    proof -
      assume cong: "PROP ?cong"
      assume "PROP ?eq" and "P ⌊a⌋ ⌊b⌋"
      hence "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⌋" .
        ultimately show "P ⌊pick ⌊a⌋⌋ ⌊pick ⌊b⌋⌋" by (simp only:)
      qed
      finally show ?thesis .
    qed

    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"
    proof -
      case rule_context from this TrueI
      show ?thesis by (rule quot_cond_function)
    qed

    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 only: quot_equality)+

    end

### Equivalence relations and quotient types

lemma equiv_not_sym:

      ¬ x ∼ y ==> ¬ y ∼ x

lemma not_equiv_trans1:

      [| ¬ x ∼ y; y ∼ z |] ==> ¬ x ∼ z

lemma not_equiv_trans2:

      [| x ∼ y; ¬ y ∼ z |] ==> ¬ x ∼ z

lemma quotI:

      {x. a ∼ x} ∈ quot

lemma quotE:

      [| R ∈ quot; !!a. R = {x. a ∼ x} ==> C |] ==> C

theorem quot_exhaust:

      ∃a. A = ⌊a⌋

lemma quot_cases:

      (!!a. A = ⌊a⌋ ==> C) ==> C

### Equality on quotients

theorem quot_equality:

      (⌊a⌋ = ⌊b⌋) = (a ∼ b)

### Picking representing elements

theorem pick_equiv:

      pick ⌊a⌋ ∼ a

theorem pick_inverse:

      ⌊pick A⌋ = A

theorem quot_cond_function:

      [| !!X Y. P X Y ==> f X Y == g (pick X) (pick Y);
         !!x x' y y'.
            [| ⌊x⌋ = ⌊x'⌋; ⌊y⌋ = ⌊y'⌋; P ⌊x⌋ ⌊y⌋; P ⌊x'⌋ ⌊y'⌋ |] ==> g x y = g x' y';
         P ⌊a⌋ ⌊b⌋ |]
      ==> f ⌊a⌋ ⌊b⌋ = g a b

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

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