Theory With_Type.Misc_With_Type

section ‹‹Misc_With_Type› -- Some auxiliary definitions and lemmas›

theory Misc_With_Type
  imports Main
begin

lemma type_definition_bij_betw_iff: ‹type_definition rep (inv rep) S ⟷ bij_betw rep UNIV S›
  by (smt (verit, best) UNIV_I bij_betw_def bij_betw_iff_bijections inj_on_def inv_f_eq type_definition.Rep_inject type_definition.Rep_range type_definition.intro)

inductive rel_unit_itself :: ‹unit ⇒ 'a itself ⇒ bool› where
― ‹A canonical relation between \<^typ>‹unit› and \<^typ>‹'a itself›.
  Note that while the latter may not be a singleton type, in many situations we treat it as 
  one by only using the element \<^term>‹TYPE('a)›.›
  ‹rel_unit_itself () TYPE('a)›

lemma Domain_rel_unit_itself[simp]: ‹Domainp rel_unit_itself x›
  by (simp add: Domainp_iff rel_unit_itself.simps)
lemma rel_unit_itself_iff[simp]: ‹rel_unit_itself x y ⟷ (y = TYPE('a))›
  by (simp add: rel_unit_itself.simps)

end