src/HOL/Library/Quotient.thy
 author wenzelm Tue Nov 21 19:03:06 2000 +0100 (2000-11-21) changeset 10505 b89e6cc963e3 parent 10499 2f33d0fd242e child 10551 ec9fab41b3a0 permissions -rw-r--r--
unsymbolize;
     1 (*  Title:      HOL/Library/Quotient.thy

     2     ID:         $Id$

     3     Author:     Markus Wenzel, TU Muenchen

     4 *)

     5

     6 header {*

     7   \title{Quotient types}

     8   \author{Markus Wenzel}

     9 *}

    10

    11 theory Quotient = Main:

    12

    13 text {*

    14  We introduce the notion of quotient types over equivalence relations

    15  via axiomatic type classes.

    16 *}

    17

    18 subsection {* Equivalence relations and quotient types *}

    19

    20 text {*

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

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

    23 *}

    24

    25 axclass eqv < "term"

    26 consts

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

    28

    29 axclass equiv < eqv

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

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

    32   equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"

    33

    34 lemma not_equiv_sym [elim?]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"

    35 proof -

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

    37     by (rule contrapos_nn) (rule equiv_sym)

    38 qed

    39

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

    41 proof -

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

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

    44   proof

    45     assume "x \<sim> z"

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

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

    48     thus False by contradiction

    49   qed

    50 qed

    51

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

    53 proof -

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

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

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

    57 qed

    58

    59 text {*

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

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

    62 *}

    63

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

    65   by blast

    66

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

    68   by (unfold quot_def) blast

    69

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

    71   by (unfold quot_def) blast

    72

    73 text {*

    74  \medskip Abstracted equivalence classes are the canonical

    75  representation of elements of a quotient type.

    76 *}

    77

    78 constdefs

    79   equivalence_class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")

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

    81

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

    83 proof (cases A)

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

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

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

    87   thus ?thesis by (unfold equivalence_class_def)

    88 qed

    89

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

    91   by (insert quot_exhaust) blast

    92

    93

    94 subsection {* Equality on quotients *}

    95

    96 text {*

    97  Equality of canonical quotient elements coincides with the original

    98  relation.

    99 *}

   100

   101 theorem quot_equality: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"

   102 proof

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

   104   show "a \<sim> b"

   105   proof -

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

   107       by (simp only: equivalence_class_def Abs_quot_inject quotI)

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

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

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

   111     thus ?thesis ..

   112   qed

   113 next

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

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

   116   proof -

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

   118     proof (rule Collect_cong)

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

   120       proof

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

   122         also assume "a \<sim> x"

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

   124       next

   125         note ab

   126         also assume "b \<sim> x"

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

   128       qed

   129     qed

   130     thus ?thesis by (simp only: equivalence_class_def)

   131   qed

   132 qed

   133

   134 lemma quot_equalI [intro?]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"

   135   by (simp only: quot_equality)

   136

   137 lemma quot_equalD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> b"

   138   by (simp only: quot_equality)

   139

   140 lemma quot_not_equalI [intro?]: "\<not> (a \<sim> b) ==> \<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor>"

   141   by (simp add: quot_equality)

   142

   143 lemma quot_not_equalD [dest?]: "\<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor> ==> \<not> (a \<sim> b)"

   144   by (simp add: quot_equality)

   145

   146

   147 subsection {* Picking representing elements *}

   148

   149 constdefs

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

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

   152

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

   154 proof (unfold pick_def)

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

   156   proof (rule someI2)

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

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

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

   160   qed

   161 qed

   162

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

   164 proof (cases A)

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

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

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

   168   with a show ?thesis by simp

   169 qed

   170

   171 text {*

   172  \medskip The following rules support canonical function definitions

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

   174  stripped-down version without additional conditions is sufficient

   175  most of the time.

   176 *}

   177

   178 theorem quot_cond_function:

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

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

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

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

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

   184 proof -

   185   assume cong: "PROP ?cong"

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

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

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

   189   proof (rule cong)

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

   191     moreover

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

   193     moreover

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

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

   196   qed

   197   finally show ?thesis .

   198 qed

   199

   200 theorem quot_function:

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

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

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

   204 proof -

   205   case antecedent from this TrueI

   206   show ?thesis by (rule quot_cond_function)

   207 qed

   208

   209 theorem quot_function':

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

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

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

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

   214

   215 end