Theory IsaFoR_Ground_Critical_Pairs

theory IsaFoR_Ground_Critical_Pairs
  imports 
    Parallel_Induct
    IsaFoR_Ground_Context
    Ground_Critical_Peaks
begin

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

type_synonym 'f ground_rewrite_system = "'f gterm rel"

interpretation ground_term_rewrite_system where
  hole = □ and apply_context = apply_ground_context and compose_context = "(∘c)"
  by unfold_locales

lemma parallel_rewrite_in_context:
  assumes 
    parallel: "p1 ⊥ p2" and
    p1_in_t: "p1 ∈ positionsG t" and
    p2_in_t: "p2 ∈ positionsG t" and
    l2: "l2 = t !tG p2" and
    l2_r2: "(l2, r2) ∈ R" 
  shows "(t⟦p1 := v⟧, t⟦p1 := v⟧⟦p2 := r2⟧) ∈ rewrite_in_context R" (is "(?t1,?t2) ∈ _")
proof (unfold rewrite_in_context_def mem_Collect_eq, intro exI conjI)
  let ?c = "t⟦p1 := v⟧ !c p2"

  show "(?t1, ?t2) = (?c⟨l2⟩G, ?c⟨r2⟩G)"
    unfolding l2 parallel_replace_atG[OF parallel p1_in_t p2_in_t] gsubt_at_id[OF p2_in_t] ..  
qed (rule l2_r2)

interpretation ground_critical_peaks where
  hole = □ and 
  apply_context = apply_ground_context and 
  compose_context = actxt_compose
proof unfold_locales
  fix R :: "'f ground_rewrite_system" and t u s
  assume 
    t_u: "(t, u) ∈ rewrite_in_context R" and
    t_s: "(t, s) ∈ rewrite_in_context R"

  show "(s, u) ∈ join (rewrite_in_context R) ∨
    (∃c l m r. s = c⟨l⟩G ∧ t = c⟨m⟩G ∧ u = c⟨r⟩G ∧ 
    ((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⟩G" and 
      u: "u = c1⟨r1⟩G"
      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⟩G" and 
      s: "s = c2⟨r2⟩G"
      unfolding rewrite_in_context_def
      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

        show ?thesis
          using l1_r1 l2_r2 less.prems
          unfolding ground_critical_peaks_def mem_Collect_eq
          by (metis Hole intp_actxt.simps(1))        
      next
        case c1: (More f1 ss1 c1' ts1)

        show ?thesis
        proof (cases c2)
          case Hole

          show ?thesis
            using l1_r1 l2_r2 less.prems
            unfolding ground_critical_peaks_def mem_Collect_eq
            by (metis Hole intp_actxt.simps(1))    
        next
          case c2: (More f2 ss2 c2' ts2)

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

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

          from id have f: "f1 = f2" 
            by simp

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

            with id have 
              ss: "ss1 = ss2" and 
              ts: "ts1 = ts2" and
              c': "c1'⟨l1⟩G = c2'⟨l2⟩G" 
              by auto

            let ?c = "More f2 ss2 □ ts2"

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

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

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

            have m_less_n: "m < n" 
              unfolding less m_def c1 c2 
              by auto

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

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

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

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

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

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

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

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

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

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

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

            have p2: "?p2 ∈ positionsG c1⟨l1⟩G"
              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⟩G !tG ?p2"
                unfolding c1 id
                by simp
            qed

            then have "(c1⟨r1⟩G, ?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 ∈ positionsG c2⟨l2⟩G"
                unfolding c2 id[symmetric]
                by auto
            next

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

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

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

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

            moreover have "?one⟦?p2 := r2⟧ = (c1⟨l1⟩G⟦?p2 := r2⟧⟦?p1 := r1⟧)"
              by (rule parallel_replace_atG[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
qed

end