Theory Finite_Inj

subsection ‹ Finite Injections ›

theory Finite_Inj
  imports Partial_Inj Finite_Fun
begin

typedef ('a, 'b) finj = "{f :: 'a ⤔ 'b. finite(pidom(f))}"
  morphisms pinj_of_finj finj_of_pinj
  by (metis CollectI infinite_imp_nonempty pidom_empty)

setup_lifting type_definition_ffun
setup_lifting type_definition_finj

type_notation finj (infixr "⤕" 1)

lift_definition ffun_of_finj :: "'a ⤕ 'b ⇒ 'a ⇻ 'b" is "λ x. pfun_of_pinj (pinj_of_finj x)"
  by (transfer, simp, metis mem_Collect_eq pidom.rep_eq pinj_of_finj)

text ‹ Hide implementation details for finite functions and injections ›

lifting_update ffun.lifting
lifting_forget ffun.lifting

lifting_update finj.lifting
lifting_forget finj.lifting

end