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