src/HOL/ex/PER.thy
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 12338 de0f4a63baa5
child 16417 9bc16273c2d4
permissions -rw-r--r--
keep a copy of generated files in repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/PER.thy
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     3
    Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     4
*)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     5
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     6
header {* Partial equivalence relations *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     7
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     8
theory PER = Main:
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
     9
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    10
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    11
  Higher-order quotients are defined over partial equivalence
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    12
  relations (PERs) instead of total ones.  We provide axiomatic type
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    13
  classes @{text "equiv < partial_equiv"} and a type constructor
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    14
  @{text "'a quot"} with basic operations.  This development is based
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    15
  on:
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    16
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    17
  Oscar Slotosch: \emph{Higher Order Quotients and their
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    18
  Implementation in Isabelle HOL.}  Elsa L. Gunter and Amy Felty,
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    19
  editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    20
  Springer LNCS 1275, 1997.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    21
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    22
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    23
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    24
subsection {* Partial equivalence *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    25
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    26
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    27
  Type class @{text partial_equiv} models partial equivalence
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    28
  relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    29
  bool"} relation, which is required to be symmetric and transitive,
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    30
  but not necessarily reflexive.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    31
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    32
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    33
consts
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    34
  eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    35
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    36
axclass partial_equiv < type
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    37
  partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    38
  partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    39
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    40
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    41
  \medskip The domain of a partial equivalence relation is the set of
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    42
  reflexive elements.  Due to symmetry and transitivity this
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    43
  characterizes exactly those elements that are connected with
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    44
  \emph{any} other one.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    45
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    46
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    47
constdefs
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    48
  domain :: "'a::partial_equiv set"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    49
  "domain == {x. x \<sim> x}"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    50
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    51
lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    52
  by (unfold domain_def) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    53
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    54
lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    55
  by (unfold domain_def) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    56
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    57
theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    58
proof
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    59
  assume xy: "x \<sim> y"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    60
  also from xy have "y \<sim> x" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    61
  finally show "x \<sim> x" .
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    62
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    63
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    64
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    65
subsection {* Equivalence on function spaces *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    66
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    67
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    68
  The @{text \<sim>} relation is lifted to function spaces.  It is
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    69
  important to note that this is \emph{not} the direct product, but a
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    70
  structural one corresponding to the congruence property.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    71
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    72
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    73
defs (overloaded)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    74
  eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    75
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    76
lemma partial_equiv_funI [intro?]:
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    77
    "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    78
  by (unfold eqv_fun_def) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    79
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    80
lemma partial_equiv_funD [dest?]:
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    81
    "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    82
  by (unfold eqv_fun_def) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    83
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    84
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    85
  The class of partial equivalence relations is closed under function
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
    86
  spaces (in \emph{both} argument positions).
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    87
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    88
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    89
instance fun :: (partial_equiv, partial_equiv) partial_equiv
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    90
proof
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    91
  fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    92
  assume fg: "f \<sim> g"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    93
  show "g \<sim> f"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    94
  proof
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    95
    fix x y :: 'a
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    96
    assume x: "x \<in> domain" and y: "y \<in> domain"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    97
    assume "x \<sim> y" hence "y \<sim> x" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    98
    with fg y x have "f y \<sim> g x" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
    99
    thus "g x \<sim> f y" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   100
  qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   101
  assume gh: "g \<sim> h"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   102
  show "f \<sim> h"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   103
  proof
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   104
    fix x y :: 'a
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   105
    assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   106
    with fg have "f x \<sim> g y" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   107
    also from y have "y \<sim> y" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   108
    with gh y y have "g y \<sim> h y" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   109
    finally show "f x \<sim> h y" .
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   110
  qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   111
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   112
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   113
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   114
subsection {* Total equivalence *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   115
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   116
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   117
  The class of total equivalence relations on top of PERs.  It
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   118
  coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   119
  :: 'a => 'a => bool"} is required to be reflexive, transitive and
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   120
  symmetric.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   121
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   122
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   123
axclass equiv < partial_equiv
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   124
  eqv_refl [intro]: "x \<sim> x"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   125
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   126
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   127
  On total equivalences all elements are reflexive, and congruence
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   128
  holds unconditionally.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   129
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   130
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   131
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   132
proof
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   133
  show "x \<sim> x" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   134
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   135
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   136
theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   137
proof -
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   138
  assume "f \<sim> g"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   139
  moreover have "x \<in> domain" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   140
  moreover have "y \<in> domain" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   141
  moreover assume "x \<sim> y"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   142
  ultimately show ?thesis ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   143
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   144
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   145
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   146
subsection {* Quotient types *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   147
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   148
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   149
  The quotient type @{text "'a quot"} consists of all
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   150
  \emph{equivalence classes} over elements of the base type @{typ 'a}.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   151
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   152
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   153
typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   154
  by blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   155
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   156
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   157
  by (unfold quot_def) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   158
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   159
lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   160
  by (unfold quot_def) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   161
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   162
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   163
  \medskip Abstracted equivalence classes are the canonical
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   164
  representation of elements of a quotient type.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   165
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   166
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   167
constdefs
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   168
  eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>")
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   169
  "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   170
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   171
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   172
proof (cases A)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   173
  fix R assume R: "A = Abs_quot R"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   174
  assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   175
  with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   176
  thus ?thesis by (unfold eqv_class_def)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   177
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   178
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   179
lemma quot_cases [case_names rep, cases type: quot]:
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   180
    "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   181
  by (insert quot_rep) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   182
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   183
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   184
subsection {* Equality on quotients *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   185
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   186
text {*
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   187
  Equality of canonical quotient elements corresponds to the original
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 10352
diff changeset
   188
  relation as follows.
10352
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   189
*}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   190
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   191
theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   192
proof -
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   193
  assume ab: "a \<sim> b"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   194
  have "{x. a \<sim> x} = {x. b \<sim> x}"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   195
  proof (rule Collect_cong)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   196
    fix x show "(a \<sim> x) = (b \<sim> x)"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   197
    proof
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   198
      from ab have "b \<sim> a" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   199
      also assume "a \<sim> x"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   200
      finally show "b \<sim> x" .
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   201
    next
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   202
      note ab
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   203
      also assume "b \<sim> x"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   204
      finally show "a \<sim> x" .
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   205
    qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   206
  qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   207
  thus ?thesis by (simp only: eqv_class_def)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   208
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   209
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   210
theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   211
proof (unfold eqv_class_def)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   212
  assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   213
  hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   214
  moreover assume "a \<in> domain" hence "a \<sim> a" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   215
  ultimately have "a \<in> {x. b \<sim> x}" by blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   216
  hence "b \<sim> a" by blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   217
  thus "a \<sim> b" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   218
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   219
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   220
theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   221
proof (rule eqv_class_eqD')
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   222
  show "a \<in> domain" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   223
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   224
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   225
lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   226
  by (insert eqv_class_eqI eqv_class_eqD') blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   227
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   228
lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   229
  by (insert eqv_class_eqI eqv_class_eqD) blast
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   230
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   231
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   232
subsection {* Picking representing elements *}
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   233
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   234
constdefs
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   235
  pick :: "'a::partial_equiv quot => 'a"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   236
  "pick A == SOME a. A = \<lfloor>a\<rfloor>"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   237
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   238
theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   239
proof (unfold pick_def)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   240
  assume a: "a \<in> domain"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   241
  show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   242
  proof (rule someI2)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   243
    show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   244
    fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   245
    hence "a \<sim> x" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   246
    thus "x \<sim> a" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   247
  qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   248
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   249
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   250
theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   251
proof (rule pick_eqv')
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   252
  show "a \<in> domain" ..
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   253
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   254
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   255
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   256
proof (cases A)
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   257
  fix a assume a: "A = \<lfloor>a\<rfloor>"
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   258
  hence "pick A \<sim> a" by simp
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   259
  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   260
  with a show ?thesis by simp
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   261
qed
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   262
638e1fc6ca74 Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff changeset
   263
end