Theory Conditional_Critical_Pairs

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2016)
Author:  Julian Nagele <julian.nagele@uibk.ac.at> (2017)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Conditional Critical Pairs›

theory Conditional_Critical_Pairs
imports
  Conditional_Rewriting
  QTRS.More_Abstract_Rewriting
begin

(*TODO: move*)
lemma greaterThanLessThan_all_conv:
  "(∀i∈{m <..< n}. P i) ⟷ (∀i. m < i ∧ i < n ⟶ P i)"
by auto

subsection ‹Conditional Overlaps and Conditional Critical Pairs›

definition "overlap R r r' p ⟷
  (∃p. p ∙ r ∈ R) ∧ (∃p. p ∙ r' ∈ R) ∧ vars_crule r ∩ vars_crule r' = {} ∧
  p ∈ funposs (clhs r) ∧ (∃σ. mgu (clhs r |_ p) (clhs r') = Some σ)"

definition
  CCP :: "('f, 'v :: infinite) ctrs ⇒ ('f, 'v) crule set"
where
  "CCP R =
    {((crhs ρ⇩1 ⋅ σ, replace_at (clhs ρ⇩1) p (crhs ρ⇩2) ⋅ σ), subst_list σ (snd ρ⇩1 @ snd ρ⇩2)) | ρ⇩1 ρ⇩2 σ p.
      overlap R ρ⇩1 ρ⇩2 p ∧ mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some σ ∧ (p = ε ⟶ ¬ (∃π. π ∙ ρ⇩1 = ρ⇩2))}"

lemma overlapI [intro]:
  assumes "∃π. π ∙ ρ⇩1 ∈ R" and "∃π. π ∙ ρ⇩2 ∈ R"
    and "vars_crule ρ⇩1 ∩ vars_crule ρ⇩2 = {}"
    and "p ∈ funposs (clhs ρ⇩1)"
    and "mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some σ"
  shows "overlap R ρ⇩1 ρ⇩2 p"
using assms unfolding overlap_def by blast

lemma overlap_mguD:
  assumes "overlap R ρ⇩1 ρ⇩2 p"
  obtains σ where "mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some σ"
using assms by (auto simp: overlap_def)

lemma CCP_I:
  assumes "∃π. π ∙ ρ⇩1 ∈ R" and "∃π. π ∙ ρ⇩2 ∈ R"
    and "vars_crule ρ⇩1 ∩ vars_crule ρ⇩2 = {}"
    and "p ∈ funposs (clhs ρ⇩1)"
    and "mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some σ"
    and "p = ε ⟹ ¬ (∃π. π ∙ ρ⇩1 = ρ⇩2)"
  shows "((crhs ρ⇩1 ⋅ σ, replace_at (clhs ρ⇩1) p (crhs ρ⇩2) ⋅ σ), subst_list σ (snd ρ⇩1 @ snd ρ⇩2)) ∈ CCP R"
using assms unfolding CCP_def by blast

text ‹
  Almost orthogonality modulo infeasibility (that is, all overlaps are either trivial,
  we have a root-overlap of two variants of the same rule,
  or the corresponding conditions are not all satisfiable at the same time).
›
definition almost_orthogonal :: "('f, 'v :: infinite) ctrs ⇒ bool"
where
  "almost_orthogonal R ⟷
    left_linear_trs (Ru R) ∧ (∀ρ⇩1 ρ⇩2 p. overlap R ρ⇩1 ρ⇩2 p ⟶
      (let μ = the (mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2)) in
      p = ε ∧ crhs ρ⇩1 ⋅ μ = crhs ρ⇩2 ⋅ μ ∨
      p = ε ∧ (∃p. p ∙ ρ⇩1 = ρ⇩2) ∨
      (∀m n. comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*) ⟶
        ¬ (∃σ. conds_n_sat R m (subst_list μ (snd ρ⇩1)) σ ∧
               conds_n_sat R n (subst_list μ (snd ρ⇩2)) σ))))"

lemma almost_orthogonal_imp_linear [simp]:
  "almost_orthogonal R ⟹ ((l, r), cs) ∈ R ⟹ linear_term l"
  by (auto simp: almost_orthogonal_def left_linear_trs_def Ru_def)

lemma almost_orthogonal_overlap_cases [consumes 2, cases pred: almost_orthogonal]:
  assumes "almost_orthogonal R" and "overlap R ρ⇩1 ρ⇩2 p"
  obtains (trivial) σ where "p = ε" and "mgu (clhs ρ⇩1) (clhs ρ⇩2) = Some σ"
    and "crhs ρ⇩1 ⋅ σ = crhs ρ⇩2 ⋅ σ"
  | (variants) π where "p = ε" and "π ∙ ρ⇩1 = ρ⇩2"
  | (infeasible) σ where "mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some σ"
    and "⋀m n. comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*) ⟹
      ¬ (∃τ. conds_n_sat R m (subst_list σ (snd ρ⇩1)) τ ∧
             conds_n_sat R n (subst_list σ (snd ρ⇩2)) τ)"
apply (rule overlap_mguD [OF ‹overlap R ρ⇩1 ρ⇩2 p›])
apply (insert assms)
apply (simp only: almost_orthogonal_def Let_def)
  by (metis option.sel subt_at.simps(1))

lemma CCP_E:
  fixes s :: "('f, 'v :: infinite) term"
  assumes "((s, t), cs) ∈ CCP R"
  shows "∃ρ⇩1 ρ⇩2 p σ. s = crhs ρ⇩1 ⋅ σ ∧ t = replace_at (clhs ρ⇩1) p (crhs ρ⇩2) ⋅ σ ∧
    cs = subst_list σ (snd ρ⇩1 @ snd ρ⇩2) ∧
    overlap R ρ⇩1 ρ⇩2 p ∧ mgu (clhs ρ⇩1 |_ p) (clhs ρ⇩2) = Some σ ∧ (p = ε ⟶ ¬ (∃π. π ∙ ρ⇩1 = ρ⇩2))"
using assms unfolding CCP_def by blast

end