src/HOL/Library/Quotient.thy
author wenzelm
Wed Oct 18 23:29:13 2000 +0200 (2000-10-18)
changeset 10250 ca93fe25a84b
child 10278 ea1bf4b6255c
permissions -rw-r--r--
Quotient types;
     1 (*  Title:      HOL/Library/Quotient.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {*
     7   \title{Quotients}
     8   \author{Gertrud Bauer and Markus Wenzel}
     9 *}
    10 
    11 theory Quotient = Main:
    12 
    13 text {*
    14  Higher-order quotients are defined over partial equivalence relations
    15  (PERs) instead of total ones.  We provide axiomatic type classes
    16  @{text "equiv < partial_equiv"} and a type constructor
    17  @{text "'a quot"} with basic operations.  Note that conventional
    18  quotient constructions emerge as a special case.  This development is
    19  loosely based on \cite{Slotosch:1997}.
    20 *}
    21 
    22 
    23 subsection {* Equivalence relations *}
    24 
    25 subsubsection {* Partial equivalence *}
    26 
    27 text {*
    28  Type class @{text partial_equiv} models partial equivalence relations
    29  (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
    30  which is required to be symmetric and transitive, but not necessarily
    31  reflexive.
    32 *}
    33 
    34 consts
    35   eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
    36 
    37 axclass partial_equiv < "term"
    38   eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    39   eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    40 
    41 text {*
    42  \medskip The domain of a partial equivalence relation is the set of
    43  reflexive elements.  Due to symmetry and transitivity this
    44  characterizes exactly those elements that are connected with
    45  \emph{any} other one.
    46 *}
    47 
    48 constdefs
    49   domain :: "'a::partial_equiv set"
    50   "domain == {x. x \<sim> x}"
    51 
    52 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
    53   by (unfold domain_def) blast
    54 
    55 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
    56   by (unfold domain_def) blast
    57 
    58 theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
    59 proof
    60   assume xy: "x \<sim> y"
    61   also from xy have "y \<sim> x" ..
    62   finally show "x \<sim> x" .
    63 qed
    64 
    65 
    66 subsubsection {* Equivalence on function spaces *}
    67 
    68 text {*
    69  The @{text \<sim>} relation is lifted to function spaces.  It is
    70  important to note that this is \emph{not} the direct product, but a
    71  structural one corresponding to the congruence property.
    72 *}
    73 
    74 defs (overloaded)
    75   eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
    76 
    77 lemma partial_equiv_funI [intro?]:
    78     "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
    79   by (unfold eqv_fun_def) blast
    80 
    81 lemma partial_equiv_funD [dest?]:
    82     "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
    83   by (unfold eqv_fun_def) blast
    84 
    85 text {*
    86  The class of partial equivalence relations is closed under function
    87  spaces (in \emph{both} argument positions).
    88 *}
    89 
    90 instance fun :: (partial_equiv, partial_equiv) partial_equiv
    91 proof intro_classes
    92   fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
    93   assume fg: "f \<sim> g"
    94   show "g \<sim> f"
    95   proof
    96     fix x y :: 'a
    97     assume x: "x \<in> domain" and y: "y \<in> domain"
    98     assume "x \<sim> y" hence "y \<sim> x" ..
    99     with fg y x have "f y \<sim> g x" ..
   100     thus "g x \<sim> f y" ..
   101   qed
   102   assume gh: "g \<sim> h"
   103   show "f \<sim> h"
   104   proof
   105     fix x y :: 'a
   106     assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"
   107     with fg have "f x \<sim> g y" ..
   108     also from y have "y \<sim> y" ..
   109     with gh y y have "g y \<sim> h y" ..
   110     finally show "f x \<sim> h y" .
   111   qed
   112 qed
   113 
   114 
   115 subsubsection {* Total equivalence *}
   116 
   117 text {*
   118  The class of total equivalence relations on top of PERs.  It
   119  coincides with the standard notion of equivalence, i.e.\
   120  @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
   121  and symmetric.
   122 *}
   123 
   124 axclass equiv < partial_equiv
   125   eqv_refl [intro]: "x \<sim> x"
   126 
   127 text {*
   128  On total equivalences all elements are reflexive, and congruence
   129  holds unconditionally.
   130 *}
   131 
   132 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
   133 proof
   134   show "x \<sim> x" ..
   135 qed
   136 
   137 theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
   138 proof -
   139   assume "f \<sim> g"
   140   moreover have "x \<in> domain" ..
   141   moreover have "y \<in> domain" ..
   142   moreover assume "x \<sim> y"
   143   ultimately show ?thesis ..
   144 qed
   145 
   146 
   147 subsection {* Quotient types *}
   148 
   149 subsubsection {* General quotients and equivalence classes *}
   150 
   151 text {*
   152  The quotient type @{text "'a quot"} consists of all \emph{equivalence
   153  classes} over elements of the base type @{typ 'a}.
   154 *}
   155 
   156 typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
   157   by blast
   158 
   159 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   160   by (unfold quot_def) blast
   161 
   162 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
   163   by (unfold quot_def) blast
   164 
   165 
   166 text {*
   167  \medskip Standard properties of type-definitions.\footnote{(FIXME)
   168  Better incorporate these into the typedef package?}
   169 *}
   170 
   171 theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)"
   172 proof
   173   assume "Rep_quot x = Rep_quot y"
   174   hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:)
   175   thus "x = y" by (simp only: Rep_quot_inverse)
   176 next
   177   assume "x = y"
   178   thus "Rep_quot x = Rep_quot y" by simp
   179 qed
   180 
   181 theorem Abs_quot_inject:
   182   "x \<in> quot ==> y \<in> quot ==> (Abs_quot x = Abs_quot y) = (x = y)"
   183 proof
   184   assume "Abs_quot x = Abs_quot y"
   185   hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp
   186   also assume "x \<in> quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse)
   187   also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
   188   finally show "x = y" .
   189 next
   190   assume "x = y"
   191   thus "Abs_quot x = Abs_quot y" by simp
   192 qed
   193 
   194 theorem Rep_quot_induct: "y \<in> quot ==> (!!x. P (Rep_quot x)) ==> P y"
   195 proof -
   196   assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" .
   197   also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
   198   finally show "P y" .
   199 qed
   200 
   201 theorem Abs_quot_induct: "(!!y. y \<in> quot ==> P (Abs_quot y)) ==> P x"
   202 proof -
   203   assume r: "!!y. y \<in> quot ==> P (Abs_quot y)"
   204   have "Rep_quot x \<in> quot" by (rule Rep_quot)
   205   hence "P (Abs_quot (Rep_quot x))" by (rule r)
   206   also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse)
   207   finally show "P x" .
   208 qed
   209 
   210 text {*
   211  \medskip Abstracted equivalence classes are the canonical
   212  representation of elements of a quotient type.
   213 *}
   214 
   215 constdefs
   216   eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>")
   217   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
   218 
   219 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
   220 proof (unfold eqv_class_def)
   221   show "\<exists>a. A = Abs_quot {x. a \<sim> x}"
   222   proof (induct A rule: Abs_quot_induct)
   223     fix R assume "R \<in> quot"
   224     hence "\<exists>a. R = {x. a \<sim> x}" by blast
   225     thus "\<exists>a. Abs_quot R = Abs_quot {x. a \<sim> x}" by blast
   226   qed
   227 qed
   228 
   229 lemma quot_cases [case_names rep, cases type: quot]:
   230     "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
   231   by (insert quot_rep) blast
   232 
   233 
   234 subsubsection {* Equality on quotients *}
   235 
   236 text {*
   237  Equality of canonical quotient elements corresponds to the original
   238  relation as follows.
   239 *}
   240 
   241 theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   242 proof -
   243   assume ab: "a \<sim> b"
   244   have "{x. a \<sim> x} = {x. b \<sim> x}"
   245   proof (rule Collect_cong)
   246     fix x show "(a \<sim> x) = (b \<sim> x)"
   247     proof
   248       from ab have "b \<sim> a" ..
   249       also assume "a \<sim> x"
   250       finally show "b \<sim> x" .
   251     next
   252       note ab
   253       also assume "b \<sim> x"
   254       finally show "a \<sim> x" .
   255     qed
   256   qed
   257   thus ?thesis by (simp only: eqv_class_def)
   258 qed
   259 
   260 theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"  (* FIXME [dest] would cause trouble with blast due to overloading *)
   261 proof (unfold eqv_class_def)
   262   assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
   263   hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
   264   moreover assume "a \<in> domain" hence "a \<sim> a" ..
   265   ultimately have "a \<in> {x. b \<sim> x}" by blast
   266   hence "b \<sim> a" by blast
   267   thus "a \<sim> b" ..
   268 qed
   269 
   270 theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"  (* FIXME [dest] would cause trouble with blast due to overloading *)
   271 proof (rule eqv_class_eqD')
   272   show "a \<in> domain" ..
   273 qed
   274 
   275 lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   276   by (insert eqv_class_eqI eqv_class_eqD') blast
   277 
   278 lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
   279   by (insert eqv_class_eqI eqv_class_eqD) blast
   280 
   281 
   282 subsubsection {* Picking representing elements *}
   283 
   284 constdefs
   285   pick :: "'a::partial_equiv quot => 'a"
   286   "pick A == SOME a. A = \<lfloor>a\<rfloor>"
   287 
   288 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)
   289 proof (unfold pick_def)
   290   assume a: "a \<in> domain"
   291   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   292   proof (rule someI2)
   293     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   294     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   295     hence "a \<sim> x" ..
   296     thus "x \<sim> a" ..
   297   qed
   298 qed
   299 
   300 theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"
   301 proof (rule pick_eqv')
   302   show "a \<in> domain" ..
   303 qed
   304 
   305 theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"   (* FIXME tune proof *)
   306 proof (cases A)
   307   fix a assume a: "A = \<lfloor>a\<rfloor>"
   308   hence "pick A \<sim> a" by (simp only: pick_eqv)
   309   hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
   310   with a show ?thesis by simp
   311 qed
   312 
   313 end