Theory Binary_Relations_Right_Unique

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Right Unique›
theory Binary_Relations_Right_Unique
  imports
    Binary_Relations_Injective
    Binary_Relations_Extend
begin

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

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

lemma right_unique_onI [intro]:
  assumes "⋀x y y'. P x ⟹ R x y ⟹ R x y' ⟹ y = y'"
  shows "right_unique_on P R"
  using assms unfolding right_unique_on_pred_def by blast

lemma right_unique_onD:
  assumes "right_unique_on P R"
  and "P x"
  and "R x y" "R x y'"
  shows "y = y'"
  using assms unfolding right_unique_on_pred_def by blast

lemma antimono_right_unique_on:
  "((≤) ⇛⇩m (≤) ⇛ (≥)) (right_unique_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool)"
  by (fastforce dest: right_unique_onD)

lemma mono_right_unique_on_top_right_unique_on_inf_rel_restrict_left:
  "((R : right_unique_on P) ⇛⇩m (P' : ⊤) ⇛⇩m right_unique_on (P ⊓ P')) rel_restrict_left"
  by (fast dest: right_unique_onD)

lemma mono_right_unique_on_comp:
  "((R : right_unique_on P) ⇛⇩m right_unique_on (in_codom (R↾⇘P⇙)) ⇛⇩m right_unique_on P) (∘∘)"
  by (fast dest: right_unique_onD)

context
  fixes P :: "'a ⇒ bool" and ℛ :: "('a ⇒ 'b ⇒ bool) ⇒ bool"
begin

lemma right_unique_on_glue_if_right_unique_on_sup:
  assumes "⋀R R'. ℛ R ⟹ ℛ R' ⟹ right_unique_on P (R ⊔ R')"
  shows "right_unique_on P (glue ℛ)"
  using assms by (fastforce dest: right_unique_onD)

lemma right_unique_on_if_right_unique_on_glue:
  assumes "right_unique_on P (glue ℛ)"
  and "ℛ R"
  shows "right_unique_on P R"
  using assms by (intro right_unique_onI) (auto dest: right_unique_onD)

end

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

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

lemma right_unique_atI [intro]:
  assumes "⋀x y y'. P y ⟹ P y' ⟹ R x y ⟹ R x y' ⟹ y = y'"
  shows "right_unique_at P R"
  using assms unfolding right_unique_at_pred_def by blast

lemma right_unique_atD:
  assumes "right_unique_at P R"
  and "P y"
  and "P y'"
  and "R x y" "R x y'"
  shows "y = y'"
  using assms unfolding right_unique_at_pred_def by blast

lemma right_unique_at_rel_inv_iff_rel_injective_on [iff]:
  "right_unique_at (P :: 'a ⇒ bool) (R¯ :: 'b ⇒ 'a ⇒ bool) ⟷ rel_injective_on P R"
  by (blast dest: right_unique_atD rel_injective_onD)

lemma rel_injective_on_rel_inv_iff_right_unique_at [iff]:
  "rel_injective_on (P :: 'a ⇒ bool) (R¯ :: 'a ⇒ 'b ⇒ bool) ⟷ right_unique_at P R"
  by (blast dest: right_unique_atD rel_injective_onD)

lemma right_unique_on_rel_inv_iff_rel_injective_at [iff]:
  "right_unique_on (P :: 'a ⇒ bool) (R¯ :: 'a ⇒ 'b ⇒ bool) ⟷ rel_injective_at P R"
  by (blast dest: right_unique_onD rel_injective_atD)

lemma rel_injective_at_rel_inv_iff_right_unique_on [iff]:
  "rel_injective_at (P :: 'b ⇒ bool) (R¯ :: 'a ⇒ 'b ⇒ bool) ⟷ right_unique_on P R"
  by (blast dest: right_unique_onD rel_injective_atD)

lemma right_unique_on_if_Fun_Rel_imp_if_right_unique_at:
  assumes "right_unique_at (Q :: 'b ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool)"
  and "(R ⇛ (⟶)) P Q"
  shows "right_unique_on P R"
  using assms by (intro right_unique_onI) (auto dest: right_unique_atD)

