renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
authorwenzelm
Wed Feb 10 19:37:34 2010 +0100 (2010-02-10)
changeset 3510053754ec7360b
parent 35099 7722bcb5c37c
child 35101 6ce9177d6b38
child 35103 d74fe18f01e9
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/Quotient_Type.thy
     1.1 --- a/NEWS	Wed Feb 10 17:05:40 2010 +0100
     1.2 +++ b/NEWS	Wed Feb 10 19:37:34 2010 +0100
     1.3 @@ -126,6 +126,9 @@
     1.4  
     1.5  * Theory List: added transpose.
     1.6  
     1.7 +* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
     1.8 +clash with new theory Quotient in Main HOL.
     1.9 +
    1.10  
    1.11  *** ML ***
    1.12  
     2.1 --- a/src/HOL/IsaMakefile	Wed Feb 10 17:05:40 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Wed Feb 10 19:37:34 2010 +0100
     2.3 @@ -386,12 +386,12 @@
     2.4    Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
     2.5    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
     2.6    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
     2.7 -  Library/Lattice_Algebras.thy						\
     2.8 -  Library/Lattice_Syntax.thy Library/Library.thy			\
     2.9 -  Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy	\
    2.10 -  Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
    2.11 -  Library/Quotient.thy Library/Quicksort.thy Library/Nat_Infinity.thy	\
    2.12 -  Library/Word.thy Library/README.html Library/Continuity.thy		\
    2.13 +  Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
    2.14 +  Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
    2.15 +  Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy	\
    2.16 +  Library/Permutation.thy Library/Quotient_Type.thy			\
    2.17 +  Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
    2.18 +  Library/README.html Library/Continuity.thy				\
    2.19    Library/Order_Relation.thy Library/Nested_Environment.thy		\
    2.20    Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
    2.21    Library/Library/document/root.tex Library/Library/document/root.bib	\
     3.1 --- a/src/HOL/Library/Library.thy	Wed Feb 10 17:05:40 2010 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Wed Feb 10 19:37:34 2010 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4    Preorder
     3.5    Product_Vector
     3.6    Quicksort
     3.7 -  Quotient
     3.8 +  Quotient_Type
     3.9    Ramsey
    3.10    Reflection
    3.11    RBT
     4.1 --- a/src/HOL/Library/Quotient.thy	Wed Feb 10 17:05:40 2010 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,196 +0,0 @@
     4.4 -(*  Title:      HOL/Library/Quotient.thy
     4.5 -    Author:     Markus Wenzel, TU Muenchen
     4.6 -*)
     4.7 -
     4.8 -header {* Quotient types *}
     4.9 -
    4.10 -theory Quotient
    4.11 -imports Main
    4.12 -begin
    4.13 -
    4.14 -text {*
    4.15 - We introduce the notion of quotient types over equivalence relations
    4.16 - via type classes.
    4.17 -*}
    4.18 -
    4.19 -subsection {* Equivalence relations and quotient types *}
    4.20 -
    4.21 -text {*
    4.22 - \medskip Type class @{text equiv} models equivalence relations @{text
    4.23 - "\<sim> :: 'a => 'a => bool"}.
    4.24 -*}
    4.25 -
    4.26 -class eqv =
    4.27 -  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    4.28 -
    4.29 -class equiv = eqv +
    4.30 -  assumes equiv_refl [intro]: "x \<sim> x"
    4.31 -  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    4.32 -  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    4.33 -
    4.34 -lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    4.35 -proof -
    4.36 -  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
    4.37 -    by (rule contrapos_nn) (rule equiv_sym)
    4.38 -qed
    4.39 -
    4.40 -lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
    4.41 -proof -
    4.42 -  assume "\<not> (x \<sim> y)" and "y \<sim> z"
    4.43 -  show "\<not> (x \<sim> z)"
    4.44 -  proof
    4.45 -    assume "x \<sim> z"
    4.46 -    also from `y \<sim> z` have "z \<sim> y" ..
    4.47 -    finally have "x \<sim> y" .
    4.48 -    with `\<not> (x \<sim> y)` show False by contradiction
    4.49 -  qed
    4.50 -qed
    4.51 -
    4.52 -lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
    4.53 -proof -
    4.54 -  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
    4.55 -  also assume "x \<sim> y" then have "y \<sim> x" ..
    4.56 -  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
    4.57 -qed
    4.58 -
    4.59 -text {*
    4.60 - \medskip The quotient type @{text "'a quot"} consists of all
    4.61 - \emph{equivalence classes} over elements of the base type @{typ 'a}.
    4.62 -*}
    4.63 -
    4.64 -typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
    4.65 -  by blast
    4.66 -
    4.67 -lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    4.68 -  unfolding quot_def by blast
    4.69 -
    4.70 -lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
    4.71 -  unfolding quot_def by blast
    4.72 -
    4.73 -text {*
    4.74 - \medskip Abstracted equivalence classes are the canonical
    4.75 - representation of elements of a quotient type.
    4.76 -*}
    4.77 -
    4.78 -definition
    4.79 -  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
    4.80 -  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
    4.81 -
    4.82 -theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    4.83 -proof (cases A)
    4.84 -  fix R assume R: "A = Abs_quot R"
    4.85 -  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
    4.86 -  with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    4.87 -  then show ?thesis unfolding class_def .
    4.88 -qed
    4.89 -
    4.90 -lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    4.91 -  using quot_exhaust by blast
    4.92 -
    4.93 -
    4.94 -subsection {* Equality on quotients *}
    4.95 -
    4.96 -text {*
    4.97 - Equality of canonical quotient elements coincides with the original
    4.98 - relation.
    4.99 -*}
   4.100 -
   4.101 -theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   4.102 -proof
   4.103 -  assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   4.104 -  show "a \<sim> b"
   4.105 -  proof -
   4.106 -    from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
   4.107 -      by (simp only: class_def Abs_quot_inject quotI)
   4.108 -    moreover have "a \<sim> a" ..
   4.109 -    ultimately have "a \<in> {x. b \<sim> x}" by blast
   4.110 -    then have "b \<sim> a" by blast
   4.111 -    then show ?thesis ..
   4.112 -  qed
   4.113 -next
   4.114 -  assume ab: "a \<sim> b"
   4.115 -  show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   4.116 -  proof -
   4.117 -    have "{x. a \<sim> x} = {x. b \<sim> x}"
   4.118 -    proof (rule Collect_cong)
   4.119 -      fix x show "(a \<sim> x) = (b \<sim> x)"
   4.120 -      proof
   4.121 -        from ab have "b \<sim> a" ..
   4.122 -        also assume "a \<sim> x"
   4.123 -        finally show "b \<sim> x" .
   4.124 -      next
   4.125 -        note ab
   4.126 -        also assume "b \<sim> x"
   4.127 -        finally show "a \<sim> x" .
   4.128 -      qed
   4.129 -    qed
   4.130 -    then show ?thesis by (simp only: class_def)
   4.131 -  qed
   4.132 -qed
   4.133 -
   4.134 -
   4.135 -subsection {* Picking representing elements *}
   4.136 -
   4.137 -definition
   4.138 -  pick :: "'a::equiv quot => 'a" where
   4.139 -  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   4.140 -
   4.141 -theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   4.142 -proof (unfold pick_def)
   4.143 -  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   4.144 -  proof (rule someI2)
   4.145 -    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   4.146 -    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   4.147 -    then have "a \<sim> x" .. then show "x \<sim> a" ..
   4.148 -  qed
   4.149 -qed
   4.150 -
   4.151 -theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
   4.152 -proof (cases A)
   4.153 -  fix a assume a: "A = \<lfloor>a\<rfloor>"
   4.154 -  then have "pick A \<sim> a" by (simp only: pick_equiv)
   4.155 -  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   4.156 -  with a show ?thesis by simp
   4.157 -qed
   4.158 -
   4.159 -text {*
   4.160 - \medskip The following rules support canonical function definitions
   4.161 - on quotient types (with up to two arguments).  Note that the
   4.162 - stripped-down version without additional conditions is sufficient
   4.163 - most of the time.
   4.164 -*}
   4.165 -
   4.166 -theorem quot_cond_function:
   4.167 -  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
   4.168 -    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   4.169 -      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   4.170 -    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   4.171 -  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   4.172 -proof -
   4.173 -  from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   4.174 -  also have "... = g a b"
   4.175 -  proof (rule cong)
   4.176 -    show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
   4.177 -    moreover
   4.178 -    show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
   4.179 -    moreover
   4.180 -    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
   4.181 -    ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
   4.182 -  qed
   4.183 -  finally show ?thesis .
   4.184 -qed
   4.185 -
   4.186 -theorem quot_function:
   4.187 -  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
   4.188 -    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   4.189 -  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   4.190 -  using assms and TrueI
   4.191 -  by (rule quot_cond_function)
   4.192 -
   4.193 -theorem quot_function':
   4.194 -  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   4.195 -    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
   4.196 -    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   4.197 -  by (rule quot_function) (simp_all only: quot_equality)
   4.198 -
   4.199 -end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Quotient_Type.thy	Wed Feb 10 19:37:34 2010 +0100
     5.3 @@ -0,0 +1,196 @@
     5.4 +(*  Title:      HOL/Library/Quotient_Type.thy
     5.5 +    Author:     Markus Wenzel, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* Quotient types *}
     5.9 +
    5.10 +theory Quotient_Type
    5.11 +imports Main
    5.12 +begin
    5.13 +
    5.14 +text {*
    5.15 + We introduce the notion of quotient types over equivalence relations
    5.16 + via type classes.
    5.17 +*}
    5.18 +
    5.19 +subsection {* Equivalence relations and quotient types *}
    5.20 +
    5.21 +text {*
    5.22 + \medskip Type class @{text equiv} models equivalence relations @{text
    5.23 + "\<sim> :: 'a => 'a => bool"}.
    5.24 +*}
    5.25 +
    5.26 +class eqv =
    5.27 +  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    5.28 +
    5.29 +class equiv = eqv +
    5.30 +  assumes equiv_refl [intro]: "x \<sim> x"
    5.31 +  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    5.32 +  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    5.33 +
    5.34 +lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    5.35 +proof -
    5.36 +  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
    5.37 +    by (rule contrapos_nn) (rule equiv_sym)
    5.38 +qed
    5.39 +
    5.40 +lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
    5.41 +proof -
    5.42 +  assume "\<not> (x \<sim> y)" and "y \<sim> z"
    5.43 +  show "\<not> (x \<sim> z)"
    5.44 +  proof
    5.45 +    assume "x \<sim> z"
    5.46 +    also from `y \<sim> z` have "z \<sim> y" ..
    5.47 +    finally have "x \<sim> y" .
    5.48 +    with `\<not> (x \<sim> y)` show False by contradiction
    5.49 +  qed
    5.50 +qed
    5.51 +
    5.52 +lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
    5.53 +proof -
    5.54 +  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
    5.55 +  also assume "x \<sim> y" then have "y \<sim> x" ..
    5.56 +  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
    5.57 +qed
    5.58 +
    5.59 +text {*
    5.60 + \medskip The quotient type @{text "'a quot"} consists of all
    5.61 + \emph{equivalence classes} over elements of the base type @{typ 'a}.
    5.62 +*}
    5.63 +
    5.64 +typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
    5.65 +  by blast
    5.66 +
    5.67 +lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    5.68 +  unfolding quot_def by blast
    5.69 +
    5.70 +lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
    5.71 +  unfolding quot_def by blast
    5.72 +
    5.73 +text {*
    5.74 + \medskip Abstracted equivalence classes are the canonical
    5.75 + representation of elements of a quotient type.
    5.76 +*}
    5.77 +
    5.78 +definition
    5.79 +  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
    5.80 +  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
    5.81 +
    5.82 +theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    5.83 +proof (cases A)
    5.84 +  fix R assume R: "A = Abs_quot R"
    5.85 +  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
    5.86 +  with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    5.87 +  then show ?thesis unfolding class_def .
    5.88 +qed
    5.89 +
    5.90 +lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    5.91 +  using quot_exhaust by blast
    5.92 +
    5.93 +
    5.94 +subsection {* Equality on quotients *}
    5.95 +
    5.96 +text {*
    5.97 + Equality of canonical quotient elements coincides with the original
    5.98 + relation.
    5.99 +*}
   5.100 +
   5.101 +theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   5.102 +proof
   5.103 +  assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   5.104 +  show "a \<sim> b"
   5.105 +  proof -
   5.106 +    from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
   5.107 +      by (simp only: class_def Abs_quot_inject quotI)
   5.108 +    moreover have "a \<sim> a" ..
   5.109 +    ultimately have "a \<in> {x. b \<sim> x}" by blast
   5.110 +    then have "b \<sim> a" by blast
   5.111 +    then show ?thesis ..
   5.112 +  qed
   5.113 +next
   5.114 +  assume ab: "a \<sim> b"
   5.115 +  show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   5.116 +  proof -
   5.117 +    have "{x. a \<sim> x} = {x. b \<sim> x}"
   5.118 +    proof (rule Collect_cong)
   5.119 +      fix x show "(a \<sim> x) = (b \<sim> x)"
   5.120 +      proof
   5.121 +        from ab have "b \<sim> a" ..
   5.122 +        also assume "a \<sim> x"
   5.123 +        finally show "b \<sim> x" .
   5.124 +      next
   5.125 +        note ab
   5.126 +        also assume "b \<sim> x"
   5.127 +        finally show "a \<sim> x" .
   5.128 +      qed
   5.129 +    qed
   5.130 +    then show ?thesis by (simp only: class_def)
   5.131 +  qed
   5.132 +qed
   5.133 +
   5.134 +
   5.135 +subsection {* Picking representing elements *}
   5.136 +
   5.137 +definition
   5.138 +  pick :: "'a::equiv quot => 'a" where
   5.139 +  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   5.140 +
   5.141 +theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   5.142 +proof (unfold pick_def)
   5.143 +  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   5.144 +  proof (rule someI2)
   5.145 +    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   5.146 +    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   5.147 +    then have "a \<sim> x" .. then show "x \<sim> a" ..
   5.148 +  qed
   5.149 +qed
   5.150 +
   5.151 +theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
   5.152 +proof (cases A)
   5.153 +  fix a assume a: "A = \<lfloor>a\<rfloor>"
   5.154 +  then have "pick A \<sim> a" by (simp only: pick_equiv)
   5.155 +  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   5.156 +  with a show ?thesis by simp
   5.157 +qed
   5.158 +
   5.159 +text {*
   5.160 + \medskip The following rules support canonical function definitions
   5.161 + on quotient types (with up to two arguments).  Note that the
   5.162 + stripped-down version without additional conditions is sufficient
   5.163 + most of the time.
   5.164 +*}
   5.165 +
   5.166 +theorem quot_cond_function:
   5.167 +  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
   5.168 +    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   5.169 +      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   5.170 +    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   5.171 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   5.172 +proof -
   5.173 +  from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   5.174 +  also have "... = g a b"
   5.175 +  proof (rule cong)
   5.176 +    show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
   5.177 +    moreover
   5.178 +    show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
   5.179 +    moreover
   5.180 +    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
   5.181 +    ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
   5.182 +  qed
   5.183 +  finally show ?thesis .
   5.184 +qed
   5.185 +
   5.186 +theorem quot_function:
   5.187 +  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
   5.188 +    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   5.189 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   5.190 +  using assms and TrueI
   5.191 +  by (rule quot_cond_function)
   5.192 +
   5.193 +theorem quot_function':
   5.194 +  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   5.195 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
   5.196 +    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   5.197 +  by (rule quot_function) (simp_all only: quot_equality)
   5.198 +
   5.199 +end