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