src/HOL/Library/Quotient.thy
author wenzelm
Wed, 18 Oct 2000 23:29:13 +0200
changeset 10250 ca93fe25a84b
child 10278 ea1bf4b6255c
permissions -rw-r--r--
Quotient types;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10250
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Library/Quotient.thy
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     3
    Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     4
*)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     5
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     6
header {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     7
  \title{Quotients}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     8
  \author{Gertrud Bauer and Markus Wenzel}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
     9
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    10
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    11
theory Quotient = Main:
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    12
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    13
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    14
 Higher-order quotients are defined over partial equivalence relations
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    15
 (PERs) instead of total ones.  We provide axiomatic type classes
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    16
 @{text "equiv < partial_equiv"} and a type constructor
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    17
 @{text "'a quot"} with basic operations.  Note that conventional
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    18
 quotient constructions emerge as a special case.  This development is
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    19
 loosely based on \cite{Slotosch:1997}.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    20
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    21
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    22
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    23
subsection {* Equivalence relations *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    24
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    25
subsubsection {* Partial equivalence *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    26
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    27
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    28
 Type class @{text partial_equiv} models partial equivalence relations
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    29
 (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    30
 which is required to be symmetric and transitive, but not necessarily
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    31
 reflexive.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    32
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    33
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    34
consts
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    35
  eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    36
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    37
axclass partial_equiv < "term"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    38
  eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    39
  eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    40
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    41
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    42
 \medskip The domain of a partial equivalence relation is the set of
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    43
 reflexive elements.  Due to symmetry and transitivity this
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    44
 characterizes exactly those elements that are connected with
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    45
 \emph{any} other one.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    46
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    47
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    48
constdefs
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    49
  domain :: "'a::partial_equiv set"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    50
  "domain == {x. x \<sim> x}"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    51
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    52
lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    53
  by (unfold domain_def) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    54
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    55
lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    56
  by (unfold domain_def) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    57
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    58
theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    59
proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    60
  assume xy: "x \<sim> y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    61
  also from xy have "y \<sim> x" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    62
  finally show "x \<sim> x" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    63
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    64
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    65
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    66
subsubsection {* Equivalence on function spaces *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    67
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    68
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    69
 The @{text \<sim>} relation is lifted to function spaces.  It is
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    70
 important to note that this is \emph{not} the direct product, but a
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    71
 structural one corresponding to the congruence property.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    72
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    73
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    74
defs (overloaded)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    75
  eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    76
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    77
lemma partial_equiv_funI [intro?]:
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    78
    "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    79
  by (unfold eqv_fun_def) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    80
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    81
lemma partial_equiv_funD [dest?]:
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    82
    "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    83
  by (unfold eqv_fun_def) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    84
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    85
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    86
 The class of partial equivalence relations is closed under function
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    87
 spaces (in \emph{both} argument positions).
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    88
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    89
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    90
instance fun :: (partial_equiv, partial_equiv) partial_equiv
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    91
proof intro_classes
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    92
  fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    93
  assume fg: "f \<sim> g"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    94
  show "g \<sim> f"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    95
  proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    96
    fix x y :: 'a
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    97
    assume x: "x \<in> domain" and y: "y \<in> domain"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    98
    assume "x \<sim> y" hence "y \<sim> x" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
    99
    with fg y x have "f y \<sim> g x" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   100
    thus "g x \<sim> f y" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   101
  qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   102
  assume gh: "g \<sim> h"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   103
  show "f \<sim> h"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   104
  proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   105
    fix x y :: 'a
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   106
    assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   107
    with fg have "f x \<sim> g y" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   108
    also from y have "y \<sim> y" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   109
    with gh y y have "g y \<sim> h y" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   110
    finally show "f x \<sim> h y" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   111
  qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   112
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   113
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   114
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   115
subsubsection {* Total equivalence *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   116
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   117
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   118
 The class of total equivalence relations on top of PERs.  It
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   119
 coincides with the standard notion of equivalence, i.e.\
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   120
 @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   121
 and symmetric.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   122
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   123
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   124
axclass equiv < partial_equiv
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   125
  eqv_refl [intro]: "x \<sim> x"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   126
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   127
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   128
 On total equivalences all elements are reflexive, and congruence
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   129
 holds unconditionally.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   130
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   131
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   132
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   133
proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   134
  show "x \<sim> x" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   135
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   136
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   137
theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   138
proof -
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   139
  assume "f \<sim> g"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   140
  moreover have "x \<in> domain" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   141
  moreover have "y \<in> domain" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   142
  moreover assume "x \<sim> y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   143
  ultimately show ?thesis ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   144
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   145
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   146
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   147
subsection {* Quotient types *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   148
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   149
subsubsection {* General quotients and equivalence classes *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   150
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   151
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   152
 The quotient type @{text "'a quot"} consists of all \emph{equivalence
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   153
 classes} over elements of the base type @{typ 'a}.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   154
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   155
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   156
typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   157
  by blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   158
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   159
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   160
  by (unfold quot_def) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   161
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   162
lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   163
  by (unfold quot_def) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   164
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   165
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   166
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   167
 \medskip Standard properties of type-definitions.\footnote{(FIXME)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   168
 Better incorporate these into the typedef package?}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   169
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   170
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   171
theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   172
proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   173
  assume "Rep_quot x = Rep_quot y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   174
  hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   175
  thus "x = y" by (simp only: Rep_quot_inverse)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   176
next
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   177
  assume "x = y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   178
  thus "Rep_quot x = Rep_quot y" by simp
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   179
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   180
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   181
theorem Abs_quot_inject:
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   182
  "x \<in> quot ==> y \<in> quot ==> (Abs_quot x = Abs_quot y) = (x = y)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   183
proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   184
  assume "Abs_quot x = Abs_quot y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   185
  hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   186
  also assume "x \<in> quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   187
  also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   188
  finally show "x = y" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   189
next
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   190
  assume "x = y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   191
  thus "Abs_quot x = Abs_quot y" by simp
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   192
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   193
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   194
theorem Rep_quot_induct: "y \<in> quot ==> (!!x. P (Rep_quot x)) ==> P y"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   195
proof -
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   196
  assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   197
  also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   198
  finally show "P y" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   199
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   200
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   201
theorem Abs_quot_induct: "(!!y. y \<in> quot ==> P (Abs_quot y)) ==> P x"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   202
proof -
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   203
  assume r: "!!y. y \<in> quot ==> P (Abs_quot y)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   204
  have "Rep_quot x \<in> quot" by (rule Rep_quot)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   205
  hence "P (Abs_quot (Rep_quot x))" by (rule r)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   206
  also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   207
  finally show "P x" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   208
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   209
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   210
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   211
 \medskip Abstracted equivalence classes are the canonical
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   212
 representation of elements of a quotient type.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   213
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   214
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   215
constdefs
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   216
  eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>")
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   217
  "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   218
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   219
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   220
proof (unfold eqv_class_def)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   221
  show "\<exists>a. A = Abs_quot {x. a \<sim> x}"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   222
  proof (induct A rule: Abs_quot_induct)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   223
    fix R assume "R \<in> quot"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   224
    hence "\<exists>a. R = {x. a \<sim> x}" by blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   225
    thus "\<exists>a. Abs_quot R = Abs_quot {x. a \<sim> x}" by blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   226
  qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   227
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   228
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   229
lemma quot_cases [case_names rep, cases type: quot]:
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   230
    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   231
  by (insert quot_rep) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   232
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   233
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   234
subsubsection {* Equality on quotients *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   235
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   236
text {*
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   237
 Equality of canonical quotient elements corresponds to the original
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   238
 relation as follows.
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   239
*}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   240
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   241
theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   242
proof -
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   243
  assume ab: "a \<sim> b"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   244
  have "{x. a \<sim> x} = {x. b \<sim> x}"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   245
  proof (rule Collect_cong)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   246
    fix x show "(a \<sim> x) = (b \<sim> x)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   247
    proof
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   248
      from ab have "b \<sim> a" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   249
      also assume "a \<sim> x"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   250
      finally show "b \<sim> x" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   251
    next
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   252
      note ab
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   253
      also assume "b \<sim> x"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   254
      finally show "a \<sim> x" .
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   255
    qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   256
  qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   257
  thus ?thesis by (simp only: eqv_class_def)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   258
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   259
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   260
theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"  (* FIXME [dest] would cause trouble with blast due to overloading *)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   261
proof (unfold eqv_class_def)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   262
  assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   263
  hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   264
  moreover assume "a \<in> domain" hence "a \<sim> a" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   265
  ultimately have "a \<in> {x. b \<sim> x}" by blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   266
  hence "b \<sim> a" by blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   267
  thus "a \<sim> b" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   268
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   269
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   270
theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"  (* FIXME [dest] would cause trouble with blast due to overloading *)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   271
proof (rule eqv_class_eqD')
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   272
  show "a \<in> domain" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   273
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   274
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   275
lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   276
  by (insert eqv_class_eqI eqv_class_eqD') blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   277
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   278
lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   279
  by (insert eqv_class_eqI eqv_class_eqD) blast
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   280
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   281
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   282
subsubsection {* Picking representing elements *}
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   283
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   284
constdefs
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   285
  pick :: "'a::partial_equiv quot => 'a"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   286
  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   287
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   288
theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   289
proof (unfold pick_def)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   290
  assume a: "a \<in> domain"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   291
  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   292
  proof (rule someI2)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   293
    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   294
    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   295
    hence "a \<sim> x" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   296
    thus "x \<sim> a" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   297
  qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   298
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   299
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   300
theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   301
proof (rule pick_eqv')
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   302
  show "a \<in> domain" ..
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   303
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   304
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   305
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"   (* FIXME tune proof *)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   306
proof (cases A)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   307
  fix a assume a: "A = \<lfloor>a\<rfloor>"
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   308
  hence "pick A \<sim> a" by (simp only: pick_eqv)
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   309
  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   310
  with a show ?thesis by simp
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   311
qed
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   312
ca93fe25a84b Quotient types;
wenzelm
parents:
diff changeset
   313
end