simplified quotients (only plain total equivs);
authorwenzelm
Sun Oct 22 22:18:40 2000 +0200 (2000-10-22)
changeset 102856949e17f314a
parent 10284 ec98fc455272
child 10286 fdcdb8a80988
simplified quotients (only plain total equivs);
src/HOL/Library/Quotient.thy
src/HOL/Library/document/root.bib
     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.69 -defs (overloaded)
    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
     2.1 --- a/src/HOL/Library/document/root.bib	Fri Oct 20 19:46:53 2000 +0200
     2.2 +++ b/src/HOL/Library/document/root.bib	Sun Oct 22 22:18:40 2000 +0200
     2.3 @@ -1,8 +1,3 @@
     2.4 -
     2.5 -@InProceedings{Slotosch:1997,
     2.6 -  author = 	 {Oscar Slotosch},
     2.7 -  title = 	 {Higher Order Quotients and their Implementation in {Isabelle HOL}},
     2.8 -  crossref =     {tphols97}}
     2.9  
    2.10  @InProceedings{paulin-tlca,
    2.11    author	= {Christine Paulin-Mohring},
    2.12 @@ -18,10 +13,3 @@
    2.13    year		= 1993,
    2.14    publisher	= {Springer},
    2.15    series	= {LNCS 664}}
    2.16 -
    2.17 -@Proceedings{tphols97,
    2.18 -  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
    2.19 -  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
    2.20 -  editor	= {Elsa L. Gunter and Amy Felty},
    2.21 -  series	= {LNCS 1275},
    2.22 -  year		= 1997}