src/HOL/Library/Quotient_Type.thy
 author nipkow Tue Sep 22 14:31:22 2015 +0200 (2015-09-22) changeset 61225 1a690dce8cfc parent 59192 a1d6d6db781b child 61260 e6f03fae14d5 permissions -rw-r--r--
tuned references
     1 (*  Title:      HOL/Library/Quotient_Type.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 section \<open>Quotient types\<close>

     6

     7 theory Quotient_Type

     8 imports Main

     9 begin

    10

    11 text \<open>We introduce the notion of quotient types over equivalence relations

    12   via type classes.\<close>

    13

    14

    15 subsection \<open>Equivalence relations and quotient types\<close>

    16

    17 text \<open>Type class @{text equiv} models equivalence relations

    18   @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>

    19

    20 class eqv =

    21   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)

    22

    23 class equiv = eqv +

    24   assumes equiv_refl [intro]: "x \<sim> x"

    25     and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"

    26     and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"

    27 begin

    28

    29 lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x"

    30 proof -

    31   assume "\<not> x \<sim> y"

    32   then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym)

    33 qed

    34

    35 lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"

    36 proof -

    37   assume "\<not> x \<sim> y" and "y \<sim> z"

    38   show "\<not> x \<sim> z"

    39   proof

    40     assume "x \<sim> z"

    41     also from \<open>y \<sim> z\<close> have "z \<sim> y" ..

    42     finally have "x \<sim> y" .

    43     with \<open>\<not> x \<sim> y\<close> show False by contradiction

    44   qed

    45 qed

    46

    47 lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"

    48 proof -

    49   assume "\<not> y \<sim> z"

    50   then have "\<not> z \<sim> y" ..

    51   also

    52   assume "x \<sim> y"

    53   then have "y \<sim> x" ..

    54   finally have "\<not> z \<sim> x" .

    55   then show "\<not> x \<sim> z" ..

    56 qed

    57

    58 end

    59

    60 text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence

    61   classes} over elements of the base type @{typ 'a}.\<close>

    62

    63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"

    64

    65 typedef 'a quot = "quot :: 'a::eqv set set"

    66   unfolding quot_def by blast

    67

    68 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"

    69   unfolding quot_def by blast

    70

    71 lemma quotE [elim]:

    72   assumes "R \<in> quot"

    73   obtains a where "R = {x. a \<sim> x}"

    74   using assms unfolding quot_def by blast

    75

    76 text \<open>Abstracted equivalence classes are the canonical representation of

    77   elements of a quotient type.\<close>

    78

    79 definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  ("\<lfloor>_\<rfloor>")

    80   where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"

    81

    82 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"

    83 proof (cases A)

    84   fix R

    85   assume R: "A = Abs_quot R"

    86   assume "R \<in> quot"

    87   then have "\<exists>a. R = {x. a \<sim> x}" by blast

    88   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast

    89   then show ?thesis unfolding class_def .

    90 qed

    91

    92 lemma quot_cases [cases type: quot]:

    93   obtains a where "A = \<lfloor>a\<rfloor>"

    94   using quot_exhaust by blast

    95

    96

    97 subsection \<open>Equality on quotients\<close>

    98

    99 text \<open>Equality of canonical quotient elements coincides with the original

   100   relation.\<close>

   101

   102 theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"

   103 proof

   104   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"

   105   show "a \<sim> b"

   106   proof -

   107     from eq have "{x. a \<sim> x} = {x. b \<sim> x}"

   108       by (simp only: class_def Abs_quot_inject quotI)

   109     moreover have "a \<sim> a" ..

   110     ultimately have "a \<in> {x. b \<sim> x}" by blast

   111     then have "b \<sim> a" by blast

   112     then show ?thesis ..

   113   qed

   114 next

   115   assume ab: "a \<sim> b"

   116   show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"

   117   proof -

   118     have "{x. a \<sim> x} = {x. b \<sim> x}"

   119     proof (rule Collect_cong)

   120       fix x show "(a \<sim> x) = (b \<sim> x)"

   121       proof

   122         from ab have "b \<sim> a" ..

   123         also assume "a \<sim> x"

   124         finally show "b \<sim> x" .

   125       next

   126         note ab

   127         also assume "b \<sim> x"

   128         finally show "a \<sim> x" .

   129       qed

   130     qed

   131     then show ?thesis by (simp only: class_def)

   132   qed

   133 qed

   134

   135

   136 subsection \<open>Picking representing elements\<close>

   137

   138 definition pick :: "'a::equiv quot \<Rightarrow> 'a"

   139   where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"

   140

   141 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"

   142 proof (unfold pick_def)

   143   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"

   144   proof (rule someI2)

   145     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..

   146     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"

   147     then have "a \<sim> x" ..

   148     then show "x \<sim> a" ..

   149   qed

   150 qed

   151

   152 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"

   153 proof (cases A)

   154   fix a assume a: "A = \<lfloor>a\<rfloor>"

   155   then have "pick A \<sim> a" by (simp only: pick_equiv)

   156   then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..

   157   with a show ?thesis by simp

   158 qed

   159

   160 text \<open>The following rules support canonical function definitions on quotient

   161   types (with up to two arguments). Note that the stripped-down version

   162   without additional conditions is sufficient most of the time.\<close>

   163

   164 theorem quot_cond_function:

   165   assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)"

   166     and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>

   167       \<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"

   168     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"

   169   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   170 proof -

   171   from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)

   172   also have "... = g a b"

   173   proof (rule cong)

   174     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..

   175     moreover

   176     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..

   177     moreover

   178     show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)

   179     ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)

   180   qed

   181   finally show ?thesis .

   182 qed

   183

   184 theorem quot_function:

   185   assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)"

   186     and "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"

   187   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   188   using assms and TrueI

   189   by (rule quot_cond_function)

   190

   191 theorem quot_function':

   192   "(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow>

   193     (\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow>

   194     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"

   195   by (rule quot_function) (simp_all only: quot_equality)

   196

   197 end