summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 22 Oct 2000 22:18:40 +0200 | |

changeset 10285 | 6949e17f314a |

parent 10284 | ec98fc455272 |

child 10286 | fdcdb8a80988 |

simplified quotients (only plain total equivs);

src/HOL/Library/Quotient.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/document/root.bib | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Quotient.thy Fri Oct 20 19:46:53 2000 +0200 +++ b/src/HOL/Library/Quotient.thy Sun Oct 22 22:18:40 2000 +0200 @@ -11,149 +11,32 @@ theory Quotient = Main: text {* - Higher-order quotients are defined over partial equivalence relations - (PERs) instead of total ones. We provide axiomatic type classes - @{text "equiv < partial_equiv"} and a type constructor - @{text "'a quot"} with basic operations. Note that conventional - quotient constructions emerge as a special case. This development is - loosely based on \cite{Slotosch:1997}. -*} - - -subsection {* Equivalence relations *} - -subsubsection {* Partial equivalence *} - -text {* - Type class @{text partial_equiv} models partial equivalence relations - (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation, - which is required to be symmetric and transitive, but not necessarily - reflexive. -*} - -consts - eqv :: "'a => 'a => bool" (infixl "\<sim>" 50) - -axclass partial_equiv < "term" - eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x" - eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" - -text {* - \medskip The domain of a partial equivalence relation is the set of - reflexive elements. Due to symmetry and transitivity this - characterizes exactly those elements that are connected with - \emph{any} other one. + We introduce the notion of quotient types over equivalence relations + via axiomatic type classes. *} -constdefs - domain :: "'a::partial_equiv set" - "domain == {x. x \<sim> x}" - -lemma domainI [intro]: "x \<sim> x ==> x \<in> domain" - by (unfold domain_def) blast - -lemma domainD [dest]: "x \<in> domain ==> x \<sim> x" - by (unfold domain_def) blast - -theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain" -proof - assume xy: "x \<sim> y" - also from xy have "y \<sim> x" .. - finally show "x \<sim> x" . -qed - - -subsubsection {* Equivalence on function spaces *} - -text {* - The @{text \<sim>} relation is lifted to function spaces. It is - important to note that this is \emph{not} the direct product, but a - structural one corresponding to the congruence property. -*} - -defs (overloaded) - eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y" - -lemma partial_equiv_funI [intro?]: - "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g" - by (unfold eqv_fun_def) blast - -lemma partial_equiv_funD [dest?]: - "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y" - by (unfold eqv_fun_def) blast +subsection {* Equivalence relations and quotient types *} text {* - The class of partial equivalence relations is closed under function - spaces (in \emph{both} argument positions). + \medskip Type class @{text equiv} models equivalence relations using + the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation. *} -instance fun :: (partial_equiv, partial_equiv) partial_equiv -proof intro_classes - fix f g h :: "'a::partial_equiv => 'b::partial_equiv" - assume fg: "f \<sim> g" - show "g \<sim> f" - proof - fix x y :: 'a - assume x: "x \<in> domain" and y: "y \<in> domain" - assume "x \<sim> y" hence "y \<sim> x" .. - with fg y x have "f y \<sim> g x" .. - thus "g x \<sim> f y" .. - qed - assume gh: "g \<sim> h" - show "f \<sim> h" - proof - fix x y :: 'a - assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y" - with fg have "f x \<sim> g y" .. - also from y have "y \<sim> y" .. - with gh y y have "g y \<sim> h y" .. - finally show "f x \<sim> h y" . - qed -qed +axclass eqv < "term" +consts + eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) - -subsubsection {* Total equivalence *} +axclass equiv < eqv + eqv_refl [intro]: "x \<sim> x" + eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" + eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x" text {* - The class of total equivalence relations on top of PERs. It - coincides with the standard notion of equivalence, i.e.\ - @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive - and symmetric. -*} - -axclass equiv < partial_equiv - eqv_refl [intro]: "x \<sim> x" - -text {* - On total equivalences all elements are reflexive, and congruence - holds unconditionally. + \medskip The quotient type @{text "'a quot"} consists of all + \emph{equivalence classes} over elements of the base type @{typ 'a}. *} -theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain" -proof - show "x \<sim> x" .. -qed - -theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)" -proof - - assume "f \<sim> g" - moreover have "x \<in> domain" .. - moreover have "y \<in> domain" .. - moreover assume "x \<sim> y" - ultimately show ?thesis .. -qed - - -subsection {* Quotient types *} - -subsubsection {* General quotients and equivalence classes *} - -text {* - The quotient type @{text "'a quot"} consists of all \emph{equivalence - classes} over elements of the base type @{typ 'a}. -*} - -typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}" +typedef 'a quot = "{{x. a \<sim> x}| a::'a::eqv. True}" by blast lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" @@ -168,7 +51,7 @@ *} constdefs - eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") + equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" @@ -176,7 +59,7 @@ fix R assume R: "A = Abs_quot R" assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast - thus ?thesis by (unfold eqv_class_def) + thus ?thesis by (unfold equivalence_class_def) qed lemma quot_cases [case_names rep, cases type: quot]: @@ -184,83 +67,105 @@ by (insert quot_rep) blast -subsubsection {* Equality on quotients *} +subsection {* Equality on quotients *} text {* Equality of canonical quotient elements corresponds to the original relation as follows. *} -theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" -proof - +theorem equivalence_class_eq [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" +proof + assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" + show "a \<sim> b" + proof - + from eq have "{x. a \<sim> x} = {x. b \<sim> x}" + by (simp only: equivalence_class_def Abs_quot_inject quotI) + moreover have "a \<sim> a" .. + ultimately have "a \<in> {x. b \<sim> x}" by blast + hence "b \<sim> a" by blast + thus ?thesis .. + qed +next assume ab: "a \<sim> b" - have "{x. a \<sim> x} = {x. b \<sim> x}" - proof (rule Collect_cong) - fix x show "(a \<sim> x) = (b \<sim> x)" - proof - from ab have "b \<sim> a" .. - also assume "a \<sim> x" - finally show "b \<sim> x" . - next - note ab - also assume "b \<sim> x" - finally show "a \<sim> x" . + show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" + proof - + have "{x. a \<sim> x} = {x. b \<sim> x}" + proof (rule Collect_cong) + fix x show "(a \<sim> x) = (b \<sim> x)" + proof + from ab have "b \<sim> a" .. + also assume "a \<sim> x" + finally show "b \<sim> x" . + next + note ab + also assume "b \<sim> x" + finally show "a \<sim> x" . + qed qed + thus ?thesis by (simp only: equivalence_class_def) qed - thus ?thesis by (simp only: eqv_class_def) qed -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 *) -proof (unfold eqv_class_def) - assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}" - hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI) - moreover assume "a \<in> domain" hence "a \<sim> a" .. - ultimately have "a \<in> {x. b \<sim> x}" by blast - hence "b \<sim> a" by blast - thus "a \<sim> b" .. -qed -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 *) -proof (rule eqv_class_eqD') - show "a \<in> domain" .. -qed - -lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" - by (insert eqv_class_eqI eqv_class_eqD') blast - -lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))" - by (insert eqv_class_eqI eqv_class_eqD) blast - - -subsubsection {* Picking representing elements *} +subsection {* Picking representing elements *} constdefs - pick :: "'a::partial_equiv quot => 'a" + pick :: "'a::equiv quot => 'a" "pick A == SOME a. A = \<lfloor>a\<rfloor>" -theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *) +theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" proof (unfold pick_def) - assume a: "a \<in> domain" show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" proof (rule someI2) show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" - hence "a \<sim> x" .. - thus "x \<sim> a" .. + hence "a \<sim> x" .. thus "x \<sim> a" .. qed qed -theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)" -proof (rule pick_eqv') - show "a \<in> domain" .. -qed - -theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" +theorem pick_inverse: "\<lfloor>pick A\<rfloor> = A" proof (cases A) fix a assume a: "A = \<lfloor>a\<rfloor>" - hence "pick A \<sim> a" by simp - hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp + hence "pick A \<sim> a" by (simp only: pick_equiv) + hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. with a show ?thesis by simp qed +text {* + \medskip The following rules support canonical function definitions + on quotient types. +*} + +theorem cong_definition1: + "(!!X. f X == g (pick X)) ==> + (!!x x'. x \<sim> x' ==> g x = g x') ==> + f \<lfloor>a\<rfloor> = g a" +proof - + assume cong: "!!x x'. x \<sim> x' ==> g x = g x'" + assume "!!X. f X == g (pick X)" + hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:) + also have "\<dots> = g a" + proof (rule cong) + show "pick \<lfloor>a\<rfloor> \<sim> a" .. + qed + finally show ?thesis . +qed + +theorem cong_definition2: + "(!!X Y. f X Y == g (pick X) (pick Y)) ==> + (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> + f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" +proof - + assume cong: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y'" + assume "!!X Y. f X Y == g (pick X) (pick Y)" + hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) + also have "\<dots> = g a b" + proof (rule cong) + show "pick \<lfloor>a\<rfloor> \<sim> a" .. + show "pick \<lfloor>b\<rfloor> \<sim> b" .. + qed + finally show ?thesis . +qed + end

--- a/src/HOL/Library/document/root.bib Fri Oct 20 19:46:53 2000 +0200 +++ b/src/HOL/Library/document/root.bib Sun Oct 22 22:18:40 2000 +0200 @@ -1,8 +1,3 @@ - -@InProceedings{Slotosch:1997, - author = {Oscar Slotosch}, - title = {Higher Order Quotients and their Implementation in {Isabelle HOL}}, - crossref = {tphols97}} @InProceedings{paulin-tlca, author = {Christine Paulin-Mohring}, @@ -18,10 +13,3 @@ year = 1993, publisher = {Springer}, series = {LNCS 664}} - -@Proceedings{tphols97, - title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, - booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97}, - editor = {Elsa L. Gunter and Amy Felty}, - series = {LNCS 1275}, - year = 1997}