(* 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