From 2a2e7bcea8900ef4f90ebf55fd1c82faab131b83 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 18 Aug 2010 16:59:02 +0000 Subject: Another test file --- isar/ex/PER.thy | 269 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 269 insertions(+) create mode 100644 isar/ex/PER.thy (limited to 'isar') diff --git a/isar/ex/PER.thy b/isar/ex/PER.thy new file mode 100644 index 00000000..7f59c742 --- /dev/null +++ b/isar/ex/PER.thy @@ -0,0 +1,269 @@ +(********** + This file is copied from Isabelle2009-2. + It has been beautified with Tokens \ Replace Shortcuts + **********) + +(* Title: HOL/ex/PER.thy + Author: Oscar Slotosch and Markus Wenzel, TU Muenchen +*) + +header {* Partial equivalence relations *} + +theory PER imports Main begin + +text {* + Higher-order quotients are defined over partial equivalence + relations (PERs) instead of total ones. We provide axiomatic type + classes @{text "equiv < partial_equiv"} and a type constructor + @{text "'a quot"} with basic operations. This development is based + on: + + Oscar Slotosch: \emph{Higher Order Quotients and their + Implementation in Isabelle HOL.} Elsa L. Gunter and Amy Felty, + editors, Theorem Proving in Higher Order Logics: TPHOLs '97, + Springer LNCS 1275, 1997. +*} + + +subsection {* Partial equivalence *} + +text {* + Type class @{text partial_equiv} models partial equivalence + relations (PERs) using the polymorphic @{text "\ :: 'a \ 'a \ + bool"} relation, which is required to be symmetric and transitive, + but not necessarily reflexive. +*} + +class partial_equiv = + fixes eqv :: "'a \ 'a \ bool" (infixl "\" 50) + assumes partial_equiv_sym [elim?]: "x \ y \ y \ x" + assumes partial_equiv_trans [trans]: "x \ y \ y \ z \ x \ z" + +text {* + \medskip The domain of a partial equivalence relation is the set of + reflexive elements. Due to symmetry and transitivity this + characterizes exactly those elements that are connected with + \emph{any} other one. +*} + +definition + "domain" :: "'a::partial_equiv set" where + "domain = {x. x \ x}" + +lemma domainI [intro]: "x \ x \ x \ domain" + unfolding domain_def by blast + +lemma domainD [dest]: "x \ domain \ x \ x" + unfolding domain_def by blast + +theorem domainI' [elim?]: "x \ y \ x \ domain" +proof + assume xy: "x \ y" + also from xy have "y \ x" .. + finally show "x \ x" . +qed + + +subsection {* Equivalence on function spaces *} + +text {* + The @{text \} relation is lifted to function spaces. It is + important to note that this is \emph{not} the direct product, but a + structural one corresponding to the congruence property. +*} + +instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv +begin + +definition + eqv_fun_def: "f \ g \ \x \ domain. \y \ domain. x \ y \ f x \ g y" + +lemma partial_equiv_funI [intro?]: + "(\x y. x \ domain \ y \ domain \ x \ y \ f x \ g y) \ f \ g" + unfolding eqv_fun_def by blast + +lemma partial_equiv_funD [dest?]: + "f \ g \ x \ domain \ y \ domain \ x \ y \ f x \ g y" + unfolding eqv_fun_def by blast + +text {* + The class of partial equivalence relations is closed under function + spaces (in \emph{both} argument positions). +*} + +instance proof + fix f g h :: "'a::partial_equiv \ 'b::partial_equiv" + assume fg: "f \ g" + show "g \ f" + proof + fix x y :: 'a + assume x: "x \ domain" and y: "y \ domain" + assume "x \ y" then have "y \ x" .. + with fg y x have "f y \ g x" .. + then show "g x \ f y" .. + qed + assume gh: "g \ h" + show "f \ h" + proof + fix x y :: 'a + assume x: "x \ domain" and y: "y \ domain" and "x \ y" + with fg have "f x \ g y" .. + also from y have "y \ y" .. + with gh y y have "g y \ h y" .. + finally show "f x \ h y" . + qed +qed + +end + + +subsection {* Total equivalence *} + +text {* + The class of total equivalence relations on top of PERs. It + coincides with the standard notion of equivalence, i.e.\ @{text "\ + :: 'a \ 'a \ bool"} is required to be reflexive, transitive and + symmetric. +*} + +class equiv = + assumes eqv_refl [intro]: "x \ x" + +text {* + On total equivalences all elements are reflexive, and congruence + holds unconditionally. +*} + +theorem equiv_domain [intro]: "(x::'a::equiv) \ domain" +proof + show "x \ x" .. +qed + +theorem equiv_cong [dest?]: "f \ g \ x \ y \ f x \ g (y::'a::equiv)" +proof - + assume "f \ g" + moreover have "x \ domain" .. + moreover have "y \ domain" .. + moreover assume "x \ y" + ultimately show ?thesis .. +qed + + +subsection {* Quotient types *} + +text {* + The quotient type @{text "'a quot"} consists of all + \emph{equivalence classes} over elements of the base type @{typ 'a}. +*} + +typedef 'a quot = "{{x. a \ x}| a::'a::partial_equiv. True}" + by blast + +lemma quotI [intro]: "{x. a \ x} \ quot" + unfolding quot_def by blast + +lemma quotE [elim]: "R \ quot \ (\a. R = {x. a \ x} \ C) \ C" + unfolding quot_def by blast + +text {* + \medskip Abstracted equivalence classes are the canonical + representation of elements of a quotient type. +*} + +definition + eqv_class :: "('a::partial_equiv) \ 'a quot" ("\_\") where + "\a\ = Abs_quot {x. a \ x}" + +theorem quot_rep: "\a. A = \a\" +proof (cases A) + fix R assume R: "A = Abs_quot R" + assume "R \ quot" then have "\a. R = {x. a \ x}" by blast + with R have "\a. A = Abs_quot {x. a \ x}" by blast + then show ?thesis by (unfold eqv_class_def) +qed + +lemma quot_cases [cases type: quot]: + obtains (rep) a where "A = \a\" + using quot_rep by blast + + +subsection {* Equality on quotients *} + +text {* + Equality of canonical quotient elements corresponds to the original + relation as follows. +*} + +theorem eqv_class_eqI [intro]: "a \ b \ \a\ = \b\" +proof - + assume ab: "a \ b" + have "{x. a \ x} = {x. b \ x}" + proof (rule Collect_cong) + fix x show "(a \ x) = (b \ x)" + proof + from ab have "b \ a" .. + also assume "a \ x" + finally show "b \ x" . + next + note ab + also assume "b \ x" + finally show "a \ x" . + qed + qed + then show ?thesis by (simp only: eqv_class_def) +qed + +theorem eqv_class_eqD' [dest?]: "\a\ = \b\ \ a \ domain \ a \ b" +proof (unfold eqv_class_def) + assume "Abs_quot {x. a \ x} = Abs_quot {x. b \ x}" + then have "{x. a \ x} = {x. b \ x}" by (simp only: Abs_quot_inject quotI) + moreover assume "a \ domain" then have "a \ a" .. + ultimately have "a \ {x. b \ x}" by blast + then have "b \ a" by blast + then show "a \ b" .. +qed + +theorem eqv_class_eqD [dest?]: "\a\ = \b\ \ a \ (b::'a::equiv)" +proof (rule eqv_class_eqD') + show "a \ domain" .. +qed + +lemma eqv_class_eq' [simp]: "a \ domain \ (\a\ = \b\) = (a \ b)" + using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl) + +lemma eqv_class_eq [simp]: "(\a\ = \b\) = (a \ (b::'a::equiv))" + using eqv_class_eqI eqv_class_eqD by blast + + +subsection {* Picking representing elements *} + +definition + pick :: "'a::partial_equiv quot \ 'a" where + "pick A = (SOME a. A = \a\)" + +theorem pick_eqv' [intro?, simp]: "a \ domain \ pick \a\ \ a" +proof (unfold pick_def) + assume a: "a \ domain" + show "(SOME x. \a\ = \x\) \ a" + proof (rule someI2) + show "\a\ = \a\" .. + fix x assume "\a\ = \x\" + from this and a have "a \ x" .. + then show "x \ a" .. + qed +qed + +theorem pick_eqv [intro, simp]: "pick \a\ \ (a::'a::equiv)" +proof (rule pick_eqv') + show "a \ domain" .. +qed + +theorem pick_inverse: "\pick A\ = (A::'a::equiv quot)" +proof (cases A) + fix a assume a: "A = \a\" + then have "pick A \ a" by simp + then have "\pick A\ = \a\" by simp + with a show ?thesis by simp +qed + +end -- cgit v1.2.3