Theory Abstract_Rewriting_Extra

theory Abstract_Rewriting_Extra
  imports
    First_Order_Clause.Transitive_Closure_Extra
    "Abstract-Rewriting.Abstract_Rewriting"
begin

lemma mem_join_union_iff_mem_join_lhs:
  assumes
    "⋀z. (x, z) ∈ A⇧^* ⟹ z ∉ Domain B" and
    "⋀z. (y, z) ∈ A⇧^* ⟹ z ∉ Domain B"
  shows "(x, y) ∈ (A ∪ B)⇧^↓ ⟷ (x, y) ∈ A⇧^↓"
proof (rule iffI)
  assume "(x, y) ∈ (A ∪ B)⇧^↓"
  then obtain z where
    "(x, z) ∈ (A ∪ B)⇧^*" and "(y, z) ∈ (A ∪ B)⇧^*"
    by auto

  show "(x, y) ∈ A⇧^↓"
  proof (rule joinI)
    from assms(1) show "(x, z) ∈ A⇧^*"
      using ‹(x, z) ∈ (A ∪ B)⇧^*› mem_rtrancl_union_iff_mem_rtrancl_lhs[of x A B z] by simp
  next
    from assms(2) show "(y, z) ∈ A⇧^*"
      using ‹(y, z) ∈ (A ∪ B)⇧^*› mem_rtrancl_union_iff_mem_rtrancl_lhs[of y A B z] by simp
  qed
next
  show "(x, y) ∈ A⇧^↓ ⟹ (x, y) ∈ (A ∪ B)⇧^↓"
    by (metis UnCI join_mono subset_Un_eq sup.left_idem)
qed

lemma mem_join_union_iff_mem_join_rhs:
  assumes
    "⋀z. (x, z) ∈ B⇧^* ⟹ z ∉ Domain A" and
    "⋀z. (y, z) ∈ B⇧^* ⟹ z ∉ Domain A"
  shows "(x, y) ∈ (A ∪ B)⇧^↓ ⟷ (x, y) ∈ B⇧^↓"
  using mem_join_union_iff_mem_join_lhs
  by (metis assms(1) assms(2) sup_commute)

lemma refl_join: "refl (r⇧^↓)"
  by (simp add: joinI_right reflI)

lemma trans_join:
  assumes strongly_norm: "SN r" and confluent: "WCR r"
  shows "trans (r⇧^↓)"
proof -
  from confluent strongly_norm have "CR r"
    using Newman by metis
  hence "r⇧^↔⇧^* = r⇧^↓"
    using CR_imp_conversionIff_join by metis
  thus ?thesis
    using conversion_trans by metis
qed

end