theory Orthogonality
imports
"Check-NT.Critical_Pairs"
begin
text ‹this theory contains the result, that weak orthogonality implies confluence›
text ‹we prove the diamond property of par_rstep for weakly orthogonal systems.›
lemma weakly_orthogonal_main: fixes R :: "('f,string)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 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 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"
hence 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_var_disjoint_string_complete[OF unif] obtain μ1 μ2 δ where
mgu: "mgu_var_disjoint_string 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
hence "?bra ! j = ?r" using bef i by (simp add: nth_append)
thus ?thesis using tsi True by simp
next
case False
hence "?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
hence "δ x = σ x" unfolding delta by auto
thus ?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"
hence 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" .
}
hence "∀ 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)
thus ?thesis by simp
next
case (root_step l' r' τ)
hence t2: "t2 = r' ⋅ τ" by auto
have id: "Fun f ls = □⟨Fun f ls⟩" by simp
from mgu_var_disjoint_string_complete[OF root_step(1)] obtain mu1 mu2 delta where
mgu: "mgu_var_disjoint_string (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
hence id: "r ⋅ σ = r' ⋅ τ" unfolding sigma tau by simp
show ?thesis unfolding t2 id by auto
next
case (par_step_fun ts ls' g)
hence 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 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 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)" .
thus ?thesis unfolding CR_on_def join_def rtrancl_converse par_rsteps_rsteps .
qed
end