src/HOL/Library/Quotient_Type.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69593 3dda49e08b9d
permissions -rw-r--r--
improved code equations taken over from AFP
     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 \<open>equiv\<close> models equivalence relations
    18   \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.\<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 \<open>'a quot\<close> consists of all \emph{equivalence
    61   classes} over elements of the base type \<^typ>\<open>'a\<close>.\<close>
    62 
    63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
    64 
    65 typedef (overloaded) '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