Quelle  PER.thy

(*  Title:      HOL/ex/PER.thy
  Author: Oscar Slotosch and Markus Wenzel, TU Muenchen
*)

section ‹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 ‹equiv 🚫› and a type constructor
  ‹'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 ‹partial_equiv› models partial equivalence
  relations (PERs) using the polymorphic ‹∼ :: 'a ==> 'a ==>
  bool›
  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 ‹∼› 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 "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.\ ‹∼
  :: 'a ==> 'a ==> bool›
  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 ‹'a quot› consists of all
  \emph{equivalence classes} over elements of the base type 🍋‹'a›.
 ›

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 ‹
  \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