Theory Quotient_Type

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Quotient Type Emulation for Locales›

theory Quotient_Type
imports
  Main
begin

locale quotient =
  fixes
    eq :: "'a ⇒ 'a ⇒ bool"
  and
    Rep :: "'b ⇒ 'a"
  and
    Abs :: "'a ⇒ 'b"
  assumes
    Rep_inverse: "Abs (Rep a) = a"
  and
    Abs_eq: "Abs x = Abs y ⟷ eq x y"
begin

lemma Rep_inject:
  "Rep x = Rep y ⟷ x = y"
  by (metis Rep_inverse)

lemma Rep_Abs_eq:
  "eq x (Rep (Abs x))"
  by (metis Abs_eq Rep_inverse)

end

end