Theory First_Order_Clause.Ground_Critical_Pairs

theory Ground_Critical_Pairs
  imports Ground_Term_Rewrite_System
begin

context ground_term_rewrite_system
begin

definition ground_critical_pairs :: "'t rel ⇒ 't rel" where
  "ground_critical_pairs R = {(c⟨r⇩2⟩, r⇩1) | c l r⇩1 r⇩2. (c⟨l⟩, r⇩1) ∈ R ∧ (l, r⇩2) ∈ R}"

abbreviation ground_critical_pair_theorem where
  "ground_critical_pair_theorem R ≡ 
    WCR (rewrite_in_context R) ⟷ ground_critical_pairs R ⊆ (rewrite_in_context R)⇧↓"

lemma ground_critical_pairs_fork:
  fixes R :: "'t rel"
  assumes ground_critical_pairs: "(l, r) ∈ ground_critical_pairs R"
  shows "(r, l) ∈ (rewrite_in_context R)¯ O rewrite_in_context R"
proof -

  obtain c t t' where "l = c⟨t'⟩" and "(c⟨t⟩, r) ∈ R" and "(t, t') ∈ R" 
    using ground_critical_pairs
    unfolding ground_critical_pairs_def
    by auto

  have "(r, c⟨t⟩) ∈ (rewrite_in_context R)¯"
    using ‹(c⟨t⟩, r) ∈ R› subset_rewrite_in_context 
    by blast

  moreover have "(c⟨t⟩, l) ∈ rewrite_in_context R"
    using ‹(t, t') ∈ R› ‹l = c⟨t'⟩› rewrite_in_context_def
    by fast

  ultimately show ?thesis 
    by auto
qed

lemma ground_critical_pairs_complete:
  fixes R :: "'t rel"
  assumes 
    ground_critical_pairs: "(l, r) ∈ ground_critical_pairs R" and
    no_join: "(l, r) ∉ (rewrite_in_context R)⇧↓"
  shows "¬ WCR (rewrite_in_context R)"
  using ground_critical_pairs_fork[OF ground_critical_pairs] no_join
  by auto

end

locale ground_critical_pairs = ground_term_rewrite_system +
  assumes ground_critical_pairs_main: 
    "⋀R s t⇩1 t⇩2.
      (s, t⇩1) ∈ rewrite_in_context R ⟹
      (s, t⇩2) ∈ rewrite_in_context R ⟹
      (t⇩1, t⇩2) ∈ (rewrite_in_context R)⇧↓ ∨
       (∃c l r. t⇩1 = c⟨l⟩ ∧ t⇩2 = c⟨r⟩ ∧
         ((l, r) ∈ ground_critical_pairs R ∨ (r, l) ∈ ground_critical_pairs R))"
begin

lemma ground_critical_pairs:
  assumes ground_critical_pairs:
    "⋀l r. (l, r) ∈ ground_critical_pairs R ⟹ l ≠ r ⟹
      ∃s. (l, s) ∈ (rewrite_in_context R)⇧* ∧ (r, s) ∈ (rewrite_in_context R)⇧*"
  shows "WCR (rewrite_in_context R)"
proof (intro WCR_onI)

  let ?R = "rewrite_in_context R"
  let ?CP = "ground_critical_pairs R"

  fix s t⇩1 t⇩2

  assume steps: "(s, t⇩1) ∈ ?R" "(s, t⇩2) ∈ ?R"

  let ?p = "λs'. (t⇩1, s') ∈ ?R⇧* ∧ (t⇩2, s') ∈ ?R⇧*"

  from ground_critical_pairs_main [OF steps]
  have "∃s'. ?p s'"
    using ground_critical_pairs rewrite_in_context_trancl_add_context
    by (metis joinE rtrancl.rtrancl_refl)
 
  then show "(t⇩1, t⇩2) ∈ ?R⇧↓"
    by auto
qed

theorem ground_critical_pair_theorem: "ground_critical_pair_theorem R" (is "?l = ?r")
proof (rule iffI)
  assume ?l

  with ground_critical_pairs_complete show ?r 
    by auto
next
  assume ?r

  with ground_critical_pairs show ?l
    by auto
qed

end

end