(* Title: HOL/ex/PER.thy
Author: Oscar Slotosch and Markus Wenzel, TU Muenchen
*)
section \<open>Partial equivalence relations\<close>
theory PER
imports Main
begin
text \<open>
Higher-order quotients are defined over partial equivalence
relations (PERs) instead of total ones. We provide axiomatic type
classes \<open>equiv < partial_equiv\<close> and a type constructor
\<open>'a quot\<close> 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.
\<close>
subsection \<open>Partial equivalence\<close>
text \<open>
Type class \<open>partial_equiv\<close> models partial equivalence
relations (PERs) using the polymorphic \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow>
bool\<close> relation, which is required to be symmetric and transitive,
but not necessarily reflexive.
\<close>
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 \<open>
\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.
\<close>
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 \<open>Equivalence on function spaces\<close>
text \<open>
The \<open>\<sim>\<close> 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.
\<close>
instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
begin
definition "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 \<open>
The class of partial equivalence relations is closed under function
spaces (in \emph{both} argument positions).
\<close>
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 \<open>Total equivalence\<close>
text \<open>
The class of total equivalence relations on top of PERs. It
coincides with the standard notion of equivalence, i.e.\ \<open>\<sim>
:: 'a \ 'a \ bool\ is required to be reflexive, transitive and
symmetric.
\<close>
class equiv =
assumes eqv_refl [intro]: "x \ x"
text \<open>
On total equivalences all elements are reflexive, and congruence
holds unconditionally.
\<close>
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 \<open>Quotient types\<close>
text \<open>
The quotient type \<open>'a quot\<close> consists of all
\emph{equivalence classes} over elements of the base type \<^typ>\<open>'a\<close>.
\<close>
definition "quot = {{x. a \ x}| a::'a::partial_equiv. True}"
typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set"
unfolding quot_def 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 \<open>
\medskip Abstracted equivalence classes are the canonical
representation of elements of a quotient type.
\<close>
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 \<open>Equality on quotients\<close>
text \<open>
Equality of canonical quotient elements corresponds to the original
relation as follows.
\<close>
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 \<open>Picking representing elements\<close>
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
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
