Theory Functions_Injective

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Injective›
theory Functions_Injective
  imports
    Bounded_Quantifiers
    Functions_Monotone
    HOL_Syntax_Bundles_Lattices
begin

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

overloading
  injective_on_pred ≡ "injective_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
begin
  definition "injective_on_pred P f ≡ ∀x x' : P. f x = f x' ⟶ x = x'"
end

lemma injective_onI [intro]:
  assumes "⋀x x'. P x ⟹ P x' ⟹ f x = f x' ⟹ x = x'"
  shows "injective_on P f"
  unfolding injective_on_pred_def using assms by blast

lemma injective_onD:
  assumes "injective_on P f"
  and "P x" "P x'"
  and "f x = f x'"
  shows "x = x'"
  using assms unfolding injective_on_pred_def by blast

lemma injective_on_comp_if_injective_onI:
  assumes "injective_on (P :: 'a ⇒ bool) f" "injective_on Q g"
  and "(P ⇒ Q) f"
  shows "injective_on P (g ∘ f)"
  by (urule injective_onI) (use assms in ‹auto dest: injective_onD›)


consts injective :: "'a ⇒ bool"

overloading
  injective ≡ "injective :: ('a ⇒ 'b) ⇒ bool"
begin
  definition "(injective :: ('a ⇒ 'b) ⇒ bool) ≡ injective_on (⊤ :: 'a ⇒ bool)"
end

lemma injective_eq_injective_on:
  "(injective :: ('a ⇒ 'b) ⇒ bool) = injective_on (⊤ :: 'a ⇒ bool)"
  unfolding injective_def ..

lemma injective_eq_injective_on_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "injective :: ('a ⇒ 'b) ⇒ bool ≡ injective_on P"
  using assms by (simp add: injective_eq_injective_on)

lemma injectiveI [intro]:
  assumes "⋀x x'. f x = f x' ⟹ x = x'"
  shows "injective f"
  using assms by (urule injective_onI)

lemma injectiveD:
  assumes "injective f"
  and "f x = f x'"
  shows "x = x'"
  using assms by (urule (d) injective_onD where chained = insert) simp_all

lemma injective_on_if_injective:
  fixes P :: "'a ⇒ bool" and f :: "'a ⇒ _"
  assumes "injective f"
  shows "injective_on P f"
  using assms by (intro injective_onI) (blast dest: injectiveD)


paragraph ‹Instantiations›

lemma injective_id: "injective id" by auto


end