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:
  "((≤)  (≤)  (≥)) (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