Theory Binary_Relations_Connected

✐‹creator "Kevin Kappelmann"›
subsubsection ‹Connected›
theory Binary_Relations_Connected
  imports
    Binary_Relation_Functions
    Functions_Injective
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

lemma connected_on_rel_map_if_injective_on_if_mono_wrt_pred_if_connected_on:
  fixes P :: "'a ⇒ bool" and R :: "'a ⇒ 'a ⇒ bool"
  assumes "connected_on P R"
  and "(Q ⇒ P) f"
  and "injective_on Q f"
  shows "connected_on Q (rel_map f R)"
  using assms by (fastforce dest: injective_onD)

lemma antimono_connected_on: "antimono (connected_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by (intro antimonoI) auto

lemma mono_connected_on:
  "((≤) ⇒ (≥) ⇛ (≥)) (connected_on :: ('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool)"
  by blast

lemma in_field_restrict_eq_if_ex_ne_if_connected_on:
  assumes conn: "connected_on P R"
  and eq_ne: "∃x y : P. x ≠ y"
  shows "in_field R↑⇘P⇙ = P"
proof (intro ext iffI)
  fix x assume "P x"
  moreover with eq_ne obtain y where "P y" "x ≠ y" by blast
  ultimately have "R x y ∨ R y x" using conn by blast
  with ‹P x› ‹P y› show "in_field R↑⇘P⇙ x" by fastforce
qed auto

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