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