Theory Orthogonality

section‹Orthogonality›

theory Orthogonality
  imports 
    Critical_Pairs
    Parallel_Rewriting
begin

text ‹This theory contains the result, that weak orthogonality implies confluence.›

text ‹We prove the diamond property of @{const par_rstep} for weakly orthogonal systems.›       
context
  fixes ren :: "'v :: infinite renaming2" 
begin
lemma weakly_orthogonal_main: fixes R :: "('f,'v)trs"
  assumes st1: "(s,t1) ∈ par_rstep R" and st2: "(s,t2) ∈ par_rstep R" and weak_ortho:
    "left_linear_trs R" "⋀ b l r. (b,l,r) ∈ critical_pairs ren R R ⟹ l = r" 
    and wf: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
  shows "∃ u. (t1,u) ∈ par_rstep R ∧ (t2,u) ∈ par_rstep R"
proof -
  let ?R = "par_rstep R"
  let ?CP = "critical_pairs ren R R"
  {
    fix ls ts σ f r
    assume below: "⋀ i. i < length ls ⟹ ((map (λ l. l ⋅ σ) ls) ! i, ts ! i) ∈ ?R"
      and rule: "(Fun f ls, r) ∈ R"
      and len: "length ts = length ls"
    let ?ls = "map (λ l. l ⋅ σ) ls"
    from weak_ortho(1) rule have lin: "linear_term (Fun f ls)" unfolding left_linear_trs_def by auto
    let ?p1 = "λ τ i. ts ! i = ls ! i ⋅ τ ∧ (∀ x ∈ vars_term (ls ! i). (σ x, τ x) ∈ par_rstep R)"
    let ?p2 = "λ τ i. (∃ C l'' l' r'. ls ! i = C⟨l''⟩ ∧ is_Fun l'' ∧ (l',r') ∈ R ∧ (l'' ⋅ σ = l' ⋅ τ) ∧ ((C ⋅⇩c σ) ⟨ r' ⋅ τ ⟩, ts ! i) ∈ par_rstep R)"
    {
      fix i
      assume i: "i < length ls"
      then have i2: "i < length ts" using len by simp
      from below[OF i] have step: "(ls ! i ⋅ σ, ts ! i) ∈ ?R" using i by auto
      from i have mem: "ls ! i ∈ set ls" by auto
      from lin i have lin: "linear_term (ls ! i)" by auto
      from par_rstep_linear_subst[OF lin step] have "∃ τ. ?p1 τ i ∨ ?p2 τ i" .
    } note p12 = this
    have "∃ u. (r ⋅ σ, u) ∈ ?R ∧ (Fun f ts, u) ∈ ?R"
    proof (cases "∃ i τ. i < length ls ∧ ?p2 τ i")
      case True
      then obtain i τ where i: "i < length ls" and p2: "?p2 τ i" by blast
      from p2 obtain C l'' l' r' where lsi: "ls ! i = C ⟨ l'' ⟩" and l'': "is_Fun (l'')" and lr': "(l',r') ∈ R"
        and unif: "l'' ⋅ σ = l' ⋅ τ" and tsi: "((C ⋅⇩c σ) ⟨ r' ⋅ τ ⟩, ts ! i) ∈ ?R"  by blast
      from id_take_nth_drop[OF i] obtain bef aft where ls: "ls = bef @ C ⟨ l'' ⟩ # aft" and bef: "bef = take i ls" unfolding lsi by auto
      from i bef have bef: "length bef = i" by auto
      let ?C = "More f bef C aft"
      from bef have hp: "hole_pos ?C = i # hole_pos C" by simp
      have fls: "Fun f ls = ?C ⟨ l'' ⟩" unfolding ls by simp
      from mgu_vd_complete[OF unif] obtain μ1 μ2 δ where 
        mgu: "mgu_vd ren l'' l' = Some (μ1, μ2)" and id: "l'' ⋅ μ1 = l' ⋅ μ2" 
        and sigma: "σ = μ1 ∘⇩s δ" and tau: "τ = μ2 ∘⇩s δ" by blast
      let ?sig = "map (λ s. s ⋅ σ)"
      let ?r = "(C ⋅⇩c σ) ⟨ r' ⋅ τ⟩"
      let ?bra = "?sig bef @ ?r # ?sig aft"
      from weak_ortho(2)[OF critical_pairsI[OF rule lr' fls l'' mgu refl refl refl]]      
      have id: "r ⋅ σ = (?C ⋅⇩c σ) ⟨r' ⋅ τ ⟩" unfolding sigma tau by simp
      also have "... = Fun f ?bra" by simp
      also have "(..., Fun f ts) ∈ ?R"
      proof (rule par_rstep.par_step_fun)
        show "length ?bra = length ts" unfolding len unfolding ls by simp
      next
        fix j
        assume j: "j < length ts"
        show "(?bra ! j, ts ! j) ∈ ?R"
        proof (cases "j = i")
          case True
          then have "?bra ! j = ?r" using bef i by (simp add: nth_append)
          then show ?thesis using tsi True by simp
        next
          case False
          then have "?bra ! j = (?sig bef @ (C ⟨ l'' ⟩ ⋅ σ) # ?sig aft) ! j" using False bef i by (simp add: nth_append)
          also have "... = ?sig ls ! j" unfolding ls by simp
          finally show ?thesis
            using below[OF j[unfolded len]] by auto
        qed
      qed
      finally have step: "(r ⋅ σ, Fun f ts) ∈ ?R" .
      show "∃ u. (r ⋅ σ, u) ∈ ?R ∧ (Fun f ts, u) ∈ ?R" 
        by (rule exI, rule conjI[OF step par_rstep_refl])
    next
      case False
      with p12
      have "∀ i. (∃ τ. i < length ls ⟶ ?p1 τ i)" by blast
      from choice[OF this] obtain tau where tau: "⋀ i. i < length ls ⟹ ?p1 (tau i) i" by blast
      from lin have "is_partition (map vars_term ls)" by auto
      from subst_merge[OF this, of tau] obtain τ where τ: "⋀ i x. i < length ls ⟹ x ∈ vars_term (ls ! i) ⟹ τ x = tau i x"
        by blast
      obtain δ where delta: "δ = (λ x. if x ∈ vars_term (Fun f ls) then τ x else σ x)" by auto
      {
        fix i
        assume i: "i < length ls"
        from tau[OF i] have p: "?p1 (tau i) i" .
        have id1: "ls ! i ⋅ tau i = ls ! i ⋅ τ"
          by (rule term_subst_eq[OF τ[OF i, symmetric]])
        have id2: "... = ls ! i ⋅ δ"
          by (rule term_subst_eq, unfold delta, insert i, auto)
        have p: "?p1 δ i" using p using τ[OF i] unfolding id1 id2 using id2 unfolding delta by auto
      } note delt = this
      have r_delt: "(r ⋅ σ, r ⋅ δ) ∈ ?R"
      proof (rule all_ctxt_closed_subst_step)
        fix x
        assume x: "x ∈ vars_term r"
        show "(σ x, δ x) ∈ ?R" 
        proof (cases "x ∈ vars_term (Fun f ls)")
          case True
          then obtain l where l: "l ∈ set ls" and x: "x ∈ vars_term l" by auto
          from l[unfolded set_conv_nth] obtain i where i: "i < length ls" and l: "l = ls ! i" by auto
          from delt[OF i] x l show ?thesis by auto
        next
          case False
          then have "δ x = σ x" unfolding delta by auto
          then show ?thesis by auto
        qed
      qed auto
      {
        let ?ls = "map (λ l. l ⋅ δ) ls"
        have "ts = map (λ i. ts ! i) [0 ..< length ts]" by (rule map_nth[symmetric])
        also have "... = map (λ i. ts ! i) [0 ..< length ls]" unfolding len by simp
        also have "... = map (λ i. ?ls ! i) [0 ..< length ?ls]"
          by (rule nth_map_conv, insert delt[THEN conjunct1], auto)
        also have "... = ?ls"
          by (rule map_nth)
        finally have "Fun f ts = Fun f ls ⋅ δ" by simp
      } note id = this
      have l_delt: "(Fun f ts, r ⋅ δ) ∈ ?R" unfolding id
        by (rule par_rstep.root_step[OF rule])
      show "∃ u. (r ⋅ σ, u) ∈ ?R ∧ (Fun f ts, u) ∈ ?R"
        by (intro exI conjI, rule r_delt, rule l_delt)
    qed
  } note root_arg = this
  from st1 st2 show ?thesis
  proof (induct arbitrary: t2 rule: par_rstep.induct)
    case (par_step_var x t2)
    have t2: "t2 = Var x" 
      by (rule wf_trs_par_rstep[OF wf par_step_var])
    show "∃ u. (Var x,u) ∈ ?R ∧ (t2, u) ∈ ?R" unfolding t2
      by (intro conjI exI par_rstep.par_step_var, auto)
  next
    case (par_step_fun ts1 ss f t2)
    note IH = this
    show ?case using IH(4)
    proof (cases rule: par_rstep.cases)
      case (par_step_fun ts2)
      from IH(3) par_step_fun(3) have len: "length ts2 = length ts1" by simp
      {
        fix i
        assume i: "i < length ts1"
        then have i2: "i < length ts2" using len by simp
        from par_step_fun(2)[OF i2] have step2: "(ss ! i, ts2 ! i) ∈ ?R" .
        from IH(2)[OF i step2] have "∃ u. (ts1 ! i, u) ∈ ?R ∧ (ts2 ! i, u) ∈ ?R" .
      }
      then have "∀ i. ∃ u. (i < length ts1 ⟶ (ts1 ! i, u) ∈ ?R ∧ (ts2 ! i, u) ∈ ?R)" by blast
      from choice[OF this] obtain us where join: "⋀ i. i < length ts1 ⟹ (ts1 ! i, us i) ∈ ?R ∧ (ts2 ! i, us i) ∈ ?R" by blast
      let ?us = "map us [0 ..< length ts1]"
      {
        fix i
        assume i: "i < length ts1"
        from join[OF this] i have " (ts1 ! i, ?us ! i) ∈ ?R" "(ts2 ! i, ?us ! i) ∈ ?R" by auto 
      } note join = this
      let ?u = "Fun f ?us"
      have step1: "(Fun f ts1, ?u) ∈ ?R"
        by (rule par_rstep.par_step_fun[OF join(1)], auto)
      have step2: "(Fun f ts2, ?u) ∈ ?R"
        by (rule par_rstep.par_step_fun[OF join(2)], insert len, auto)
      show ?thesis unfolding par_step_fun(1) using step1 step2 by blast
    next
      case (root_step l r σ)
      from wf[OF root_step(3)] root_step(1) obtain ls where l: "l = Fun f ls"
        by auto
      from root_step(1) l have ss: "ss = map (λ l. l ⋅ σ) ls" (is "_ = ?ls") by simp
      from root_step(3) l have rule: "(Fun f ls, r) ∈ R" by simp
      from root_step(2) have t2: "t2 = r ⋅ σ" .
      from par_step_fun(3) ss have len: "length ts1 = length ls" by simp
      from root_arg[OF par_step_fun(1)[unfolded ss len] rule len]
      show ?thesis unfolding t2 by blast
    qed
  next
    case (root_step l r σ)
    note IH = this
    from wf[OF IH(1)] IH(1) obtain f ls where l: "l = Fun f ls" and rule: "(Fun f ls,r) ∈ R" 
      by (cases l, auto)
    from IH(2)[unfolded l] show ?case
    proof (cases rule: par_rstep.cases)
      case (par_step_var x)
      then show ?thesis by simp
    next
      case (root_step l' r' τ)
      then have t2: "t2 = r' ⋅ τ" by auto
      have id: "Fun f ls = □⟨Fun f ls⟩" by simp
      from mgu_vd_complete[OF root_step(1), of ren] obtain mu1 mu2 delta where 
        mgu: "mgu_vd ren (Fun f ls) l' = Some (mu1, mu2)" and sigma: "σ = mu1 ∘⇩s delta"
        and tau: "τ = mu2 ∘⇩s delta" by auto
      from weak_ortho(2)[OF critical_pairsI[OF rule root_step(3) id _ mgu refl refl]]
      have "r ⋅ mu1 = r' ⋅ mu2" by simp
      then have id: "r ⋅ σ = r' ⋅ τ" unfolding sigma tau by simp
      show ?thesis unfolding t2 id by auto
    next
      case (par_step_fun ts ls' g)
      then have ls': "ls' = map (λ l. l ⋅ σ) ls" and g: "g = f" and len: "length ts = length ls" by auto
      note par_step_fun = par_step_fun[unfolded ls' g len]
      from root_arg[OF par_step_fun(3) rule len]
      show ?thesis unfolding par_step_fun(2) .
    qed
  qed
qed


lemma weakly_orthogonal_par_rstep_CR:
  assumes weak_ortho: "left_linear_trs R" "⋀ b l r. (b,l,r) ∈ critical_pairs ren R R ⟹ l = r" 
    and wf: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
  shows "CR (par_rstep R)"
proof -
  let ?R = "par_rstep R"
  from weakly_orthogonal_main[OF _ _ weak_ortho wf] 
  have diamond: "⋀ s t1 t2. (s,t1) ∈ ?R ⟹ (s,t2) ∈ ?R ⟹ ∃ u. (t1,u) ∈ ?R ∧ (t2,u) ∈ ?R" .
  show ?thesis
    by (rule diamond_imp_CR, rule diamond_I, insert diamond, blast)
qed

lemma weakly_orthogonal_rstep_CR:
  assumes weak_ortho: "left_linear_trs R" "⋀ b l r. (b,l,r) ∈ critical_pairs ren R R ⟹ l = r" 
    and wf: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
  shows "CR (rstep R)"
proof -
  from weakly_orthogonal_par_rstep_CR[OF assms] have "CR (par_rstep R)" .
  then show ?thesis unfolding CR_on_def join_def rtrancl_converse par_rsteps_rsteps .
qed

end
end