✐‹creator "Kevin Kappelmann"› section ‹Transport for HOL Type Definitions› theory Transport_Typedef_Base imports HOL_Alignment_Binary_Relations Transport_Bijections HOL.Typedef begin context type_definition begin abbreviation (input) "L :: 'a ⇒ 'a ⇒ bool ≡ (=⇘A⇙)" abbreviation (input) "R :: 'b ⇒ 'b ⇒ bool ≡ (=)" sublocale transport? : transport_eq_restrict_bijection "mem_of A" "⊤ :: 'b ⇒ bool" Abs Rep rewrites "(=⇘mem_of A⇙) ≡ L" and "(=⇘⊤ :: 'b ⇒ bool⇙) ≡ R" and "(galois_rel.Galois (=) (=) Rep)↾⇘mem_of A⇙↿⇘⊤ :: 'b ⇒ bool⇙ ≡ (galois_rel.Galois (=) (=) Rep)" using Abs_inverse Rep_inverse by (intro transport_eq_restrict_bijection.intro bijection_onI) (auto intro!: eq_reflection galois_rel.left_GaloisI Rep elim: galois_rel.left_GaloisE) interpretation galois L R Abs Rep . lemma Rep_left_Galois_self: "Rep y ⇘L⇙⪅ y" using Rep by (intro left_GaloisI) auto definition "AR x y ≡ x = Rep y" lemma left_Galois_eq_AR: "left_Galois = AR" unfolding AR_def by (auto intro!: galois_rel.left_GaloisI Rep elim: galois_rel.left_GaloisE) end end