src/HOL/Library/Quotient.thy
 author kleing Mon Jun 21 10:25:57 2004 +0200 (2004-06-21) changeset 14981 e73f8140af78 parent 14706 71590b7733b7 child 15131 c69542757a4d permissions -rw-r--r--
Merged in license change from Isabelle2004
     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 = Main:

     9

    10 text {*

    11  We introduce the notion of quotient types over equivalence relations

    12  via axiomatic type classes.

    13 *}

    14

    15 subsection {* Equivalence relations and quotient types *}

    16

    17 text {*

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

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

    20 *}

    21

    22 axclass eqv \<subseteq> type

    23 consts

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

    25

    26 axclass equiv \<subseteq> eqv

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

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

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

    30

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

    32 proof -

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

    34     by (rule contrapos_nn) (rule equiv_sym)

    35 qed

    36

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

    38 proof -

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

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

    41   proof

    42     assume "x \<sim> z"

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

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

    45     thus False by contradiction

    46   qed

    47 qed

    48

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

    50 proof -

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

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

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

    54 qed

    55

    56 text {*

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

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

    59 *}

    60

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

    62   by blast

    63

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

    65   by (unfold quot_def) blast

    66

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

    68   by (unfold quot_def) blast

    69

    70 text {*

    71  \medskip Abstracted equivalence classes are the canonical

    72  representation of elements of a quotient type.

    73 *}

    74

    75 constdefs

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

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

    78

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

    80 proof (cases A)

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

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

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

    84   thus ?thesis by (unfold class_def)

    85 qed

    86

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

    88   by (insert quot_exhaust) blast

    89

    90

    91 subsection {* Equality on quotients *}

    92

    93 text {*

    94  Equality of canonical quotient elements coincides with the original

    95  relation.

    96 *}

    97

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

    99 proof

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

   101   show "a \<sim> b"

   102   proof -

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

   104       by (simp only: class_def Abs_quot_inject quotI)

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

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

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

   108     thus ?thesis ..

   109   qed

   110 next

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

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

   113   proof -

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

   115     proof (rule Collect_cong)

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

   117       proof

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

   119         also assume "a \<sim> x"

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

   121       next

   122         note ab

   123         also assume "b \<sim> x"

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

   125       qed

   126     qed

   127     thus ?thesis by (simp only: class_def)

   128   qed

   129 qed

   130

   131

   132 subsection {* Picking representing elements *}

   133

   134 constdefs

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

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

   137

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

   139 proof (unfold pick_def)

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

   141   proof (rule someI2)

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

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

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

   145   qed

   146 qed

   147

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

   149 proof (cases A)

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

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

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

   153   with a show ?thesis by simp

   154 qed

   155

   156 text {*

   157  \medskip The following rules support canonical function definitions

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

   159  stripped-down version without additional conditions is sufficient

   160  most of the time.

   161 *}

   162

   163 theorem quot_cond_function:

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

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

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

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

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

   169 proof -

   170   assume cong: "PROP ?cong"

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

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

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

   174   proof (rule cong)

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

   176     moreover

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

   178     moreover

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

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

   181   qed

   182   finally show ?thesis .

   183 qed

   184

   185 theorem quot_function:

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

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

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

   189 proof -

   190   case rule_context from this TrueI

   191   show ?thesis by (rule quot_cond_function)

   192 qed

   193

   194 theorem quot_function':

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

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

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

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

   199

   200 end