Theory Ground_Critical_Pairs

theory Ground_Critical_Pairs
  imports 
    Generic_Term_Context
    Ground_Term_Rewrite_System
    Parallel_Rewrite
begin

(* TODO: Create generalized version that works with ground and nonground terms *)
text‹Adapted from First\_Order\_Rewriting.Critical\_Pairs›

context ground_term_rewrite_system
begin

definition ground_critical_pairs :: "'t rel ⇒ 't rel" where
  "ground_critical_pairs R = {(c⟨r2⟩, r1) | c l r1 r2. (c⟨l⟩, r1) ∈ R ∧ (l, r2) ∈ 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

definition ground_critical_peaks ::"'t rel ⇒ ('t × 't × 't) set" where
  "ground_critical_peaks R = { (c⟨r'⟩, c⟨l⟩, r) | l r r' c. (c⟨l⟩, r) ∈ R ∧ (l, r') ∈ R }"

lemma ground_critical_peak_to_pair: 
  assumes "(l, m, r) ∈ ground_critical_peaks R" 
  shows "(l, r) ∈ ground_critical_pairs R" 
  using assms 
  unfolding ground_critical_peaks_def ground_critical_pairs_def 
  by blast

end

locale ground_critical_pairs =
  term_context_interpretation where More = More and is_var = "λ_. False" +
  parallel_rewrite where Fun = Fun
for        
  More :: "'f ⇒ 'e ⇒ 't list ⇒ 'c ⇒ 't list ⇒ 'c"
begin

lemma ground_critical_peaks_main: 
  fixes R :: "'t rel" and  t u s :: 't
  assumes t_u: "(t, u) ∈ rewrite_in_context R" and t_s: "(t, s) ∈ rewrite_in_context R"
  shows 
    "(s, u) ∈ join (rewrite_in_context R) ∨
      (∃c l m r. s = c⟨l⟩ ∧ t = c⟨m⟩ ∧ u = c⟨r⟩ ∧
        ((l, m, r) ∈ ground_critical_peaks R ∨ (r, m, l) ∈ ground_critical_peaks R))"
