Theory Binary_Relations_Symmetric

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Symmetric›
theory Binary_Relations_Symmetric
  imports
    Functions_Monotone
begin

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

overloading
  symmetric_on_pred ≡ "symmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "symmetric_on_pred P R ≡ ∀x y : P. R x y ⟶ R y x"
end

lemma symmetric_onI [intro]:
  assumes "⋀x y. P x ⟹ P y ⟹ R x y ⟹ R y x"
  shows "symmetric_on P R"
  unfolding symmetric_on_pred_def using assms by blast

lemma symmetric_onD:
  assumes "symmetric_on P R"
  and "P x" "P y"
  and "R x y"
  shows "R y x"
  using assms unfolding symmetric_on_pred_def by blast

lemma symmetric_on_rel_inv_iff_symmetric_on [iff]:
  "symmetric_on P R¯ ⟷ symmetric_on (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool)"
  by (blast dest: symmetric_onD)

lemma antimono_symmetric_on: "antimono (symmetric_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by (intro antimonoI) (auto dest: symmetric_onD)

lemma symmetric_on_if_le_pred_if_symmetric_on:
  fixes P' :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "symmetric_on P R"
  and "P' ≤ P"
  shows "symmetric_on P' R"
  using assms antimono_symmetric_on by blast

consts symmetric :: "'a ⇒ bool"

overloading
  symmetric ≡ "symmetric :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "(symmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ symmetric_on (⊤ :: 'a ⇒ bool)"
end

lemma symmetric_eq_symmetric_on:
  "(symmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) = symmetric_on (⊤ :: 'a ⇒ bool)"
  unfolding symmetric_def ..

lemma symmetric_eq_symmetric_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (symmetric :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ symmetric_on P"
  by (simp add: symmetric_eq_symmetric_on)

lemma symmetricI [intro]:
  assumes "⋀x y. R x y ⟹ R y x"
  shows "symmetric R"
  using assms by (urule symmetric_onI)

lemma symmetricD:
  assumes "symmetric R"
  and "R x y"
  shows "R y x"
  using assms by (urule (d) symmetric_onD where chained = insert) simp_all

lemma symmetric_on_if_symmetric:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "symmetric R"
  shows "symmetric_on P R"
  using assms by (intro symmetric_onI) (blast dest: symmetricD)

lemma symmetric_rel_inv_iff_symmetric [iff]: "symmetric R¯ ⟷ symmetric (R :: 'a ⇒ 'a ⇒ bool)"
  by (blast dest: symmetricD)

lemma rel_inv_eq_self_if_symmetric [simp]:
  assumes "symmetric R"
  shows "R¯ = R"
  using assms by (blast dest: symmetricD)

lemma rel_iff_rel_if_symmetric:
  assumes "symmetric R"
  shows "R x y ⟷ R y x"
  using assms by (blast dest: symmetricD)

lemma symmetric_if_rel_inv_eq_self:
  assumes "R¯ = R"
  shows "symmetric R"
  by (intro symmetricI, subst assms[symmetric]) simp

lemma symmetric_iff_rel_inv_eq_self: "symmetric R ⟷ R¯ = R"
  using rel_inv_eq_self_if_symmetric symmetric_if_rel_inv_eq_self by blast

lemma symmetric_if_symmetric_on_in_field:
  assumes "symmetric_on (in_field R) R"
  shows "symmetric R"
  using assms by (intro symmetricI) (blast dest: symmetric_onD)

corollary symmetric_on_in_field_iff_symmetric [iff]:
  "symmetric_on (in_field R) R ⟷ symmetric R"
  using symmetric_if_symmetric_on_in_field symmetric_on_if_symmetric
  by blast


paragraph ‹Instantiations›

lemma symmetric_eq [iff]: "symmetric (=)"
  by (rule symmetricI) (rule sym)

lemma symmetric_top: "symmetric (⊤ :: 'a ⇒ 'a ⇒ bool)"
  by (rule symmetricI) auto

end