Theory Binary_Relations_Injective

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Injective›
theory Binary_Relations_Injective
  imports
    Functions_Monotone
    Reverse_Implies
begin

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

overloading
  rel_injective_on_pred ≡ "rel_injective_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool"
begin
  definition "rel_injective_on_pred P R ≡ ∀x x' : P. ∀ y. R x y ∧ R x' y ⟶ x = x'"
end

lemma rel_injective_onI [intro]:
  assumes "⋀x x' y. P x ⟹ P x' ⟹ R x y ⟹ R x' y ⟹ x = x'"
  shows "rel_injective_on P R"
  unfolding rel_injective_on_pred_def using assms by blast

lemma rel_injective_onD:
  assumes "rel_injective_on P R"
  and "P x" "P x'"
  and "R x y" "R x' y"
  shows "x = x'"
  using assms unfolding rel_injective_on_pred_def by blast

lemma antimono_rel_injective_on:
  "((≤) ⇛⇩m (≤) ⇛ (≥)) (rel_injective_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool)"
  by (intro mono_wrt_relI) (auto dest: rel_injective_onD intro!: rel_injective_onI)


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

overloading
  rel_injective_at_pred ≡ "rel_injective_at :: ('a ⇒ bool) ⇒ ('b ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "rel_injective_at_pred P R ≡ ∀x x' y. P y ∧ R x y ∧ R x' y ⟶ x = x'"
end

lemma rel_injective_atI [intro]:
  assumes "⋀x x' y. P y ⟹ R x y ⟹ R x' y ⟹ x = x'"
  shows "rel_injective_at P R"
  unfolding rel_injective_at_pred_def using assms by blast

lemma rel_injective_atD:
  assumes "rel_injective_at P R"
  and "P y"
  and "R x y" "R x' y"
  shows "x = x'"
  using assms unfolding rel_injective_at_pred_def by blast

lemma rel_injective_on_if_Fun_Rel_imp_if_rel_injective_at:
  assumes "rel_injective_at (Q :: 'b ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool)"
  and "(R ⇛ (⟶)) P Q"
  shows "rel_injective_on P R"
  using assms by (intro rel_injective_onI) (auto dest: rel_injective_atD)

lemma rel_injective_at_if_Fun_Rel_rev_imp_if_rel_injective_on:
  assumes "rel_injective_on (P :: 'a ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool)"
  and "(R ⇛ (⟵)) P Q"
  shows "rel_injective_at Q R"
  using assms by (intro rel_injective_atI) (auto dest: rel_injective_onD)


consts rel_injective :: "'a ⇒ bool"

overloading
  rel_injective ≡ "rel_injective :: ('a ⇒ 'b ⇒ bool) ⇒ bool"
begin
  definition "(rel_injective :: ('a ⇒ 'b ⇒ bool) ⇒ bool) ≡ rel_injective_on (⊤ :: 'a ⇒ bool)"
end

lemma rel_injective_eq_rel_injective_on:
  "(rel_injective :: ('a ⇒ 'b ⇒ bool) ⇒ _) = rel_injective_on (⊤ :: 'a ⇒ bool)"
  unfolding rel_injective_def ..

lemma rel_injective_eq_rel_injective_on_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "rel_injective :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡ rel_injective_on P"
  using assms by (simp add: rel_injective_eq_rel_injective_on)

lemma rel_injectiveI [intro]:
  assumes "⋀x x' y. R x y ⟹ R x' y ⟹ x = x'"
  shows "rel_injective R"
  using assms by (urule rel_injective_onI)

lemma rel_injectiveD:
  assumes "rel_injective R"
  and "R x y" "R x' y"
  shows "x = x'"
  using assms by (urule (d) rel_injective_onD where chained = insert) simp_all

lemma rel_injective_eq_rel_injective_at:
  "(rel_injective :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = rel_injective_at (⊤ :: 'b ⇒ bool)"
  by (intro ext iffI rel_injectiveI) (auto dest: rel_injective_atD rel_injectiveD)

lemma rel_injective_eq_rel_injective_at_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'b ⇒ bool)"
  shows "rel_injective :: ('a ⇒ 'b ⇒ bool) ⇒ bool ≡ rel_injective_at P"
  using assms by (simp add: rel_injective_eq_rel_injective_at)

lemma rel_injective_on_if_rel_injective:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'b ⇒ bool"
  assumes "rel_injective R"
  shows "rel_injective_on P R"
  using assms by (blast dest: rel_injectiveD)

lemma rel_injective_at_if_rel_injective:
  fixes P :: "'a ⇒ bool" and R :: "'b ⇒ 'a ⇒ bool"
  assumes "rel_injective R"
  shows "rel_injective_at P R"
  using assms by (blast dest: rel_injectiveD)

lemma rel_injective_if_rel_injective_on_in_dom:
  assumes "rel_injective_on (in_dom R) R"
  shows "rel_injective R"
  using assms by (blast dest: rel_injective_onD)

lemma rel_injective_if_rel_injective_at_in_codom:
  assumes "rel_injective_at (in_codom R) R"
  shows "rel_injective R"
  using assms by (blast dest: rel_injective_atD)

corollary rel_injective_on_in_dom_iff_rel_injective [simp]:
  "rel_injective_on (in_dom R) R ⟷ rel_injective R"
  using rel_injective_if_rel_injective_on_in_dom rel_injective_on_if_rel_injective
  by blast

corollary rel_injective_at_in_codom_iff_rel_injective [iff]:
  "rel_injective_at (in_codom R) R ⟷ rel_injective R"
  using rel_injective_if_rel_injective_at_in_codom rel_injective_at_if_rel_injective
  by blast

lemma rel_injective_on_compI:
  fixes P :: "'a ⇒ bool"
  assumes "rel_injective (R :: 'a ⇒ 'b ⇒ bool)"
  and "rel_injective_on (in_codom R ⊓ in_dom S) (S :: 'b ⇒ 'c ⇒ bool)"
  shows "rel_injective_on P (R ∘∘ S)"
proof (rule rel_injective_onI)
  fix x x' y
  assume "P x" "P x'" "(R ∘∘ S) x y" "(R ∘∘ S) x' y"
  then obtain z z' where "R x z" "S z y" "R x' z'" "S z' y" by blast
  with assms have "z = z'" by (auto dest: rel_injective_onD)
  with ‹R x z› ‹R x' z'› assms show "x = x'" by (auto dest: rel_injectiveD)
qed


end