Theory Critical_Pairs

section ‹Critical Pairs›

theory Critical_Pairs
  imports
    Trs
    First_Order_Terms.Unification
begin

text‹We also consider overlaps between the same rule at top level,
   in this way we are not restricted to @{const wf_trs}.›
context
  fixes ren :: "'v :: infinite renaming2"  (* fix some renaming scheme *)
begin

definition
  critical_Peaks :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ((('f, 'v)term × ('f,'v)term × ('f,'v)term)) set"
  where
    "critical_Peaks P R = { ((C ⋅⇩c σ)⟨r' ⋅ τ⟩, l ⋅ σ, r ⋅ σ) | l r l' r' l'' C σ τ.
    (l, r) ∈ P ∧ (l', r') ∈ R ∧ l = C⟨l''⟩ ∧ is_Fun l'' ∧
    mgu_vd ren l'' l' = Some (σ, τ) }"

definition
  critical_pairs :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ (bool × ('f, 'v) rule) set"
  where
    "critical_pairs P R = { (C = □, (C ⋅⇩c σ)⟨r' ⋅ τ⟩, r ⋅ σ) | l r l' r' l'' C σ τ.
    (l, r) ∈ P ∧ (l', r') ∈ R ∧ l = C⟨l''⟩ ∧ is_Fun l'' ∧
    mgu_vd ren l'' l' = Some (σ, τ) }"

lemma critical_pairsI:
  assumes "(l, r) ∈ P" and "(l', r') ∈ R" and "l = C⟨l''⟩"
    and "is_Fun l''" and "mgu_vd ren l'' l' = Some (σ, τ)" and "t = r ⋅ σ"
    and "s = (C ⋅⇩c σ)⟨r' ⋅ τ⟩" and "b = (C = □)"
  shows "(b, s, t) ∈ critical_pairs P R"
  using assms unfolding critical_pairs_def by blast

lemma critical_pairs_mono:
  assumes "S⇩1 ⊆ R⇩1" and "S⇩2 ⊆ R⇩2" shows "critical_pairs S⇩1 S⇩2 ⊆ critical_pairs R⇩1 R⇩2"
  unfolding critical_pairs_def using assms by blast

lemma critical_Peaks_main:
  fixes P R :: "('f, 'v) trs"
  assumes tu: "(t, u) ∈ rrstep P" and ts: "(t, s) ∈ rstep R"
  shows "(s, u) ∈ (rstep R)^* O rrstep P O ((rstep R)^*)^-1 ∨
    (∃ C l m r σ. s = C⟨l ⋅ σ⟩ ∧ t = C⟨m ⋅ σ⟩ ∧ u = C⟨r ⋅ σ⟩ ∧ 
    (l, m, r) ∈ critical_Peaks P R)"
