section ‹Level Confluence›
theory Level_Confluence
imports
Conditional_Critical_Pairs
TA.Multihole_Context
begin
subsection ‹Properties of CTRSs›
lemma right_stable_perm_rhsD:
assumes "right_stable R" and "π ∙ ρ ∈ R" and "i < length (snd ρ)"
shows "(vars_term (clhs ρ) ∪ ⋃(vars_term ` lhss (set (take (Suc i) (snd ρ)))) ∪
⋃(vars_term ` (rhss (set (take i (snd ρ)))))) ∩ vars_term (snd (snd ρ ! i)) = {}"
proof -
have "i < length (snd (π ∙ ρ))" using assms by (cases ρ; simp add: eqvt)
with right_stable_rhsD [OF assms(1, 2) this]
show ?thesis
by (cases ρ; auto simp: eqvt [symmetric] take_map sup.commute sup.left_commute)
qed
lemma right_stable_perm_rhs_cases [consumes 3, case_names lct [linear cterm] gnf [ground nf]]:
assumes "right_stable R" and "π ∙ ρ ∈ R"
and "t ∈ rhss (set (snd ρ))"
obtains
(lct) "linear_term t" and "funas_term t ⊆ funas_ctrs R - {f. defined (Ru R) f}" |
(gnf) "ground t" and "t ∈ NF (rstep (Ru R))"
proof -
have "π ∙ t ∈ rhss (set (snd (π ∙ ρ)))"
using assms(3) and rule_pt.snd_eqvt by (fastforce simp: eqvt [symmetric])
from assms(1, 2) and this
show ?thesis by (cases rule: right_stable_rhs_cases) (auto intro: that)
qed
text ‹The usual definition of infeasibility is a sufficient condition.›
lemma infeasible_sufficient:
assumes "¬ (∃σ n. conds_n_sat R n (cs⇩1 @ cs⇩2) σ)"
shows "∀m n. comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*) ⟶
¬ (∃σ. conds_n_sat R m cs⇩1 σ ∧ conds_n_sat R n cs⇩2 σ)"
proof -
{ fix m n
have "¬ (∃σ. conds_n_sat R m cs⇩1 σ ∧ conds_n_sat R n cs⇩2 σ)"
using assms and conds_n_sat_mono [of m "max m n"] and conds_n_sat_mono [of n "max m n"] by force }
then show ?thesis by blast
qed
definition level_confluent :: "('f, 'v) ctrs ⇒ bool"
where
"level_confluent R ⟷ (∀ n. CR (cstep_n R n))"
lemma cstep_n_varpeak:
assumes "CCP R = {}" and rule1: "((l, r), cs) ∈ R"
and "linear_term l"
and l_σ: "l ⋅ σ = C⟨t⟩" and "C ≠ □" and cstep: "(t, u) ∈ cstep_n R n"
shows "∃τ. l ⋅ τ = C⟨u⟩ ∧ subst_domain τ ⊆ vars_term l ∧
(∀x ∈ vars_term l. (σ x, τ x) ∈ (cstep_n R n)⇧*)"
proof -
from cstep [THEN cstep_nE] obtain D l⇩2 r⇩2 σ⇩2 cs⇩2 k
where rule2: "((l⇩2, r⇩2), cs⇩2) ∈ R" and [simp]: "n = Suc k"
and conds: "conds_n_sat R k cs⇩2 σ⇩2"
and t: "t = D⟨l⇩2 ⋅ σ⇩2⟩" and u: "u = D⟨r⇩2 ⋅ σ⇩2⟩"
unfolding conds_n_sat_iff by metis
define p where "p ≡ hole_pos C <#> hole_pos D"
have *: "p ∈ poss (l ⋅ σ)" by (simp add: assms t p_def)
show ?thesis
proof (cases "p ∈ funposs l")
case False
with * obtain q⇩1 q⇩2 x
where p: "p = q⇩1 <#> q⇩2" and q⇩1: "q⇩1 ∈ poss l"
and lq⇩1: "l |_ q⇩1 = Var x" and q⇩2: "q⇩2 ∈ poss (σ x)"
by (rule poss_subst_apply_term)
moreover
have [simp]: "l ⋅ σ |_ p = l⇩2 ⋅ σ⇩2" using assms p_def t by auto
ultimately
have [simp]: "σ x |_ q⇩2 = l⇩2 ⋅ σ⇩2" by simp
define τ where "τ ≡ λy. if y = x then replace_at (σ x) q⇩2 (r⇩2 ⋅ σ⇩2) else (σ |s vars_term l) y"
have τ_x: "τ x = replace_at (σ x) q⇩2 (r⇩2 ⋅ σ⇩2)" by (simp add: τ_def)
have [simp]: "⋀y. y ∈ vars_term l ⟹ y ≠ x ⟹ τ y = σ y" by (simp add: τ_def)
have "(σ x, τ x) ∈ cstep_n R n"
proof -
let ?C = "ctxt_of_pos_term q⇩2 (σ x)"
have "(?C⟨l⇩2 ⋅ σ⇩2⟩, ?C⟨r⇩2 ⋅ σ⇩2⟩) ∈ cstep_n R n"
using conds by (auto intro!: cstep_n_SucI rule2 simp: conds_n_sat_iff)
then show ?thesis using q⇩2 by (simp add: τ_def replace_at_ident)
qed
then have "∀x ∈ vars_term l. (σ x, τ x) ∈ (cstep_n R n)⇧*" by (auto simp: τ_def)
moreover have "subst_domain τ ⊆ vars_term l"
using lq⇩1 and vars_term_subt_at [OF q⇩1]
by (auto simp: subst_domain_def τ_def subst_restrict_def)
moreover have "l ⋅ τ = C⟨u⟩"
proof -
have [simp]: "ctxt_of_pos_term p (l ⋅ σ) = C ∘⇩c D"
by (simp add: assms t p_def ctxt_of_pos_term_append)
have "l ⋅ σ |_ q⇩1 = σ x" by (simp add: lq⇩1 q⇩1)
from linear_term_replace_in_subst [OF ‹linear_term l› q⇩1 lq⇩1, of σ τ, OF _ τ_x, folded ctxt_ctxt_compose]
and q⇩1 and ctxt_of_pos_term_append [of q⇩1 "l ⋅ σ" q⇩2, folded p, unfolded this, symmetric]
show "l ⋅ τ = C⟨u⟩" by (simp add: u)
qed
ultimately show ?thesis by blast
next
case True
from vars_crule_disjoint obtain π⇩1
where π⇩1: "vars_crule (π⇩1 ∙ ((l, r), cs)) ∩ vars_crule ((l⇩2, r⇩2), cs⇩2) = {}" ..
define l⇩1 r⇩1 cs⇩1 σ⇩1 where "l⇩1 ≡ π⇩1 ∙ l" and "r⇩1 ≡ π⇩1 ∙ r"
and "cs⇩1 ≡ π⇩1 ∙ cs" and "σ⇩1 ≡ sop (-π⇩1) ∘⇩s σ"
note rename = l⇩1_def r⇩1_def cs⇩1_def σ⇩1_def
have *: "-π⇩1 ∙ ((l⇩1, r⇩1), cs⇩1) ∈ R" and "0 ∙ ((l⇩2, r⇩2), cs⇩2) ∈ R"
using rule1 and rule2 by (simp_all add: eqvt rename o_def)
then have rule_variants: "∃π. π ∙ ((l⇩1, r⇩1), cs⇩1) ∈ R" "∃π. π ∙ ((l⇩2, r⇩2), cs⇩2) ∈ R" by blast+
have disj: "vars_crule ((l⇩1, r⇩1), cs⇩1) ∩ vars_crule ((l⇩2, r⇩2), cs⇩2) = {}"
using π⇩1 by (auto simp: eqvt rename)
from True have funposs: "p ∈ funposs (clhs ((l⇩1, r⇩1), cs⇩1))" by (simp add: rename)
then have "p ∈ poss l⇩1" by (auto dest: funposs_imp_poss)
with vars_term_subt_at [OF this] and disj and l_σ
have "vars_term (l⇩1 |_ p) ∩ vars_term l⇩2 = {}" and "(l⇩1 |_ p) ⋅ σ⇩1 = l⇩2 ⋅ σ⇩2"
by (auto simp: eqvt vars_crule_def vars_rule_def rename)
(metis hole_pos_poss p_def subt_at_append subt_at_hole_pos subt_at_subst t)
from vars_term_disjoint_imp_unifier [OF this]
obtain μ where mgu: "mgu (l⇩1 |_ p) l⇩2 = Some μ"
using mgu_complete by (auto simp: unifiers_def)
have "p ≠ ε" using ‹C ≠ □› by (cases C) (simp_all add: p_def)
with CCP_I [OF rule_variants disj funposs] and mgu and ‹CCP R = {}›
show ?thesis by auto
qed
qed
subsection ‹Extended Parallel Rewriting›
definition "epar_n_mctxt R n C =
{(s, t). ∃ss ts. s =⇩f (C, ss) ∧ t =⇩f (C, ts) ∧
(∀i<length ss. (ss ! i, ts ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*)}"
definition "epar_n R n =
{(s, t). ∃C ss ts. s =⇩f (C, ss) ∧ t =⇩f (C, ts) ∧
(∀i<length ss. (ss ! i, ts ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*)}"
lemma epar_n_epar_n_mctxt_conv:
"(s, t) ∈ epar_n R n ⟷ (∃C. (s, t) ∈ epar_n_mctxt R n C)"
by (auto simp: epar_n_def epar_n_mctxt_def)
lemma epar_n_0 [simp]:
"epar_n R 0 = Id"
by (auto simp: epar_n_def eq_fill.simps list_eq_iff_nth_eq intro: arg_cong)
(metis eqfE mctxt_of_term)
lemma epar_n_SucE:
assumes "(s, t) ∈ epar_n R (Suc n)"
obtains C ss ts where "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "length ss = length ts"
and "∀i<length ss. (ss ! i, ts ! i) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*"
proof -
obtain C ss ts where "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "∀i<length ss. (ss ! i, ts ! i) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*"
using assms by (auto simp: epar_n_def)
then have "length ss = length ts" by (auto dest!: eqfE)
show ?thesis by (rule) fact+
qed
lemma epar_n_mctxt_SucE:
assumes "(s, t) ∈ epar_n_mctxt R (Suc n) C"
obtains ss ts where "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "length ss = length ts"
and "∀i<length ss. (ss ! i, ts ! i) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*"
using assms by (auto simp: epar_n_mctxt_def elim!: eq_fill.cases) (metis eqf_refl)
lemma epar_n_mctxtI:
assumes "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*"
shows "(s, t) ∈ epar_n_mctxt R n C"
using assms by (auto simp: epar_n_mctxt_def)
lemma epar_nI:
assumes "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*"
shows "(s, t) ∈ epar_n R n"
using assms by (auto simp: epar_n_def)
lemma trs_n_subset_epar_n:
"trs_n R n ⊆ epar_n R n"
by (auto intro!: epar_nI [of s MHole "[s]" t "[t]" R n for s t])
lemma epar_n_par_rstep_1_conv:
"epar_n R 1 = par_rstep (trs_n R 1)"
by (auto simp: epar_n_def) (force intro: par_rstep_mctxt par_rstep_id dest: par_rstep_mctxtD)+
lemma cstep_n_subset_epar_n:
"cstep_n R n ⊆ epar_n R n"
proof
fix s t
assume "(s, t) ∈ cstep_n R n"
then obtain C σ l r where [simp]: "s = C⟨l ⋅ σ⟩" and [simp]:"t = C⟨r ⋅ σ⟩"
and "(l, r) ∈ trs_n R n"
unfolding "cstep_n_rstep_trs_n_conv" by fast
then have "(l ⋅ σ, r ⋅ σ) ∈ trs_n R n" using trs_n_subst by fast
then show "(s, t) ∈ epar_n R n"
by (auto intro: epar_nI[OF mctxt_of_ctxt mctxt_of_ctxt])
qed
lemma epar_n_NF_imp_cstep_n_NF:
"t ∈ NF (epar_n R n) ⟹ t ∈ NF (cstep_n R n)"
using NF_anti_mono [OF cstep_n_subset_epar_n] by blast
lemma epar_n_subset_csteps_n:
"epar_n R n ⊆ (cstep_n R n)⇧*"
proof (cases n)
case (Suc k)
then show ?thesis
using rtrancl_mono [OF rstep_mono [OF trs_n_Suc_mono [of R k]]]
by (auto elim!: epar_n_SucE simp: cstep_n_rstep_trs_n_conv) (rule rsteps_mctxt, auto+)
qed simp
lemma epars_n_subset_csteps_n:
"(epar_n R n)⇧* ⊆ (cstep_n R n)⇧*"
using rtrancl_mono [OF epar_n_subset_csteps_n] and rtrancl_idemp by auto
lemma epar_n_refl [simp]:
"(t, t) ∈ epar_n R n"
by (auto simp: epar_n_def intro: mctxt_of_term)
lemma refl_epar_n:
"refl (epar_n R n)"
by (simp add: refl_on_def)
lemma csteps_n_subset_epar_n_Suc:
"(cstep_n R n)⇧* ⊆ epar_n R (Suc n)"
proof
fix s t
assume "(s, t) ∈ (cstep_n R n)⇧*"
then show "(s, t) ∈ epar_n R (Suc n)"
proof (induct)
case (step t u)
then show ?case
by (intro epar_nI [of _ MHole "[s]" _ "[u]"])
(auto elim!: epar_n_SucE dest: rtrancl_into_rtrancl)
qed simp
qed
lemma epar_n_Suc_mono:
"epar_n R n ⊆ epar_n R (Suc n)"
using epar_n_subset_csteps_n csteps_n_subset_epar_n_Suc by blast
lemma rtrancl_epar_n_conv:
"(epar_n R n)⇧* = (cstep_n R n)⇧*"
by (intro rtrancl_subset cstep_n_subset_epar_n epar_n_subset_csteps_n)
lemma epar_n_rtrancl_Suc_mono:
"(epar_n R n)⇧* ⊆ epar_n R (Suc n)"
using rtrancl_mono [OF epar_n_subset_csteps_n]
and csteps_n_subset_epar_n_Suc by (simp) blast
lemma epar_n_mono:
assumes "n ≤ m"
shows "epar_n R n ⊆ epar_n R m"
using assms
proof (induct "m - n" arbitrary: n)
case (Suc k)
then have "k = m - (Suc n)" and "Suc n ≤ m" by arith+
from Suc.hyps(1) [OF this]
show ?case using epar_n_Suc_mono by blast
qed simp
definition "epar R = (⋃n. epar_n R n)"
lemma epar_iff:
"(s, t) ∈ epar R ⟷ (∃n. (s, t) ∈ epar_n R n)"
by (auto simp: epar_def)
lemma all_ctxt_closed_epar_n [simp]:
"all_ctxt_closed UNIV (epar_n R n)"
proof -
{ fix f ts ss
assume [simp]: "length ts = length ss"
and "∀i<length ss. (ts ! i, ss ! i) ∈ epar_n R n"
then have "∀i<length ss. ∃C us vs.
ts ! i =⇩f (C, us) ∧ ss ! i =⇩f (C, vs) ∧
(∀i < length us. (us ! i, vs ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*)"
(is "∀i<length ss. ∃C us vs. ?P i C us vs") by (auto simp: epar_n_def)
then have "∀i<length ss. ∃x. ?P i (fst x) (fst (snd x)) (snd (snd x))" by force
then obtain c where "∀i<length ss. ?P i (fst (c i)) (fst (snd (c i))) (snd (snd (c i)))"
unfolding choice_iff' by blast
moreover
define Cs us vs where "Cs ≡ map (fst ∘ c) [0 ..< length ss]"
and "us ≡ map (fst ∘ snd ∘ c) [0 ..< length ss]"
and "vs ≡ map (snd ∘ snd ∘ c) [0 ..< length ss]"
ultimately have [simp]: "length Cs = length ts" "length us = length ts" "length vs = length ts"
and *: "∀i<length ss. ?P i (Cs ! i) (us ! i) (vs ! i)"
by (simp_all)
define C where "C ≡ MFun f Cs"
have "Fun f ts =⇩f (C, concat us)" and "Fun f ss =⇩f (C, concat vs)"
using * by (auto simp: C_def intro: eqf_MFunI)
moreover have "∀i<length (concat us). (concat us ! i, concat vs ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*"
using * by (intro concat_all_nth) (auto simp: eq_fill.simps)
ultimately have "(Fun f ts, Fun f ss) ∈ epar_n R n" by (auto intro!: epar_nI) }
then show ?thesis by (auto simp: all_ctxt_closed_def)
qed
lemma epar_n_mctxt:
assumes "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "∀i<length ss. (ss ! i, ts ! i) ∈ epar_n R n"
shows "(s, t) ∈ epar_n R n"
proof -
have [simp]: "length ss = length ts" using assms by (auto dest!: eqfE)
have [simp]: "t = fill_holes C ts" using assms by (auto dest: eqfE)
have "(s, fill_holes C ts) ∈ epar_n R n"
using assms by (intro eqf_all_ctxt_closed_step [of UNIV _ s C ss, THEN conjunct1]) auto
then show ?thesis by simp
qed
lemma epar_n_mctxt_mctxt:
assumes "s =⇩f (C, ss)" and "t =⇩f (C, ts)" and "length Cs = length ss"
and "∀i < length ss. (ss ! i, ts ! i) ∈ epar_n_mctxt R n (Cs ! i)"
shows "(s, t) ∈ epar_n_mctxt R n (fill_holes_mctxt C Cs)"
proof -
have "∀i < length ss. ∃us vs. ss ! i =⇩f (Cs ! i, us) ∧ ts ! i =⇩f (Cs ! i, vs) ∧
(∀j < length us. (us ! j, vs ! j) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*)"
using assms by (auto simp: epar_n_mctxt_def)
then obtain f and g where *: "∀i < length ss. ss ! i =⇩f (Cs ! i, f i) ∧ ts ! i =⇩f (Cs ! i, g i)"
and **: "∀i < length ss.
(∀j < length (f i). (f i ! j, g i ! j) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*)" by metis
moreover define sss tss where "sss ≡ map f [0 ..< length ss]" and "tss ≡ map g [0 ..< length ss]"
ultimately have "s =⇩f (fill_holes_mctxt C Cs, concat sss)"
and "t =⇩f (fill_holes_mctxt C Cs, concat tss)"
using assms by (auto intro: fill_holes_mctxt_sound elim!: eq_fill.cases)
moreover
{ fix i
assume "i < length (concat sss)"
from less_length_concat [OF this] obtain j k
where "j < length sss" and "k < length (sss ! j)"
and "i = sum_list (map length (take j sss)) + k"
and "concat sss ! i = sss ! j ! k" by blast
moreover then have "j < length tss" and "k < length (tss ! j)"
and "i = sum_list (map length (take j tss)) + k"
using *
by (auto simp: sss_def tss_def dest!: eqfE intro!: arg_cong [of _ _ sum_list] nth_equalityI)
moreover from concat_nth [OF this] have "concat tss ! i = tss ! j ! k" .
ultimately have "(concat sss ! i, concat tss ! i) ∈ trs_n R n ∪ (cstep_n R (n - 1))⇧*"
using ** by (auto simp: sss_def tss_def) }
ultimately show ?thesis by (rule epar_n_mctxtI)
qed
lemma Var_epar_n [dest]:
assumes "(Var x, t) ∈ epar_n R n"
and "∀((l, r), cs) ∈ R. is_Fun l"
shows "t = Var x"
using assms
by (cases n)
(force elim!: epar_n_SucE eq_fill.cases fill_holes_eq_Var_cases intro: fill_holes_MHole)+
lemma subst_epar_n_imp_epar_n:
fixes σ τ :: "('f, 'v) subst"
assumes "∀x ∈ vars_term t. (σ x, τ x) ∈ epar_n R n"
shows "(t ⋅ σ, t ⋅ τ) ∈ epar_n R n"
using assms by (intro all_ctxt_closed_subst_step) simp_all
lemma epar_n_ctxt:
assumes "(s, t) ∈ epar_n R n"
shows "(C⟨s⟩, C⟨t⟩) ∈ epar_n R n"
using epar_n_mctxt [of "C⟨s⟩" "mctxt_of_ctxt C" "[s]" "C⟨t⟩" "[t]" R n]
and assms by simp
lemma epar_n_rtrancl_all_ctxt_closed [simp]:
"all_ctxt_closed UNIV ((epar_n R n)⇧*)"
by (rule trans_ctxt_imp_all_ctxt_closed)
(auto simp: ctxt.closed_def elim!: ctxt.closure.cases intro: refl_rtrancl trans_rtrancl epar_n_ctxt [THEN rtrancl_map])
lemma subst_epar_n_imp_epar_n_rtrancl:
fixes σ τ :: "('f, 'v) subst"
assumes "∀x ∈ vars_term t. (σ x, τ x) ∈ (epar_n R n)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (epar_n R n)⇧*"
using assms by (intro all_ctxt_closed_subst_step) simp_all
lemma linear_term_epar_n_mctxt_cases':
fixes s :: "('f, 'v) term" and σ :: "('f, 'v) subst"
assumes "linear_term s"
and "(s ⋅ σ, t) ∈ epar_n_mctxt R (Suc n) C"
shows "(∃τ. t = s ⋅ τ ∧ (∀x. (σ x, τ x) ∈ epar_n R (Suc n))) ∨
(∃τ u p q. p ∈ hole_poss C ∧ p <#> q ∈ funposs s ∧
(∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*) ∧
(s ⋅ τ |_ (p <#> q), u) ∈ trs_n R (Suc n))"
(is "(∃τ. ?P1 τ s t) ∨ _" is "?P C s t")
using assms
proof (induction s arbitrary: C t)
case (Var x C t)
then show ?case
using epar_n_epar_n_mctxt_conv [THEN iffD2, of _ _ R]
by (intro disjI1 exI [of _ "λy. if x = y then t else σ y"]) auto
next
case (Fun f ss)
from epar_n_mctxt_SucE [OF Fun.prems(2)] obtain ts us
where eqf: "Fun f ss ⋅ σ =⇩f (C, ts)" "t =⇩f (C, us)" and [simp]: "length ts = length us"
and *: "∀i < length ts. (ts ! i, us ! i) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*" by blast
show ?case
proof (cases "C = MHole")
case True
with * have "(Fun f ss ⋅ σ, t) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*"
using eqf by (cases ts) (auto elim!: eq_fill.cases simp: Suc_length_conv)
then show ?thesis
proof
assume "(Fun f ss ⋅ σ, t) ∈ trs_n R (Suc n)"
with True have "ε ∈ hole_poss C"
and "ε <#> ε ∈ funposs (Fun f ss)"
and "(Fun f ss ⋅ σ |_ (ε <#> ε), t) ∈ trs_n R (Suc n)" by auto
then show ?thesis by blast
next
assume "(Fun f ss ⋅ σ, t) ∈ (cstep_n R n)⇧*"
with Fun.prems(1) show ?thesis
proof (cases rule: linear_term_rtrancl_cstep_n_cases)
case (varposs τ)
then show ?thesis using csteps_n_subset_epar_n_Suc [of R n] by blast
next
case (funposs τ q u)
moreover then have "ε <#> q ∈ funposs (Fun f ss)"
and "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
and "(Fun f ss ⋅ τ |_ (ε <#> q), u) ∈ trs_n R n"
using funposs_imp_poss [THEN vars_term_subt_at, of q "Fun f ss"] by auto
moreover have "ε ∈ hole_poss C" by (simp add: True)
ultimately show ?thesis using trs_n_Suc_mono [of R n] by blast
qed
qed
next
case False
then obtain Cs where C: "C = MFun f Cs"
and [simp]: "length Cs = length ss" "sum_list (map num_holes Cs) = length ts"
and eqfs: "∀i < length ss. (ss ! i) ⋅ σ =⇩f (Cs ! i, partition_holes ts Cs ! i)"
using eqf by (cases C) (auto dest!: eqf_Fun_MFun elim: eq_fill.cases)
let ?ts = "partition_holes ts Cs"
let ?us = "partition_holes us Cs"
let ?u = "λi. fill_holes (Cs ! i) (?us ! i)"
have "∀i < length ts. (ts ! i, us ! i) ∈ epar_n_mctxt R (Suc n) MHole"
using * by (auto intro!: epar_n_mctxtI [of s MHole "[s]" t "[t]" for s t])
then have "∀i < length ts. (concat ?ts ! i, concat ?us ! i) ∈ epar_n_mctxt R (Suc n) MHole"
by (simp)
then have **: "∀i < length ss. (∀j < length (?ts ! i). (?ts ! i ! j, ?us ! i ! j) ∈ epar_n_mctxt R (Suc n) MHole)"
using concat_nth_length [of _ ?ts]
by (auto simp: concat_nth_length partition_by_nth_nth take_map [symmetric])
{ fix i assume "i < length ss"
then have "((ss ! i) ⋅ σ, ?u i) ∈
epar_n_mctxt R (Suc n) (fill_holes_mctxt (Cs ! i) (replicate (num_holes (Cs ! i)) MHole))"
using eqfs and ** by (intro epar_n_mctxt_mctxt) (auto elim!: eq_fill.cases) }
with Fun(1, 2) have IH: "∀i < length ss. ?P (Cs ! i) (ss ! i) (?u i)" by auto
show ?thesis
proof (cases "∀i < length ss. (∃τ. ?P1 τ (ss ! i) (?u i))")
case False
then obtain i and τ and u and p and q where "i < length ss"
and "p ∈ hole_poss (Cs ! i)" and "p <#> q ∈ funposs (ss ! i)"
and "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
and "((ss ! i) ⋅ τ |_ (p <#> q), u) ∈ trs_n R (Suc n)"
using IH by blast
moreover then have "i <# p ∈ hole_poss C" and "(i <# p) <#> q ∈ funposs (Fun f ss)"
and "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
and "(Fun f ss ⋅ τ |_ ((i <# p) <#> q), u) ∈ trs_n R (Suc n)" by (auto simp: C)
ultimately show ?thesis by blast
next
case True
then obtain τ where **: "∀i < length ss. ?P1 (τ i) (ss ! i) (?u i)"
unfolding choice_iff' [of "λi. i < length ss"] by auto
have "is_partition (map vars_term ss)" using ‹linear_term (Fun f ss)› by simp
from subst_merge [OF this, of τ] obtain μ
where [simp]: "⋀i x. i < length ss ⟹ x ∈ vars_term (ss ! i) ⟹ μ x = τ i x" by blast
then have [simp]: "⋀i. i < length ss ⟹ ss ! i ⋅ τ i = ss ! i ⋅ μ"
by (simp add: term_subst_eq_conv)
let ?μ = "λx. if x ∈ vars_term (Fun f ss) then μ x else σ x"
have "t = Fun f ss ⋅ ?μ"
proof -
from eqf have "t = fill_holes C us" by (auto dest: eqfE)
moreover have "∀i < length Cs. fill_holes (Cs ! i) (?us ! i) = (ss ! i) ⋅ ?μ"
using ** by (auto intro!: term_subst_eq simp: subst_restrict_def)
ultimately show ?thesis
by (auto simp del: fill_holes.simps simp: C partition_holes_fill_holes_conv
intro: nth_map_conv)
qed
moreover have "∀x. (σ x, ?μ x) ∈ epar_n R (Suc n)"
using ** by (auto dest: in_set_idx)
ultimately show ?thesis by blast
qed
qed
qed
lemma linear_term_epar_n_mctxt_cases [consumes 2]:
fixes s :: "('f, 'v) term" and σ :: "('f, 'v) subst"
assumes "linear_term s"
and "(s ⋅ σ, t) ∈ epar_n_mctxt R (Suc n) C"
obtains (varposs) τ where "t = s ⋅ τ"
and "∀x. (σ x, τ x) ∈ epar_n R (Suc n)"
| (funposs) τ u p q where "p ∈ hole_poss C" and "p <#> q ∈ funposs s"
and "∀x. (σ x, τ x) ∈ (cstep_n R n)⇧*"
and "(s ⋅ τ |_ (p <#> q), u) ∈ trs_n R (Suc n)"
using linear_term_epar_n_mctxt_cases' [OF assms] by blast
lemma linear_term_epar_n_cases [consumes 2]:
fixes s :: "('f, 'v) term" and σ :: "('f, 'v) subst"
assumes "linear_term s"
and "(s ⋅ σ, t) ∈ epar_n R (Suc n)"
obtains (varposs) τ where "t = s ⋅ τ" and "∀x. (σ x, τ x) ∈ epar_n R (Suc n)"
| (funposs) τ u p where "p ∈ funposs s" and "(s ⋅ τ |_ p, u) ∈ trs_n R (Suc n)"
using assms by (auto simp: epar_n_epar_n_mctxt_conv elim!: linear_term_epar_n_mctxt_cases)
definition "supports_linear_cases R S ⟷ (∀s (σ::('f, 'v) subst) t P.
linear_term s ⟶ (s ⋅ σ, t) ∈ S ⟶
(∀τ. s ⋅ τ = t ⟶ (∀x. (σ x, τ x) ∈ S) ⟶ P) ⟶
(∀τ p u n. p ∈ funposs s ⟶ (s ⋅ τ |_ p, u) ∈ trs_n R n ⟶ P) ⟶ P)"
lemma supports_linear_cases [consumes 3]:
fixes σ :: "('f, 'v) subst"
assumes "supports_linear_cases R S" and "linear_term s" and "(s ⋅ σ, t) ∈ S"
obtains (varposs) τ where "s ⋅ τ = t" and "∀x. (σ x, τ x) ∈ S"
| (funposs) τ p u n where "p ∈ funposs s" and "(s ⋅ τ |_ p, u) ∈ trs_n R n"
using assms unfolding supports_linear_cases_def by metis
lemma conds_n_sat_extend_subst:
fixes R :: "('f, 'v::{infinite}) ctrs"
assumes linear_cases: "supports_linear_cases R S"
and refl: "refl S"
and acc: "all_ctxt_closed UNIV S"
and S_imp_csteps: "S ⊆ (cstep R)⇧*"
and comm: "comm ((cstep_n R m)⇧*) S"
and vars: "∀((l, r), cs) ∈ R. is_Fun l"
and rs: "right_stable R"
and rule: "π ∙ ((l, r), cs) ∈ R"
and "∀x. (σ x, τ x) ∈ S"
and conds: "conds_n_sat R m cs σ"
obtains δ where "∀x ∈ vars_term l. δ x = τ x" and "conds_n_sat R m cs δ"
and "∀x ∈ vars_term l ∪ ⋃(vars_rule ` set cs). (σ x, δ x) ∈ S"
proof -
have [simp]: "⋀x. (x, x) ∈ S" using refl by (simp add: refl_on_def)
let ?c = "λi. take i cs"
let ?V = "λi. ⋃(vars_rule ` set (?c i))"
let ?P⇩1 = "λδ. ∀x ∈ vars_term l. δ x = τ x"
let ?P⇩2 = "λδ i. conds_n_sat R m (?c i) δ"
let ?P⇩3 = "λδ i. ∀x ∈ vars_term l ∪ ?V i. (σ x, δ x) ∈ S"
{ fix i :: nat
assume "i ≤ length cs"
then have "∃δ. ?P⇩1 δ ∧ ?P⇩2 δ i ∧ ?P⇩3 δ i"
proof (induction i)
case 0
show ?case using assms by (intro exI [of _ τ]) (simp add: subst_compose)
next
case (Suc i)
then obtain δ⇩i where [simp]: "?P⇩1 δ⇩i"
and P⇩2: "?P⇩2 δ⇩i i" and P⇩3: "?P⇩3 δ⇩i i" and i: "i < length cs" by auto
let ?s = "fst (cs ! i)" and ?t = "snd (cs ! i)"
have [simp]: "take (Suc i) cs = take i cs @ [(?s, ?t)]"
using i by (simp add: take_Suc_conv_app_nth)
define δ' where [simp]: "δ' ≡ λx. if x ∈ vars_term ?s - (vars_term l ∪ ?V i) then σ x else δ⇩i x"
have "(?s ⋅ σ, ?t ⋅ σ) ∈ (cstep_n R m)⇧*"
using i and conds by (auto simp: conds_n_sat_iff)
moreover have "(?s ⋅ σ, ?s ⋅ δ') ∈ S"
using P⇩3 by (simp add: acc all_ctxt_closed_subst_step)
ultimately obtain t'
where n_t': "(?t ⋅ σ, t') ∈ S" and m_t': "(?s ⋅ δ', t') ∈ (cstep_n R m)⇧*"
using comm by (auto elim: commE)
have "?t ∈ rhss (set (snd ((l, r), cs)))" using i by auto
with rs and rule show ?case
proof (induct rule: right_stable_perm_rhs_cases)
case (gnf)
then have "?t ⋅ σ = ?t" and "?t ⋅ σ ∈ NF (cstep R)"
by (auto simp: ground_subst_apply dest: Ru_NF_imp_R_NF)
moreover with n_t' have "?t ⋅ σ = t'"
using S_imp_csteps by (auto dest: intro: NF_not_suc)
ultimately have t': "t' = ?t ⋅ δ'" using gnf.ground by (simp add: ground_subst_apply)
show ?thesis
proof (intro exI [of _ δ'] conjI)
{ fix s t
assume *: "(s, t) ∈ set (take i cs)"
with P⇩2 have "(s ⋅ δ⇩i, t ⋅ δ⇩i) ∈ (cstep_n R m)⇧*" by (auto simp: conds_n_sat_iff)
moreover have "s ⋅ δ' = s ⋅ δ⇩i" and "t ⋅ δ' = t ⋅ δ⇩i"
using * by (auto simp: vars_defs term_subst_eq_conv)
ultimately have "(s ⋅ δ', t ⋅ δ') ∈ (cstep_n R m)⇧*" by auto }
then have "conds_n_sat R m (take i cs) δ'" by (auto simp: conds_n_sat_iff)
then show "?P⇩2 δ' (Suc i)" using m_t' by (auto simp: t')
next
have "vars_term ?t = {}" using gnf by (simp add: ground_vars_term_empty)
then show "?P⇩3 δ' (Suc i)" using P⇩3 by (auto simp: vars_defs)
qed simp
next
case (lct)
from linear_cases and lct.linear and n_t' obtain γ
where "?t ⋅ γ = t'" and *: "∀x. (σ x, γ x) ∈ S"
using no_step_from_constructor [OF vars lct.cterm]
by (cases rule: supports_linear_cases; blast)
have inter: "(vars_term l ∪ ?V i ∪ vars_term ?s) ∩ vars_term ?t = {}"
using right_stable_perm_rhsD [OF rs rule, of i] by (auto simp: i vars_defs)
define δ where [simp]: "δ ≡ λx. (if x ∈ vars_term ?t then γ x else δ' x)"
show ?thesis using inter
proof (intro exI [of _ δ] conjI)
{ fix s t
assume *: "(s, t) ∈ set (take i cs)"
with P⇩2 have "(s ⋅ δ⇩i, t ⋅ δ⇩i) ∈ (cstep_n R m)⇧*" by (auto simp: conds_n_sat_iff)
moreover have "s ⋅ δ = s ⋅ δ⇩i" and "t ⋅ δ = t ⋅ δ⇩i"
using * and inter by (fastforce simp: vars_defs term_subst_eq_conv)+
ultimately have "(s ⋅ δ, t ⋅ δ) ∈ (cstep_n R m)⇧*" by auto }
then have [simp]: "conds_n_sat R m (take i cs) δ" using P⇩2 by (auto simp: conds_n_sat_iff)
have "?s ⋅ δ = ?s ⋅ δ'" and "?t ⋅ δ = ?t ⋅ γ"
using inter by (auto simp: term_subst_eq_conv vars_defs)
then have "(?s ⋅ δ, ?t ⋅ δ) ∈ (cstep_n R m)⇧*" using ‹?t ⋅ γ = t'› and m_t' by simp
then show "?P⇩2 δ (Suc i)" by (simp del: δ_def)
next
show "?P⇩3 δ (Suc i)" using P⇩3 and * by (auto simp: vars_defs)
qed auto
qed
qed }
then obtain δ where "∀x ∈ vars_term l. δ x = τ x" and "conds_n_sat R m cs δ"
and "∀x ∈ vars_term l ∪ ⋃(vars_rule ` set cs). (σ x, δ x) ∈ S" by force
then show ?thesis by (intro that) auto
qed
lemma supports_linear_cases_csteps_n:
"supports_linear_cases R ((cstep_n R n)⇧*)"
unfolding supports_linear_cases_def by (blast elim: linear_term_rtrancl_cstep_n_cases)
lemma epar_n_subset_csteps:
"epar_n R n ⊆ (cstep R)⇧*"
using epar_n_subset_csteps_n and csteps_n_subset_csteps by blast
lemma supports_linear_cases_epar_n:
"supports_linear_cases R (epar_n R (Suc n))"
unfolding supports_linear_cases_def by (blast elim: linear_term_epar_n_cases)
lemmas conds_n_sat_extend_subst_csteps_n =
conds_n_sat_extend_subst [OF supports_linear_cases_csteps_n refl_rtrancl
all_ctxt_closed_csteps_n csteps_n_subset_csteps]
lemmas conds_n_sat_extend_subst_epar_n =
conds_n_sat_extend_subst [OF supports_linear_cases_epar_n refl_epar_n all_ctxt_closed_epar_n
epar_n_subset_csteps]
lemma epar_n_varpeak':
assumes comm: "comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*)"
and vars: "∀((l, r), cs) ∈ R. is_Fun l"
and ao: "almost_orthogonal R"
and rs: "right_stable R"
and rule: "((l, r), cs) ∈ R"
and conds: "conds_n_sat R m cs σ"
and l_σ: "l ⋅ σ =⇩f (C, ts)" and "C ≠ MHole"
and epar: "∀i<length ts. (ts ! i, us ! i) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*"
and len: "length us = length ts"
shows "∃τ. l ⋅ τ =⇩f (C, us) ∧ (∀x. (σ x, τ x) ∈ epar_n R (Suc n))"
proof -
have "linear_term l" using assms by simp
have "(l ⋅ σ, fill_holes C us) ∈ epar_n_mctxt R (Suc n) C"
using epar and l_σ and len
by (intro epar_n_mctxtI [OF l_σ, of "fill_holes C us" us]) (auto elim!: eq_fill.cases)
with ‹linear_term l› show ?thesis
proof (cases rule: linear_term_epar_n_mctxt_cases)
case (varposs τ)
moreover then have "l ⋅ τ =⇩f (C, us)" using l_σ and len by (auto elim!: eq_fill.cases)
ultimately show ?thesis by blast
next
case (funposs τ u p q)
obtain l⇩2 r⇩2 cs⇩2 σ⇩2
where l_τ: "l ⋅ τ |_ (p <#> q) = l⇩2 ⋅ σ⇩2" and u: "u = r⇩2 ⋅ σ⇩2"
and rule2: "((l⇩2, r⇩2), cs⇩2) ∈ R"
and conds2: "conds_n_sat R n cs⇩2 σ⇩2"
by (rule funposs(4) [THEN trs_n_SucE]) (auto simp: cstep_n_rstep_trs_n_conv conds_n_sat_iff)
from vars_crule_disjoint obtain π⇩1
where π⇩1: "vars_crule (π⇩1 ∙ ((l, r), cs)) ∩ vars_crule ((l⇩2, r⇩2), cs⇩2) = {}" ..
define l⇩1 r⇩1 cs⇩1 σ⇩1 where "l⇩1 ≡ π⇩1 ∙ l" and "r⇩1 ≡ π⇩1 ∙ r"
and "cs⇩1 ≡ π⇩1 ∙ cs" and "σ⇩1 ≡ sop (-π⇩1) ∘⇩s τ"
note rename = this
have rule1: "-π⇩1 ∙ ((l⇩1, r⇩1), cs⇩1) ∈ R" and "0 ∙ ((l⇩2, r⇩2), cs⇩2) ∈ R"
using rule and rule2 by (simp_all add: eqvt rename o_def)
then have rule_variants: "∃π. π ∙ ((l⇩1, r⇩1), cs⇩1) ∈ R" "∃π. π ∙ ((l⇩2, r⇩2), cs⇩2) ∈ R" by blast+
have disj: "vars_crule ((l⇩1, r⇩1), cs⇩1) ∩ vars_crule ((l⇩2, r⇩2), cs⇩2) = {}"
using π⇩1 by (auto simp: eqvt rename)
from funposs have fp: "p <#> q ∈ funposs (clhs ((l⇩1, r⇩1), cs⇩1))" by (simp add: rename)
then have "p <#> q ∈ poss l⇩1" by (auto dest: funposs_imp_poss)
with vars_term_subt_at [OF this] and disj and l_τ
have "vars_term (l⇩1 |_ (p <#> q)) ∩ vars_term l⇩2 = {}" and "(l⇩1 |_ (p <#> q)) ⋅ σ⇩1 = l⇩2 ⋅ σ⇩2"
by (auto simp: vars_crule_def vars_rule_def rename)
(metis subt_at_eqvt term_pt.permute_minus_cancel(2))
from vars_term_disjoint_imp_unifier [OF this]
obtain μ where mgu: "mgu (l⇩1 |_ (p <#> q)) l⇩2 = Some μ"
using mgu_complete by (auto simp: unifiers_def)
let ?σ = "σ ∘ Rep_perm (-π⇩1)"
have "∀x. (?σ x, σ⇩1 x) ∈ (cstep_n R n)⇧*" using funposs(3) by (simp add: rename subst_compose)
moreover have "conds_n_sat R m cs⇩1 ?σ"
using conds
by (simp only: rename conds_n_sat_perm_shift o_assoc [symmetric] Rep_perm_add [symmetric])
(simp add: Rep_perm_0)
ultimately obtain ν
where conds1: "conds_n_sat R m cs⇩1 ν" and ν: "∀x ∈ vars_term l⇩1. ν x = σ⇩1 x"
using conds_n_sat_extend_subst_csteps_n [OF comm vars rs rule1] by metis
define δ where "δ ≡ λx. if x ∈ vars_crule ((l⇩1, r⇩1), cs⇩1) then ν x else σ⇩2 x"
from funposs have fp: "p <#> q ∈ funposs (clhs ((l⇩1, r⇩1), cs⇩1))" by (simp add: rename)
then have pq: "p <#> q ∈ poss l⇩1" by (auto dest: funposs_imp_poss)
with vars_term_subt_at [OF pq] and disj and l_τ
have "(l⇩1 |_ (p <#> q)) ⋅ σ⇩1 = l⇩2 ⋅ σ⇩2"
by (auto simp: rename; metis subt_at_eqvt term_pt.permute_minus_cancel(2))
moreover have "(l⇩1 |_ (p <#> q)) ⋅ σ⇩1 = (l⇩1 |_ (p <#> q)) ⋅ δ" and "l⇩2 ⋅ σ⇩2 = l⇩2 ⋅ δ"
using vars_term_subt_at [OF pq] and disj and ν
unfolding term_subst_eq_conv
by (auto simp: δ_def σ⇩1_def vars_crule_def vars_rule_def)
ultimately have eq: "(l⇩1 |_ (p <#> q)) ⋅ δ = l⇩2 ⋅ δ" by simp
then have "δ ∈ unifiers {(l⇩1 |_ (p <#> q), l⇩2)}" by (simp add: unifiers_def)
with mgu_sound [OF mgu] have [simp]: "μ ∘⇩s δ = δ" by (simp add: is_imgu_def)
{ fix s t assume "(s, t) ∈ set cs⇩2"
then have "s ⋅ δ = s ⋅ σ⇩2" and "t ⋅ δ = t ⋅ σ⇩2"
using disj by (force simp: term_subst_eq_conv δ_def vars_crule_def vars_defs)+ }
then have "conds_n_sat R n cs⇩2 δ" using conds2 by (auto simp: conds_n_sat_iff)
then have conds2': "conds_n_sat R n (subst_list μ cs⇩2) δ" by (simp add: conds_n_sat_subst_list)
{ fix s t assume "(s, t) ∈ set cs⇩1"
then have "s ⋅ δ = s ⋅ ν" and "t ⋅ δ = t ⋅ ν"
by (auto simp: term_subst_eq_conv δ_def vars_crule_def vars_defs) }
then have "conds_n_sat R m cs⇩1 δ" using conds1 by (auto simp: conds_n_sat_iff)
then have conds1': "conds_n_sat R m (subst_list μ cs⇩1) δ" by (simp add: conds_n_sat_subst_list)
from overlapI [OF rule_variants disj fp] and mgu
have "overlap R ((l⇩1, r⇩1), cs⇩1) ((l⇩2, r⇩2), cs⇩2) (p <#> q)" by auto
with ao show ?thesis
using funposs(1) and ‹C ≠ MHole› and conds1' and conds2' and comm and mgu
by (cases; cases C) auto
qed
qed
context
fixes R :: "('f, 'v :: infinite) ctrs"
assumes ao: "almost_orthogonal R"
and epo: "extended_properly_oriented R"
and rs: "right_stable R"
and t3: "type3 R"
and vars: "∀((l, r), cs) ∈ R. is_Fun l"
begin
lemma trs_n_peak:
assumes "(s, t) ∈ trs_n R (Suc m)" and "(s, u) ∈ trs_n R (Suc n)"
and "⋀m' n'. m' + n' < (Suc m) + (Suc n) ⟹ comm ((epar_n R m')⇧*) ((epar_n R n')⇧*)"
shows "∃v. (t, v) ∈ epar_n R (Suc n) ∧ (u, v) ∈ epar_n R (Suc m)"
proof -
from assms(1) obtain l⇩1' r⇩1' cs⇩1' σ⇩1' where s1: "s = l⇩1' ⋅ σ⇩1'" and t: "t = r⇩1' ⋅ σ⇩1'"
and rule1': "((l⇩1', r⇩1'), cs⇩1') ∈ R"
and cs1': "∀(s', t') ∈ set cs⇩1'. (s' ⋅ σ⇩1', t' ⋅ σ⇩1') ∈ (rstep (trs_n R m))⇧*"
and conds1': "conds_n_sat R m cs⇩1' σ⇩1'"
by (auto elim: trs_n_SucE simp: conds_n_sat_iff cstep_n_rstep_trs_n_conv)
from assms(2) obtain l⇩2 r⇩2 cs⇩2 σ⇩2 where s2: "s = l⇩2 ⋅ σ⇩2" and u: "u = r⇩2 ⋅ σ⇩2"
and rule2: "((l⇩2, r⇩2), cs⇩2) ∈ R"
and cs2: "∀(s', t') ∈ set cs⇩2. (s' ⋅ σ⇩2, t' ⋅ σ⇩2) ∈ (rstep (trs_n R n))⇧*"
and conds2: "conds_n_sat R n cs⇩2 σ⇩2"
by (auto elim: trs_n_SucE simp: conds_n_sat_iff cstep_n_rstep_trs_n_conv)
from vars_crule_disjoint obtain π⇩1
where π⇩1: "vars_crule (π⇩1 ∙ ((l⇩1', r⇩1'), cs⇩1')) ∩ vars_crule ((l⇩2, r⇩2), cs⇩2) = {}" ..
define l⇩1 r⇩1 cs⇩1 σ⇩1 where "l⇩1 ≡ π⇩1 ∙ l⇩1'" and "r⇩1 ≡ π⇩1 ∙ r⇩1'"
and "cs⇩1 ≡ π⇩1 ∙ cs⇩1'" and "σ⇩1 ≡ sop (-π⇩1) ∘⇩s σ⇩1'"
note rename = l⇩1_def r⇩1_def cs⇩1_def σ⇩1_def
have rule1: "-π⇩1 ∙ ((l⇩1, r⇩1), cs⇩1) ∈ R" and "0 ∙ ((l⇩2, r⇩2), cs⇩2) ∈ R"
using rule1' and rule2 by (simp_all add: eqvt rename o_def)
then have rule_variants: "∃π. π ∙ ((l⇩1, r⇩1), cs⇩1) ∈ R" "∃π. π ∙ ((l⇩2, r⇩2), cs⇩2) ∈ R" by blast+
have disj: "vars_crule ((l⇩1, r⇩1), cs⇩1) ∩ vars_crule ((l⇩2, r⇩2), cs⇩2) = {}"
using π⇩1 by (auto simp: eqvt rename)
have "ε ∈ funposs l⇩1'" using rule1' and vars by (cases l⇩1') (auto)
then have funposs: "ε ∈ funposs (clhs ((l⇩1, r⇩1), cs⇩1))" by (simp add: rename)
have "vars_term (l⇩1 |_ ε) ∩ vars_term l⇩2 = {}"
and l: "(l⇩1 |_ ε) ⋅ σ⇩1 = l⇩2 ⋅ σ⇩2" using s1 and s2 and disj
by (auto simp: vars_crule_def vars_rule_def rename)
from vars_term_disjoint_imp_unifier [OF this]
obtain μ where mgu: "mgu (l⇩1 |_ ε) l⇩2 = Some μ"
using mgu_complete by (auto simp: unifiers_def)
have "overlap R ((l⇩1, r⇩1), cs⇩1) ((l⇩2, r⇩2), cs⇩2) ε"
using overlapI [OF rule_variants disj funposs] and mgu by auto
with ao have "r⇩1 ⋅ μ = r⇩2 ⋅ μ ∨ (∃π. π ∙ ((l⇩1, r⇩1), cs⇩1) = ((l⇩2, r⇩2), cs⇩2)) ∨
(∀m n. comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*) ⟶
¬ (∃σ. conds_n_sat R m (subst_list μ cs⇩1) σ ∧ conds_n_sat R n (subst_list μ cs⇩2) σ))"
using mgu by (cases) (auto)
moreover {
define τ where "τ ≡ λx. if x ∈ vars_crule ((l⇩1, r⇩1), cs⇩1) then σ⇩1 x else σ⇩2 x"
have "l⇩1 ⋅ τ = l⇩1 ⋅ σ⇩1" and "l⇩2 ⋅ τ = l⇩2 ⋅ σ⇩2"
and [simp]: "r⇩1 ⋅ τ = r⇩1 ⋅ σ⇩1" "r⇩2 ⋅ τ = r⇩2 ⋅ σ⇩2"
using disj by (auto simp: term_subst_eq_conv vars_crule_def vars_rule_def τ_def)
then have "l⇩1 ⋅ τ = l⇩2 ⋅ τ" using l by simp
from the_mgu [OF this] and mgu have "τ = μ ∘⇩s τ" by (auto simp: the_mgu_def)
moreover assume "r⇩1 ⋅ μ = r⇩2 ⋅ μ"
ultimately have "r⇩1 ⋅ τ = r⇩2 ⋅ τ" by (metis subst_subst)
then have "(t, t) ∈ epar_n R (Suc n) ∧ (u, t) ∈ epar_n R (Suc m)"
by (simp add: t u) (simp add: rename)
then have ?thesis ..
}
moreover {
assume "∀m n. comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*) ⟶
¬ (∃σ. conds_n_sat R m (subst_list μ cs⇩1) σ ∧ conds_n_sat R n (subst_list μ cs⇩2) σ)"
moreover have "comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*)" using assms(3) [of m n]
by (auto simp: rtrancl_epar_n_conv)
ultimately have infeasible:
"¬ (∃σ. conds_n_sat R m (subst_list μ cs⇩1) σ ∧ conds_n_sat R n (subst_list μ cs⇩2) σ)" by blast
define δ where "δ ≡ λx. if x ∈ vars_crule ((l⇩1, r⇩1), cs⇩1) then σ⇩1 x else σ⇩2 x"
have "l⇩1 ⋅ δ = l⇩1 ⋅ σ⇩1" and "l⇩2 ⋅ δ = l⇩2 ⋅ σ⇩2"
using disj by (auto simp: term_subst_eq_conv δ_def vars_crule_def vars_defs)
then have "l⇩1 ⋅ δ = l⇩2 ⋅ δ" using l by simp
then have "δ ∈ unifiers {(l⇩1, l⇩2)}" by (simp add: unifiers_def)
then have [simp]: "μ ∘⇩s δ = δ" using mgu_sound [OF mgu] by (simp add: is_imgu_def)
{ fix s t assume "(s, t) ∈ set cs⇩1"
then have "s ⋅ δ = s ⋅ sop (-π⇩1) ∘⇩s σ⇩1'" and "t ⋅ δ = t ⋅ sop (-π⇩1) ∘⇩s σ⇩1'"
using disj
unfolding term_subst_eq_conv
by (auto simp: δ_def vars_crule_def vars_defs σ⇩1_def) }
then have "conds_n_sat R m cs⇩1 δ"
using conds1' by (auto simp: conds_n_sat_iff) (auto simp: rename eqvt)
then have conds1: "conds_n_sat R m (subst_list μ cs⇩1) δ" by (simp add: conds_n_sat_subst_list)
{ fix s t assume "(s, t) ∈ set cs⇩2"
then have "s ⋅ δ = s ⋅ σ⇩2" and "t ⋅ δ = t ⋅ σ⇩2"
using disj by (force simp: term_subst_eq_conv δ_def vars_crule_def vars_defs)+ }
then have "conds_n_sat R n cs⇩2 δ"
using conds2 by (auto simp: conds_n_sat_iff)
then have conds2: "conds_n_sat R n (subst_list μ cs⇩2) δ" by (simp add: conds_n_sat_subst_list)
with infeasible and conds1 have ?thesis by blast
}
moreover {
assume "∃π. π ∙ ((l⇩1, r⇩1), cs⇩1) = ((l⇩2, r⇩2), cs⇩2)"
then obtain π where vt: "π ∙ ((l⇩1, r⇩1), cs⇩1) = ((l⇩2, r⇩2), cs⇩2)" using mgu by auto
let ?σ⇩2 = "(sop π) ∘⇩s σ⇩2"
have σ: "∀x ∈ vars_term l⇩1. σ⇩1 x = ?σ⇩2 x"
using vt l by (auto simp: subst_compose permute_term_subst_apply_term term_subst_eq_conv eqvt)
have ?thesis
proof (cases "vars_term r⇩1 ⊆ vars_term l⇩1")
case True
then have "r⇩1 ⋅ σ⇩1 = r⇩1 ⋅ ?σ⇩2" unfolding term_subst_eq_conv using σ by auto
then have "(t, t) ∈ epar_n R (Suc n) ∧ (u, t) ∈ epar_n R (Suc m)"
using vt u t r⇩1_def σ⇩1_def σ by (auto simp add: term_subst_eq_conv eqvt)
then show ?thesis ..
next
case False
let ?ρ⇩1 = "((l⇩1, r⇩1), cs⇩1)"
from epo [unfolded extended_properly_oriented_def, THEN bspec, OF rule1']
have "vars_term r⇩1' ⊆ vars_term l⇩1' ∨ (∃m ≤ length cs⇩1'.
(∀i < m. vars_term (fst (cs⇩1' ! i)) ⊆ X_vars ((l⇩1', r⇩1'), cs⇩1') i) ∧
(∀i ∈ {m ..< length cs⇩1'}. vars_term r⇩1' ∩ vars_rule (cs⇩1' ! i) ⊆
X_vars ((l⇩1', r⇩1'), cs⇩1') m))" by simp
with False obtain k where "k ≤ length cs⇩1'"
and "(∀i < k. vars_term (fst (cs⇩1' ! i)) ⊆ X_vars ((l⇩1', r⇩1'), cs⇩1') i) ∧
(∀i ∈ {k ..< length cs⇩1'}. vars_term r⇩1' ∩ vars_rule (cs⇩1' ! i) ⊆ X_vars ((l⇩1', r⇩1'), cs⇩1') k)"
apply (auto simp: l⇩1_def r⇩1_def cs⇩1_def eqvt)
using atom_set_pt.subset_eqvt permute_boolI vars_term_eqvt by blast
from this(1) and permute_boolI [OF this(2), of π⇩1, unfolded eqvt bool_pt.all_eqvt' bool_pt.ball_eqvt']
have k: "k ≤ length cs⇩1"
and ext_vars1: "∀i < k. vars_term (fst (cs⇩1 ! i)) ⊆ X_vars ?ρ⇩1 i"
and ext_vars2: "∀i∈{k ..< length cs⇩1}. vars_term r⇩1 ∩ vars_rule (cs⇩1 ! i) ⊆ X_vars ?ρ⇩1 k"
by (auto simp: l⇩1_def r⇩1_def cs⇩1_def eqvt)
let ?c = "λi. take (min i k) cs⇩1"
let ?V = "λi. ⋃(vars_rule ` set (?c i))"
let ?d = "λi. take (i - k) (drop k cs⇩1)"
let ?W = "λi. vars_term r⇩1 ∩ ⋃(vars_rule ` set (?d i))"
let ?P⇩1 = "λσ. ∀x ∈ vars_term l⇩1. σ x = σ⇩1 x ∧ σ⇩1 x = ?σ⇩2 x"
let ?P⇩2 = "λσ i. ∀x ∈ vars_term l⇩1 ∪ ?V i ∪ ?W i.
(σ⇩1 x, σ x) ∈ (epar_n R n)⇧* ∧ (?σ⇩2 x, σ x) ∈ (epar_n R m)⇧*"
have "vars_term r⇩1' ⊆ vars_term l⇩1' ∪ ⋃(vars_rule ` set cs⇩1')"
using t3 and rule1' by (force simp: type3_def vars_defs)
from permute_boolI [OF this, of π⇩1, unfolded eqvt]
have t3': "vars_term r⇩1 ⊆ vars_term l⇩1 ∪ ⋃(vars_rule ` set cs⇩1)"
by (auto simp: l⇩1_def r⇩1_def cs⇩1_def eqvt)
have "set (take (min (length cs⇩1) k) cs⇩1) ∪
set (take (length cs⇩1 - k) (drop k cs⇩1)) = set cs⇩1"
by (metis append_take_drop_id k length_drop min.absorb2 order_refl set_append take_all)
then have rhs: "vars_term r⇩1 ⊆ vars_term l⇩1 ∪ ?V (length cs⇩1) ∪ ?W (length cs⇩1)"
using t3' by force
{ fix i :: nat
assume "i ≤ length cs⇩1"
then have "∃σ. ?P⇩1 σ ∧ ?P⇩2 σ i"
proof (induction i)
case 0
show ?case using σ by (intro exI [of _ σ⇩1]; simp add: o_def)
next
case (Suc i)
then obtain σ where a: "?P⇩1 σ" and c: "?P⇩2 σ i" and i: "i < length cs⇩1"
by (auto simp: subst_compose)
let ?s = "fst (cs⇩1 ! i)" and ?t = "snd (cs⇩1 ! i)"
have [simp]: "take (Suc i) cs⇩1 = take i cs⇩1 @ [(?s, ?t)]"
by (auto simp: i take_Suc_conv_app_nth)
consider "i > k" | "i = k" | "i < k" by arith
then show ?case
proof (cases)
case 1
then have "k ≤ i" by auto
have "?P⇩1 σ" by fact
moreover have "?P⇩2 σ (Suc i)"
using c and ext_vars2 [THEN bspec, of i] and 1 and k and i
apply (simp add: min_def Suc_diff_le [OF ‹k ≤ i›] take_Suc_conv_app_nth X_vars_def)
apply (unfold vars_rule_def)
by (blast 8)
ultimately show ?thesis by blast
next
case [simp]: 2
have "?P⇩1 σ" by fact
moreover have "?P⇩2 σ (Suc i)"
using ext_vars2 [THEN bspec, of i] and c and k and i
by (auto simp add: min_def X_vars_def take_Suc_conv_app_nth vars_rule_def)
ultimately show ?thesis by blast
next
case 3
from ext_vars1 [THEN spec, THEN mp, OF 3]
have ssubs: "vars_term ?s ⊆ vars_term l⇩1 ∪ ?V i"
using 3 by (auto simp: min_def X_vars_def vars_rule_def)
then have "∀x ∈ vars_term ?s. (σ⇩1 x, σ x) ∈ (epar_n R n)⇧* ∧ (?σ⇩2 x, σ x) ∈ (epar_n R m)⇧*"
using c by auto
then have 1: "(?s ⋅ σ⇩1, ?s ⋅ σ) ∈ (epar_n R n)⇧*" and 2: "(?s ⋅ ?σ⇩2, ?s ⋅ σ) ∈ (epar_n R m)⇧*"
using subst_epar_n_imp_epar_n_rtrancl [of ?s σ⇩1 σ R n]
and subst_epar_n_imp_epar_n_rtrancl [of ?s ?σ⇩2 σ R m] by auto
from cs2 and vt have "(?s ⋅ ?σ⇩2, ?t ⋅ ?σ⇩2) ∈ (rstep (trs_n R n))⇧*" by (auto simp: i eqvt)
from rev_subsetD [OF this] have 3: "(?s ⋅ ?σ⇩2, ?t ⋅ ?σ⇩2) ∈ (epar_n R n)⇧*"
using cstep_n_rstep_trs_n_conv [of R n] and cstep_n_subset_epar_n [of R n]
by (auto simp add: rtrancl_mono)
from i and cs1' have "(?s ⋅ σ⇩1, ?t ⋅ σ⇩1) ∈ (rstep (trs_n R m))⇧*"
by (auto simp: cs⇩1_def σ⇩1_def eqvt)
from rev_subsetD [OF this] have 4: "(?s ⋅ σ⇩1, ?t ⋅ σ⇩1) ∈ (epar_n R m)⇧*"
using cstep_n_rstep_trs_n_conv [of R m] and cstep_n_subset_epar_n [of R m]
by (auto simp add: rtrancl_mono)
from assms(3) have comm: "comm ((epar_n R m)⇧*) ((epar_n R n)⇧*)" by auto
obtain u where 8: "(?t ⋅ σ⇩1, u) ∈ (epar_n R n)⇧*"
and 5: "(?s ⋅ σ, u) ∈ (epar_n R m)⇧*"
using commE [OF comm 4 1] by auto
from 2 and 5 have 6: "(?s ⋅ ?σ⇩2, u) ∈ (epar_n R m)⇧*" by auto
obtain s' where 9: "(u, s') ∈ (epar_n R n)⇧*"
and 10: "(?t ⋅ ?σ⇩2, s') ∈ (epar_n R m)⇧*"
using commE [OF comm 6 3] by auto
from 8 9 have 7: "(?t ⋅ σ⇩1, s') ∈ (epar_n R n)⇧*" by auto
have "?t ∈ rhss (set (snd ((l⇩1, r⇩1), cs⇩1)))" using Suc by auto
with rs and rule1 show ?thesis
proof (induct rule: right_stable_perm_rhs_cases)
case gnf
show ?thesis
proof (intro exI [of _ σ] conjI)
show "?P⇩1 σ" by (fact a)
next
from gnf.ground have "vars_term ?t = {}" by (simp add: ground_vars_term_empty)
with ssubs have "vars_rule (?s, ?t) ⊆ vars_term l⇩1 ∪ ?V i" by (simp add: vars_defs)
then show "?P⇩2 σ (Suc i)" using c and ‹i < k› and k and i
by (auto simp: min_def)
qed
next
case lct
from lct.linear and 10 obtain γ
where *: "?t ⋅ γ = s'" "∀x. (?σ⇩2 x, γ x) ∈ (epar_n R m)⇧*"
using no_step_from_constructor [OF vars lct.cterm]
by (auto elim: linear_term_rtrancl_cstep_n_cases simp: rtrancl_epar_n_conv
simp del: subst_subst_compose)
from lct.linear and 7 obtain δ
where **: "?t ⋅ δ = s'" "∀x ∈ vars_term ?t. (σ⇩1 x, δ x) ∈ (epar_n R n)⇧*"
using no_step_from_constructor [OF vars lct.cterm]
by (auto elim: linear_term_rtrancl_cstep_n_cases simp: rtrancl_epar_n_conv)
have inter: "(vars_term l⇩1 ∪ ?V i ∪ vars_term ?s) ∩ vars_term ?t = {}"
using right_stable_perm_rhsD [OF rs rule1, of i] and ‹i < k›
by (auto simp: min_def i vars_defs)
let ?ρ⇩i = "λx. (if x ∈ vars_term ?t then δ x else σ x)"
show ?thesis
proof (intro exI [of _ ?ρ⇩i] conjI)
from inter have "∀x ∈ vars_term l⇩1. ?ρ⇩i x = σ x" by auto
then show "?P⇩1 ?ρ⇩i" using a by auto
next
{ fix x
assume "x ∈ vars_term l⇩1 ∪ ?V (Suc i) ∪ ?W (Suc i)"
then have "x ∈ vars_term l⇩1 ∪ ?V i ∨ x ∈ vars_term ?t"
using ssubs and i and ‹i < k› and 3
by (auto simp: min_def vars_defs split: if_splits)
then have "(σ⇩1 x, ?ρ⇩i x) ∈ (epar_n R n)⇧* ∧ (?σ⇩2 x, ?ρ⇩i x) ∈ (epar_n R m)⇧*"
proof
assume "x ∈ vars_term l⇩1 ∪ ?V i"
moreover with c have "(σ⇩1 x, σ x) ∈ (epar_n R n)⇧*"
and "(?σ⇩2 x, σ x) ∈ (epar_n R m)⇧*" by auto
ultimately show ?thesis using inter by (auto simp: vars_defs)
next
assume "x ∈ vars_term ?t"
with * and ** show ?thesis using ‹i < k› and 3
by (auto simp: term_subst_eq_conv)
qed }
then show "?P⇩2 ?ρ⇩i (Suc i)" ..
qed
qed
qed
qed }
from this [OF le_refl] obtain ρ where C: "?P⇩2 ρ (length cs⇩1)" by auto
have "vars_term r⇩1' ⊆ vars_term l⇩1' ∪ ⋃(vars_rule ` set cs⇩1')"
using t3 and rule1' by (force simp: type3_def vars_defs)
from permute_boolI [OF this, of π⇩1, unfolded eqvt]
have "vars_term r⇩1 ⊆ vars_term l⇩1 ∪ ⋃(vars_rule ` set cs⇩1)"
by (auto simp add: l⇩1_def r⇩1_def cs⇩1_def eqvt)
from rhs and C subst_epar_n_imp_epar_n_rtrancl [of r⇩1 _ _ R]
have "(r⇩1 ⋅ σ⇩1, r⇩1 ⋅ ρ) ∈ (epar_n R n)⇧*"
and "(r⇩1 ⋅ ?σ⇩2, r⇩1 ⋅ ρ) ∈ (epar_n R m)⇧*"
by (simp_all add: subset_eq subst_compose_def)
moreover have "u = π ∙ r⇩1 ⋅ σ⇩2" using vt by (simp add: u eqvt)
ultimately have "(t, r⇩1 ⋅ ρ) ∈ epar_n R (Suc n)"
and "(u, r⇩1 ⋅ ρ) ∈ epar_n R (Suc m)"
using epar_n_rtrancl_Suc_mono
by (auto simp: t r⇩1_def σ⇩1_def)
then show ?thesis by blast
qed }
ultimately show ?thesis by blast
qed
lemma epar_n_varpeak:
assumes s: "s =⇩f (C, ts)" and ne: "C ≠ MHole" and len: "length us = length ts"
and trs_m: "(s, t) ∈ trs_n R (Suc m)"
and *: "∀i < length ts. (ts ! i, us ! i) ∈ trs_n R (Suc n) ∪ (cstep_n R n)⇧*"
and comm1: "⋀m' n'. m' + n' < (Suc m) + (Suc n) ⟹ comm ((epar_n R m')⇧*) ((epar_n R n'))"
and comm2: "⋀m' n'. m' + n' < (Suc m) + (Suc n) ⟹ comm ((epar_n R m')⇧*) ((epar_n R n')⇧*)"
shows "∃v. (t, v) ∈ epar_n R (Suc n) ∧ (fill_holes C us, v) ∈ epar_n R (Suc m)"
proof -
obtain l r σ cs
where s': "s = l ⋅ σ" and t: "t = r ⋅ σ"
and rule: "((l, r), cs) ∈ R"
and ***: "∀(s⇩i, t⇩i) ∈ set cs. (s⇩i ⋅ σ, t⇩i ⋅ σ) ∈ (rstep (trs_n R m))⇧*"
by (rule trs_n_SucE [OF trs_m])
then have l_σ: "l ⋅ σ =⇩f (C, ts)" and conds: "conds_n_sat R m cs σ"
using s by (auto simp: conds_n_sat_iff cstep_n_rstep_trs_n_conv)
from comm2 [of m n] have comm: "comm ((cstep_n R m)⇧*) ((cstep_n R n)⇧*)"
by (auto simp: rtrancl_epar_n_conv)
from rule and ao have "linear_term l" by simp
from epar_n_varpeak' [OF comm vars ao rs rule conds l_σ ne * len] obtain τ
where l_τ: "l ⋅ τ =⇩f (C, us)"
and **: "∀x. (σ x, τ x) ∈ epar_n R (Suc n)" by blast
let ?c = "λi. take i cs"
let ?V = "λi. ⋃(vars_rule ` set (?c i))"
let ?P⇩1 = "λδ. ∀x ∈ vars_term l. δ x = τ x"
let ?P⇩2 = "λδ i. conds_n_sat R m (?c i) δ"
let ?P⇩3 = "λδ i. ∀x ∈ vars_term l ∪ ?V i. (σ x, δ x) ∈ epar_n R (Suc n)"
have comm: "comm ((cstep_n R m)⇧*) (epar_n R (Suc n))"
using comm1 [of m "Suc n"] by (auto simp: rtrancl_epar_n_conv)
have "0 ∙ ((l, r), cs) ∈ R" using rule by auto
from conds_n_sat_extend_subst_epar_n [OF comm vars rs this ** conds]
obtain δ where "?P⇩1 δ" and P⇩2: "?P⇩2 δ (length cs)" and P⇩3: "?P⇩3 δ (length cs)" by auto
then have "l ⋅ τ = l ⋅ δ" by (simp add: term_subst_eq_conv)
moreover have "conds_n_sat R m cs δ" using P⇩2 by simp
ultimately have "(l ⋅ τ, r ⋅ δ) ∈ cstep_n R (Suc m)"
using rule
by (auto simp: conds_n_sat_iff cstep_n_rstep_trs_n_conv intro: trs_n_SucI [THEN rstep.rule])
then have "(fill_holes C us, r ⋅ δ) ∈ epar_n R (Suc m)"
using cstep_n_subset_epar_n eqfE(1) l_τ by fastforce
moreover have "(t, r ⋅ δ) ∈ epar_n R (Suc n)"
proof -
have "vars_term r ⊆ vars_term l ∪ ⋃(vars_rule ` set cs)"
using t3 and rule by (force simp: type3_def vars_trs_def vars_rule_def)
then show ?thesis using P⇩3 by (auto simp: t subset_iff subst_epar_n_imp_epar_n)
qed
ultimately show ?thesis by blast
qed
lemma comm_epar_n:
assumes "(s, t) ∈ epar_n R m" and "(s, u) ∈ epar_n R n"
shows "∃v. (t, v) ∈ epar_n R n ∧ (u, v) ∈ epar_n R m"
using assms
proof (induct "m + n" arbitrary: s t u m n rule: less_induct)
case (less)
have "⋀m' n'. m' + n' < m + n ⟹ comm (epar_n R m') (epar_n R n')"
using less.hyps by (auto simp: comm_def)
have IH⇩1: "⋀m' n'. m' + n' < m + n ⟹ comm ((epar_n R m')⇧*) (epar_n R n')"
by (rule comm_rtrancl) fact
have IH⇩2: "⋀m' n'. m' + n' < m + n ⟹ comm ((epar_n R m')⇧*) ((epar_n R n')⇧*)"
by (subst comm_swap, rule comm_rtrancl, subst comm_swap) fact
consider (0) "m = 0 ∨ n = 0" | (Suc) m' and n' where "m = Suc m'" "n = Suc n'" by (cases m; cases n; auto)
then show ?case
proof (cases)
case 0 then show ?thesis using less.prems by auto
next
case [simp]: (Suc m' n')
from less.prems obtain C ss ts and D us vs
where s: "s =⇩f (C, ss)" and t: "t =⇩f (C, ts)" and [simp]: "length ts = length ss"
and ss: "∀i < length ss. (ss ! i, ts ! i) ∈ trs_n R m ∪ (cstep_n R m')⇧*"
and s': "s =⇩f (D, us)" and u: "u =⇩f (D, vs)" and [simp]: "length vs = length us"
and us: "∀i < length us. (us ! i, vs ! i) ∈ trs_n R n ∪ (cstep_n R n')⇧*"
by (auto elim!: epar_n_SucE)
then have ss_epar: "∀i < length ss. (ss ! i, ts ! i) ∈ epar_n R m"
and us_epar: "∀i < length us. (us ! i, vs ! i) ∈ epar_n R n"
using trs_n_subset_epar_n [of R] and csteps_n_subset_epar_n_Suc [of R]
by (simp_all) (blast)+
have [simp]: "num_holes C = length ss" "num_holes D = length us"
using t and u by (auto dest: eqfE)
define E Cs Ds where "E ≡ C ⊓ D" and "Cs ≡ inf_mctxt_args C D" and "Ds ≡ inf_mctxt_args D C"
have len_Cs: "num_holes E = length Cs" and C: "C = fill_holes_mctxt E Cs"
and len_Ds: "num_holes E = length Ds" and D: "D = fill_holes_mctxt E Ds"
by (simp_all add: E_def Cs_def Ds_def num_holes_inf_mctxt
inf_mctxt_inf_mctxt_args inf_mctxt_inf_mctxt_args2)
(metis inf_commute num_holes_inf_mctxt)
have s_left: "s = fill_holes (fill_holes_mctxt E Cs) ss"
and [simp]: "t = fill_holes (fill_holes_mctxt E Cs) ts"
and s_right: "s = fill_holes (fill_holes_mctxt E Ds) us"
and [simp]: "u = fill_holes (fill_holes_mctxt E Ds) vs"
using s and s' and t and u by (auto simp: C D dest: eqfE)
define sss where [simp]: "sss ≡ partition_holes ss Cs"
define tss where [simp]: "tss ≡ partition_holes ts Cs"
define uss where [simp]: "uss ≡ partition_holes us Ds"
define vss where [simp]: "vss ≡ partition_holes vs Ds"
define ss' where "ss' ≡ map (λi. fill_holes (Cs ! i) (sss ! i)) [0..<length Cs]"
define ts' where "ts' ≡ map (λi. fill_holes (Cs ! i) (tss ! i)) [0..<length Cs]"
define us' where "us' ≡ map (λi. fill_holes (Ds ! i) (uss ! i)) [0..<length Ds]"
define vs' where "vs' ≡ map (λi. fill_holes (Ds ! i) (vss ! i)) [0..<length Ds]"
have [simp]: "sum_list (map num_holes Cs) = length ss"
using s by (auto simp: C len_Cs num_holes_fill_holes_mctxt dest: eqfE)
have [simp]: "sum_list (map num_holes Ds) = length us"
using s' by (auto simp: D len_Ds num_holes_fill_holes_mctxt dest: eqfE)
have len_ss: "length ss = sum_list (map num_holes Cs)"
using s by (auto simp: C len_Cs num_holes_fill_holes_mctxt dest: eqfE)
have len_us: "length us = sum_list (map num_holes Ds)"
using s' by (auto simp: D len_Ds num_holes_fill_holes_mctxt dest: eqfE)
have len_vs: "length vs = sum_list (map num_holes Ds)"
using s' by (auto simp: D len_Ds num_holes_fill_holes_mctxt dest: eqfE)
have ss'_i: "⋀i. i < length Cs ⟹ ss' ! i = fill_holes (Cs ! i) (sss ! i)"
and us'_i: "⋀i. i < length Cs ⟹ us' ! i = fill_holes (Ds ! i) (uss ! i)"
and ts'_i: "⋀i. i < length Cs ⟹ ts' ! i = fill_holes (Cs ! i) (tss ! i)"
and vs'_i: "⋀i. i < length Cs ⟹ vs' ! i = fill_holes (Ds ! i) (vss ! i)"
using len_Cs len_Ds by (auto simp: ss'_def us'_def ts'_def vs'_def)
have [simp]: "⋀i. i < length Cs ⟹ length (vss ! i) = length (uss ! i)"
using len_Cs and len_Ds and len_vs by simp
have "s = fill_holes E ss'"
using fill_holes_mctxt_fill_holes [of Cs E ss]
by (simp add: s_left ss'_def len_Cs C [symmetric])
moreover
have "s = fill_holes E us'"
using fill_holes_mctxt_fill_holes [of Ds E us]
by (simp add: s_right us'_def len_Ds D [symmetric])
ultimately
have us'_ss': "us' = ss'"
using len_Cs and len_Ds
by (intro fill_holes_inj [of E]) (simp_all add: ss'_def us'_def)
have "∀i < length ts'. ∃v. (ts' ! i, v) ∈ epar_n R n ∧ (vs' ! i, v) ∈ epar_n R m"
(is "∀i < length ts'. ∃v. ?P i v")
proof (intro allI impI)
fix i
assume [simp]: "i < length ts'"
then have [simp]: "i < length ss'" "i < length vs'" "i < length us'"
using len_Cs and len_Ds by (simp_all add: us'_ss' ts'_def ss'_def vs'_def)
then have [simp]: "i < length Cs" "i < length Ds"
using len_Cs and len_Ds by (simp_all add: ss'_def)
then have "i < length (inf_mctxt_args C D)" by (simp add: Cs_def)
moreover have "(C, D) ∈ comp_mctxt" using s and s' by (metis eqf_comp_mctxt)
ultimately have "Cs ! i = MHole ∨ Ds ! i = MHole"
using inf_mctxt_args_MHole by (auto simp: Cs_def Ds_def)
then show "∃v. ?P i v"
proof
assume [simp]: "Cs ! i = MHole"
define j where "j ≡ sum_list (map length (take i tss))"
have "j < length ss"
unfolding len_ss
by (subst id_take_nth_drop [OF ‹i < length Cs›])
(simp add: take_map [symmetric] drop_map [symmetric] j_def)
have "ts' ! i = tss ! i ! 0" by (auto simp: ts'_def intro: fill_holes_MHole)
then have [simp]: "ts' ! i = ts ! j"
using partition_by_nth_nth_old [of i ts "map num_holes Cs" 0] by (simp add: j_def)
have "ss' ! i = sss ! i ! 0" by (auto simp: ss'_def intro: fill_holes_MHole)
then have [simp]: "ss' ! i = ss ! j"
using partition_by_nth_nth_old [of i ss "map num_holes Cs" 0]
by (auto simp: j_def
intro!: arg_cong [of _ _ "nth ss"] arg_cong [of _ _ sum_list] arg_cong [of _ _ "take i"] nth_map_conv)
have "∀i < length (concat uss). (concat uss ! i, concat vss ! i) ∈ epar_n R n"
using us_epar by simp
moreover have "i < length uss"
using len_Cs and len_Ds by simp
ultimately have epar_uss: "∀j < length (uss ! i). (uss ! i ! j, vss ! i ! j) ∈ epar_n R n"
using concat_nth_length [of i uss] and concat_nth_length [of i vss]
by (auto simp: concat_nth [symmetric, OF _ _ refl] take_map [symmetric])
then have epar_us': "(us' ! i, vs' ! i) ∈ epar_n R n"
using len_Cs len_Ds by (intro epar_n_mctxt [of _ "Ds ! i"]) (auto simp: us'_i vs'_i)
have uss: "∀j < length (uss ! i). (uss ! i ! j, vss ! i ! j) ∈ trs_n R (Suc n') ∪ (cstep_n R n')⇧*"
using concat_nth_length [of i uss] and concat_nth_length [of i vss] and us
by (auto simp: concat_nth [symmetric, OF _ _ refl] take_map [symmetric])
have [simp]: "ss ! j = us' ! i" by (simp add: us'_ss')
have epar_ss': "(ss' ! i, ts' ! i) ∈ epar_n R m"
using ‹j < length ss› and ss_epar by auto
have "(ss' ! i, ts' ! i) ∈ trs_n R m ∪ (cstep_n R m')⇧*" using ss and ‹j < length ss› by auto
moreover
{ assume "(ss' ! i, ts' ! i) ∈ (cstep_n R m')⇧*"
then have "(ss' ! i, ts' ! i) ∈ (epar_n R m')⇧*"
using rtrancl_mono [OF cstep_n_subset_epar_n] by blast
moreover have "comm ((epar_n R m')⇧*) (epar_n R n)" using IH⇩1 by simp
moreover have "(ss' ! i, vs' ! i) ∈ (epar_n R n)" using epar_us' by simp
ultimately obtain v where "(ts' ! i, v) ∈ epar_n R n"
and "(vs' ! i, v) ∈ (epar_n R m')⇧*" by (auto elim: commE)
then have ?thesis using epar_n_rtrancl_Suc_mono [of R m'] by auto }
moreover
{ assume trs_m: "(ss' ! i, ts' ! i) ∈ trs_n R m"
have ?thesis
proof (cases "Ds ! i = MHole")
case True note [simp] = this
define k where "k ≡ sum_list (map length (take i uss))"
have "k < length us"
unfolding len_us
by (subst id_take_nth_drop [OF ‹i < length Ds›])
(simp add: k_def take_map [symmetric])
have "vs' ! i = vss ! i ! 0" by (auto simp: vs'_def intro: fill_holes_MHole)
then have [simp]: "vs' ! i = vs ! k"
using partition_by_nth_nth_old [of i vs "map num_holes Ds" 0]
by (simp add: k_def take_map [symmetric])
have "us' ! i = uss ! i ! 0" by (auto simp: us'_def intro: fill_holes_MHole)
then have [simp]: "us' ! i = us ! k"
using partition_by_nth_nth_old [of i us "map num_holes Ds" 0] by (simp add: k_def)
have "(us' ! i, vs' ! i) ∈ trs_n R n ∪ (cstep_n R n')⇧*"
using us and ‹k < length us› by auto
moreover
{ assume "(us' ! i, vs' ! i) ∈ (cstep_n R n')⇧*"
then have "(us' ! i, vs' ! i) ∈ (epar_n R n')⇧*"
using rtrancl_mono [OF cstep_n_subset_epar_n] by blast
moreover have "comm ((epar_n R n')⇧*) (epar_n R m)" using IH⇩1 by simp
moreover have "(us' ! i, ts' ! i) ∈ (epar_n R m)" using epar_ss' by simp
ultimately obtain v where "(ts' ! i, v) ∈ (epar_n R n')⇧*"
and "(vs' ! i, v) ∈ epar_n R m" by (auto elim: commE)
then have ?thesis using epar_n_rtrancl_Suc_mono [of R n'] by auto }
moreover
{ assume "(us' ! i, vs' ! i) ∈ trs_n R n"
with trs_m have ?thesis using IH⇩2 by (auto elim: trs_n_peak) }
ultimately show ?thesis by blast
next
case False
have *: "us' ! i =⇩f (Ds ! i, uss ! i)"
using len_Cs and len_Ds by (auto simp: us'_i)
have len_vss: "length (vss ! i) = length (uss ! i)" by simp
from epar_n_varpeak [OF * False len_vss trs_m [simplified] uss IH⇩1 IH⇩2]
show ?thesis by (simp add: vs'_i)
qed }
ultimately show ?thesis by blast
next
assume [simp]: "Ds ! i = MHole"
define j where "j ≡ sum_list (map length (take i vss))"
have "j < length us"
unfolding len_us
by (subst id_take_nth_drop [OF ‹i < length Ds›])
(simp add: take_map [symmetric] drop_map [symmetric] j_def)
have "vs' ! i = vss ! i ! 0" by (auto simp: vs'_def intro: fill_holes_MHole)
then have [simp]: "vs' ! i = vs ! j"
using partition_by_nth_nth_old [of i vs "map num_holes Ds" 0] by (simp add: j_def)
have "us' ! i = uss ! i ! 0" by (auto simp: us'_def intro: fill_holes_MHole)
then have [simp]: "us' ! i = us ! j"
using partition_by_nth_nth_old [of i us "map num_holes Ds" 0]
by (auto simp: j_def
intro!: arg_cong [of _ _ "nth us"] arg_cong [of _ _ sum_list] arg_cong [of _ _ "take i"] nth_map_conv)
have "∀i < length (concat sss). (concat sss ! i, concat tss ! i) ∈ epar_n R m"
using ss_epar by simp
moreover have "i < length sss"
using len_Cs and len_Ds by simp
ultimately have epar_uss: "∀j < length (sss ! i). (sss ! i ! j, tss ! i ! j) ∈ epar_n R m"
using concat_nth_length [of i sss] and concat_nth_length [of i tss]
by (auto simp: concat_nth [symmetric, OF _ _ refl] take_map [symmetric])
then have epar_ss': "(ss' ! i, ts' ! i) ∈ epar_n R m"
using len_Cs len_Ds by (intro epar_n_mctxt [of _ "Cs ! i"]) (auto simp: ss'_i ts'_i)
have sss: "∀j < length (sss ! i). (sss ! i ! j, tss ! i ! j) ∈ trs_n R (Suc m') ∪ (cstep_n R m')⇧*"
using concat_nth_length [of i sss] and concat_nth_length [of i tss] and ss
by (auto simp: concat_nth [symmetric, OF _ _ refl] take_map [symmetric])
have [simp]: "us ! j = ss' ! i" by (simp add: us'_ss' [symmetric])
have epar_us': "(us' ! i, vs' ! i) ∈ epar_n R n"
using ‹j < length us› and us_epar by auto
have "(us' ! i, vs' ! i) ∈ trs_n R n ∪ (cstep_n R n')⇧*" using us and ‹j < length us› by auto
moreover
{ assume "(us' ! i, vs' ! i) ∈ (cstep_n R n')⇧*"
then have "(us' ! i, vs' ! i) ∈ (epar_n R n')⇧*"
using rtrancl_mono [OF cstep_n_subset_epar_n] by blast
moreover have "comm ((epar_n R n')⇧*) (epar_n R m)" using IH⇩1 by simp
moreover have "(us' ! i, ts' ! i) ∈ (epar_n R m)" using epar_ss' by simp
ultimately obtain v where "(vs' ! i, v) ∈ epar_n R m"
and "(ts' ! i, v) ∈ (epar_n R n')⇧*" by (auto elim: commE)
then have ?thesis using epar_n_rtrancl_Suc_mono [of R n'] by auto }
moreover
{ assume trs_n: "(us' ! i, vs' ! i) ∈ trs_n R n"
have ?thesis
proof (cases "Cs ! i = MHole")
case True note [simp] = this
define k where "k ≡ sum_list (map length (take i sss))"
have "k < length ss"
unfolding len_ss
by (subst id_take_nth_drop [OF ‹i < length Cs›])
(simp add: k_def take_map [symmetric])
have "ts' ! i = tss ! i ! 0" by (auto simp: ts'_def intro: fill_holes_MHole)
then have [simp]: "ts' ! i = ts ! k"
using partition_by_nth_nth_old [of i ts "map num_holes Cs" 0]
by (simp add: k_def take_map [symmetric])
have "ss' ! i = sss ! i ! 0" by (auto simp: ss'_def intro: fill_holes_MHole)
then have [simp]: "ss' ! i = ss ! k"
using partition_by_nth_nth_old [of i ss "map num_holes Cs" 0] by (simp add: k_def)
have "(ss' ! i, ts' ! i) ∈ trs_n R m ∪ (cstep_n R m')⇧*"
using ss and ‹k < length ss› by auto
moreover
{ assume "(ss' ! i, ts' ! i) ∈ (cstep_n R m')⇧*"
then have "(ss' ! i, ts' ! i) ∈ (epar_n R m')⇧*"
using rtrancl_mono [OF cstep_n_subset_epar_n] by blast
moreover have "comm ((epar_n R m')⇧*) (epar_n R n)" using IH⇩1 by simp
moreover have "(ss' ! i, vs' ! i) ∈ (epar_n R n)" using epar_us' by simp
ultimately obtain v where "(vs' ! i, v) ∈ (epar_n R m')⇧*"
and "(ts' ! i, v) ∈ epar_n R n" by (auto elim: commE)
then have ?thesis using epar_n_rtrancl_Suc_mono [of R m'] by auto }
moreover
{ assume "(ss' ! i, ts' ! i) ∈ trs_n R m"
with trs_n have ?thesis using IH⇩2 by (auto elim: trs_n_peak) }
ultimately show ?thesis by blast
next
case False
have *: "ss' ! i =⇩f (Cs ! i, sss ! i)"
using len_Cs and len_Ds by (auto simp: ss'_i)
have len_tss: "length (tss ! i) = length (sss ! i)" by simp
from epar_n_varpeak [OF * False len_tss trs_n [simplified] sss IH⇩1 IH⇩2]
show ?thesis by (auto simp: ts'_i)
qed }
ultimately show ?thesis by blast
qed
qed
then obtain v where "∀i < length ts'. ?P i (v i)" unfolding choice_iff' by blast
moreover define ws where "ws ≡ map v [0 ..< length ts']"
ultimately have *: "∀i < length ts'. ?P i (ws ! i)" by (simp)
have [simp]: "length ts' = length vs'"
by (simp add: vs'_def ts'_def len_Cs [symmetric] len_Ds)
define w where "w ≡ fill_holes E ws"
have [simp]: "num_holes (fill_holes_mctxt E Cs) = length ss"
using s by (auto simp: C [symmetric] dest!: eqfE)
have [simp]: "num_holes (fill_holes_mctxt E Ds) = length vs"
using s' by (auto simp: D [symmetric] dest!: eqfE)
have "(t, w) ∈ epar_n R n"
using *
by (intro epar_n_mctxt [of _ E ts' _ ws])
(auto simp: ts'_def eq_fill.simps len_Cs fill_holes_mctxt_fill_holes w_def ws_def)
moreover have "(u, w) ∈ epar_n R m"
using *
by (intro epar_n_mctxt [of _ E vs' _ ws])
(auto simp: vs'_def eq_fill.simps len_Ds fill_holes_mctxt_fill_holes w_def ws_def len_Cs)
ultimately show ?thesis by blast
qed
qed
text ‹
Almost orthogonal (modulo infeasibility), properly oriented, right-stable 3-CTRSs
are level-confluent.
›
lemma level_confluence:
shows "level_confluent R"
unfolding level_confluent_def
proof (intro allI diamond_imp_CR')
fix n
show "cstep_n R n ⊆ epar_n R n" by (rule cstep_n_subset_epar_n)
show "epar_n R n ⊆ (cstep_n R n)⇧*" by (rule epar_n_subset_csteps_n)
show "◇ (epar_n R n)" using comm_epar_n by fast
qed
end
lemma level_confluent_imp_CR:
assumes "level_confluent R"
shows "CR (cstep R)"
proof
fix a b c
assume "(a, b) ∈ (cstep R)⇧*"
and "(a, c) ∈ (cstep R)⇧*"
then obtain n and m where "(a, b) ∈ (cstep_n R n)⇧*"
and "(a, c) ∈ (cstep_n R m)⇧*" using csteps_imp_csteps_n[of _ _ R] by blast
then have "(a, b) ∈ (cstep_n R (n + m))⇧*"
and "(a, c) ∈ (cstep_n R (n + m))⇧*"
using cstep_n_mono [THEN rtrancl_mono, of _ "n + m" R]
and le_add1[of n m] and le_add2[of m n] by blast+
then obtain d where bd: "(b, d) ∈ (cstep_n R (n + m))⇧*"
and cd: "(c, d) ∈ (cstep_n R (n + m))⇧*" using assms
by (auto simp: level_confluent_def CR_defs) (metis joinE)
then have "(b, d) ∈ (cstep R)⇧*" and "(c, d) ∈ (cstep R)⇧*"
by (metis (erased, hide_lams) contra_subsetD cstep_iff rtrancl_mono subrelI)+
then show "(b, c) ∈ (cstep R)⇧↓" by auto
qed
end