diff options
Diffstat (limited to 'isar/ex')
-rw-r--r-- | isar/ex/PER.thy | 269 |
1 files changed, 269 insertions, 0 deletions
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 \<rightarrow> 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 "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> + bool"} relation, which is required to be symmetric and transitive, + but not necessarily reflexive. +*} + +class partial_equiv = + fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) + assumes partial_equiv_sym [elim?]: "x \<sim> y \<Longrightarrow> y \<sim> x" + assumes partial_equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> 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 \<sim> x}" + +lemma domainI [intro]: "x \<sim> x \<Longrightarrow> x \<in> domain" + unfolding domain_def by blast + +lemma domainD [dest]: "x \<in> domain \<Longrightarrow> x \<sim> x" + unfolding domain_def by blast + +theorem domainI' [elim?]: "x \<sim> y \<Longrightarrow> x \<in> domain" +proof + assume xy: "x \<sim> y" + also from xy have "y \<sim> x" .. + finally show "x \<sim> x" . +qed + + +subsection {* Equivalence on function spaces *} + +text {* + The @{text \<sim>} 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 \<sim> g \<equiv> \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y \<longrightarrow> f x \<sim> g y" + +lemma partial_equiv_funI [intro?]: + "(\<And>x y. x \<in> domain \<Longrightarrow> y \<in> domain \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g y) \<Longrightarrow> f \<sim> g" + unfolding eqv_fun_def by blast + +lemma partial_equiv_funD [dest?]: + "f \<sim> g \<Longrightarrow> x \<in> domain \<Longrightarrow> y \<in> domain \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> 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 \<Rightarrow> 'b::partial_equiv" + assume fg: "f \<sim> g" + show "g \<sim> f" + proof + fix x y :: 'a + assume x: "x \<in> domain" and y: "y \<in> domain" + assume "x \<sim> y" then have "y \<sim> x" .. + with fg y x have "f y \<sim> g x" .. + then show "g x \<sim> f y" .. + qed + assume gh: "g \<sim> h" + show "f \<sim> h" + proof + fix x y :: 'a + assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y" + with fg have "f x \<sim> g y" .. + also from y have "y \<sim> y" .. + with gh y y have "g y \<sim> h y" .. + finally show "f x \<sim> 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 "\<sim> + :: 'a \<Rightarrow> 'a \<Rightarrow> bool"} is required to be reflexive, transitive and + symmetric. +*} + +class equiv = + assumes eqv_refl [intro]: "x \<sim> x" + +text {* + On total equivalences all elements are reflexive, and congruence + holds unconditionally. +*} + +theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain" +proof + show "x \<sim> x" .. +qed + +theorem equiv_cong [dest?]: "f \<sim> g \<Longrightarrow> x \<sim> y \<Longrightarrow> f x \<sim> g (y::'a::equiv)" +proof - + assume "f \<sim> g" + moreover have "x \<in> domain" .. + moreover have "y \<in> domain" .. + moreover assume "x \<sim> 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 \<sim> x}| a::'a::partial_equiv. True}" + by blast + +lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" + unfolding quot_def by blast + +lemma quotE [elim]: "R \<in> quot \<Longrightarrow> (\<And>a. R = {x. a \<sim> x} \<Longrightarrow> C) \<Longrightarrow> 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) \<Rightarrow> 'a quot" ("\<lfloor>_\<rfloor>") where + "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" + +theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" +proof (cases A) + fix R assume R: "A = Abs_quot R" + assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast + with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast + then show ?thesis by (unfold eqv_class_def) +qed + +lemma quot_cases [cases type: quot]: + obtains (rep) a where "A = \<lfloor>a\<rfloor>" + 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 \<sim> b \<Longrightarrow> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" +proof - + assume ab: "a \<sim> b" + have "{x. a \<sim> x} = {x. b \<sim> x}" + proof (rule Collect_cong) + fix x show "(a \<sim> x) = (b \<sim> x)" + proof + from ab have "b \<sim> a" .. + also assume "a \<sim> x" + finally show "b \<sim> x" . + next + note ab + also assume "b \<sim> x" + finally show "a \<sim> x" . + qed + qed + then show ?thesis by (simp only: eqv_class_def) +qed + +theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<Longrightarrow> a \<in> domain \<Longrightarrow> a \<sim> b" +proof (unfold eqv_class_def) + assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}" + then have "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI) + moreover assume "a \<in> domain" then have "a \<sim> a" .. + ultimately have "a \<in> {x. b \<sim> x}" by blast + then have "b \<sim> a" by blast + then show "a \<sim> b" .. +qed + +theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<Longrightarrow> a \<sim> (b::'a::equiv)" +proof (rule eqv_class_eqD') + show "a \<in> domain" .. +qed + +lemma eqv_class_eq' [simp]: "a \<in> domain \<Longrightarrow> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" + using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl) + +lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))" + using eqv_class_eqI eqv_class_eqD by blast + + +subsection {* Picking representing elements *} + +definition + pick :: "'a::partial_equiv quot \<Rightarrow> 'a" where + "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" + +theorem pick_eqv' [intro?, simp]: "a \<in> domain \<Longrightarrow> pick \<lfloor>a\<rfloor> \<sim> a" +proof (unfold pick_def) + assume a: "a \<in> domain" + show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" + proof (rule someI2) + show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. + fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" + from this and a have "a \<sim> x" .. + then show "x \<sim> a" .. + qed +qed + +theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)" +proof (rule pick_eqv') + show "a \<in> domain" .. +qed + +theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" +proof (cases A) + fix a assume a: "A = \<lfloor>a\<rfloor>" + then have "pick A \<sim> a" by simp + then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp + with a show ?thesis by simp +qed + +end |