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