src/HOL/Library/Quotient.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15131 c69542757a4d child 18372 2bffdf62fe7f permissions -rw-r--r--
import -> imports
     1 (*  Title:      HOL/Library/Quotient.thy

     2     ID:         $Id$

     3     Author:     Markus Wenzel, TU Muenchen

     4 *)

     5

     6 header {* Quotient types *}

     7

     8 theory Quotient

     9 imports Main

    10 begin

    11

    12 text {*

    13  We introduce the notion of quotient types over equivalence relations

    14  via axiomatic type classes.

    15 *}

    16

    17 subsection {* Equivalence relations and quotient types *}

    18

    19 text {*

    20  \medskip Type class @{text equiv} models equivalence relations @{text

    21  "\<sim> :: 'a => 'a => bool"}.

    22 *}

    23

    24 axclass eqv \<subseteq> type

    25 consts

    26   eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)

    27

    28 axclass equiv \<subseteq> eqv

    29   equiv_refl [intro]: "x \<sim> x"

    30   equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"

    31   equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"

    32

    33 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"

    34 proof -

    35   assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"

    36     by (rule contrapos_nn) (rule equiv_sym)

    37 qed

    38

    39 lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"

    40 proof -

    41   assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"

    42   show "\<not> (x \<sim> z)"

    43   proof

    44     assume "x \<sim> z"

    45     also from yz have "z \<sim> y" ..

    46     finally have "x \<sim> y" .

    47     thus False by contradiction

    48   qed

    49 qed

    50

    51 lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"

    52 proof -

    53   assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..

    54   also assume "x \<sim> y" hence "y \<sim> x" ..

    55   finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..

    56 qed

    57

    58 text {*

    59  \medskip The quotient type @{text "'a quot"} consists of all

    60  \emph{equivalence classes} over elements of the base type @{typ 'a}.

    61 *}

    62

    63 typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"

    64   by blast

    65

    66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"

    67   by (unfold quot_def) blast

    68

    69 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"

    70   by (unfold quot_def) blast

    71

    72 text {*

    73  \medskip Abstracted equivalence classes are the canonical

    74  representation of elements of a quotient type.

    75 *}

    76

    77 constdefs

    78   class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")

    79   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"

    80

    81 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"

    82 proof (cases A)

    83   fix R assume R: "A = Abs_quot R"

    84   assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast

    85   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast

    86   thus ?thesis by (unfold class_def)

    87 qed

    88

    89 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"

    90   by (insert quot_exhaust) blast

    91

    92

    93 subsection {* Equality on quotients *}

    94

    95 text {*

    96  Equality of canonical quotient elements coincides with the original

    97  relation.

    98 *}

    99

   100 theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"

   101 proof

   102   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"

   103   show "a \<sim> b"

   104   proof -

   105     from eq have "{x. a \<sim> x} = {x. b \<sim> x}"

   106       by (simp only: class_def Abs_quot_inject quotI)

   107     moreover have "a \<sim> a" ..

   108     ultimately have "a \<in> {x. b \<sim> x}" by blast

   109     hence "b \<sim> a" by blast

   110     thus ?thesis ..

   111   qed

   112 next

   113   assume ab: "a \<sim> b"

   114   show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"

   115   proof -

   116     have "{x. a \<sim> x} = {x. b \<sim> x}"

   117     proof (rule Collect_cong)

   118       fix x show "(a \<sim> x) = (b \<sim> x)"

   119       proof

   120         from ab have "b \<sim> a" ..

   121         also assume "a \<sim> x"

   122         finally show "b \<sim> x" .

   123       next

   124         note ab

   125         also assume "b \<sim> x"

   126         finally show "a \<sim> x" .

   127       qed

   128     qed

   129     thus ?thesis by (simp only: class_def)

   130   qed

   131 qed

   132

   133

   134 subsection {* Picking representing elements *}

   135

   136 constdefs

   137   pick :: "'a::equiv quot => 'a"

   138   "pick A == SOME a. A = \<lfloor>a\<rfloor>"

   139

   140 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"

   141 proof (unfold pick_def)

   142   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"

   143   proof (rule someI2)

   144     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..

   145     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"

   146     hence "a \<sim> x" .. thus "x \<sim> a" ..

   147   qed

   148 qed

   149

   150 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"

   151 proof (cases A)

   152   fix a assume a: "A = \<lfloor>a\<rfloor>"

   153   hence "pick A \<sim> a" by (simp only: pick_equiv)

   154   hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..

   155   with a show ?thesis by simp

   156 qed

   157

   158 text {*

   159  \medskip The following rules support canonical function definitions

   160  on quotient types (with up to two arguments).  Note that the

   161  stripped-down version without additional conditions is sufficient

   162  most of the time.

   163 *}

   164

   165 theorem quot_cond_function:

   166   "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>

   167     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>

   168       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>

   169     P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   170   (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")

   171 proof -

   172   assume cong: "PROP ?cong"

   173   assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"

   174   hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)

   175   also have "... = g a b"

   176   proof (rule cong)

   177     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..

   178     moreover

   179     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..

   180     moreover

   181     show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .

   182     ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)

   183   qed

   184   finally show ?thesis .

   185 qed

   186

   187 theorem quot_function:

   188   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>

   189     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>

   190     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   191 proof -

   192   case rule_context from this TrueI

   193   show ?thesis by (rule quot_cond_function)

   194 qed

   195

   196 theorem quot_function':

   197   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>

   198     (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>

   199     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   200   by  (rule quot_function) (simp only: quot_equality)+

   201

   202 end