Theory First_Order_Clause.Transitive_Closure_Extra

theory Transitive_Closure_Extra
  imports Main
begin

lemma reflclp_iff: "⋀R x y. R⇧=⇧= x y ⟷ R x y ∨ x = y"
  by (metis (full_types) sup2CI sup2E)

lemma reflclp_refl: "R⇧=⇧= x x"
  by simp

lemma transpD_strict_non_strict:
  assumes "transp R"
  shows "⋀x y z. R x y ⟹ R⇧=⇧= y z ⟹ R x z"
  using ‹transp R›[THEN transpD] by blast

lemma transpD_non_strict_strict:
  assumes "transp R"
  shows "⋀x y z. R⇧=⇧= x y ⟹ R y z ⟹ R x z"
  using ‹transp R›[THEN transpD] by blast

lemma mem_rtrancl_union_iff_mem_rtrancl_lhs:
  assumes "⋀z. (x, z) ∈ A⇧* ⟹ z ∉ Domain B"
  shows "(x, y) ∈ (A ∪ B)⇧* ⟷ (x, y) ∈ A⇧*"
  using assms
  by (meson Domain.DomainI in_rtrancl_UnI rtrancl_Un_separatorE)

lemma mem_rtrancl_union_iff_mem_rtrancl_rhs:
  assumes
    "⋀z. (x, z) ∈ B⇧* ⟹ z ∉ Domain A"
  shows "(x, y) ∈ (A ∪ B)⇧* ⟷ (x, y) ∈ B⇧*"
  using assms
  by (metis mem_rtrancl_union_iff_mem_rtrancl_lhs sup_commute)

end