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