src/HOL/Library/Quotient.thy
changeset 10250 ca93fe25a84b
child 10278 ea1bf4b6255c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Quotient.thy	Wed Oct 18 23:29:13 2000 +0200
     1.3 @@ -0,0 +1,313 @@
     1.4 +(*  Title:      HOL/Library/Quotient.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {*
    1.10 +  \title{Quotients}
    1.11 +  \author{Gertrud Bauer and Markus Wenzel}
    1.12 +*}
    1.13 +
    1.14 +theory Quotient = Main:
    1.15 +
    1.16 +text {*
    1.17 + Higher-order quotients are defined over partial equivalence relations
    1.18 + (PERs) instead of total ones.  We provide axiomatic type classes
    1.19 + @{text "equiv < partial_equiv"} and a type constructor
    1.20 + @{text "'a quot"} with basic operations.  Note that conventional
    1.21 + quotient constructions emerge as a special case.  This development is
    1.22 + loosely based on \cite{Slotosch:1997}.
    1.23 +*}
    1.24 +
    1.25 +
    1.26 +subsection {* Equivalence relations *}
    1.27 +
    1.28 +subsubsection {* Partial equivalence *}
    1.29 +
    1.30 +text {*
    1.31 + Type class @{text partial_equiv} models partial equivalence relations
    1.32 + (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
    1.33 + which is required to be symmetric and transitive, but not necessarily
    1.34 + reflexive.
    1.35 +*}
    1.36 +
    1.37 +consts
    1.38 +  eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
    1.39 +
    1.40 +axclass partial_equiv < "term"
    1.41 +  eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    1.42 +  eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    1.43 +
    1.44 +text {*
    1.45 + \medskip The domain of a partial equivalence relation is the set of
    1.46 + reflexive elements.  Due to symmetry and transitivity this
    1.47 + characterizes exactly those elements that are connected with
    1.48 + \emph{any} other one.
    1.49 +*}
    1.50 +
    1.51 +constdefs
    1.52 +  domain :: "'a::partial_equiv set"
    1.53 +  "domain == {x. x \<sim> x}"
    1.54 +
    1.55 +lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
    1.56 +  by (unfold domain_def) blast
    1.57 +
    1.58 +lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
    1.59 +  by (unfold domain_def) blast
    1.60 +
    1.61 +theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
    1.62 +proof
    1.63 +  assume xy: "x \<sim> y"
    1.64 +  also from xy have "y \<sim> x" ..
    1.65 +  finally show "x \<sim> x" .
    1.66 +qed
    1.67 +
    1.68 +
    1.69 +subsubsection {* Equivalence on function spaces *}
    1.70 +
    1.71 +text {*
    1.72 + The @{text \<sim>} relation is lifted to function spaces.  It is
    1.73 + important to note that this is \emph{not} the direct product, but a
    1.74 + structural one corresponding to the congruence property.
    1.75 +*}
    1.76 +
    1.77 +defs (overloaded)
    1.78 +  eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
    1.79 +
    1.80 +lemma partial_equiv_funI [intro?]:
    1.81 +    "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
    1.82 +  by (unfold eqv_fun_def) blast
    1.83 +
    1.84 +lemma partial_equiv_funD [dest?]:
    1.85 +    "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
    1.86 +  by (unfold eqv_fun_def) blast
    1.87 +
    1.88 +text {*
    1.89 + The class of partial equivalence relations is closed under function
    1.90 + spaces (in \emph{both} argument positions).
    1.91 +*}
    1.92 +
    1.93 +instance fun :: (partial_equiv, partial_equiv) partial_equiv
    1.94 +proof intro_classes
    1.95 +  fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
    1.96 +  assume fg: "f \<sim> g"
    1.97 +  show "g \<sim> f"
    1.98 +  proof
    1.99 +    fix x y :: 'a
   1.100 +    assume x: "x \<in> domain" and y: "y \<in> domain"
   1.101 +    assume "x \<sim> y" hence "y \<sim> x" ..
   1.102 +    with fg y x have "f y \<sim> g x" ..
   1.103 +    thus "g x \<sim> f y" ..
   1.104 +  qed
   1.105 +  assume gh: "g \<sim> h"
   1.106 +  show "f \<sim> h"
   1.107 +  proof
   1.108 +    fix x y :: 'a
   1.109 +    assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"
   1.110 +    with fg have "f x \<sim> g y" ..
   1.111 +    also from y have "y \<sim> y" ..
   1.112 +    with gh y y have "g y \<sim> h y" ..
   1.113 +    finally show "f x \<sim> h y" .
   1.114 +  qed
   1.115 +qed
   1.116 +
   1.117 +
   1.118 +subsubsection {* Total equivalence *}
   1.119 +
   1.120 +text {*
   1.121 + The class of total equivalence relations on top of PERs.  It
   1.122 + coincides with the standard notion of equivalence, i.e.\
   1.123 + @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
   1.124 + and symmetric.
   1.125 +*}
   1.126 +
   1.127 +axclass equiv < partial_equiv
   1.128 +  eqv_refl [intro]: "x \<sim> x"
   1.129 +
   1.130 +text {*
   1.131 + On total equivalences all elements are reflexive, and congruence
   1.132 + holds unconditionally.
   1.133 +*}
   1.134 +
   1.135 +theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
   1.136 +proof
   1.137 +  show "x \<sim> x" ..
   1.138 +qed
   1.139 +
   1.140 +theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
   1.141 +proof -
   1.142 +  assume "f \<sim> g"
   1.143 +  moreover have "x \<in> domain" ..
   1.144 +  moreover have "y \<in> domain" ..
   1.145 +  moreover assume "x \<sim> y"
   1.146 +  ultimately show ?thesis ..
   1.147 +qed
   1.148 +
   1.149 +
   1.150 +subsection {* Quotient types *}
   1.151 +
   1.152 +subsubsection {* General quotients and equivalence classes *}
   1.153 +
   1.154 +text {*
   1.155 + The quotient type @{text "'a quot"} consists of all \emph{equivalence
   1.156 + classes} over elements of the base type @{typ 'a}.
   1.157 +*}
   1.158 +
   1.159 +typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
   1.160 +  by blast
   1.161 +
   1.162 +lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   1.163 +  by (unfold quot_def) blast
   1.164 +
   1.165 +lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
   1.166 +  by (unfold quot_def) blast
   1.167 +
   1.168 +
   1.169 +text {*
   1.170 + \medskip Standard properties of type-definitions.\footnote{(FIXME)
   1.171 + Better incorporate these into the typedef package?}
   1.172 +*}
   1.173 +
   1.174 +theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)"
   1.175 +proof
   1.176 +  assume "Rep_quot x = Rep_quot y"
   1.177 +  hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:)
   1.178 +  thus "x = y" by (simp only: Rep_quot_inverse)
   1.179 +next
   1.180 +  assume "x = y"
   1.181 +  thus "Rep_quot x = Rep_quot y" by simp
   1.182 +qed
   1.183 +
   1.184 +theorem Abs_quot_inject:
   1.185 +  "x \<in> quot ==> y \<in> quot ==> (Abs_quot x = Abs_quot y) = (x = y)"
   1.186 +proof
   1.187 +  assume "Abs_quot x = Abs_quot y"
   1.188 +  hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp
   1.189 +  also assume "x \<in> quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse)
   1.190 +  also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
   1.191 +  finally show "x = y" .
   1.192 +next
   1.193 +  assume "x = y"
   1.194 +  thus "Abs_quot x = Abs_quot y" by simp
   1.195 +qed
   1.196 +
   1.197 +theorem Rep_quot_induct: "y \<in> quot ==> (!!x. P (Rep_quot x)) ==> P y"
   1.198 +proof -
   1.199 +  assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" .
   1.200 +  also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
   1.201 +  finally show "P y" .
   1.202 +qed
   1.203 +
   1.204 +theorem Abs_quot_induct: "(!!y. y \<in> quot ==> P (Abs_quot y)) ==> P x"
   1.205 +proof -
   1.206 +  assume r: "!!y. y \<in> quot ==> P (Abs_quot y)"
   1.207 +  have "Rep_quot x \<in> quot" by (rule Rep_quot)
   1.208 +  hence "P (Abs_quot (Rep_quot x))" by (rule r)
   1.209 +  also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse)
   1.210 +  finally show "P x" .
   1.211 +qed
   1.212 +
   1.213 +text {*
   1.214 + \medskip Abstracted equivalence classes are the canonical
   1.215 + representation of elements of a quotient type.
   1.216 +*}
   1.217 +
   1.218 +constdefs
   1.219 +  eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>")
   1.220 +  "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
   1.221 +
   1.222 +theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
   1.223 +proof (unfold eqv_class_def)
   1.224 +  show "\<exists>a. A = Abs_quot {x. a \<sim> x}"
   1.225 +  proof (induct A rule: Abs_quot_induct)
   1.226 +    fix R assume "R \<in> quot"
   1.227 +    hence "\<exists>a. R = {x. a \<sim> x}" by blast
   1.228 +    thus "\<exists>a. Abs_quot R = Abs_quot {x. a \<sim> x}" by blast
   1.229 +  qed
   1.230 +qed
   1.231 +
   1.232 +lemma quot_cases [case_names rep, cases type: quot]:
   1.233 +    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
   1.234 +  by (insert quot_rep) blast
   1.235 +
   1.236 +
   1.237 +subsubsection {* Equality on quotients *}
   1.238 +
   1.239 +text {*
   1.240 + Equality of canonical quotient elements corresponds to the original
   1.241 + relation as follows.
   1.242 +*}
   1.243 +
   1.244 +theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   1.245 +proof -
   1.246 +  assume ab: "a \<sim> b"
   1.247 +  have "{x. a \<sim> x} = {x. b \<sim> x}"
   1.248 +  proof (rule Collect_cong)
   1.249 +    fix x show "(a \<sim> x) = (b \<sim> x)"
   1.250 +    proof
   1.251 +      from ab have "b \<sim> a" ..
   1.252 +      also assume "a \<sim> x"
   1.253 +      finally show "b \<sim> x" .
   1.254 +    next
   1.255 +      note ab
   1.256 +      also assume "b \<sim> x"
   1.257 +      finally show "a \<sim> x" .
   1.258 +    qed
   1.259 +  qed
   1.260 +  thus ?thesis by (simp only: eqv_class_def)
   1.261 +qed
   1.262 +
   1.263 +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 *)
   1.264 +proof (unfold eqv_class_def)
   1.265 +  assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
   1.266 +  hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
   1.267 +  moreover assume "a \<in> domain" hence "a \<sim> a" ..
   1.268 +  ultimately have "a \<in> {x. b \<sim> x}" by blast
   1.269 +  hence "b \<sim> a" by blast
   1.270 +  thus "a \<sim> b" ..
   1.271 +qed
   1.272 +
   1.273 +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 *)
   1.274 +proof (rule eqv_class_eqD')
   1.275 +  show "a \<in> domain" ..
   1.276 +qed
   1.277 +
   1.278 +lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   1.279 +  by (insert eqv_class_eqI eqv_class_eqD') blast
   1.280 +
   1.281 +lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
   1.282 +  by (insert eqv_class_eqI eqv_class_eqD) blast
   1.283 +
   1.284 +
   1.285 +subsubsection {* Picking representing elements *}
   1.286 +
   1.287 +constdefs
   1.288 +  pick :: "'a::partial_equiv quot => 'a"
   1.289 +  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
   1.290 +
   1.291 +theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)
   1.292 +proof (unfold pick_def)
   1.293 +  assume a: "a \<in> domain"
   1.294 +  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   1.295 +  proof (rule someI2)
   1.296 +    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   1.297 +    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   1.298 +    hence "a \<sim> x" ..
   1.299 +    thus "x \<sim> a" ..
   1.300 +  qed
   1.301 +qed
   1.302 +
   1.303 +theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"
   1.304 +proof (rule pick_eqv')
   1.305 +  show "a \<in> domain" ..
   1.306 +qed
   1.307 +
   1.308 +theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"   (* FIXME tune proof *)
   1.309 +proof (cases A)
   1.310 +  fix a assume a: "A = \<lfloor>a\<rfloor>"
   1.311 +  hence "pick A \<sim> a" by (simp only: pick_eqv)
   1.312 +  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
   1.313 +  with a show ?thesis by simp
   1.314 +qed
   1.315 +
   1.316 +end