src/HOL/Library/Quotient.thy
 author chaieb Mon Jun 11 11:06:04 2007 +0200 (2007-06-11) changeset 23315 df3a7e9ebadb parent 22473 753123c89d72 child 23373 ead82c82da9e permissions -rw-r--r--
tuned Proof
     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 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 class eqv = type +

    25   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)

    26

    27 class equiv = eqv +

    28   assumes equiv_refl [intro]: "x \<^loc>\<sim> x"

    29   assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"

    30   assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"

    31

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

    33 proof -

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

    35     by (rule contrapos_nn) (rule equiv_sym)

    36 qed

    37

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

    39 proof -

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

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

    42   proof

    43     assume "x \<sim> z"

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

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

    46     thus False by contradiction

    47   qed

    48 qed

    49

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

    51 proof -

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

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

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

    55 qed

    56

    57 text {*

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

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

    60 *}

    61

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

    63   by blast

    64

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

    66   unfolding quot_def by blast

    67

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

    69   unfolding quot_def by blast

    70

    71 text {*

    72  \medskip Abstracted equivalence classes are the canonical

    73  representation of elements of a quotient type.

    74 *}

    75

    76 definition

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

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

    79

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

    81 proof (cases A)

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

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

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

    85   thus ?thesis unfolding class_def .

    86 qed

    87

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

    89   using quot_exhaust by blast

    90

    91

    92 subsection {* Equality on quotients *}

    93

    94 text {*

    95  Equality of canonical quotient elements coincides with the original

    96  relation.

    97 *}

    98

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

   100 proof

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

   102   show "a \<sim> b"

   103   proof -

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

   105       by (simp only: class_def Abs_quot_inject quotI)

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

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

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

   109     thus ?thesis ..

   110   qed

   111 next

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

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

   114   proof -

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

   116     proof (rule Collect_cong)

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

   118       proof

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

   120         also assume "a \<sim> x"

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

   122       next

   123         note ab

   124         also assume "b \<sim> x"

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

   126       qed

   127     qed

   128     thus ?thesis by (simp only: class_def)

   129   qed

   130 qed

   131

   132

   133 subsection {* Picking representing elements *}

   134

   135 definition

   136   pick :: "'a::equiv quot => 'a" where

   137   "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"

   138

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

   140 proof (unfold pick_def)

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

   142   proof (rule someI2)

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

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

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

   146   qed

   147 qed

   148

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

   150 proof (cases A)

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

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

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

   154   with a show ?thesis by simp

   155 qed

   156

   157 text {*

   158  \medskip The following rules support canonical function definitions

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

   160  stripped-down version without additional conditions is sufficient

   161  most of the time.

   162 *}

   163

   164 theorem quot_cond_function:

   165   assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"

   166     and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>

   167       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"

   168     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"

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

   170 proof -

   171   from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)

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

   173   proof (rule cong)

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

   175     moreover

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

   177     moreover

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

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

   180   qed

   181   finally show ?thesis .

   182 qed

   183

   184 theorem quot_function:

   185   assumes "!!X Y. f X Y == g (pick X) (pick Y)"

   186     and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"

   187   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   188   using prems and TrueI

   189   by (rule quot_cond_function)

   190

   191 theorem quot_function':

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

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

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

   195   by (rule quot_function) (simp_all only: quot_equality)

   196

   197 end