src/HOL/ex/PER.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 35315 fbdc860d87a3 child 45694 4a8743618257 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
     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