lemma right_unique_at_if_Fun_Rel_rev_imp_if_right_unique_on:
  assumes "right_unique_on (P :: 'a ⇒ bool) (R :: 'a ⇒ 'b ⇒ bool)"
  and "(R ⇛ (⟵)) P Q"
  shows "right_unique_at Q R"
  using assms by (intro right_unique_atI) (auto dest: right_unique_onD)


consts right_unique :: "'a ⇒ bool"

overloading
  right_unique ≡ "right_unique :: ('a ⇒ 'b ⇒ bool) ⇒ bool"
begin
  definition "(right_unique :: ('a ⇒ 'b ⇒ bool) ⇒ bool) ≡ right_unique_on (⊤ :: 'a ⇒ bool)"
end

lemma right_unique_eq_right_unique_on:
  "(right_unique :: ('a ⇒ 'b ⇒ bool) ⇒ _) = right_unique_on (⊤ :: 'a ⇒ bool)"
  unfolding right_unique_def ..

lemma right_unique_eq_right_unique_on_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "right_unique :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡ right_unique_on P"
  using assms by (simp only: right_unique_eq_right_unique_on)

lemma right_uniqueI [intro]:
  assumes "⋀x y y'. R x y ⟹ R x y' ⟹ y = y'"
  shows "right_unique R"
  using assms by (urule right_unique_onI)

lemma right_uniqueD:
  assumes "right_unique R"
  and "R x y" "R x y'"
  shows "y = y'"
  using assms by (urule (d) right_unique_onD where chained = insert) simp_all

lemma right_unique_eq_right_unique_at:
  "(right_unique :: ('a ⇒ 'b ⇒ bool) ⇒ bool) = right_unique_at (⊤ :: 'b ⇒ bool)"
  by (intro ext iffI right_uniqueI) (auto dest: right_unique_atD right_uniqueD)

lemma right_unique_eq_right_unique_at_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'b ⇒ bool)"
  shows "right_unique :: ('a ⇒ 'b ⇒ bool) ⇒ _ ≡ right_unique_at P"
  using assms by (simp only: right_unique_eq_right_unique_at)

lemma right_unique_on_if_right_unique:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'b ⇒ bool"
  assumes "right_unique R"
  shows "right_unique_on P R"
  using assms by (blast dest: right_uniqueD)

lemma right_unique_at_if_right_unique:
  fixes P :: "'a ⇒ bool" and R :: "'b ⇒ 'a ⇒ bool"
  assumes "right_unique R"
  shows "right_unique_at P R"
  using assms by (blast dest: right_uniqueD)

lemma right_unique_if_right_unique_on_in_dom:
  assumes "right_unique_on (in_dom R) R"
  shows "right_unique R"
  using assms by (blast dest: right_unique_onD)

lemma right_unique_if_right_unique_at_in_codom:
  assumes "right_unique_at (in_codom R) R"
  shows "right_unique R"
  using assms by (blast dest: right_unique_atD)

corollary right_unique_on_in_dom_iff_right_unique [iff]:
  "right_unique_on (in_dom R) R ⟷ right_unique R"
  using right_unique_if_right_unique_on_in_dom right_unique_on_if_right_unique
  by blast

corollary right_unique_at_in_codom_iff_right_unique [iff]:
  "right_unique_at (in_codom R) R ⟷ right_unique R"
  using right_unique_if_right_unique_at_in_codom right_unique_at_if_right_unique
  by blast

lemma right_unique_rel_inv_iff_rel_injective [iff]:
  "right_unique R¯ ⟷ rel_injective R"
  by (blast dest: right_uniqueD rel_injectiveD)

lemma rel_injective_rel_inv_iff_right_unique [iff]:
  "rel_injective R¯ ⟷ right_unique R"
  by (blast dest: right_uniqueD rel_injectiveD)


paragraph ‹Instantiations›

lemma right_unique_eq: "right_unique (=)"
  by (rule right_uniqueI) blast


end