Theory Relation_Extra

theory Relation_Extra
  imports HOL.Relation
begin

lemma transp_on_empty[simp]: "transp_on {} R"
  by (auto intro: transp_onI)

lemma asymp_on_empty[simp]: "asymp_on {} R"
  by (auto intro: asymp_onI)

lemma partition_set_around_element:
  assumes tot: "totalp_on N R" and x_in: "x ∈ N"
  shows "N = {y ∈ N. R y x} ∪ {x} ∪ {y ∈ N. R x y}"
proof (intro Set.equalityI Set.subsetI)
  fix z assume "z ∈ N"
  hence "R z x ∨ z = x ∨ R x z"
    using tot[THEN totalp_onD] x_in by auto
  thus "z ∈ {y ∈ N. R y x} ∪ {x} ∪ {y ∈ N. R x y}" 
    using ‹z ∈ N› by auto
next
  fix z assume "z ∈ {y ∈ N. R y x} ∪ {x} ∪ {y ∈ N. R x y}"
  hence "z ∈ N ∨ z = x"
    by auto
  thus "z ∈ N"
    using x_in by auto
qed

end