Theory Binary_Relations_Connected

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Connected›
theory Binary_Relations_Connected
  imports
    Binary_Relation_Functions
begin

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

overloading
  connected_on_pred ≡ "connected_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "connected_on_pred P R ≡ ∀x y : P. x ≠ y ⟶ R x y ∨ R y x"
end

lemma connected_onI [intro]:
  assumes "⋀x y. P x ⟹ P y ⟹ x ≠ y ⟹ R x y ∨ R y x"
  shows "connected_on P R"
  using assms unfolding connected_on_pred_def by blast

lemma connected_onE [elim]:
  assumes "connected_on P R"
  and "P x" "P y"
  obtains "x = y" | "R x y" | "R y x"
  using assms unfolding connected_on_pred_def by auto

lemma connected_on_rel_inv_iff_connected_on [iff]:
  "connected_on (P :: 'a ⇒ bool) (R :: 'a ⇒ 'a ⇒ bool)¯ ⟷ connected_on P R"
  by blast

consts connected :: "'a ⇒ bool"

overloading
  connected ≡ "connected :: ('a ⇒ 'a ⇒ bool) ⇒ bool"
begin
  definition "connected :: ('a ⇒ 'a ⇒ bool) ⇒ bool ≡ connected_on (⊤ :: 'a ⇒ bool)"
end

lemma connected_eq_connected_on:
  "(connected :: ('a ⇒ 'a ⇒ bool) ⇒ _) = connected_on (⊤ :: 'a ⇒ bool)"
  unfolding connected_def ..

lemma connected_eq_connected_on_uhint [uhint]:
  "P ≡ (⊤ :: 'a ⇒ bool) ⟹ (connected :: ('a ⇒ 'a ⇒ bool) ⇒ _) ≡ connected_on P"
  by (simp add: connected_eq_connected_on)

lemma connectedI [intro]:
  assumes "⋀x y. x ≠ y ⟹ R x y ∨ R y x"
  shows "connected R"
  using assms by (urule connected_onI)

lemma connectedE [elim]:
  assumes "connected R"
  and "x ≠ y"
  obtains "R x y" | "R y x"
  using assms by (urule (e) connected_onE where chained = insert) auto

lemma connected_on_if_connected:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "connected R"
  shows "connected_on P R"
  using assms by (intro connected_onI) blast


end