src/HOL/Library/Quotient_Type.thy
author wenzelm
Sun Dec 28 12:37:03 2014 +0100 (2014-12-28)
changeset 59192 a1d6d6db781b
parent 58881 b9556a055632
child 61260 e6f03fae14d5
permissions -rw-r--r--
modernized historic example;
wenzelm@35100
     1
(*  Title:      HOL/Library/Quotient_Type.thy
wenzelm@10483
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10250
     3
*)
wenzelm@10250
     4
wenzelm@59192
     5
section \<open>Quotient types\<close>
wenzelm@10250
     6
wenzelm@35100
     7
theory Quotient_Type
haftmann@30738
     8
imports Main
nipkow@15131
     9
begin
wenzelm@10250
    10
wenzelm@59192
    11
text \<open>We introduce the notion of quotient types over equivalence relations
wenzelm@59192
    12
  via type classes.\<close>
wenzelm@59192
    13
wenzelm@10250
    14
wenzelm@59192
    15
subsection \<open>Equivalence relations and quotient types\<close>
wenzelm@10250
    16
wenzelm@59192
    17
text \<open>Type class @{text equiv} models equivalence relations
wenzelm@59192
    18
  @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>
wenzelm@10250
    19
haftmann@29608
    20
class eqv =
wenzelm@59192
    21
  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)
wenzelm@10250
    22
haftmann@22390
    23
class equiv = eqv +
haftmann@25062
    24
  assumes equiv_refl [intro]: "x \<sim> x"
wenzelm@59192
    25
    and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
wenzelm@59192
    26
    and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
wenzelm@59192
    27
begin
wenzelm@10250
    28
wenzelm@59192
    29
lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x"
wenzelm@10477
    30
proof -
wenzelm@59192
    31
  assume "\<not> x \<sim> y"
wenzelm@59192
    32
  then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym)
wenzelm@10477
    33
qed
wenzelm@10477
    34
wenzelm@59192
    35
lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
wenzelm@10477
    36
proof -
wenzelm@59192
    37
  assume "\<not> x \<sim> y" and "y \<sim> z"
wenzelm@59192
    38
  show "\<not> x \<sim> z"
wenzelm@10477
    39
  proof
wenzelm@10477
    40
    assume "x \<sim> z"
wenzelm@59192
    41
    also from \<open>y \<sim> z\<close> have "z \<sim> y" ..
wenzelm@10477
    42
    finally have "x \<sim> y" .
wenzelm@59192
    43
    with \<open>\<not> x \<sim> y\<close> show False by contradiction
wenzelm@10477
    44
  qed
wenzelm@10477
    45
qed
wenzelm@10477
    46
wenzelm@59192
    47
lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
wenzelm@10477
    48
proof -
wenzelm@59192
    49
  assume "\<not> y \<sim> z"
wenzelm@59192
    50
  then have "\<not> z \<sim> y" ..
wenzelm@59192
    51
  also
wenzelm@59192
    52
  assume "x \<sim> y"
wenzelm@59192
    53
  then have "y \<sim> x" ..
wenzelm@59192
    54
  finally have "\<not> z \<sim> x" .
wenzelm@59192
    55
  then show "\<not> x \<sim> z" ..
wenzelm@10477
    56
qed
wenzelm@10477
    57
wenzelm@59192
    58
end
wenzelm@10250
    59
wenzelm@59192
    60
