src/HOL/Library/Quotient_Type.thy
changeset 35100 53754ec7360b
parent 30738 0842e906300c
child 45694 4a8743618257
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Quotient_Type.thy	Wed Feb 10 19:37:34 2010 +0100
     1.3 @@ -0,0 +1,196 @@
     1.4 +(*  Title:      HOL/Library/Quotient_Type.thy
     1.5 +    Author:     Markus Wenzel, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Quotient types *}
     1.9 +
    1.10 +theory Quotient_Type
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 + We introduce the notion of quotient types over equivalence relations
    1.16 + via type classes.
    1.17 +*}
    1.18 +
    1.19 +subsection {* Equivalence relations and quotient types *}
    1.20 +
    1.21 +text {*
    1.22 + \medskip Type class @{text equiv} models equivalence relations @{text
    1.23 + "\<sim> :: 'a => 'a => bool"}.
    1.24 +*}
    1.25 +
    1.26 +class eqv =
    1.27 +  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    1.28 +
    1.29 +class equiv = eqv +
    1.30 +  assumes equiv_refl [intro]: "x \<sim> x"
    1.31 +  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    1.32 +  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    1.33 +
    1.34 +lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    1.35 +proof -
    1.36 +  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
    1.37 +    by (rule contrapos_nn) (rule equiv_sym)
    1.38 +qed
    1.39 +
    1.40 +lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
    1.41 +proof -
    1.42 +  assume "\<not> (x \<sim> y)" and "y \<sim> z"
    1.43 +  show "\<not> (x \<sim> z)"
    1.44 +  proof
    1.45 +    assume "x \<sim> z"
    1.46 +    also from `y \<sim> z` have "z \<sim> y" ..
    1.47 +    finally have "x \<sim> y" .
    1.48 +    with `\<not> (x \<sim> y)` show False by contradiction
    1.49 +  qed
    1.50 +qed
    1.51 +
    1.52 +lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
    1.53 +proof -
    1.54 +  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
    1.55 +  also assume "x \<sim> y" then have "y \<sim> x" ..
    1.56 +  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
    1.57 +qed
    1.58 +
    1.59 +text {*
    1.60 + \medskip The quotient type @{text "'a quot"} consists of all
    1.61 + \emph{equivalence classes} over elements of the base type @{typ 'a}.
    1.62 +*}
    1.63 +
    1.64 +typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
    1.65 +  by blast
    1.66 +
    1.67 +lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    1.68 +  unfolding quot_def by blast
    1.69 +
    1.70 +lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
    1.71 +  unfolding quot_def by blast
    1.72 +
    1.73 +text {*
    1.74 + \medskip Abstracted equivalence classes are the canonical
    1.75 + representation of elements of a quotient type.
    1.76 +*}
    1.77 +
    1.78 +definition
    1.79 +  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
    1.80 +  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
    1.81 +
    1.82 +theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    1.83 +proof (cases A)
    1.84 +  fix R assume R: "A = Abs_quot R"
    1.85 +  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
    1.86 +  with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    1.87 +  then show ?thesis unfolding class_def .
    1.88 +qed
    1.89 +
    1.90 +lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    1.91 +  using quot_exhaust by blast
    1.92 +
    1.93 +
    1.94 +subsection {* Equality on quotients *}
    1.95 +
    1.96 +text {*
    1.97 + Equality of canonical quotient elements coincides with the original
    1.98 + relation.
    1.99 +*}
   1.100 +
   1.101 +theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   1.102 +proof
   1.103 +  assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   1.104 +  show "a \<sim> b"
   1.105 +  proof -
   1.106 +    from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
   1.107 +      by (simp only: class_def Abs_quot_inject quotI)
   1.108 +    moreover have "a \<sim> a" ..
   1.109 +    ultimately have "a \<in> {x. b \<sim> x}" by blast
   1.110 +    then have "b \<sim> a" by blast
   1.111 +    then show ?thesis ..
   1.112 +  qed
   1.113 +next
   1.114 +  assume ab: "a \<sim> b"
   1.115 +  show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   1.116 +  proof -
   1.117 +    have "{x. a \<sim> x} = {x. b \<sim> x}"
   1.118 +    proof (rule Collect_cong)
   1.119 +      fix x show "(a \<sim> x) = (b \<sim> x)"
   1.120 +      proof
   1.121 +        from ab have "b \<sim> a" ..
   1.122 +        also assume "a \<sim> x"
   1.123 +        finally show "b \<sim> x" .
   1.124 +      next
   1.125 +        note ab
   1.126 +        also assume "b \<sim> x"
   1.127 +        finally show "a \<sim> x" .
   1.128 +      qed
   1.129 +    qed
   1.130 +    then show ?thesis by (simp only: class_def)
   1.131 +  qed
   1.132 +qed
   1.133 +
   1.134 +
   1.135 +subsection {* Picking representing elements *}
   1.136 +
   1.137 +definition
   1.138 +  pick :: "'a::equiv quot => 'a" where
   1.139 +  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   1.140 +
   1.141 +theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   1.142 +proof (unfold pick_def)
   1.143 +  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   1.144 +  proof (rule someI2)
   1.145 +    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   1.146 +    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   1.147 +    then have "a \<sim> x" .. then show "x \<sim> a" ..
   1.148 +  qed
   1.149 +qed
   1.150 +
   1.151 +theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
   1.152 +proof (cases A)
   1.153 +  fix a assume a: "A = \<lfloor>a\<rfloor>"
   1.154 +  then have "pick A \<sim> a" by (simp only: pick_equiv)
   1.155 +  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   1.156 +  with a show ?thesis by simp
   1.157 +qed
   1.158 +
   1.159 +text {*
   1.160 + \medskip The following rules support canonical function definitions
   1.161 + on quotient types (with up to two arguments).  Note that the
   1.162 + stripped-down version without additional conditions is sufficient
   1.163 + most of the time.
   1.164 +*}
   1.165 +
   1.166 +theorem quot_cond_function:
   1.167 +  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
   1.168 +    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   1.169 +      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   1.170 +    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   1.171 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   1.172 +proof -
   1.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:)
   1.174 +  also have "... = g a b"
   1.175 +  proof (rule cong)
   1.176 +    show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
   1.177 +    moreover
   1.178 +    show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
   1.179 +    moreover
   1.180 +    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
   1.181 +    ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
   1.182 +  qed
   1.183 +  finally show ?thesis .
   1.184 +qed
   1.185 +
   1.186 +theorem quot_function:
   1.187 +  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
   1.188 +    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   1.189 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   1.190 +  using assms and TrueI
   1.191 +  by (rule quot_cond_function)
   1.192 +
   1.193 +theorem quot_function':
   1.194 +  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   1.195 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
   1.196 +    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   1.197 +  by (rule quot_function) (simp_all only: quot_equality)
   1.198 +
   1.199 +end