Theory Total_Fun

section ‹ Total functions ›

theory Total_Fun
  imports Partial_Fun
begin

subsection ‹ Total function type and operations ›

text ‹ It may seem a little strange to create this, given we already have @{type fun}, but it's
  necessary to implement Z's type hierarchy. ›

typedef ('a, 'b) tfun = "{f :: 'a ⇸ 'b. pdom(f) = UNIV}" 
  morphisms pfun_of_tfun Abs_tfun
  by (meson mem_Collect_eq pdom_pfun_entries)

type_notation tfun (infixr "⇒⇩t" 0)

setup_lifting type_definition_tfun

lift_definition mk_tfun :: "('a ⇒ 'b) ⇒ ('a ⇒⇩t 'b)" is
"λ f. fun_pfun f" by simp

lemma pfun_of_tfun_mk_tfun [simp]: "pfun_of_tfun (mk_tfun f) = fun_pfun f"
  by (transfer, simp)

end