text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence
wenzelm@59192
    61
  classes} over elements of the base type @{typ 'a}.\<close>
wenzelm@59192
    62
wenzelm@59192
    63
definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
wenzelm@45694
    64
wenzelm@49834
    65
typedef 'a quot = "quot :: 'a::eqv set set"
wenzelm@45694
    66
  unfolding quot_def by blast
wenzelm@10250
    67
wenzelm@10250
    68
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
wenzelm@18730
    69
  unfolding quot_def by blast
wenzelm@10250
    70
wenzelm@59192
    71
lemma quotE [elim]:
wenzelm@59192
    72
  assumes "R \<in> quot"
wenzelm@59192
    73
  obtains a where "R = {x. a \<sim> x}"
wenzelm@59192
    74
  using assms unfolding quot_def by blast
wenzelm@10250
    75
wenzelm@59192
    76
text \<open>Abstracted equivalence classes are the canonical representation of
wenzelm@59192
    77
  elements of a quotient type.\<close>
wenzelm@10250
    78
wenzelm@59192
    79
definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  ("\<lfloor>_\<rfloor>")
wenzelm@59192
    80
  where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
wenzelm@10250
    81
wenzelm@10311
    82
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
wenzelm@10278
    83
proof (cases A)
wenzelm@59192
    84
  fix R
wenzelm@59192
    85
  assume R: "A = Abs_quot R"
wenzelm@59192
    86
  assume "R \<in> quot"
wenzelm@59192
    87
  then have "\<exists>a. R = {x. a \<sim> x}" by blast
wenzelm@10278
    88
  with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
wenzelm@23373
    89
  then show ?thesis unfolding class_def .
wenzelm@10250
    90
qed
wenzelm@10250
    91
wenzelm@59192
    92
lemma quot_cases [cases type: quot]:
wenzelm@59192
    93
  obtains a where "A = \<lfloor>a\<rfloor>"
wenzelm@18730
    94
  using quot_exhaust by blast
wenzelm@10250
    95
wenzelm@10250
    96
wenzelm@59192
    97
subsection \<open>Equality on quotients\<close>
wenzelm@10250
    98
wenzelm@59192
    99
text \<open>Equality of canonical quotient elements coincides with the original
wenzelm@59192
   100
  relation.\<close>
wenzelm@10250
   101
wenzelm@59192
   102
theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"
wenzelm@10285
   103
proof
wenzelm@10285
   104
  assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
wenzelm@10285
   105
  show "a \<sim> b"
wenzelm@10285
   106
  proof -
wenzelm@10285
   107
    from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
wenzelm@10551
   108
      by (simp only: class_def Abs_quot_inject quotI)
wenzelm@10285
   109
    moreover have "a \<sim> a" ..
wenzelm@10285
   110
    ultimately have "a \<in> {x. b \<sim> x}" by blast
wenzelm@23373
   111
    then have "b \<sim> a" by blast
wenzelm@23373
   112
    then show ?thesis ..
wenzelm@10285
   113
  qed
wenzelm@10285
   114
next
wenzelm@10250
   115
  assume ab: "a \<sim> b"
wenzelm@10285
   116
  show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
wenzelm@10285
   117
  proof -
wenzelm@10285
   118
    have "{x. a \<sim> x} = {x. b \<sim> x}"
wenzelm@10285
   119
    proof (rule Collect_cong)
wenzelm@10285
   120
      fix x show "(a \<sim> x) = (b \<sim> x)"
wenzelm@10285
   121
      proof
wenzelm@10285
   122
        from ab have "b \<sim> a" ..
wenzelm@10285
   123
        also assume "a \<sim> x"
wenzelm@10285
   124
        finally show "b \<sim> x" .
wenzelm@10285
   125
      next
wenzelm@10285
   126
        note ab
wenzelm@10285
   127
        also assume "b \<sim> x"
wenzelm@10285
   128
        finally show "a \<sim> x" .
wenzelm@10285
   129
      qed
wenzelm@10250
   130
    qed
wenzelm@23373
   131
    then show ?thesis by (simp only: class_def)
wenzelm@10250
   132
  qed
wenzelm@10250
   133
qed
wenzelm@10250
   134
wenzelm@10250
   135
wenzelm@59192
   136
subsection \<open>Picking representing elements\<close>
wenzelm@10250
   137
wenzelm@59192
   138
definition pick :: "'a::equiv quot \<Rightarrow> 'a"
wenzelm@59192
   139
  where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
wenzelm@10250
   140
wenzelm@10285
   141
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
wenzelm@10250
   142
proof (unfold pick_def)
wenzelm@10250
   143
  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
wenzelm@10250
   144
  proof (rule someI2)
wenzelm@10250
   145
    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
wenzelm@10250
   146
    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
wenzelm@59192
   147
    then have "a \<sim> x" ..
wenzelm@59192
   148
    then show "x \<sim> a" ..
wenzelm@10250
   149
  qed
wenzelm@10250
   150
qed
wenzelm@10250
   151
wenzelm@10483
   152
theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
wenzelm@10250
   153
proof (cases A)
wenzelm@10250
   154
  fix a assume a: "A = \<lfloor>a\<rfloor>"
wenzelm@23373
   155
  then have "pick A \<sim> a" by (simp only: pick_equiv)
wenzelm@23373
   156
  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
wenzelm@10250
   157
  with a show ?thesis by simp
wenzelm@10250
   158
qed
wenzelm@10250
   159
wenzelm@59192
   160
text \<open>The following rules support canonical function definitions on quotient
wenzelm@59192
   161
  types (with up to two arguments). Note that the stripped-down version
wenzelm@59192
   162
  without additional conditions is sufficient most of the time.\<close>
wenzelm@10285
   163
wenzelm@10483
   164
theorem quot_cond_function:
wenzelm@59192
   165
  assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)"
wenzelm@59192
   166
    and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
wenzelm@59192
   167
      \<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"
wenzelm@18372
   168
    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
wenzelm@18372
   169
  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@10473
   170
proof -
wenzelm@18372
   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:)
wenzelm@10505
   172
  also have "... = g a b"
wenzelm@10491
   173
  proof (rule cong)
wenzelm@10483
   174
    show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
wenzelm@10483
   175
    moreover
wenzelm@10483
   176
    show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
wenzelm@10491
   177
    moreover
wenzelm@23373
   178
    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
wenzelm@10491
   179
    ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
wenzelm@10285
   180
  qed
wenzelm@10285
   181
  finally show ?thesis .
wenzelm@10285
   182
qed
wenzelm@10285
   183
wenzelm@10483
   184
theorem quot_function:
wenzelm@59192
   185
  assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)"
wenzelm@59192
   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'"
wenzelm@18372
   187
  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@23394
   188
  using assms and TrueI
wenzelm@18372
   189
  by (rule quot_cond_function)
wenzelm@10285
   190
bauerg@10499
   191
theorem quot_function':
wenzelm@59192
   192
  "(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow>
wenzelm@59192
   193
    (\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow>
bauerg@10499
   194
    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
wenzelm@18372
   195
  by (rule quot_function) (simp_all only: quot_equality)
bauerg@10499
   196
wenzelm@10250
   197
end