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