proof -
  let ?R = "rstep R"
  let ?CP = "critical_Peaks P R"
  from rrstepE[OF tu] obtain l1 r1 σ1 where lr1: "(l1, r1) ∈ P" and t1: "t = l1 ⋅ σ1" and u: "u = r1 ⋅ σ1" by auto
  from ts obtain C l2 r2 σ2 where lr2: "(l2, r2) ∈ R" and t2: "t = C⟨l2 ⋅ σ2⟩" and s: "s = C⟨r2 ⋅ σ2⟩" by auto
  from t1 t2 have id: "l1 ⋅ σ1 = C⟨l2 ⋅ σ2⟩" by auto
  let ?p = "hole_pos C"
  show ?thesis
  proof (cases "?p ∈ poss l1 ∧ is_Fun (l1 |_ ?p)")
    case True
    then have p: "?p ∈ poss l1" by auto
    from ctxt_supt_id [OF p] obtain D where Dl1: "D⟨l1 |_ ?p⟩ = l1"
      and D: "D = ctxt_of_pos_term (hole_pos C) l1" by blast
    from arg_cong [OF Dl1, of "λ t. t ⋅ σ1"]
    have "(D ⋅⇩c σ1)⟨(l1 |_ ?p) ⋅ σ1⟩ = C⟨l2 ⋅ σ2⟩" unfolding id by simp
    from arg_cong [OF this, of "λ t. t |_ ?p"]
    have "l2 ⋅ σ2 = (D ⋅⇩c σ1)⟨(l1 |_ ?p) ⋅ σ1⟩ |_ ?p" by simp
    also have "... = (D ⋅⇩c σ1)⟨(l1 |_ ?p) ⋅ σ1⟩ |_ (hole_pos (D ⋅⇩c σ1))"
      using hole_pos_ctxt_of_pos_term [OF p] unfolding D by simp
    also have "... = (l1 |_ ?p) ⋅ σ1" by (rule subt_at_hole_pos)
    finally have ident: "l2 ⋅ σ2 = l1 |_ ?p ⋅ σ1" by auto
    from mgu_vd_complete [OF ident [symmetric]]
    obtain μ1 μ2 ρ where mgu: "mgu_vd ren (l1 |_ ?p) l2 = Some (μ1, μ2)" and
      μ1: "σ1 = μ1 ∘⇩s ρ"
      and μ2: "σ2 = μ2 ∘⇩s ρ"
      and ident': "l1 |_ ?p ⋅ μ1 = l2 ⋅ μ2" by blast
    have in_cp: "((D ⋅⇩c μ1)⟨r2 ⋅ μ2⟩, l1 ⋅ μ1, r1 ⋅ μ1) ∈ ?CP"
      unfolding critical_Peaks_def
      apply clarify
      apply (intro exI conjI)
           apply (rule refl)
          apply (rule lr1)
         apply (rule lr2)
        apply (rule Dl1[symmetric])
       apply (rule True[THEN conjunct2])
      apply (rule mgu)
      done
    from hole_pos_ctxt_of_pos_term [OF p] D have pD: "?p = hole_pos D" by simp
    from id have C: "C = ctxt_of_pos_term ?p (l1 ⋅ σ1)" by simp
    have "C⟨r2 ⋅ σ2⟩ = (ctxt_of_pos_term ?p (l1 ⋅ σ1))⟨r2 ⋅ σ2⟩" using C by simp
    also have "... = (ctxt_of_pos_term ?p l1 ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" unfolding ctxt_of_pos_term_subst [OF p] ..
    also have "... = (D ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" unfolding D ..
    finally have Crσ: "C⟨r2 ⋅ σ2⟩ = (D ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" .
    show ?thesis unfolding Crσ s u t1 unfolding μ1 μ2
    proof (rule disjI2, intro exI, intro conjI)
      show "r1 ⋅ μ1 ∘⇩s ρ = □⟨r1 ⋅ μ1 ⋅ ρ⟩" by simp
    qed (insert in_cp, auto)
  next
    case False
    from pos_into_subst [OF id _ False]
    obtain q q' x where p: "?p = q @ q'" and q: "q ∈ poss l1" and l1q: "l1 |_ q = Var x" by auto
    have "l2 ⋅ σ2 = C⟨l2 ⋅ σ2⟩ |_ (q @ q')" unfolding p [symmetric] by simp
    also have "... = l1 ⋅ σ1 |_ (q @ q')" unfolding id ..
    also have "... = l1 |_ q ⋅ σ1 |_ q'" using q by simp
    also have "... = σ1 x |_ q'" unfolding l1q by simp
    finally have l2x: "l2 ⋅ σ2 = σ1 x |_ q'" by simp
    have pp: "?p ∈ poss (l1 ⋅ σ1)" unfolding id by simp
    then have "q @ q' ∈ poss (l1 ⋅ σ1)" unfolding p .
    then have "q' ∈ poss (l1 ⋅ σ1 |_ q)" unfolding poss_append_poss ..
    with q have "q' ∈ poss (l1 |_ q ⋅ σ1)" by auto
    then have q'x: "q' ∈ poss (σ1 x)" unfolding l1q by simp
    from ctxt_supt_id [OF q'x] obtain E where σ1x: "E⟨l2 ⋅ σ2⟩ = σ1 x"
      and E: "E = ctxt_of_pos_term q' (σ1 x)"
      unfolding l2x by blast
    let ?e = "E⟨r2 ⋅ σ2⟩"
    from hole_pos_ctxt_of_pos_term [OF q'x] E have q': "q' = hole_pos E" by simp
    from σ1x have σ1x': "σ1 x = E⟨l2 ⋅ σ2⟩" by simp
    let ?σ = "λ y. if y = x then ?e else σ1 y"
    have "(u, r1 ⋅ ?σ) ∈ (rstep R)^*" unfolding u
    proof (rule subst_rsteps_imp_rsteps)
      fix y
      show "(σ1 y, ?σ y) ∈ (rstep R)^*"
      proof (cases "y = x")
        case True
        show ?thesis unfolding True σ1x' using lr2 by auto
      qed simp
    qed
    hence r1u: "(r1 ⋅ ?σ, u) ∈ ((rstep R)^*)^-1" by auto
    show ?thesis
    proof (rule disjI1, intro relcompI)
      show "(r1 ⋅ ?σ, u) ∈ ((rstep R)^*)^-1" by fact
      show "(l1 ⋅ ?σ, r1 ⋅ ?σ) ∈ rrstep P" using lr1 by auto
      from q have ql1:  "q ∈ poss (l1 ⋅ σ1)" by simp
      have "s = replace_at (C⟨l2 ⋅ σ2⟩) ?p (r2 ⋅ σ2)" unfolding s by simp
      also have "... = replace_at (l1 ⋅ σ1) ?p (r2 ⋅ σ2)" unfolding id ..
      also have "... = replace_at (l1 ⋅ σ1) q ?e"
      proof -
        have "E = ctxt_of_pos_term q' (l1 ⋅ σ1 |_ q)"
          unfolding subt_at_subst [OF q] l1q E by simp
        then show ?thesis
          unfolding p
          unfolding ctxt_of_pos_term_append [OF ql1]
          by simp
      qed
      finally have s: "s = replace_at (l1 ⋅ σ1) q ?e" .
      from q l1q have "(replace_at (l1 ⋅ σ1) q ?e, l1 ⋅ ?σ) ∈ ?R^*"
      proof (induct l1 arbitrary: q)
        case (Fun f ls)
        from Fun(2, 3) obtain i p where q: "q = i # p" and i: "i < length ls" and p: "p ∈ poss (ls ! i)" and px: "ls ! i |_ p = Var x" by (cases q, auto)
        from i have "ls ! i ∈ set ls" by auto
        from Fun(1) [OF this p px] have rec: "(replace_at (ls ! i ⋅ σ1) p ?e, ls ! i ⋅ ?σ) ∈ ?R^*" .
        let ?lsσ = "map (λ t. t ⋅ σ1) ls"
        let ?lsσ' = "map (λ t. t ⋅ ?σ) ls"
        have id: "replace_at (Fun f ls ⋅ σ1) q ?e = Fun f (take i ?lsσ @ replace_at (ls ! i ⋅ σ1) p ?e # drop (Suc i) ?lsσ)" (is "_ = Fun f ?r")
          unfolding q using i by simp
        show ?case unfolding id unfolding eval_term.simps
        proof (rule all_ctxt_closedD [of UNIV])
          fix j
          assume j: "j < length ?r"
          show "(?r ! j, ?lsσ' ! j) ∈ ?R^*"
          proof (cases "j = i")
            case True
            show ?thesis using i True using rec by (auto simp: nth_append)
          next
            case False
            have "?r ! j = ?lsσ ! j"
              by (rule nth_append_take_drop_is_nth_conv, insert False i j, auto)
            also have "... = ls ! j ⋅ σ1" using j i by auto
            finally have idr: "?r ! j = ls ! j ⋅ σ1" .
            from j i have idl: "?lsσ' ! j = ls ! j ⋅ ?σ" by auto
            show ?thesis unfolding idr idl
            proof (rule subst_rsteps_imp_rsteps)
              fix y
              show "(σ1 y, ?σ y) ∈ ?R^*"
              proof (cases "y = x")
                case True then show ?thesis using σ1x' lr2 by auto
              qed simp
            qed
          qed
        qed (insert i, auto)
      qed simp
      then show "(s, l1 ⋅ ?σ) ∈ ?R^*" unfolding s .
    qed
  qed
qed

lemma critical_Peaks_main_rrstep:
  fixes R :: "('f, 'v) trs"
  assumes tu: "(t, u) ∈ rrstep R" and ts: "(t, s) ∈ rstep R"
  shows "(s, u) ∈ join (rstep R) ∨
    (∃ C l m r σ. s = C⟨l ⋅ σ⟩ ∧ t = C⟨m ⋅ σ⟩ ∧ u = C⟨r ⋅ σ⟩ ∧ 
    (l, m, r) ∈ critical_Peaks R R)"
  using critical_Peaks_main[OF assms] 
proof
  assume "(s, u) ∈ (rstep R)⇧* O rrstep R O ((rstep R)⇧*)¯" 
  also have "… ⊆ (rstep R)⇧* O ((rstep R)⇧*)¯" 
    unfolding rstep_iff_rrstep_or_nrrstep by regexp
  finally have "(s, u) ∈ join (rstep R)" by blast
  thus ?thesis by auto
qed auto

lemma parallel_rstep:
  fixes p1 :: pos
  assumes p12: "p1 ⊥ p2"
    and p1: "p1 ∈ poss t"
    and p2: "p2 ∈ poss t"
    and step2: "t |_ p2 = l2 ⋅ σ2" "(l2,r2) ∈ R" 
  shows "(replace_at t p1 v, replace_at (replace_at t p1 v) p2 (r2 ⋅ σ2)) ∈ rstep R" (is "(?one,?two) ∈ _")
proof -
  show ?thesis unfolding rstep_iff_rstep_r_p_s
  proof (intro exI)
    show "(?one,?two) ∈ rstep_r_p_s R (l2,r2) p2 σ2"
      unfolding rstep_r_p_s_def Let_def
      apply (intro CollectI, unfold split fst_conv snd_conv)
      using p1 p12 p2 step2
      by (metis ctxt_supt_id parallel_poss_replace_at parallel_replace_at_subt_at)
  qed
qed

lemma critical_Peaks_main_rstep:
  fixes R :: "('f, 'v) trs"
  assumes tu: "(t, u) ∈ rstep R" and ts: "(t, s) ∈ rstep R"
  shows "(s, u) ∈ join (rstep R) ∨
    (∃ C l m r σ. s = C⟨l ⋅ σ⟩ ∧ t = C⟨m ⋅ σ⟩ ∧ u = C⟨r ⋅ σ⟩ ∧ 
    ((l, m, r) ∈ critical_Peaks R R ∨ (r, m, l) ∈ critical_Peaks R R))"
proof - 
  let ?R = "rstep R"
  let ?CP = "critical_Peaks R R"
  from tu obtain C1 l1 r1 σ1 where lr1: "(l1, r1) ∈ R" and t1: "t = C1⟨l1 ⋅ σ1⟩" and u: "u = C1⟨r1 ⋅ σ1⟩" by auto
  from ts obtain C2 l2 r2 σ2 where lr2: "(l2, r2) ∈ R" and t2: "t = C2⟨l2 ⋅ σ2⟩" and s: "s = C2⟨r2 ⋅ σ2⟩" by auto
  define n where "n = size C1 + size 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
      with less(2,4) lr1 have tu: "(t, u) ∈ rrstep R" by auto
      from less(3,5) lr2 have ts: "(t, s) ∈ rstep R" by auto
      from critical_Peaks_main_rrstep[OF tu ts] show ?thesis by auto
    next
      case (More f1 bef1 D1 aft1) note C1 = this
      show ?thesis
      proof (cases C2)
        case Hole 
        with less(3,5) lr2 have ts: "(t, s) ∈ rrstep R" by auto
        from less(2,4) lr1 have tu: "(t, u) ∈ rstep R" by auto
        from critical_Peaks_main_rrstep[OF ts tu] show ?thesis by auto
      next
        case (More f2 bef2 D2 aft2) note C2 = this
        from less(2-3) C1 C2 
        have id: "(More f1 bef1 D1 aft1)⟨l1 ⋅ σ1⟩ = (More f2 bef2 D2 aft2)⟨l2 ⋅ σ2⟩" by auto
        let ?n1 = "length bef1"
        let ?n2 = "length bef2"
        from id have f: "f1 = f2" by simp
        show ?thesis
        proof (cases "?n1 = ?n2")
          case True
          with id have idb: "bef1 = bef2" and ida: "aft1 = aft2"
            and idD: "D1⟨l1 ⋅ σ1⟩ = D2⟨l2 ⋅ σ2⟩" by auto
          let ?C = "More f2 bef2 □ aft2"
          have id1: "C1 = ?C ∘⇩c D1" unfolding C1 f ida idb by simp
          have id2: "C2 = ?C ∘⇩c D2" unfolding C2 by simp
          define m where "m = size D1 + size D2" 
          have mn: "m < n" unfolding less m_def C1 C2 by auto
          note IH = less(1)[OF mn refl idD refl refl m_def]
          then show ?thesis
          proof
            assume "( D2⟨r2 ⋅ σ2⟩, D1⟨r1 ⋅ σ1⟩) ∈ join ?R"
            then obtain s' where seq1: "(D1⟨r1 ⋅ σ1⟩, s') ∈ ?R^*"
              and seq2: "(D2⟨r2 ⋅ σ2⟩, s') ∈ ?R^*" by auto
            from rsteps_closed_ctxt [OF seq1, of ?C]
            have seq1: "(C1⟨r1 ⋅ σ1⟩, ?C⟨s'⟩) ∈ ?R^*" using id1 by auto
            from rsteps_closed_ctxt [OF seq2, of ?C]
            have seq2: "(C2⟨r2 ⋅ σ2⟩, ?C⟨s'⟩) ∈ ?R^*" using id2 by auto
            from seq1 seq2 show ?thesis using less by auto
          next
            assume "∃C l m r σ. D2⟨r2 ⋅ σ2⟩ = C⟨l ⋅ σ⟩ ∧ D1⟨l1 ⋅ σ1⟩ = C⟨m ⋅ σ⟩ ∧ D1⟨r1 ⋅ σ1⟩ = C⟨r ⋅ σ⟩ ∧ ((l, m, r) ∈ ?CP ∨ (r, m, l) ∈ ?CP)"
            then obtain C l m r σ where idD: "D2⟨r2 ⋅ σ2⟩ = C⟨l ⋅ σ⟩" "D1⟨l1 ⋅ σ1⟩ = C⟨m ⋅ σ⟩" "D1⟨r1 ⋅ σ1⟩ = C⟨r ⋅ σ⟩" and mem: "((l, m, r) ∈ ?CP ∨ (r, m, l) ∈ ?CP)" by blast
            show ?thesis
              apply (intro disjI2)
              apply (unfold less id1 id2)
              apply (intro exI [of _ "?C ∘⇩c C"] exI)
              by (rule conjI [OF _ conjI [OF _ conjI[OF _ mem]]], insert idD, auto)
          qed
        next
          case False
          let ?p1 = "?n1 # hole_pos D1"
          let ?p2 = "?n2 # hole_pos D2"
          have l2: "C1⟨l1 ⋅ σ1⟩ |_ ?p2 = l2 ⋅ σ2" unfolding C1 id by simp
          have p12: "?p1  ⊥ ?p2" using False by simp
          have p1: "?p1 ∈ poss (C1⟨l1 ⋅ σ1⟩)" unfolding C1 by simp
          have p2: "?p2 ∈ poss (C1⟨l1 ⋅ σ1⟩)" unfolding C1 unfolding id by simp
          let ?one = "replace_at (C1⟨l1 ⋅ σ1⟩) ?p1 (r1 ⋅ σ1)"
          have one: "C1⟨r1 ⋅ σ1⟩ = ?one" unfolding C1 by simp
          from parallel_rstep [OF p12 p1 p2 l2 lr2, of "r1 ⋅ σ1"]
          have "(?one, replace_at ?one ?p2 (r2 ⋅ σ2)) ∈ rstep R" by auto
          then have one: "(C1⟨r1 ⋅ σ1⟩, replace_at ?one ?p2 (r2 ⋅ σ2)) ∈ (rstep R)^*" unfolding one by simp
          have l1: "C2⟨l2 ⋅ σ2⟩ |_ ?p1 = l1 ⋅ σ1" unfolding C2 id [symmetric] by simp
          have p21: "?p2  ⊥ ?p1" using False by simp
          have p1': "?p1 ∈ poss (C2⟨l2 ⋅ σ2⟩)" unfolding C2 id [symmetric] by simp
          have p2': "?p2 ∈ poss (C2⟨l2 ⋅ σ2⟩)" unfolding C2 by simp
          let ?two = "replace_at (C2⟨l2 ⋅ σ2⟩) ?p2 (r2 ⋅ σ2)"
          have two: "C2⟨r2 ⋅ σ2⟩ = ?two" unfolding C2 by simp
          from parallel_rstep [OF p21 p2' p1' l1 lr1, of "r2 ⋅ σ2"]
          have "(?two, replace_at ?two ?p1 (r1 ⋅ σ1)) ∈ rstep R" by auto
          then have two: "(C2⟨r2 ⋅ σ2⟩, replace_at ?two ?p1 (r1 ⋅ σ1)) ∈ (rstep R)^*" unfolding two by simp
          have "replace_at ?one ?p2 (r2 ⋅ σ2) = replace_at (replace_at (C1⟨l1 ⋅ σ1⟩) ?p2 (r2 ⋅ σ2)) ?p1 (r1 ⋅ σ1)"
            by (rule parallel_replace_at [OF p12 p1 p2])
          also have "... = replace_at ?two ?p1 (r1 ⋅ σ1)" unfolding C1 C2 id ..
          finally have one_two: "replace_at ?one ?p2 (r2 ⋅ σ2) = replace_at ?two ?p1 (r1 ⋅ σ1)" .
          show ?thesis unfolding less
            by (rule disjI1, insert one one_two two, auto)
        qed
      qed
    qed
  qed
qed

lemma critical_Peak_steps:
  fixes R :: "('f, 'v) trs" and S
  assumes cp: "(l, m, r) ∈ critical_Peaks R S"
  shows "(m, l) ∈ rstep S" "(m,r) ∈ rstep R" "(m,r) ∈ rrstep R" 
proof -
  from cp [unfolded critical_Peaks_def]
  obtain σ1 σ2 l1 l2 r1 r2 C where id: "r = r1 ⋅ σ1" "l = (C ⋅⇩c σ1)⟨r2 ⋅ σ2⟩" "m = (C ⋅⇩c σ1)⟨l1 ⋅ σ1⟩" 
    and r1: "(C⟨l1⟩, r1) ∈ R" and r2: "(l2, r2) ∈ S" and mgu: "mgu_vd ren l1 l2 = Some (σ1, σ2)" by auto
  have "(C⟨l1⟩ ⋅ σ1, r) ∈ rrstep R" unfolding id
    by (rule rrstepI [of "C⟨l1⟩" r1 _ _ σ1] r1, insert r1, auto)
  thus "(m,r) ∈ rrstep R" unfolding id by auto
  thus "(m,r) ∈ rstep R" by (rule rrstep_imp_rstep)
  from mgu_vd_sound [OF mgu] have change: "C⟨l1⟩ ⋅ σ1 = (C ⋅⇩c σ1)⟨l2 ⋅ σ2⟩" by simp
  have "(C⟨l1⟩ ⋅ σ1, l) ∈ rstep S" unfolding change id
    by (rule rstepI [OF r2, of _ _ σ2], auto)
  thus "(m, l) ∈ rstep S" unfolding id by auto
qed

lemma critical_Peak_to_pair: assumes "(l, m, r) ∈ critical_Peaks R R" 
  shows "∃ b. (b, l, r) ∈ critical_pairs R R" 
  using assms unfolding critical_Peaks_def critical_pairs_def by blast


lemma critical_pairs_main:
  fixes R :: "('f, 'v) trs"
  assumes st1: "(s, t1) ∈ rstep R" and st2: "(s, t2) ∈ rstep R"
  shows "(t1, t2) ∈ join (rstep R) ∨
    (∃ C b l r σ. t1 = C⟨l ⋅ σ⟩ ∧ t2 = C⟨r ⋅ σ⟩ ∧
    ((b, l, r) ∈ critical_pairs R R ∨ (b, r, l) ∈ critical_pairs R R))"
  using critical_Peaks_main_rstep[OF st2 st1]
proof 
  assume "∃C l m r σ.
       t1 = C⟨l ⋅ σ⟩ ∧ s = C⟨m ⋅ σ⟩ ∧ t2 = C⟨r ⋅ σ⟩ ∧ ((l, m, r) ∈ critical_Peaks R R ∨ (r, m, l) ∈ critical_Peaks R R)" 
  then obtain C l m r σ where id: "t1 = C⟨l ⋅ σ⟩" "t2 = C⟨r ⋅ σ⟩" and disj: "((l, m, r) ∈ critical_Peaks R R ∨ (r, m, l) ∈ critical_Peaks R R)" 
    by blast
  from critical_Peak_to_pair disj obtain b where "(b,l,r) ∈ critical_pairs R R ∨ (b,r,l) ∈ critical_pairs R R" by blast
  with id show ?thesis by blast
qed auto

lemma critical_pairs:
  fixes R :: "('f, 'v) trs"
  assumes cp: "⋀ l r b. (b, l, r) ∈ critical_pairs R R ⟹ l ≠ r ⟹
    ∃ l' r' s. instance_rule (l, r) (l', r') ∧ (l', s) ∈ (rstep R)⇧* ∧ (r', s) ∈ (rstep R)⇧*"
  shows "WCR (rstep R)"
proof
  let ?R = "rstep R"
  let ?CP = "critical_pairs R R"
  fix s t1 t2
  assume steps: "(s, t1) ∈ ?R" "(s, t2) ∈ ?R"
  let ?p = "λ s'. (t1, s') ∈ ?R^* ∧ (t2, s') ∈ ?R^*"
  from critical_pairs_main [OF steps]
  have "∃ s'. ?p s'"
  proof
    assume "∃ C b l r σ. t1 = C⟨l ⋅ σ⟩ ∧ t2 = C⟨r ⋅ σ⟩ ∧ ((b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP)"
    then obtain C b l r σ where id: "t1 = C⟨l ⋅ σ⟩" "t2 = C⟨r ⋅ σ⟩"
      and mem: "(b, l, r) ∈ ?CP ∨ (b, r, l) ∈ ?CP" by blast
    show ?thesis
    proof (cases "l = r")
      case True
      then show ?thesis unfolding id by auto
    next
      case False
      note sub_ctxt = rsteps_closed_ctxt [OF rsteps_closed_subst [OF rsteps_closed_subst]]
      from mem show ?thesis
      proof
        assume mem: "(b, l, r) ∈ ?CP"
        from cp [OF mem False] obtain l' r' s' τ where id2: "l = l' ⋅ τ" "r = r' ⋅ τ" and steps: "(l', s') ∈ ?R^*" "(r', s') ∈ ?R^*"
          unfolding instance_rule_def by auto
        show "∃ s'. ?p s'" unfolding id id2
          by (rule exI [of _ "C⟨s' ⋅ τ ⋅ σ⟩"], rule conjI, rule sub_ctxt [OF steps(1)], rule sub_ctxt [OF steps(2)])
      next
        assume mem: "(b, r, l) ∈ ?CP"
        from cp [OF mem] False obtain l' r' s' τ where id2: "r = l' ⋅ τ" "l = r' ⋅ τ" and steps: "(l', s') ∈ ?R^*" "(r', s') ∈ ?R^*"
          unfolding instance_rule_def by auto
        show "∃ s'. ?p s'" unfolding id id2
          by (rule exI [of _ "C⟨s' ⋅ τ ⋅ σ⟩"], rule conjI, rule sub_ctxt [OF steps(2)], rule sub_ctxt [OF steps(1)])
      qed
    qed
  qed auto
  then show "(t1, t2) ∈ join ?R" by auto
qed

lemma critical_pairs_fork:
  fixes R :: "('f, 'v) trs" and S
  assumes cp: "(b, l, r) ∈ critical_pairs R S"
  shows "(r, l) ∈ (rstep R)¯ O rstep S"
proof -
  from cp obtain m where "(l,m,r) ∈ critical_Peaks R S" 
    unfolding critical_pairs_def critical_Peaks_def by blast
  from critical_Peak_steps(1-2)[OF this] show ?thesis by auto
qed

lemma critical_pairs_fork': assumes "(b,l,r) ∈ critical_pairs R S" 
  shows "(l,r) ∈ (rstep S)^-1 O rstep R" 
  using critical_pairs_fork[OF assms] by auto

(* in the following lemma infiniteness of 'v is crucial, if one restricts to well-formed terms:
   Consider that we only have 5 variables and build the following TRS R = {
     f(g(x1, x2), g(x3, x4)) → h(x1, h(x2, g(x3, x4)))
     f(g(g(x1, x2), g(x3, x4)), x5) → h(x5, h(g(x1, x2), g(x3, x4)))
   the following rules are added to allow a join if one the arguments of
   the g's is a not a variable,
     h(g(k(_, _), _), h(_, _)) → ok for all k ∈ {f, g, h}
     h(g(_, k(_, _)), h(_, _)) → ok for all k ∈ {f, g, h}
     h(_, h(g(k(_, _), _), _)) → ok for all k ∈ {f, g, h}
     h(_, h(g(_, k(_, _)), _)) → ok for all k ∈ {f, g, h}
     h(_, h(_, g(k(_, _), _))) → ok for all k ∈ {f, g, h}
     h(_, h(_, g(_, k(_, _)))) → ok for all k ∈ {f, g, h}
     h(g(ok, _), h(_, _)) → ok
     h(g(_, ok), h(_, _)) → ok
     h(_, h(g(ok, _), _)) → ok
     h(_, h(g(_, ok), _)) → ok
     h(_, h(_, g(ok, _))) → ok
     h(_, h(_, g(_, ok))) → ok
   and we allow a join if two of the six arguments are identical
     h(g(x1, x2), h(g(x3, x4), g(x5, x))) → ok for all x ∈ {x1, .., x5}
     h(g(x1, x2), h(g(x3, x4), g(x, x5))) → ok for all x ∈ {x1, .., x5}
     h(g(x1, x2), h(g(x3, x), g(x4, x5))) → ok for all x ∈ {x1, .., x5}
     h(g(x1, x2), h(g(x, x3), g(x4, x5))) → ok for all x ∈ {x1, .., x5}
     h(g(x1, x), h(g(x2, x3), g(x4, x5))) → ok for all x ∈ {x1, .., x5}
     h(g(x, x1), h(g(x2, x3), g(x4, x5))) → ok for all x ∈ {x1, .., x5}
   moreover, we add one rule to join some other critical pairs
     h(x1, ok) → ok

  note that R is not WCR over the signature {f, g, h, ok} and variables {x1, .., x6} since in the critical pair
  h(g(x1, x2), h(g(x3, x4), g(x5, x6))) ← f(g(g(x1, x2), g(x3, x4)), g(x5, x6)) → h(g(x5, x6), h(g(x1, x2), g(x3, x4)))
  both h-terms are normal forms.
  However, one can prove that R over the signature {f, g, h, ok} and variables {x1, .., x5} is WCR,
  since the critical pair above cannot be build using only 5 variables, and if one of the arguments is chosen
  as non-variable, or if two arguments are identical, then both terms can be reduced to ok.
  Moreover, all over overlaps can easily be reduced to ok, too.
*)
lemma critical_pairs_complete:
  fixes R :: "('f, 'v) trs"
  assumes cp: "(b, l, r) ∈ critical_pairs R R"
    and no_join: "(l, r) ∉ (rstep R)⇧↓"
  shows "¬ WCR (rstep R)"
proof
  from critical_pairs_fork [OF cp] obtain u where ul: "(u, l) ∈ rstep R" and ur: "(u, r) ∈ rstep R" by force
  assume wcr: "WCR (rstep R)"
  with ul ur no_join show False unfolding WCR_on_def by auto
qed

lemma critical_pair_lemma:
  fixes R :: "('f, 'v) trs"
  shows "WCR (rstep R) ⟷
    (∀ (b, s, t) ∈ critical_pairs R R. (s, t) ∈ (rstep R)⇧↓)"
    (is "?l = ?r")
proof
  assume ?l
  with critical_pairs_complete [where R = R] show ?r by auto
next
  assume ?r
  show ?l
  proof (rule critical_pairs)
    fix b s t
    assume "(b, s, t) ∈ critical_pairs R R"
    with ‹?r› have "(s, t) ∈ join (rstep R)" by auto
    then obtain u where s: "(s, u) ∈ (rstep R)^*"
      and t: "(t, u) ∈ (rstep R)^*" by auto
    show "∃ s' t' u. instance_rule (s, t) (s', t') ∧ (s', u) ∈ (rstep R)^* ∧ (t', u) ∈ (rstep R)^*"
    proof (intro exI conjI)
      show "instance_rule (s, t) (s, t)" by simp
    qed (insert s t, auto)
  qed
qed

lemma critical_pairs_exI:
  fixes σ :: "('f, 'v) subst"
  assumes P: "(l, r) ∈ P" and R: "(l', r') ∈ R" and l: "l = C⟨l''⟩"
    and l'': "is_Fun l''" and unif: "l'' ⋅ σ = l' ⋅ τ"
    and b: "b = (C = □)"
  shows "∃ s t. (b, s, t) ∈ critical_pairs P R"
proof -
  from mgu_vd_complete [OF unif]
  obtain μ1 μ2  where mgu: "mgu_vd ren l'' l' = Some (μ1, μ2)" by blast
  show ?thesis
    by (intro exI, rule critical_pairsI [OF P R l l'' mgu refl refl b])
qed

end
end