Theory Functions_Surjective

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Surjective›
theory Functions_Surjective
  imports
    Functions_Base
begin

consts surjective_at :: "'a ⇒ 'b ⇒ bool"

overloading
  surjective_at_pred ≡ "surjective_at :: ('a ⇒ bool) ⇒ ('b ⇒ 'a) ⇒ bool"
begin
  definition "surjective_at_pred (P :: 'a ⇒ bool) (f :: 'b ⇒ 'a) ≡ ∀y : P. has_inverse f y"
end

lemma surjective_atI [intro]:
  assumes "⋀y. P y ⟹ has_inverse f y"
  shows "surjective_at P f"
  unfolding surjective_at_pred_def using assms by blast

lemma surjective_atE [elim]:
  assumes "surjective_at P f"
  and "P y"
  obtains x where "y = f x"
  using assms unfolding surjective_at_pred_def by blast

lemma has_inverse_if_pred_if_surjective_at:
  assumes "surjective_at P f"
  and "P y"
  shows "has_inverse f y"
  using assms by blast

consts surjective :: "'a ⇒ bool"

overloading
  surjective ≡ "surjective :: ('b ⇒ 'a) ⇒ bool"
begin
  definition "(surjective :: ('b ⇒ 'a) ⇒ bool) ≡ surjective_at (⊤ :: 'a ⇒ bool)"
end

lemma surjective_eq_surjective_at:
  "(surjective :: ('b ⇒ 'a) ⇒ bool) = surjective_at (⊤ :: 'a ⇒ bool)"
  unfolding surjective_def ..

lemma surjective_eq_surjective_at_uhint [uhint]:
  assumes "P ≡  ⊤ :: 'a ⇒ bool"
  shows "surjective :: ('b ⇒ 'a) ⇒ bool ≡ surjective_at P"
  using assms by (simp add: surjective_eq_surjective_at)

lemma surjectiveI [intro]:
  assumes "⋀y. has_inverse f y"
  shows "surjective f"
  using assms by (urule surjective_atI)

lemma surjectiveE:
  assumes "surjective f"
  obtains "⋀y. has_inverse f y"
  using assms unfolding surjective_eq_surjective_at by (force dest: has_inverseI)

lemma surjective_at_if_surjective:
  fixes P :: "'a ⇒ bool" and f :: "'b ⇒ 'a"
  assumes "surjective f"
  shows "surjective_at P f"
  using assms by (intro surjective_atI) (blast elim: surjectiveE)

end