proof -

  let ?R = "rewrite_in_context R"
  let ?CP = "ground_critical_peaks R"

  from t_u obtain c1 l1 r1 where
    l1_r1: "(l1, r1) ∈ R" and 
    t1: "t = c1⟨l1⟩" and 
    u: "u = c1⟨r1⟩"
    unfolding rewrite_in_context_def
    by auto

  from t_s obtain c2 l2 r2 where 
    l2_r2: "(l2, r2) ∈ R" and 
    t2: "t = c2⟨l2⟩" and 
    s: "s = c2⟨r2⟩"
    unfolding rewrite_in_context_def
    by auto

  define n where "n = sizec c1 + sizec c2"

  from t1 t2 u s n_def show ?thesis
  proof (induct n arbitrary: c1 c2 s t u rule: less_induct)
    case (less n c1 c2 s t u)

    show ?case
    proof (cases "c1 = □")
      case Hole: True

      show ?thesis
        using l1_r1 l2_r2 less.prems
        unfolding ground_critical_peaks_def mem_Collect_eq
        by (metis Hole apply_hole)
    next
      case c1_not_hole: False

      then obtain f1 e1 ss1 c1' ts1 where c1: "c1 = More f1 e1 ss1 c1' ts1"
        using context_destruct
        by auto

      show ?thesis
      proof (cases "c2 = □")
        case Hole: True

        show ?thesis
          using l1_r1 l2_r2 less.prems
          unfolding ground_critical_peaks_def mem_Collect_eq
          by (metis Hole apply_hole)
      next
        case c2_not_hole: False

        then obtain f2 e2 ss2 c2' ts2 where c2: "c2 = More f2 e2 ss2 c2' ts2"
          using context_destruct
          by auto

        from less(2-3) c1 c2
        have id: "(More f1 e1 ss1 c1' ts1)⟨l1⟩ = (More f2 e2 ss2 c2' ts2)⟨l2⟩"
          by auto

        then have
          f: "f1 = f2" and
          e: "e1 = e2"
          using term_inject
          by auto

        let ?n1 = "length ss1"
        let ?n2 = "length ss2"

        show ?thesis
        proof (cases "?n1 = ?n2")
          case True

          with id have 
            ss: "ss1 = ss2" and 
            ts: "ts1 = ts2" and
            c': "c1'⟨l1⟩ = c2'⟨l2⟩"
            using term_inject
            by fastforce+

          let ?c = "More f2 e2 ss2 □ ts2"

          have c1_eq: "c1 = ?c ∘c c1'" 
            unfolding c1 f e ss ts
            by simp

          have c2_eq: "c2 = ?c ∘c c2'" 
            unfolding c2 f ss ts  
            by simp

          define m where
            "m = sizec c1' + sizec c2'"

          have m_less_n: "m < n" 
            unfolding less m_def c1 c2
            using subcontext_smaller interpretation_not_hole
            by (metis add_less_mono subcontext)

          note IH = less(1)[OF m_less_n refl c' refl refl m_def]

          then show ?thesis
          proof (elim disjE)
            assume "(c2'⟨r2⟩, c1'⟨r1⟩) ∈ ?R↓"

            then obtain s' where 
              c1'_s': "(c1'⟨r1⟩, s') ∈ ?R*" and
              c2'_s': "(c2'⟨r2⟩, s') ∈ ?R*"
              by auto

            have "(c1⟨r1⟩, ?c⟨s'⟩) ∈ ?R*" 
              using c1'_s' 
              unfolding c1_eq compose_context_iff
              by blast

            moreover have "(c2⟨r2⟩, ?c⟨s'⟩) ∈ ?R*" 
              using c2'_s' 
              unfolding c2_eq compose_context_iff
              by blast

            ultimately show ?thesis 
              using less 
              by auto
          next
            assume 
              "∃c l m r.
                c2'⟨r2⟩ = c⟨l⟩ ∧
                c1'⟨l1⟩ = c⟨m⟩ ∧
                c1'⟨r1⟩ = c⟨r⟩ ∧
                ((l, m, r) ∈ ?CP ∨ (r, m, l) ∈ ?CP)"

            then show ?thesis
              by (metis c1_eq c2_eq compose_context_iff less.prems(1,3,4))
          qed
        next
          case False

          let ?p1 = "?n1 # hole_position c1'"
          let ?p2 = "?n2 # hole_position c2'"

          let ?one = "c1⟨l1⟩⟦?p1 := r1⟧"
          let ?two = "c2⟨l2⟩⟦?p2 := r2⟧"

          have parallel_p1_p2: "?p1 ⊥ ?p2" 
            using False
            by auto

          have p1: "?p1 ∈ positions c1⟨l1⟩"
            unfolding c1
            by auto

          have p2: "?p2 ∈ positions c1⟨l1⟩"
            unfolding c1 id
            by auto

          have "(?one, ?one⟦?p2 := r2⟧) ∈ rewrite_in_context R" 
          proof(rule parallel_rewrite_in_context[OF parallel_p1_p2 p1 p2 _ l2_r2])

            show "l2 = c1⟨l1⟩ !t ?p2"
              unfolding c1 id
              by simp
          qed

          then have "(c1⟨r1⟩, ?one⟦?p2 := r2⟧) ∈ (rewrite_in_context R)*"
            unfolding c1
            by simp

          moreover have "(?two, ?two⟦?p1 := r1⟧) ∈ rewrite_in_context R" 
          proof (rule parallel_rewrite_in_context[OF parallel_pos_sym[OF parallel_p1_p2]])

            show "?p1 ∈ positions c2⟨l2⟩"
              unfolding c2 id[symmetric]
              by auto
          next

            show "?p2 ∈ positions c2⟨l2⟩"
              unfolding c2
              by auto
          next

            show "l1 = c2⟨l2⟩ !t ?p1"
              unfolding c2 id[symmetric]
              by simp
          next

            show "(l1, r1) ∈ R"
              using l1_r1 .
          qed

          then have "(c2⟨r2⟩, ?two⟦?p1 := r1⟧) ∈ (rewrite_in_context R)*" 
            unfolding c2 
            by simp

          moreover have "?one⟦?p2 := r2⟧ = (c1⟨l1⟩⟦?p2 := r2⟧⟦?p1 := r1⟧)"
            by (rule parallel_replace_at[OF parallel_p1_p2 p1 p2])

          then have "?one⟦?p2 := r2⟧ = ?two⟦?p1 := r1⟧" 
            unfolding c1 c2 id .

          ultimately show ?thesis
            unfolding less
            by (intro disjI1) auto
        qed
      qed
    qed
  qed
qed

lemma ground_critical_pairs_main: 
  assumes "(s, t1) ∈ rewrite_in_context R" "(s, t2) ∈ rewrite_in_context R"
  shows
    "(t1, t2) ∈ (rewrite_in_context R)↓ ∨
       (∃c l r. t1 = c⟨l⟩ ∧ t2 = c⟨r⟩ ∧
         ((l, r) ∈ ground_critical_pairs R ∨ (r, l) ∈ ground_critical_pairs R))"
  using assms ground_critical_peaks_main ground_critical_peak_to_pair
  by metis

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 t1 t2

  assume steps: "(s, t1) ∈ ?R" "(s, t2) ∈ ?R"

  let ?p = "λs'. (t1, s') ∈ ?R* ∧ (t2, 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 "(t1, t2) ∈ ?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