theory Unraveling
imports
Quasi_Decreasingness
begin
text ‹This formalization is described in an RTA 2015 submission, and certain lemma/theorem/... numbers
refer to this paper.›
text ‹The locale for unraveling corresponds to generalized unravelings in the paper›
locale unraveling =
fixes R :: "('f,'v)ctrs"
and U :: "('f,'v)crule ⇒ nat ⇒ ('f,'v)ctxt"
begin
fun lhs_n :: "('f,'v)crule ⇒ nat ⇒ ('f,'v)term"
where "lhs_n (lr,cs) 0 = fst lr"
| "lhs_n (lr,cs) (Suc n) = (U (lr,cs) n) ⟨snd (cs ! n)⟩"
fun rhs_n :: "('f,'v)crule ⇒ nat ⇒ ('f,'v)term"
where "rhs_n (lr,cs) n = (if n < length cs then
(U (lr,cs) n)⟨fst (cs ! n)⟩
else snd lr)"
definition rules :: "('f,'v)crule ⇒ ('f,'v)trs"
where "rules crule ≡ (λ n. (lhs_n crule n, rhs_n crule n)) ` {n . n ≤ length (snd crule)}"
lemma finite_rule: "finite (rules crule)" unfolding rules_def by auto
definition UR :: "('f, 'v) trs" where
"UR ≡ ⋃(rules ` R)"
lemma finite_UR: "finite R ⟹ finite UR" unfolding UR_def using finite_rule by auto
lemma rules_unconditional[simp]: "rules ((l,r),[]) = {(l,r)}" unfolding rules_def by simp
lemma UR_simulation_main: assumes lr: "((l, r), cs) ∈ R"
and i: "i ≤ length cs"
and cs: "⋀ j. j < i ⟹ (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (rstep UR)⇧*"
shows "(l ⋅ σ, rhs_n ((l,r),cs) i ⋅ σ) ∈ (rstep UR)⇧+"
proof -
let ?lr = "((l,r),cs)"
let ?n = "length cs"
from lr have lr: "rules ?lr ⊆ UR" unfolding UR_def by auto
hence lr: "⋀ i. i ≤ ?n ⟹ (lhs_n ?lr i, rhs_n ?lr i) ∈ UR" unfolding rules_def
by auto
show ?thesis
proof (rule rtrancl_into_trancl2)
show "(l ⋅ σ,rhs_n ?lr 0 ⋅ σ) ∈ rstep UR"
by (rule rstepI[OF lr[of 0], of _ Hole σ], auto)
from i cs
show "(rhs_n ?lr 0 ⋅ σ, rhs_n ?lr i ⋅ σ) ∈ (rstep UR)⇧*"
proof (induct i)
case (Suc i)
hence i: "i < ?n" and i': "i ≤ ?n" by auto
let ?f = "U ?lr i"
let ?U = "λ t. ?f ⟨ t ⟩"
from Suc(1)[OF i' Suc(3)]
have "(rhs_n ?lr 0 ⋅ σ, rhs_n ?lr i ⋅ σ) ∈ (rstep UR)⇧*" by simp
also have "rhs_n ?lr i = ?U (fst (cs ! i))"
using i by simp
also have "(?U (fst (cs ! i)) ⋅ σ, ?U (snd (cs ! i)) ⋅ σ) ∈ (rstep UR)⇧*"
proof -
obtain si ti where csi: "cs ! i = (si,ti)" by force
from Suc(3)[of i, unfolded csi] have "(si ⋅ σ, ti ⋅ σ) ∈ (rstep UR)⇧*" by simp
from ctxt.closedD[OF ctxt.closed_rtrancl[OF ctxt_closed_rstep] this]
have "⋀ C. (C⟨si ⋅ σ⟩, C⟨ti ⋅ σ⟩) ∈ (rstep UR)⇧*" .
from this[of "?f ⋅⇩c σ"]
show ?thesis unfolding csi by simp
qed
also have "?U (snd (cs ! i)) = lhs_n ?lr (Suc i)"
unfolding lhs_n.simps by simp
also have "(lhs_n ?lr (Suc i) ⋅ σ, rhs_n ?lr (Suc i) ⋅ σ) ∈ (rstep UR)"
by (rule rstepI[OF lr[OF Suc(2)], of _ Hole σ], auto)
finally show ?case .
qed simp
qed
qed
lemma SN_quasi_reductive_order: assumes SN: "SN (rstep UR)"
shows "quasi_reductive_order R ((rstep UR)⇧+)"
proof -
let ?S = "(rstep UR)⇧+"
let ?NS = "(rstep UR)⇧*"
have id: "?S^= = ?NS" by simp
show ?thesis unfolding quasi_reductive_order_def id
proof (intro conjI allI impI)
show "SN ?S" by (rule SN_imp_SN_trancl[OF SN])
next
fix l r cs σ
assume lr: "((l, r), cs) ∈ R"
and cs: "∀j<length cs. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (rstep UR)⇧*"
from UR_simulation_main[OF lr, of "length cs" σ] cs
show "(l ⋅ σ, r ⋅ σ) ∈ (rstep UR)⇧+" by simp
next
fix l r cs σ i
assume lr: "((l, r), cs) ∈ R"
and i: "i < length cs"
and cs: "∀j<i. (fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (rstep UR)⇧*"
from UR_simulation_main[OF lr, of i σ] i cs
have lm: "(l ⋅ σ, rhs_n ((l, r), cs) i ⋅ σ) ∈ (rstep UR)⇧+" (is "(?l,?m) ∈ _") by simp
have mr: "?m ⊵ fst (cs ! i) ⋅ σ" (is "_ ⊵ ?r")
by (rule supteq_subst, insert i, auto)
let ?R = "(rstep UR)⇧+ ∪ {⊳}"
from mr have "(?m,?r) ∈ ({⊳})^=" by auto
hence mr: "(?m,?r) ∈ ?R⇧*" by auto
have lm: "(?l,?m) ∈ ?R⇧+"
by (rule trancl_mono[OF lm], auto)
from lm mr show lr: "(?l,?r) ∈ ?R⇧+" by auto
qed auto
qed
lemma SN_quasi_reductive: "SN (rstep UR) ⟹ quasi_reductive R"
unfolding quasi_reductive_def
by (rule exI, rule SN_quasi_reductive_order)
lemma completeness: assumes step: "(s,t) ∈ cstep R"
shows "(s,t) ∈ (rstep UR)⇧+"
proof -
from step[unfolded cstep_def] obtain n where "(s,t) ∈ cstep_n R n" ..
thus ?thesis
proof (induct n arbitrary: s t)
case 0 thus ?case by simp
next
case (Suc n) note IH = this
from IH(2) obtain l r cs C σ where lr: "((l,r),cs) ∈ R" and
cs: "⋀ si ti. (si,ti) ∈ set cs ⟹ (si ⋅ σ, ti ⋅ σ) ∈ (cstep_n R n)⇧*"
and s: "s = C ⟨ l ⋅ σ ⟩" and t: "t = C ⟨ r ⋅ σ ⟩" by (blast elim: cstep_n_SucE)
let ?lr = "((l,r),cs)"
let ?n = "length cs"
have rsig: "r ⋅ σ = rhs_n ?lr ?n ⋅ σ" by auto
have "(l ⋅ σ, r ⋅ σ) ∈ (rstep UR)⇧+" unfolding rsig
proof (rule UR_simulation_main[OF lr, of "length cs" σ])
fix j
assume j: "j < length cs"
obtain sj tj where csj: "cs ! j = (sj,tj)" by force
from j have "(sj,tj) ∈ set cs" unfolding csj[symmetric] set_conv_nth by auto
from cs[OF this] have steps: "(sj ⋅ σ, tj ⋅ σ) ∈ (cstep_n R n)⇧*" .
{
fix s t
assume "(s,t) ∈ (cstep_n R n)⇧*"
hence "(s,t) ∈ (rstep UR)⇧*"
proof (induct)
case (step t u)
from step(3) IH(1)[OF step(2)] show ?case by auto
qed simp
}
from this[OF steps]
show "(fst (cs ! j) ⋅ σ, snd (cs ! j) ⋅ σ) ∈ (rstep UR)⇧*"
unfolding csj by auto
qed simp
from ctxt.closedD[OF ctxt.closed_trancl[OF ctxt_closed_rstep] this, of C]
show ?case unfolding s t .
qed
qed
end
context unraveling
begin
definition Z_vars :: "(('f,'v)crule ⇒ nat ⇒ 'v list) ⇒ bool" where
"Z_vars Z = ((∀ ρ ∈ R. ∀ i < length (snd ρ).
set (Z ρ i) ⊇ X_vars ρ i ∩ Y_vars ρ i ∧ distinct (Z ρ i)))"
abbreviation ultra :: "(('f,'v) trs ⇒ bool) ⇒ bool" where "ultra P ≡ P (UR)"
abbreviation ultra_rule :: "(('f,'v) trs ⇒ bool) ⇒ ('f,'v) crule ⇒ bool"
where "ultra_rule P ρ ≡ P (rules ρ)"
definition Z_cond_0 :: "(('f,'v)crule ⇒ nat ⇒ 'v list) ⇒ bool"
where"Z_cond_0 Z ≡ ∀ρ∈R. length (snd ρ) > 0 ⟶ (set (Z ρ 0) ⊆ vars_term (clhs ρ) ∧ (vars_term (snd (snd ρ ! 0)) ∩ set (Z ρ 0)) = {})"
definition Z_cond_Suc :: "(('f,'v)crule ⇒ nat ⇒ 'v list) ⇒ bool"
where"Z_cond_Suc Z ≡ ∀ρ∈R. ∀k. length (snd ρ) = Suc k ⟶ (∀n < k.
set (Z ρ (Suc n)) ⊆ set (Z ρ n) ∪ vars_term (snd (snd ρ ! n)) ∧ vars_term (snd (snd ρ ! Suc n)) ∩ set (Z ρ (Suc n)) = {})"
end
definition source_preserving :: "('f,'v)ctrs ⇒ (('f,'v)crule ⇒ nat ⇒ 'v list) ⇒ bool"
where "source_preserving R Z ≡ (∀ ρ ∈ R. (∀ i < length (snd ρ).
(vars_term (clhs ρ) ⊆ set (Z ρ i))))"
abbreviation si :: "('f,'v) crule ⇒ nat ⇒ ('f,'v) term" where "si ρ i ≡ fst ((snd ρ)!i)"
abbreviation ti :: "('f,'v) crule ⇒ nat ⇒ ('f,'v) term" where "ti ρ i ≡ snd ((snd ρ)!i)"
definition prefix_equivalent :: "('f,'v)crule ⇒ ('f,'v)crule ⇒ nat ⇒ bool"
where "prefix_equivalent ρ ρ' m ≡ (
m < length(snd ρ) ∧ m < length(snd ρ') ∧
clhs ρ = clhs ρ' ∧ (∀i < m. ti ρ i = ti ρ' i) ∧ (∀i ≤ m. si ρ i = si ρ' i))"
definition "U_cond U R F Z ≡ ∀ ρ n. ρ ∈ R ⟶ n < length (snd ρ) ⟶ (∃ f.
(U ρ n = (More f Nil Hole (map Var (Z ρ n))) ∧ f ∉ F ∧
(∀ ρ' n' g b c a. (ρ' ∈ R ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶
f ≠ g ∨ (n = n' ∧ (∀i ≤n. U ρ i = U ρ' i) ∧ prefix_equivalent ρ ρ' n))))"
lemma U_condD: "U_cond U R F Z ⟹ ρ ∈ R ⟹ n < length (snd ρ) ⟹ ∃ f.
(U ρ n = (More f Nil Hole (map Var (Z ρ n))) ∧ f ∉ F ∧
(∀ ρ' n' g b c a. (ρ' ∈ R ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶ f ≠ g ∨ (n = n' ∧ (∀i ≤n. U ρ i = U ρ' i) ∧ prefix_equivalent ρ ρ' n)))"
unfolding U_cond_def by blast
lemma U_condI: assumes "⋀ ρ n. ρ ∈ R ⟹ n < length (snd ρ) ⟹ ∃ f.
(U ρ n = (More f Nil Hole (map Var (Z ρ n))) ∧ f ∉ F ∧
(∀ ρ' n' g b c a. (ρ' ∈ R ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶ f ≠ g ∨ (n = n' ∧ (∀i ≤n. U ρ i = U ρ' i) ∧ prefix_equivalent ρ ρ' n)))"
shows "U_cond U R F Z" using assms unfolding U_cond_def by blast
locale standard_unraveling = unraveling R U
for R :: "('f,'v) ctrs" and U :: "('f,'v) crule ⇒ nat ⇒ ('f,'v) ctxt" +
fixes F :: "'f set" and Z :: "('f,'v)crule ⇒ nat ⇒ 'v list"
assumes F: "funs_ctrs R ⊆ F" and Ucond: "U_cond U R F Z"
and Z:"Z_vars Z"
and dctrs:"dctrs R"
and type3:"type3 R"
and inf_var: "infinite (UNIV :: 'v set)"
begin
lemmas U_cond = U_condD[OF Ucond]
definition "dvars n = (SOME xs. length xs = n ∧ distinct (xs :: 'v list))"
lemma distinct_vars: "length (dvars n) = n ∧ distinct (dvars n)"
unfolding dvars_def
by (rule someI_ex, insert infinite_imp_many_elems[OF inf_var, of n], auto)
abbreviation U_fun :: "('f,'v) crule ⇒ nat ⇒ 'f ⇒ bool"
where "U_fun ρ k Uk ≡ (U ρ k = (More Uk Nil Hole (map Var (Z ρ k))))"
lemma funas_UR:"funas_trs UR = funas_ctrs R ∪ {(Uk, Suc (length (Z ρ k))) |ρ k Uk. ρ ∈ R ∧ k < length (snd ρ) ∧ U_fun ρ k Uk}"
proof(rule, rule)
fix f n
assume f:"(f, n) ∈ funas_trs UR"
let ?Us = "{(Uk, Suc (length (Z ρ k))) |ρ k Uk. ρ ∈ R ∧ k < length (snd ρ) ∧ U_fun ρ k Uk}"
let ?rhs = "funas_ctrs R ∪ ?Us"
from f[unfolded UR_def funas_trs_def] rules_def obtain ρ i where rl:"(f,n) ∈ funas_rule (lhs_n ρ i, rhs_n ρ i)" "i ≤ length (snd ρ)" "ρ ∈ R" by auto
obtain l r cs where rho:"ρ = ((l,r),cs)" by (cases ρ, auto)
{ assume fl:"(f,n) ∈ funas_term (lhs_n ρ i)"
have "(f,n) ∈ ?rhs" proof (cases i)
case 0
from fl[unfolded 0 rho lhs_n.simps] have "(f,n) ∈ funas_rule (fst ρ)" unfolding funas_rule_def rho by simp
with rl(3) funas_crule_def show "(f,n) ∈ ?rhs" unfolding funas_ctrs_def by blast
next
case (Suc j)
with rl have j:"j < length (snd ρ)" by auto
from U_cond[OF rl(3) j] obtain g where g:"U ρ j = (More g Nil Hole (map Var (Z ρ j)))" by fast
from fl[unfolded funas_term_conv] have or:"Some (f,n) = root (lhs_n ρ i) ∨ (f,n) ∈ funas_args_term (lhs_n ρ i)" by force
{ assume "Some (f,n) = root (lhs_n ρ i)"
from this[unfolded Suc rho lhs_n.simps g[unfolded rho]] have "f=g ∧ n = Suc (length (Z ρ j))" unfolding rho by simp
from g this j rl(3) have "(f,n) ∈ ?Us"
unfolding mem_Collect_eq by blast
} note A = this
{ assume "(f,n) ∈ funas_args_term (lhs_n ρ i)"
from this[unfolded Suc rho lhs_n.simps g[unfolded rho] ctxt_apply_term.simps funas_args_term_def] have "(f,n) ∈ funas_term (snd (cs ! j))" by simp
with j funas_rule_def have "(f,n) ∈ funas_trs (set (snd ρ))" unfolding rho funas_trs_def set_conv_nth snd_conv by fast
with rho rl funas_crule_def have "(f,n) ∈ funas_ctrs R" unfolding funas_ctrs_def by blast
}
with A or show "(f,n) ∈ ?rhs" by fast
qed
} note left = this
{ assume fr:"(f,n) ∈ funas_term (rhs_n ρ i)"
have "(f,n) ∈ ?rhs" proof (cases "i = length (snd ρ)")
case True
from fr[unfolded True rho rhs_n.simps] have "(f,n) ∈ funas_rule (fst ρ)" unfolding funas_rule_def rho by simp
with rl(3) funas_crule_def show "(f,n) ∈ ?rhs" unfolding funas_ctrs_def by blast
next
case False
with rl rho have i:"i < length cs" by auto
with U_cond[OF rl(3)] rho obtain g where g:"U ρ i = (More g Nil Hole (map Var (Z ρ i)))" by fastforce
from fr[unfolded funas_term_conv] have or:"Some (f,n) = root (rhs_n ρ i) ∨ (f,n) ∈ funas_args_term (rhs_n ρ i)" by force
{ assume "Some (f,n) = root (rhs_n ρ i)"
from this[unfolded rho rhs_n.simps g[unfolded rho]] i have "f=g ∧ n = Suc (length (Z ρ i))" unfolding rho by simp
with g i rl(3) rho have "(f,n) ∈ ?Us"
unfolding mem_Collect_eq by auto
} note A = this
{ assume "(f,n) ∈ funas_args_term (rhs_n ρ i)"
from i this[unfolded rho rhs_n.simps g[unfolded rho] ctxt_apply_term.simps funas_args_term_def] have "(f,n) ∈ funas_term (fst (cs ! i))" by simp
with i funas_rule_def have "(f,n) ∈ funas_trs (set (snd ρ))" unfolding rho funas_trs_def set_conv_nth snd_conv by fast
with rho rl funas_crule_def have "(f,n) ∈ funas_ctrs R" unfolding funas_ctrs_def by blast
}
with A or show "(f,n) ∈ ?rhs" by fast
qed
}
with rl(1) left show "(f,n) ∈ ?rhs" unfolding rho funas_rule_def by auto
next
{ fix fn ρ i
assume *:"ρ ∈ R" and i:"i ≤ length (snd ρ)" and f:"fn ∈ funas_term (rhs_n ρ i) ∨ fn ∈ funas_term (lhs_n ρ i)"
obtain l r cs where rho:"ρ = ((l,r), cs)" by (cases ρ, auto)
from f have "fn ∈ funas_rule (lhs_n ρ i, rhs_n ρ i)" unfolding funas_rule_def rho by auto
with i have "fn ∈ funas_trs (rules ρ)" unfolding funas_trs_def rho rules_def by fast
hence "fn ∈ funas_trs UR" unfolding UR_def funas_trs_def using * by blast
} note aux = this
{ fix f n
assume f:"(f,n) ∈ funas_ctrs R"
from f[unfolded funas_ctrs_def] obtain ρ where *:"ρ ∈ R" "(f,n) ∈ funas_crule ρ" by blast
from this[unfolded funas_crule_def] have *:"ρ ∈ R" "(f,n) ∈ funas_rule (fst ρ) ∨ (f,n) ∈ funas_trs (set (snd ρ))" by (blast, blast)
obtain l r cs where rho:"ρ = ((l,r), cs)" by (cases ρ, auto)
{ assume "(f,n) ∈ funas_term l"
hence "(f,n) ∈ funas_term (lhs_n ρ 0)" unfolding rho by auto
from aux[OF *(1) le0] this have "(f,n) ∈ funas_trs UR" by blast
} note A = this
{ assume "(f,n) ∈ funas_term r"
hence "(f,n) ∈ funas_term (rhs_n ρ (length cs))" unfolding rho by auto
from aux[OF *(1) le_refl] this have "(f,n) ∈ funas_trs UR" unfolding rho by simp
} note B = this
{ assume "(f,n) ∈ funas_trs (set cs)"
then obtain si ti where lr:"(f,n) ∈ funas_rule (si,ti)" "(si,ti) ∈ set cs" unfolding funas_trs_def by force
from this(2)[unfolded set_conv_nth] obtain i where i:"i < length cs" "cs ! i = (si,ti)" by force
from U_cond[OF *(1)] i obtain Ui where Ui:"U_fun ρ i Ui" unfolding rho by fastforce
{ assume fsi:"(f,n) ∈ funas_term si"
from i Ui fsi have "(f,n) ∈ funas_term (rhs_n ρ i)" unfolding rho by simp
from aux[OF *(1), of i] this i have "(f,n) ∈ funas_trs UR" unfolding rho by auto
} note li = this
{ assume fti:"(f,n) ∈ funas_term ti"
from i Ui fti have "(f,n) ∈ funas_term (lhs_n ρ (Suc i))" unfolding rho by simp
from aux[OF *(1), of "Suc i"] this i have "(f,n) ∈ funas_trs UR" unfolding rho by auto
} note ri = this
from li ri lr have "(f,n) ∈ funas_trs UR" unfolding funas_rule_def by fastforce
}
with *(2) A B funas_rule_def have "(f,n) ∈ funas_trs UR" unfolding rho by fastforce
} note A = this
let ?Us = "{(Uk, Suc (length (Z ρ k))) |ρ k Uk. ρ ∈ R ∧ k < length (snd ρ) ∧ U_fun ρ k Uk}"
{ fix f n
assume "(f,n) ∈ ?Us"
then obtain ρ k where *:"ρ ∈ R" "k < length (snd ρ)" "U_fun ρ k f" "n = Suc (length (Z ρ k))" by auto
obtain l r cs where rho:"ρ = ((l,r), cs)" by (cases ρ, auto)
from * have "(f,n) ∈ funas_term (rhs_n ρ k)" unfolding rho by simp
with aux[OF *(1), of k] *(2) have "(f,n) ∈ funas_trs UR" by auto
} note B = this
from A Un_least B show "funas_ctrs R ∪ ?Us ⊆ funas_trs UR" by fast
qed
lemma funs_UR:"funs_trs UR = funs_ctrs R ∪ {Uk |ρ k Uk. ρ ∈ R ∧ k < length (snd ρ) ∧ U_fun ρ k Uk}"
unfolding funs_trs_funas_trs funas_UR funs_ctrs_funas_ctrs
by auto force
lemma X_vars_Suc :
assumes inR:"ρ ∈ R" and il:"Suc i < length (snd ρ)"
shows "(X_vars ρ (Suc i)) = (X_vars ρ i) ∪ vars_term (snd (snd ρ ! i))"
proof-
let ?v = "λ m. ⋃(vars_term ` rhss (set (take m (snd ρ))))"
from il have il':"i < length (snd ρ)" by auto
from il take_Suc_conv_app_nth[OF il'] have "set (take (Suc i) (snd ρ)) = set (take i (snd ρ)) ∪ {snd ρ ! i}" by force
thus ?thesis unfolding X_vars_def by force
qed
lemma X_vars_mono :
assumes inR:"ρ ∈ R" and il:"i < length (snd ρ)" and ji:"j ≤ i"
shows "X_vars ρ j ⊆ X_vars ρ i"
proof(cases "j = i", simp)
case False
with ji have ji:"j < i" by auto
let ?v = "λ m. ⋃(vars_term ` rhss (set (take m (snd ρ))))"
from il inR have si:"X_vars ρ i = (vars_term (clhs ρ) ∪ ?v i)" unfolding X_vars_def by auto
from xt1(10)[OF il ji] inR have sj:"X_vars ρ j = vars_term (clhs ρ) ∪ ?v j" unfolding X_vars_def by blast
have "?v j ⊆ ?v i" by (rule Union_mono, rule image_mono, rule image_mono,
simp add:set_take_subset_set_take[OF less_imp_le[OF ji]])
from Un_mono[OF subset_refl this] show ?thesis unfolding si sj by auto
qed
lemma l_vars_X_vars :
assumes inR:"ρ ∈ R" and il:"i < length (snd ρ)" shows "vars_term (clhs ρ) ⊆ X_vars ρ i"
unfolding X_vars_def using X_vars_def il inR by blast
lemma l_vars_X0_vars :
assumes inR:"ρ ∈ R" and il:"0 < length (snd ρ)" shows "vars_term (clhs ρ) = X_vars ρ 0"
unfolding X_vars_def using assms by simp
lemma Y_vars_mono: assumes i: "i < length (snd ρ)" and j: "j ≤ i"
shows "Y_vars ρ j ⊇ Y_vars ρ i"
proof -
from j have ij: "⋀ k. i < k ⟹ j < k" "⋀k. i ≤ k ⟹ j ≤ k" by auto
have cong: "⋀ a b c b' c'. b ⊆ b' ⟹ c ⊆ c' ⟹ a ∪ b ∪ c ⊆ a ∪ b' ∪ c'" by blast
show ?thesis using i j
proof (unfold Y_vars_alt, subst Y_vars_alt, force, intro cong, insert ij)
show "⋃{vars_term (si ρ j) |j. i < j ∧ j < length (snd ρ)}
⊆ ⋃{vars_term (si ρ ja) |ja. j < ja ∧ ja < length (snd ρ)}" using ij by auto
show "⋃{vars_term (ti ρ j) |j. i ≤ j ∧ j < length (snd ρ)}
⊆ ⋃{vars_term (ti ρ ja) |ja. j ≤ ja ∧ ja < length (snd ρ)}" using ij by auto
qed
qed
lemma X_Y_imp_Z :
assumes inR:"ρ ∈ R" and il:"i < length (snd ρ)" and x:"x ∈ X_vars ρ i" and y:"x ∈ Y_vars ρ i"
shows "x ∈ set (Z ρ i)"
using Z[unfolded Z_vars_def, rule_format, OF inR il] x y by blast
lemma s_imp_Y :
assumes inR:"ρ ∈ R" and il:"Suc i < length (snd ρ)" and x:"x ∈ vars_term (fst (snd ρ ! (Suc i)))"
shows "x ∈ Y_vars ρ i" using assms
by (subst Y_vars_alt, auto)
lemma L3_9a :
assumes inR:"ρ ∈ R" and ull:"ultra_rule left_linear_trs ρ"
shows "linear_term (clhs ρ) ∧ (∀ i < length (snd ρ). linear_term ( snd(snd ρ ! i))) ∧
(∀ i < length (snd ρ). vars_term (snd ((snd ρ) ! i)) ∩ X_vars ρ i = {})"
proof-
obtain l r cs where rho:"ρ = ((l,r),cs)" by (cases ρ, auto)
with ull have ll:"⋀ l' r'. (l',r') ∈ rules ρ ⟹ linear_term l'" unfolding left_linear_trs_def by blast
hence "linear_term (lhs_n ρ 0)" unfolding rules_def by fast
hence 1:"linear_term (clhs ρ)" unfolding rules_def using lhs_n.simps(1) prod.collapse by metis
{ fix i
assume i:"i < length (snd ρ)"
hence i':"Suc i ≤ length (snd ρ)" by auto
let ?ti = "snd (snd ρ ! i)"
from ll[unfolded rules_def] i' have lin:"linear_term (lhs_n ρ (Suc i))" by blast
from U_cond[OF inR i] obtain f where "U ρ i = More f [] □ (map Var (Z ρ i))" by fast
from lin[unfolded rho lhs_n.simps(2) this[unfolded rho] ctxt_apply_term.simps] rho have
"linear_term (Fun f ((snd (cs!i)) # (map Var (Z ρ i))))" by auto
from this[unfolded linear_term.simps(2)] have 2:"linear_term ?ti" unfolding rho by force
have "vars_term (snd ((snd ρ)!i)) ∩ X_vars ρ i = {}"
proof(rule ccontr)
assume ne:"vars_term (snd (snd ρ ! i)) ∩ X_vars ρ i ≠ {}"
let ?ti = "(snd (snd ρ ! i))"
let ?zs = "Z ρ i"
have "vars_term ?ti ⊆ Y_vars ρ i" unfolding Y_vars_def using inR i by force
with Z[unfolded Z_vars_def] ne have iz:"vars_term ?ti ∩ set (Z ρ i) ≠ {}" using inR i by fast
have zs:"⋃ (set (map vars_term (map Var ?zs))) = set ?zs" unfolding map_map vars_term_Var_id by force
from iz have p:"¬ (is_partition (map vars_term (?ti # (map Var ?zs))))"
unfolding list.simps(9) is_partition_Cons zs by blast
let ?t = "(U ρ i)⟨snd (snd ρ ! i)⟩"
from U_cond[OF inR i] obtain f where Uri:"U ρ i = More f [] □ (map Var (Z ρ i))" by fast
from p have "¬ linear_term ?t" unfolding Uri by simp
hence l:"¬ linear_term (lhs_n ρ (Suc i))" unfolding rho by auto
have "linear_term (lhs_n ρ (Suc i))" by(rule ll[unfolded rules_def], insert i, auto)
with l show False by auto
qed
with 2 have "linear_term ?ti ∧ vars_term (snd ((snd ρ)!i)) ∩ X_vars ρ i = {}" by auto
}
with 1 show ?thesis by auto
qed
lemma part_rev : assumes p:"is_partition xs" shows "is_partition (rev xs)"
unfolding is_partition_def length_rev
proof(rule,rule)
fix j
assume j:"j < length xs"
show "∀i<j. rev xs ! i ∩ rev xs ! j = {}" proof(rule,rule)
fix i
assume i:"i < j"
from j have 1:"length xs - (Suc i) < length xs" by fastforce
from i j have 2:"length xs - (Suc j) < length xs - (Suc i)"
by (metis Suc_less_eq diff_less_mono2 less_trans_Suc)
from p[unfolded is_partition_def] 1 2
show "rev xs ! i ∩ rev xs ! j = {}" unfolding rev_nth[OF j] rev_nth[OF order.strict_trans[OF i j]] by blast
qed
qed
lemma is_partition_rev : "is_partition (rev xs) = is_partition xs "
using part_rev rev_rev_ident by force
lemma substs_rsteps':
shows "(⋀x. x ∈ vars_term t ⟹ (σ x, τ x) ∈ (cstep R)⇧*) ⟹ (t ⋅ σ, t ⋅ τ) ∈ (cstep R)⇧*"
proof (induct t)
case (Var y)
thus ?case by simp
next
case (Fun f ts)
have "⋀ s. s ∈ set ts ⟹ vars_term s ⊆ vars_term (Fun f ts)" by auto
with Fun have "⋀ s. s ∈ set ts ⟹ (s ⋅ σ, s ⋅ τ) ∈ (cstep R)⇧*" by blast
then have "∀i<length (map (λt. t ⋅ σ) ts).
(map (λt. t ⋅ σ ) ts ! i, map (λt. t ⋅ τ) ts ! i) ∈ (cstep R)⇧*" by auto
from args_steps_imp_steps[OF cstep_ctxt_closed _ this] show ?case by simp
qed
definition X_part :: "('f,'v) crule ⇒ 'v set list" where
"X_part ρ ≡ ((X_vars ρ 0) # (map (λi. X_vars ρ (Suc i) - (X_vars ρ i)) [0..< (length (snd ρ) - 1)]) @
[(vars_term (crhs ρ) ∪ (vars_term (ti ρ (length (snd ρ) - 1)))) - (X_vars ρ (length (snd ρ) - 1))])"
lemma X_part: assumes inR:"ρ ∈ R"
and l:"length (snd ρ) ≠ 0 "
shows "is_partition (X_part ρ)"
proof-
let ?k = "length (snd ρ)"
from not0_implies_Suc[OF l] obtain k' where k_suc:"?k = Suc k'" by auto
let ?xk = "(vars_term (crhs ρ) ∪ (vars_term (ti ρ k'))) - (X_vars ρ k')"
let ?xs = "λ m. (X_vars ρ 0) # (map (λi. X_vars ρ (Suc i) - (X_vars ρ i)) [0..<m])"
fix j
have key:"∀j. j < ?k ⟶ (is_partition (rev (?xs j)) ∧ ⋃set (?xs j) ⊆ X_vars ρ j)" proof(rule allI, rule)
fix j
assume "j < ?k"
thus "is_partition (rev (?xs j)) ∧ ⋃set (?xs j) ⊆ X_vars ρ j" proof(induct j)
case 0
have s:"?xs 0 = [X_vars ρ 0]" by auto
thus ?case unfolding s using rev.simps is_partition_Cons is_partition_Nil by force
next
case (Suc j)
assume lt:"Suc j < ?k"
with Suc have p:"is_partition (rev (?xs j))" and ss:"⋃set (?xs j) ⊆ X_vars ρ j" by auto
let ?xi = "λ j. X_vars ρ (Suc j) - (X_vars ρ j)"
have "?xs (Suc j) = (?xs j) @ [?xi j]" unfolding upt_Suc_append[OF le0] map_append by fastforce
hence r:"rev (?xs (Suc j)) = (?xi j) # (rev (?xs j))" using rev_eq_Cons_iff[of "?xs (Suc j)"] by auto
have "(?xi j) ∩ X_vars ρ j = {}" by auto
with ss have "(?xi j) ∩ ⋃set (rev (?xs j)) = {}" by auto
with Suc r have p:"is_partition (rev (?xs (Suc j)))" using is_partition_Cons[of "?xi j" "rev (?xs j)"] by fastforce
from ss X_vars_mono[OF inR lt less_imp_le[OF lessI]]
have "⋃set (?xs (Suc j)) ⊆ X_vars ρ (Suc j)"
unfolding upt_Suc_append[OF le0] map_append list.set(2) set_append by auto
with p show ?case by auto
qed
qed
have lt:"k' < ?k" using k_suc by auto
from key this have p:"is_partition (rev (?xs k'))" "⋃set (?xs k') ⊆ X_vars ρ k'" unfolding X_part_def by auto
from p(2) have isc:"?xk ∩ ⋃set (rev (?xs k')) = {}" by auto
from k_suc have kk:"?k - 1 = k'" by auto
have aux:"rev (?xs k' @ [?xk]) = ?xk # rev (?xs k')" using rev_eq_Cons_iff by fastforce
with p isc have "is_partition (rev (?xs k' @ [?xk]))" unfolding aux is_partition_Cons by blast
thus ?thesis using is_partition_rev unfolding X_part_def kk by force
qed
lemma Z_part: assumes inR:"ρ ∈ R"
and i:"i < length (snd ρ)"
shows "is_partition (map (λ z. {z}) (Z ρ i))"
proof-
from Z[unfolded Z_vars_def] inR i have "distinct (Z ρ i)" by fast
with distinct_conv_nth show ?thesis unfolding is_partition_def by force
qed
lemma ll_aux:
assumes "ρ ∈ R"
and "left_linear_trs UR"
shows "left_linear_trs (rules ρ)"
using assms unfolding left_linear_trs_def UR_def by blast
lemma Z_ti_disjoint:
assumes inR:"ρ ∈ R"
and i:"i < length (snd ρ)"
and ll:"left_linear_trs UR"
shows "vars_term (ti ρ i) ∩ set (Z ρ i) = {}"
proof-
from i not0_implies_Suc obtain k where l:"length (snd ρ) = Suc k" by (metis less_nat_zero_code)
from L3_9a[OF inR ll_aux[OF inR ll]] i have "vars_term (ti ρ i) ∩ (X_vars ρ i) = {}" by auto
obtain l r cs where rho:"ρ = ((l,r),cs)" by (cases ρ, auto)
from U_cond[OF inR i] obtain Ui where Ui:"U_fun ρ i Ui" by auto
from ll_aux[OF inR ll, unfolded rules_def left_linear_trs_def] i have "linear_term (lhs_n ρ (Suc i))" by auto
from this[unfolded rho lhs_n.simps Ui[unfolded rho], simplified, unfolded is_partition_Cons]
have "vars_term (ti ρ i) ∩ set (Z ρ i) = {}" unfolding rho by force
with Z[unfolded Z_vars_def] inR i show "vars_term (ti ρ i) ∩ set (Z ρ i) = {}" by auto
qed
lemma Z_part': assumes inR:"ρ ∈ R"
and i:"i < length (snd ρ)"
and ll:"left_linear_trs UR"
shows "is_partition (vars_term (ti ρ i) # map (λ z. {z}) (Z ρ i))"
proof-
from Z_part[OF inR i] have p:"is_partition (map (λ z. {z}) (Z ρ i))" by auto
with Z_ti_disjoint[OF inR i ll] is_partition_Cons show ?thesis by fastforce
qed
lemma X_part_nth :
assumes inR:"ρ ∈ R"
and l:"length (snd ρ) ≠ 0 "
and jk:"Suc j < length (snd ρ)"
shows " (X_part ρ) ! (Suc j) = (X_vars ρ (Suc j)) - (X_vars ρ j)"
proof-
let ?k = "length (snd ρ)"
let ?f = "λi. (X_vars ρ (Suc i)) - (X_vars ρ i)"
from jk have x:"j < ?k - 1 - 0" by auto
hence "map ?f [0..<?k - 1] ! j = (X_vars ρ (Suc j)) - (X_vars ρ j)"
unfolding nth_map[of j "[0..<?k - 1]", unfolded length_upt, OF x] using nth_upt by force
with nth_map[of j "[0..<?k - 1]", unfolded length_upt, OF x] show ?thesis unfolding X_part_def nth_Cons_Suc
nth_append[of "map ?f [0..<?k - 1]" _ j, unfolded length_map length_upt eqTrueI[OF x] if_True] by blast
qed
lemma X_part_last :
assumes inR:"ρ ∈ R"
and l:"length (snd ρ) ≠ 0 "
shows " (X_part ρ) ! (length (snd ρ)) =
(vars_term (crhs ρ) ∪ (vars_term (ti ρ (length (snd ρ) - 1)))) - (X_vars ρ (length (snd ρ) - 1))"
proof-
let ?k = "length (snd ρ)"
let ?f = "λi. (X_vars ρ (Suc i)) - (X_vars ρ i)"
from l have kl:"?k = length ((X_vars ρ 0) # map ?f [0..<?k - 1])" unfolding length_Cons length_map length_upt by simp
with nth_append_length show ?thesis unfolding X_part_def append_Cons[symmetric] by (metis (no_types, lifting))
qed
lemma vars_cs_vars_ti:
assumes inR: "ρ ∈ R"
and x:"x ∈ vars_trs (set (snd ρ))"
shows "x ∈ vars_term (clhs ρ) ∨ (∃ j. j< (length (snd ρ)) ∧ x ∈ vars_term (ti ρ j))"
proof-
let ?k = "length (snd ρ)"
from x[unfolded vars_trs_def set_conv_nth] have "∃ j. j< ?k ∧ (x ∈ vars_rule ((snd ρ) ! j))" by auto
with vars_rule_def obtain j where j:"j< ?k""(x ∈ vars_term (ti ρ j) ∨ x ∈ vars_term (si ρ j))" by fast
{ assume "x ∈ vars_term (si ρ j)"
with dctrs[unfolded dctrs_def, rule_format, OF inR j(1)] X_vars_alt[OF less_imp_le_nat[OF j(1)]] have
"x ∈ vars_term (clhs ρ) ∨ x ∈ ⋃((λj. vars_term (ti ρ j)) ` {ja. ja < j})" by blast
with j(1) have ?thesis by force
}
with j show ?thesis by blast
qed
abbreviation "XY ρ m ≡ (X_vars ρ m) ∩ (Y_vars ρ m)"
lemma XYi_subset_ti_XY:
assumes inR:"ρ ∈ R" and m:"Suc m < length (snd ρ)"
shows "XY ρ (Suc m) ⊆ vars_term (ti ρ m) ∪ XY ρ m"
proof-
{fix x
assume x:"x ∈ XY ρ (Suc m)"
with X_vars_Suc[OF inR m] have x':"x ∈ X_vars ρ m ∪ vars_term (ti ρ m)" by auto
from x Y_vars_mono[OF m, of m] have y:"x ∈ Y_vars ρ m" by auto
with x' y have "x ∈ vars_term (ti ρ m) ∪ XY ρ m" by auto
}
thus ?thesis by blast
qed
lemma vars_si_subset_ti_XY:
assumes inR:"ρ ∈ R" and m:"Suc m < length (snd ρ)"
shows "vars_term (si ρ (Suc m)) ⊆ vars_term (ti ρ m) ∪ XY ρ m"
proof-
{fix x
assume x:"x ∈ vars_term (si ρ (Suc m))"
from m length_drop have "length (drop m (snd ρ)) > 1" by fastforce
with x m have y:"x ∈ Y_vars ρ m"
by (subst Y_vars_alt, auto)
have " x ∈ vars_term (ti ρ m) ∪ XY ρ m" proof(cases "x ∈ vars_term (ti ρ m)", simp)
assume x':"x ∉ vars_term (ti ρ m)"
from dctrs[unfolded dctrs_def, rule_format, OF inR m] x X_vars_alt[OF less_imp_le_nat[OF m]]
have xin:"x ∈ vars_term (clhs ρ) ∪ ⋃((λj. vars_term (ti ρ j)) ` {j. j < Suc m})" by blast
have " {j. j < Suc m} = {j. j < m} ∪ {m}" by fastforce
hence "⋃((λj. vars_term (ti ρ j)) ` {j. j < Suc m}) = (⋃((λj. vars_term (ti ρ j)) ` ({j. j < m} ∪ {m} ))) ∪ vars_term (ti ρ m)" by force
hence "⋃((λj. vars_term (ti ρ j)) ` {j. j < Suc m}) = (⋃((λj. vars_term (ti ρ j)) ` {j. j < m})) ∪ vars_term (ti ρ m)" by auto
with x' xin have xin:"x ∈ vars_term (clhs ρ) ∪ ⋃((λj. vars_term (ti ρ j)) ` {j. j < m})" by auto
from m have len:"length (take m (snd ρ)) = m" by auto
with nth_take[of _ m "snd ρ"] have "take m (snd ρ) = map (λj. (snd ρ ! j)) [0..< m]"
by (metis (poly_guards_query) Suc_lessD m take_upt_idx)
with nth_take[of _ m "snd ρ"] len have "set (take m (snd ρ)) = (λj. (snd ρ ! j)) ` {j. j < m}" by auto
then have aux:"rhss (set (take m (snd ρ))) = (λj. (ti ρ j)) ` {j. j < m}" by force
from m xin aux have "x ∈ X_vars ρ m" unfolding X_vars_def by force
with y show ?thesis by auto
qed}
thus ?thesis by blast
qed
abbreviation si :: "('f,'v) crule ⇒ nat => ('f,'v) term" where "si ρ i ≡ fst ((snd ρ)!i)"
abbreviation ti :: "('f,'v) crule ⇒ nat => ('f,'v) term" where "ti ρ i ≡ snd ((snd ρ)!i)"
lemma vars_r_subset_tk_Z:
assumes inR:"((l,r),cs) ∈ R" (is "?ρ ∈ R")
and lcs:"length cs > 0"
shows "vars_term r ⊆ XY ?ρ (length cs - 1) ∪ vars_term (ti ?ρ (length cs - 1))"
proof
fix x
assume xr:"x ∈ vars_term r"
let ?k = "length cs - 1"
let ?X = "λk. ⋃((λj. vars_term (ti ?ρ j)) ` {j. j < k})"
let ?Xk = "?X (length cs)" let ?Xk' = "?X ?k"
from xr type3[unfolded type3_def, rule_format, OF inR] vars_cs_vars_ti[OF inR] have xx':"x ∈ vars_term l ∪ ?Xk" by auto
from lcs have " {j. j < length cs} = {j. j < ?k} ∪ {?k}" by fastforce
hence "?Xk = ?Xk' ∪ vars_term (ti ?ρ ?k)" by force
from xx' this have xx':"x ∈ vars_term l ∪ ?Xk' ∪ vars_term (ti ?ρ ?k)" by auto
have len:"length (take ?k (snd ?ρ)) = ?k" by auto
with nth_take[of _ ?k "snd ?ρ"] have "take ?k (snd ?ρ) = map (λj. (snd ?ρ ! j)) [0..< ?k]"
by (metis diff_less lcs snd_conv take_upt_idx zero_less_one)
hence aux:"rhss (set (take ?k (snd ?ρ))) = ((λj. (ti ?ρ j)) ` {0..< ?k})" by auto
from xx' have xx:"x ∈ X_vars ?ρ ?k ∪ vars_term (ti ?ρ ?k)" unfolding aux X_vars_def by force
from lcs xr this have y:"x ∈ Y_vars ?ρ ?k" unfolding Y_vars_def by auto
from xx y lcs show "x ∈ XY ?ρ ?k ∪ vars_term (ti ?ρ ?k)" by auto
qed
lemma Lemma_17:
assumes inR: "ρ ∈ R"
and ll: "left_linear_trs UR"
and l: "length (snd ρ) ≠ 0 "
and sl: "length (σ :: ('f, 'v) subst list) = Suc (length (snd ρ))"
and st: "∀ i < length (snd ρ). (si ρ i ⋅ (σ ! i), ti ρ i ⋅ (σ ! Suc i) ) ∈ (cstep R)⇧*"
and zrew: "∀ i < length (snd ρ). ∀ z ∈ set (Z ρ i). (Var z ⋅ (σ ! i), Var z ⋅ (σ ! Suc i)) ∈ (cstep R)⇧*"
shows "(clhs ρ ⋅ (σ ! 0), crhs ρ ⋅ (σ!(length (snd ρ)))) ∈ (cstep R)⇧+"
proof-
let ?k = "length (snd ρ)"
let ?xs = "X_part ρ"
let ?σ = "fun_merge σ ?xs"
from not0_implies_Suc l obtain k' where k_suc:"?k = Suc k'" by auto
have lx:"Suc ?k = length ?xs" unfolding X_part_def using k_suc by fastforce
from X_part[OF inR l] have p:"is_partition ?xs" by fast
{ fix t :: "('f,'v) term" fix i
assume x:"i < Suc ?k" and y:"vars_term t ⊆ ?xs!i"
from y fun_merge_part[OF p] x[unfolded lx] have "⋀ x. x ∈ (vars_term t) ⟹ ?σ x = (σ!i) x" by blast
from term_subst_eq this have "t ⋅ ?σ = t ⋅ (σ!i)" by blast
}
note subst_fact = this
let ?l = "clhs ρ" let ?r = "crhs ρ" let ?cs = "snd ρ"
from inR have rho:"((?l,?r),?cs) ∈ R " by auto
have "vars_term ?l ⊆ ?xs ! 0" using l_vars_X_vars[OF inR, OF l[unfolded neq0_conv]] unfolding X_part_def by auto
from subst_fact[OF _ this] lx have lsigma:"?l ⋅ ?σ = ?l ⋅ (σ!0)" by fast
note ull = ll_aux[OF inR ll]
{ fix i
assume ik:"i < ?k"
from conjunct2[OF conjunct2[OF L3_9a[OF inR ull]], rule_format,OF ik] have ss':"vars_term (ti ρ i) ∩ X_vars ρ i = {}" by auto
have "vars_term (ti ρ i) ⊆ ?xs!Suc i"
proof(cases "Suc i < ?k")
case True
from ik min_less_iff_conj nth_mem[of i "take (Suc i)(snd ρ)", unfolded length_take nth_take[OF lessI]]
have "ti ρ i ∈ rhss (set (take (Suc i)(snd ρ)))" by blast
with subsetI image_eqI[OF refl] have "vars_term (ti ρ i) ⊆ ⋃(vars_term ` rhss (set (take (Suc i) (snd ρ))))" by blast
hence ss:"vars_term (ti ρ i) ⊆ X_vars ρ (Suc i)" unfolding X_vars_def by auto
from X_part_nth[OF inR _ True] k_suc have "?xs ! Suc i = X_vars ρ (Suc i) - X_vars ρ i" by auto
with ss ss' show "vars_term (ti ρ i) ⊆ ?xs ! Suc i" by blast
next
case False
with ik have i:"i = ?k - 1" and ii: "Suc i = ?k" by auto
have xk: "?xs ! (Suc i) = vars_term (crhs ρ) ∪ vars_term (ti ρ i) - X_vars ρ i"
unfolding X_part_def i k_suc
using nth_append_length[of "(X_vars ρ 0) # map (λi. X_vars ρ (Suc i) - X_vars ρ i) [0..<Suc k' - 1]", unfolded length_Cons length_map length_upt]
unfolding length_Cons length_map length_upt by force
with ss' show "vars_term (ti ρ i) ⊆ ?xs!Suc i" unfolding ii by blast
qed
from subst_fact[OF _ this] ik have "(ti ρ i) ⋅ (σ! (Suc i)) = (ti ρ i) ⋅ ?σ" by fastforce
}
note t_fact = this
{ fix j x
assume y:"x ∈ Y_vars ρ j"
and lhs_or_ti:"x ∈ vars_term ?l ∨ (∃ k < Suc j. x ∈ vars_term (ti ρ k))"
and ik:"Suc j ≤ ?k"
from y Y_vars_mono Suc_le_lessD[OF ik] have y:"⋀ j'. j' ≤ j ⟹ x ∈ Y_vars ρ j'" by blast
have "(?σ x, (σ! (Suc j)) x) ∈ (cstep R)⇧*"
proof(cases "x ∈ vars_term ?l")
case True
with l_vars_X_vars[OF inR] k_suc have "x ∈ ?xs!0" unfolding X_part_def nth_Cons_0 by auto
from fun_merge_part[OF p _ this, unfolded lx[symmetric] k_suc] have sx0:"?σ x = (σ!0) x" by auto
from l_vars_X_vars[OF inR] True k_suc X_vars_mono[OF inR _ le0]
order.strict_trans2[OF _ ik] have x:"⋀ j'. j' < Suc j ⟹ x ∈ X_vars ρ j'" by blast
from x y X_Y_imp_Z[OF inR] ik k_suc have z:"⋀ j'. j' < Suc j ⟹ x ∈ set (Z ρ j')" by simp
hence xZ0:"x ∈ set (Z ρ 0)" by auto
from z ik have "((σ ! 0) x, (σ ! (Suc j)) x) ∈ (cstep R)⇧*" proof (induct j)
case 0 from zrew[rule_format, of 0] k_suc xZ0 show ?case by simp
next
case (Suc k)
hence 1:"Suc k < ?k" and 2:"⋀ j. j < Suc k ⟹ x ∈ set (Z ρ j)" by auto
from zrew[rule_format, OF 1 Suc(2)] Suc(1) 2 1 show ?case by fastforce
qed
with sx0 show ?thesis by auto
next
case False
with lhs_or_ti obtain j' where ji:"j' < Suc j" and xj:"x ∈ vars_term (ti ρ j')" by auto
from ji ik have 1:"Suc j' ≤ ?k" by auto
from L3_9a[OF inR ull] order.strict_trans2[OF ji ik] have x:"vars_term (ti ρ j') ∩ X_vars ρ j' = {}" by fast
from nth_take[OF lessI] nth_mem[of j' "take (Suc j') (snd ρ)", unfolded nth_take[OF lessI] length_take min_less_iff_conj]
order.strict_trans2[OF ji ik] image_iff[of "ti ρ j'" snd] lessI[of j']
have "ti ρ j' ∈ rhss (set (take (Suc j') ?cs))" by blast
with xj image_iff have xu:"x ∈ ⋃(vars_term ` rhss (set (take (Suc j') ?cs)))" unfolding Union_iff by blast
from xu inR False have xsj: "Suc j' < ?k ⟹ x ∈ X_vars ρ (Suc j')" unfolding X_vars_def by blast
have "x ∈ ?xs!(Suc j')"
proof(cases "Suc j' < ?k")
case True
from xsj[OF True] x xj X_part_nth[OF inR _ True] k_suc show ?thesis by auto
next
case False
with 1 have sk:"?k = Suc j'" by auto
with xj x show "x ∈ ?xs!(Suc j')" unfolding X_part_last[OF inR nat.discI[OF sk], unfolded sk] by auto
qed
from fun_merge_part[OF p _ this] lx 1 have sxSucj:"?σ x = (σ!Suc j') x" by auto
{ fix j''
assume 1:"Suc j' ≤ j''" and 2:"j'' < Suc j"
with ik have ltk:"Suc j' < ?k" by force
have "x ∈ X_vars ρ j''" proof(cases "Suc j' = j''", insert xsj[OF ltk],simp)
case False with 1 have "Suc j' < j''" by auto
from xsj[OF ltk] X_vars_mono[OF inR _ 1] 2 ik show "x ∈ X_vars ρ j''" by auto
qed
from X_Y_imp_Z[OF inR _ this y[OF 2[unfolded less_Suc_eq_le]]] 2 ik have "x ∈ set (Z ρ j'')" by auto
} note z = this
have "((σ ! Suc j') x, (σ ! (Suc j)) x) ∈ (cstep R)⇧*"
proof(cases "Suc j' = Suc j", insert ji, simp)
case False
with ji have "Suc j' < Suc j" by auto
with z ik show ?thesis proof (induct j,simp)
case (Suc k)
from Suc have z:"⋀ j''. Suc j' ≤ j'' ∧ j'' < Suc k ⟹ x ∈ set (Z ρ j'')" by auto
show ?case proof(cases "Suc j'= Suc k")
case False
with Suc(4) Suc(3) have 0:"j' < Suc k" and 1:"Suc k < ?k" and 2:"Suc j' < Suc k" by auto
from z Suc(1)[OF _ less_imp_le_nat[OF 1] 2] have "((σ ! Suc j') x, (σ ! Suc k) x) ∈ (cstep R)⇧*" by blast
with zrew[rule_format, OF 1] Suc(2)[of "Suc k", OF Suc_leI[OF 0] lessI] show ?thesis by force
next
case True
from Suc have 0:"Suc j' < ?k" by auto
from True zrew[rule_format, OF 0 Suc(2)[OF order.refl Suc(4)]] show ?thesis by simp
qed
qed
qed
with sxSucj show ?thesis by auto
qed
} note auxiliary2 = this
{ fix i x
assume ik:"i < ?k"
{ fix x
assume xs:"x ∈ vars_term (si ρ i)"
have " (?σ x, (σ!i) x) ∈ (cstep R)⇧*" proof(cases i)
case 0
from xs[unfolded 0] dctrs[unfolded dctrs_def, rule_format, OF inR ik[unfolded 0]]
X_vars_alt have "x ∈ vars_term ?l" by fast
with l_vars_X_vars[OF inR] k_suc have "x ∈ ?xs!0" unfolding X_part_def nth_Cons_0 by auto
from fun_merge_part[OF p _ this, unfolded lx[symmetric] k_suc] have "?σ x = (σ!0) x" by auto
with 0 show ?thesis by auto
next
case (Suc j)
from s_imp_Y[OF inR ik[unfolded Suc] xs[unfolded Suc]] ik have y:"x ∈ Y_vars ρ j" by blast
from rev_subsetD[OF xs dctrs[unfolded dctrs_def, rule_format, OF inR ik], unfolded X_vars_alt[OF less_imp_le_nat[OF ik]]]
auxiliary2[OF y] Suc ik show ?thesis by fastforce
qed
}
with ik substs_rsteps' have "((si ρ i) ⋅ ?σ, (si ρ i) ⋅ (σ!i)) ∈ (cstep R)⇧*" by blast
} note ss = this
{ fix i x
assume xr:"x ∈ vars_term (crhs ρ)"
note alts = rev_subsetD[OF xr type3[unfolded type3_def, rule_format, OF inR], unfolded Un_iff[of x]]
let ?goal = "x ∈ vars_term ?l ∨ (∃ j. j< ?k ∧ x ∈ vars_term (ti ρ j))"
from alts vars_cs_vars_ti[OF inR] xr have disj:?goal by blast
from xr have y:" x ∈ Y_vars ρ k'" unfolding k_suc Y_vars_def by simp
from auxiliary2[OF y] disj k_suc have "(?σ x, (σ!?k) x) ∈ (cstep R)⇧*" by auto
} note xr = this
from xr substs_rsteps' have "(?r ⋅ ?σ, ?r ⋅ (σ!?k)) ∈ (cstep R)⇧*" by blast
then obtain m where rsigma:"(?r ⋅ ?σ, ?r ⋅ (σ!?k)) ∈ (cstep_n R m)⇧*" using csteps_imp_csteps_n by blast
from ss st[rule_format] t_fact have "∀ i < ?k.((si ρ i) ⋅ ?σ,(ti ρ i) ⋅ ?σ) ∈ (cstep R)⇧*"
using rtrancl_trans[of _ _ "cstep R"] nat_less_le by metis
from all_cstep_imp_cstep_n[of "length (snd ρ)", OF this] obtain n where "∀ i < ?k. ((si ρ i) ⋅ ?σ,(ti ρ i) ⋅ ?σ) ∈ (cstep_n R n)⇧*" by blast
hence "∀(si, ti) ∈ set (snd ρ). (si ⋅ ?σ, ti ⋅ ?σ) ∈ (cstep_n R n)⇧*"
by (auto) (metis fst_conv in_set_idx snd_conv)
from cstep_n_SucI [OF rho, of _ _ "?l ⋅ ?σ" Hole "rhs_n ρ ?k ⋅ ?σ", unfolded ctxt_apply_term.simps(1), OF this, unfolded lsigma] rsigma rhs_n.simps k_suc
have "(?l ⋅ (σ ! 0), rhs_n ρ ?k ⋅ ?σ) ∈ (cstep_n R (Suc n))⇧+" by (metis less_not_refl prod.collapse r_into_trancl')
from this[unfolded rhs_n.simps[of "fst ρ" "snd ρ", unfolded prod.collapse] k_suc] have "(?l ⋅ (σ ! 0), ?r ⋅ ?σ) ∈ (cstep_n R (Suc n))⇧+" by force
from cstep_n_mono [THEN trancl_mono_set, THEN set_mp, OF _ this, of "max (Suc n) m"]
and cstep_n_mono [THEN rtrancl_mono, THEN set_mp, OF _ rsigma, of "max (Suc n) m"]
obtain n where q:"(clhs ρ ⋅ σ ! 0, crhs ρ ⋅ σ ! length (snd ρ)) ∈ (cstep_n R n)⇧+"
by (auto intro: trancl_rtrancl_trancl)
from trancl_mono_set[of "cstep_n R n" "⋃n. cstep_n R n"] q show ?thesis unfolding cstep_def by blast
qed
definition non_LV :: bool where "non_LV ≡ ∀ (l,r) ∈ UR. ¬is_Var l"
definition non_RV :: bool where "non_RV ≡ ∀ (l,r) ∈ UR. ¬is_Var r"
definition sig_F :: "('f,'v) term ⇒ bool" where "sig_F t ≡ (funs_term t ⊆ F)"
abbreviation sig_F_subst :: "('f,'v) subst ⇒ 'v set ⇒ bool" where
"sig_F_subst θ V ≡ (∀ x ∈ V. sig_F (θ x))"
lemma ur_step_exhaust_nlv:
assumes step:"(Fun f us,v) ∈ rstep_r_p_s UR (l,r) ε σ" and nlv:"non_LV"
shows "(∃ ρ ∈ R. ((l, r) = (lhs_n ρ 0, rhs_n ρ 0) ∧ f ∈ funs_ctrs R) ∨
(∃ n < length (snd ρ).((l, r) = (lhs_n ρ (Suc n), rhs_n ρ (Suc n)) ∧ U ρ n = More f [] □ (map Var (Z ρ n)) ∧ f ∉ funs_ctrs R)))"
proof-
from step[unfolded rstep_r_p_s_def] have ur:"(l,r) ∈ UR" by auto
from this[unfolded UR_def] rules_def obtain n ρ where n:"ρ ∈ R" "(l,r) = (lhs_n ρ n, rhs_n ρ n)""n ≤ length (snd ρ)" by blast
obtain s t cs where rho:"ρ = ((s,t), cs)" by (cases ρ, auto)
from nlv[unfolded non_LV_def, rule_format, OF ur, unfolded split] obtain g ls where l:"l = Fun g ls" by blast
with step[unfolded rstep_r_p_s_def ctxt_of_pos_term.simps(1) Let_def] have gf:"g = f" by simp
show ?thesis proof (cases n)
case 0
from n(2)[unfolded 0 rho lhs_n.simps(1)] have ls:"s=l" by simp
from n(1)[unfolded rho ls l[unfolded gf]] funs_crule_def have "f ∈ funs_ctrs R" unfolding funs_ctrs_def funs_rule_def by force
with n 0 show ?thesis by fast
next
case (Suc m)
with lhs_n.elims[OF conjunct1[OF n(2)[unfolded prod.simps], symmetric]] rho have l':"l = (U ρ m)⟨snd (cs ! m)⟩" by blast
from Suc n(3) have m:"m < length (snd ρ)" by fastforce
from U_cond[OF n(1) this] obtain h where u:"U ρ m = More h [] □ (map Var (Z ρ m)) ∧ h ∉ F" by auto
with l[unfolded gf] l' have "h = f" by simp
from n(1) n(2)[unfolded Suc] u[unfolded this] m F show ?thesis by auto
qed
qed
lemma ur_step_exhaust:
assumes step:"(w,v) ∈ rstep_r_p_s UR (l,r) ε σ"
shows "(∃ ρ ∈ R. ((l, r) = (lhs_n ρ 0, rhs_n ρ 0)) ∨
(∃ f us. w = Fun f us ∧ (∃ n. n < length (snd ρ) ∧ ((l, r) = (lhs_n ρ (Suc n), rhs_n ρ (Suc n))
∧ U_fun ρ n f ∧ f ∉ F))))"
proof-
from step[unfolded rstep_r_p_s_def] have ur:"(l,r) ∈ UR" by auto
from this[unfolded UR_def] rules_def obtain n ρ where n:"ρ ∈ R" "(l,r) = (lhs_n ρ n, rhs_n ρ n)""n ≤ length (snd ρ)" by blast
obtain s t cs where rho:"ρ = ((s,t), cs)" by (cases ρ, auto)
show ?thesis proof (cases n)
case 0
from n(2)[unfolded 0 rho lhs_n.simps(1)] have ls:"s=l" by simp
with n 0 show ?thesis by fast
next
case (Suc m)
with lhs_n.elims[OF conjunct1[OF n(2)[unfolded prod.simps], symmetric]] rho have l':"l = (U ρ m)⟨snd (cs ! m)⟩" by blast
from Suc n(3) have m:"m < length (snd ρ)" by fastforce
from U_cond[OF n(1) this] obtain h where u:"U_fun ρ m h" "h ∉ F" by auto
with step[unfolded rstep_r_p_s_def l'] obtain us where w:"w = Fun h us" by force
have "∃n < length (snd ρ).(l, r) = (lhs_n ρ (Suc n), rhs_n ρ (Suc n)) ∧ U_fun ρ n h ∧ h ∉ F"
by(rule exI[of _ "m"], insert n[unfolded Suc] u m, auto)
with w n(1) show ?thesis by blast
qed
qed
lemma same_U_same_rules:
assumes inR:"ρ ∈ R" "ρ' ∈ R"
and u:"U ρ n = U ρ' n"
and pe:"prefix_equivalent ρ ρ' n"
shows "∀m ≤ n. (lhs_n ρ m, rhs_n ρ m) = (lhs_n ρ' m,rhs_n ρ' m)"
proof(rule,rule)
fix m
assume m:"m ≤ n"
from pe have n:" n < length (snd ρ)" "n < length (snd ρ')" unfolding prefix_equivalent_def by auto
note pe= pe[unfolded prefix_equivalent_def]
from U_cond[OF inR(1) n(1)] inR(2) n(2) u have *:"(∀i≤n. U ρ i = U ρ' i)" by metis
obtain l r cs where rho:"ρ=((l,r),cs)" by (cases ρ, auto)
obtain l' r' cs' where rho':"ρ'=((l',r'),cs')" by (cases ρ', auto)
from rhs_n.simps[of "(l,r)" cs m] m n have r:"rhs_n ρ m = (U ρ m)⟨si ρ m⟩" unfolding rho by fastforce
from rhs_n.simps[of "(l',r')" cs' m] m n have r':"rhs_n ρ' m = (U ρ' m)⟨si ρ' m⟩" unfolding rho' by fastforce
from pe n m have s:"si ρ m = si ρ' m" by auto
from r r' have r: "rhs_n ρ m = rhs_n ρ' m" unfolding *[rule_format, OF m] s by presburger
have "lhs_n ρ m = lhs_n ρ' m" proof(cases m)
case 0
from pe have "l=l'" unfolding rho rho' by auto
thus ?thesis unfolding 0 lhs_n.simps rho rho' by auto
next
case (Suc k)
note us = *[rule_format, of k, unfolded Suc]
from lhs_n.simps(2)[of "(l,r)" cs k] have l:"lhs_n ρ m = (U ρ k)⟨ti ρ k⟩" unfolding rho Suc by simp
from lhs_n.simps(2)[of "(l',r')" cs' k] have l':"lhs_n ρ' m = (U ρ' k)⟨ti ρ' k⟩" unfolding rho' Suc by simp
from pe n m have t:"ti ρ k = ti ρ' k" unfolding Suc by auto
from l l' *[rule_format, of k] m[unfolded Suc] show ?thesis unfolding t by auto
qed
with r show "(lhs_n ρ m, rhs_n ρ m) = (lhs_n ρ' m,rhs_n ρ' m)" by simp
qed
lemma prefix_equivalent_refl:
assumes "n < length (snd ρ)"
shows "prefix_equivalent ρ ρ n"
using assms unfolding prefix_equivalent_def by auto
lemma ur_step_urule:
assumes step:"(Fun f us,v) ∈ rstep_r_p_s UR (l,r) ε σ"
and rho:"ρ ∈ R" and n:"n < length (snd ρ)"
and u:"U ρ n = More f [] □ (map Var (Z ρ n))"
shows "(f ∉ F ∧ (∃ρ'. ρ'∈R ∧ prefix_equivalent ρ ρ' n ∧ U ρ n = U ρ' n ∧ ((Fun f us,v) ∈ rstep_r_p_s UR (lhs_n ρ' (Suc n), rhs_n ρ' (Suc n)) ε σ)))
∨ (∃ρ ∈ R. (l,r) = (lhs_n ρ 0, rhs_n ρ 0))"
proof-
from U_cond[OF rho n] u have "f ∉ F" by force
from ur_step_exhaust[OF step] obtain ρ' where
d: "ρ' ∈ R""(l, r) = (lhs_n ρ' 0, rhs_n ρ' 0) ∨ (
(∃n<length (snd ρ'). (l, r) = (lhs_n ρ' (Suc n), rhs_n ρ' (Suc n)) ∧ U_fun ρ' n f ∧ f ∉ F))"
(is "?A ∨ ?B") by blast
{assume ?A
with d(1) have "∃ρ ∈ R. (l,r) = (lhs_n ρ 0, rhs_n ρ 0)" by blast
} note a = this
{assume ?B
then obtain m where m:"m<length (snd ρ')" "(l, r) = (lhs_n ρ' (Suc m), rhs_n ρ' (Suc m))"
"U_fun ρ' m f" "f ∉ F" by blast
from U_cond[OF rho n] u m d(1) have mn:"m = n" by fastforce
have "∃ρ'. ρ' ∈ R ∧ prefix_equivalent ρ ρ' n ∧ U ρ n = U ρ' n ∧ ((Fun f us,v) ∈ rstep_r_p_s UR (lhs_n ρ' (Suc n), rhs_n ρ' (Suc n)) ε σ)
∧ f ∉ F"
proof (cases "ρ = ρ'")
case True
with m mn have lr:"((l, r) = (lhs_n ρ (Suc n), rhs_n ρ (Suc n)) ∧ f ∉ F)" by meson
show ?thesis by (rule exI[of _ ρ], insert step lr prefix_equivalent_refl[OF n] rho, auto)
next
case False
from u U_cond[OF rho n] ctxt.inject[of f "[]" "□" "map Var (Z ρ n)"] have
"(∀ρ' n' g b c a. ρ' ∈ R ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a ⟶
f ≠ g ∨ n = n' ∧ (∀i≤n. U ρ i = U ρ' i) ∧ prefix_equivalent ρ ρ' n)" by metis
from this[rule_format, of ρ' m f] d(1) m(1) m(3) have us:"∀i≤n. U ρ i = U ρ' i" "prefix_equivalent ρ ρ' n" by auto
from us(1)[rule_format, of n] have u:"U ρ n = U ρ' n" by auto
show ?thesis unfolding mn by(rule exI[of _ ρ'], insert step[unfolded m(2) mn] us(2) m(4) u d(1), auto)
qed
}
with a d(2) show ?thesis by fast
qed
lemma Um_funs_R:
assumes um:"U ρ m = (More Um Nil Hole (map Var (Z ρ m)))" and len:"m < length (snd ρ)"
and rhoR:"ρ ∈ R"
shows "Um ∉ F"
using U_cond[OF rhoR len] um by auto
definition par_urstep_below_root :: "(('f,'v) term × ('f,'v) term) set" where
"par_urstep_below_root ≡ {(s,t). ∃ts ss f. s = Fun f ss ∧ t = Fun f ts ∧
(∀x<length ts. (ss ! x, ts ! x) ∈ par_rstep UR) ∧ length ss = length ts}"
lemma par_urstep_par_rstep:
"par_urstep_below_root ⊆ par_rstep UR"
unfolding par_urstep_below_root_def by auto
lemma all_ctxt_closed_par_rsteps: "all_ctxt_closed UNIV ((par_rstep UR)^*)"
using all_ctxt_closed_par_rstep by (blast intro: trans_ctxt_imp_all_ctxt_closed refl_rtrancl trans_rtrancl)
lemma par_urstep_below_root_refl: "(Fun f us, Fun f us) ∈ par_urstep_below_root"
unfolding par_urstep_below_root_def by blast
lemma par_rstep_below_root_pow_same_root1:
"(Fun f xs, t) ∈ par_urstep_below_root ^^ n ⟹ ∃ ys. t = Fun f ys"
unfolding par_urstep_below_root_def by (induct n arbitrary: t, auto)
lemma par_rstep_below_root_pow_same_root2:
"((t, Fun f xs) ∈ par_urstep_below_root ^^ n ⟹ ∃ ys. t = Fun f ys)"
proof (induct n arbitrary:t)
case 0
thus ?case unfolding par_urstep_below_root_def by auto
next
case (Suc i)
from relpow_Suc_D2[OF Suc(2)] obtain t' where d:"(t, t') ∈ par_urstep_below_root" "(t', Fun f xs) ∈ par_urstep_below_root ^^ i" by blast
from Suc(1) d(2) obtain zs where "t' = Fun f zs" by auto
from d(1)[unfolded this] show ?case unfolding par_urstep_below_root_def by auto
qed
lemma par_rstep_below_root_pow_same_length:
"(Fun f xs, Fun f ys) ∈ par_urstep_below_root ^^ n ⟹ length xs = length ys"
unfolding par_urstep_below_root_def by (induct n arbitrary: ys, auto)
lemma linear_term_ti:
assumes ll:"left_linear_trs UR"
and rho:"ρ ∈ R"
and i:"i < length (snd ρ)"
shows "linear_term (ti ρ i)"
proof-
from i have "Suc i ≤ length (snd ρ)" by auto
with rho rules_def have "(lhs_n ρ (Suc i), rhs_n ρ (Suc i)) ∈ UR" unfolding UR_def by blast
with ll[unfolded left_linear_trs_def, rule_format, OF this] have lin:"linear_term (lhs_n ρ (Suc i))" by force
from rho obtain lr cs where rho':"ρ = (lr,cs)" by fastforce
with lin lhs_n.simps(2) have "linear_term (U ρ i)⟨ti ρ i⟩" by auto
with linear_term.elims(1) U_cond[OF rho i] show ?thesis by force
qed
lemma sig_F_ti:
assumes rho:"ρ ∈ R"
and i:"i < length (snd ρ)"
shows "sig_F (ti ρ i)"
proof-
obtain lr cs where rho':"ρ = (lr, cs)" by fastforce
with i have set:"(si ρ i, ti ρ i) ∈ set cs" by fastforce
have 1:"funs_term (ti ρ i) ⊆ funs_rule (si ρ i, ti ρ i)" using funs_rule_def rho' by fastforce
with set have 2:"funs_term (ti ρ i) ⊆ funs_trs (set cs)" unfolding funs_trs_def by blast
hence "funs_term (ti ρ i) ⊆ funs_crule ρ" unfolding funs_crule_def rho' by force
with rho F show ?thesis unfolding sig_F_def funs_ctrs_def by force
qed
lemma sig_F_si:
assumes rho:"ρ ∈ R"
and i:"i < length (snd ρ)"
shows "sig_F (si ρ i)"
proof-
obtain lr cs where rho':"ρ = (lr, cs)" by fastforce
with i have set:"(si ρ i, ti ρ i) ∈ set cs" by fastforce
have 1:"funs_term (si ρ i) ⊆ funs_rule (si ρ i, ti ρ i)" using funs_rule_def rho' by fastforce
with set have 2:"funs_term (si ρ i) ⊆ funs_trs (set cs)" unfolding funs_trs_def by blast
hence "funs_term (si ρ i) ⊆ funs_crule ρ" unfolding funs_crule_def rho' by force
with rho F set show ?thesis unfolding sig_F_def funs_ctrs_def by force
qed
lemma sig_F_l: "ρ ∈ R ⟹ sig_F (clhs ρ)" using F
unfolding sig_F_def funs_ctrs_def using funs_crule_def[of ρ, unfolded funs_rule_def] by blast
lemma sig_F_r: "ρ ∈ R ⟹ sig_F (crhs ρ)" using F
unfolding sig_F_def funs_ctrs_def using funs_crule_def[of ρ, unfolded funs_rule_def] by blast
lemma sig_F_subst:
"∀x∈vars_term l. sig_F (τ x) ⟹ sig_F l ⟹ sig_F (l ⋅ τ)"
proof(induct l)
case (Var x)
from Var(1)[rule_format, unfolded Var] term.simps(17) show ?case by auto
next
case (Fun f ts)
{ fix t assume t:"t ∈ set ts"
then have "vars_term t ⊆ vars_term (Fun f ts)" by auto
with Fun(2) have v:"∀x∈vars_term t. sig_F (τ x)" by blast
from Fun(3)[unfolded sig_F_def funs_ctrs_def term.simps(16)] t have "sig_F t" unfolding sig_F_def funs_ctrs_def by auto
from Fun(1)[OF t v this] have "sig_F (t ⋅ τ)" by simp
} note args = this
from Fun(3)[unfolded sig_F_def funs_ctrs_def] have "f ∈ F" unfolding sig_F_def funs_ctrs_def by force
with args show ?case unfolding sig_F_def by auto
qed
"cond_rule"">abbreviation "cond_rule" :: "('f,'v) crule ⇒ bool"
where "cond_rule ρ ≡ ρ ∈ R ∧ length (snd ρ) > 0"
"complete_R_step_simulation"">definition "complete_R_step_simulation" :: "(nat ⇒ ('f,'v) term) ⇒ nat ⇒ ('f,'v) crule ⇒ bool"
where "complete_R_step_simulation ui n ρ ≡ ∃ j ni σi.
(∀i. 0 ≤ i ∧ i ≤ length (snd ρ) ⟶
j i < n ∧ (ui (j i), ui (Suc (j i))) ∈ (rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i))) ∧
(∀i. 0 ≤ i ∧ i < length (snd ρ) ⟶ (ui (Suc (j i)), ui (j (Suc i))) ∈ par_urstep_below_root ^^ (ni i)) ∧
j 0 + sum_list (map (Suc ∘ ni) [0..<length (snd ρ)]) = j (length (snd ρ))"
"partial_R_step_simulation"">definition "partial_R_step_simulation" :: "(nat ⇒ ('f,'v) term) ⇒ nat ⇒ ('f,'v) crule ⇒nat ⇒ bool"
where "partial_R_step_simulation ui n ρ k ≡ ∃ j ni nm σi.
k < length (snd ρ) ∧
(∀i. 0 ≤ i ∧ i ≤ k ⟶
j i < n ∧ (ui (j i), ui (Suc (j i))) ∈ (rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i))) ∧
(∀i. 0 ≤ i ∧ i < k ⟶ (ui (Suc (j i)), ui (j (Suc i))) ∈ par_urstep_below_root ^^ (ni i)) ∧
(ui (Suc (j k)), ui n) ∈ par_urstep_below_root ^^ nm ∧
j 0 + sum_list (map (Suc ∘ ni) [0..<k]) + Suc nm = n"
lemma extend_partial_R_step_sim:
assumes sim:"partial_R_step_simulation ui m ρ k" and step:"(ui m, ui (Suc m)) ∈ par_urstep_below_root"
shows "partial_R_step_simulation ui (Suc m) ρ k"
proof-
let ?usteps = "λ m k j σi. (∀i. 0 ≤ i ∧ i ≤ k ⟶ j i < m ∧ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i))"
let ?isteps = "λ k j ni. ∀i. 0 ≤ i ∧ i < k ⟶ (ui (Suc (j i)), ui (j (Suc i))) ∈ par_urstep_below_root ^^ ni i"
let ?suffix = "λ m k j nm. (ui (Suc (j k)), ui m) ∈ par_urstep_below_root ^^ nm"
let ?sum = "λ m k j ni nm. j 0 + sum_list (map (Suc ∘ ni) [0..<k]) + Suc nm = m"
from sim[unfolded partial_R_step_simulation_def] obtain j ni nm σi where
sim:"k < length (snd ρ)" "?usteps m k j σi" "?isteps k j ni" "?suffix m k j nm" "?sum m k j ni nm" by force
from sim(2) have 2:"?usteps (Suc m) k j σi" by force
from sim(4) step have 4:"?suffix (Suc m) k j (Suc nm)" by auto
from sim(5) have 5:"?sum (Suc m) k j ni (Suc nm)" by simp
from sim(1) 2 sim(3) 4 5 show ?thesis unfolding partial_R_step_simulation_def by blast
qed
lemma complete_partial_R_step_sim:
assumes sim:"partial_R_step_simulation ui m ρ (length (snd ρ) - 1)"
and step:"(ui m, ui (Suc m)) ∈ rstep_r_p_s UR (lhs_n ρ (length (snd ρ)), rhs_n ρ (length (snd ρ))) ε σk"
and lcs:"length (snd ρ) > 0"
shows "complete_R_step_simulation ui (Suc m) ρ"
proof-
let ?ustep = "λ m j σi i. j i < m ∧ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i)"
let ?istep = "λ j ni i. (ui (Suc (j i)), ui (j (Suc i))) ∈ par_urstep_below_root ^^ ni i"
let ?usteps = "λ m k j σi. (∀i. 0 ≤ i ∧ i ≤ k ⟶ ?ustep m j σi i)"
let ?isteps = "λ k j ni. ∀i. 0 ≤ i ∧ i < k ⟶ ?istep j ni i"
let ?suffix = "λ m k j nm. (ui (Suc (j k)), ui m) ∈ par_urstep_below_root ^^ nm"
let ?sum = "λ m k j ni nm. j 0 + sum_list (map (Suc ∘ ni) [0..<k]) + Suc nm = m"
let ?sum' = "λ j ni. j 0 + sum_list (map (Suc ∘ ni) [0..<length (snd ρ)]) = j (length (snd ρ))"
from lcs gr0_implies_Suc obtain k where lk:"length (snd ρ) = Suc k" by auto
with sim[unfolded partial_R_step_simulation_def] obtain j ni nm σi where
sim:"k ≤ length (snd ρ)" "?usteps m k j σi" "?isteps k j ni" "?suffix m k j nm" "?sum m k j ni nm" by force
let ?ni = "λi. if i < k then ni i else nm"
let ?j = "λi. if i ≤ k then j i else m"
let ?σi = "λi. if i ≤ k then σi i else σk"
{ fix i
assume a:"0 ≤ i" "i ≤ Suc k"
have "?ustep (Suc m) ?j ?σi i" unfolding lk by (cases "i = Suc k", insert sim(2)[rule_format, of i] step lk a, auto)
} note 1 = this
{ fix i
assume a:"0 ≤ i" "i < Suc k"
have "?istep ?j ?ni i" unfolding lk by (cases "i = k", insert sim(3)[rule_format, of i] sim(4) lk a, auto)
} note 2 = this
have l:"(map (Suc ∘ ni) [0..<k]) @ [Suc nm] = map (Suc ∘ ?ni) [0..<Suc k]" unfolding lk by (induct k, auto)
have "sum_list (map (Suc ∘ ni) [0..<k]) + Suc nm = sum_list ((map (Suc ∘ ni) [0..<k]) @ [Suc nm])" by simp
from this[unfolded l] sim(5) have 3:"?sum (Suc m) (Suc k) ?j ?ni 0" by force
show ?thesis unfolding complete_R_step_simulation_def lk by (rule exI[of _ ?j], rule exI[of _ ?ni], rule exI[of _ ?σi], insert 1 2 3 lk, auto)
qed
lemma extend_complete_R_step_sim:
assumes sim:"complete_R_step_simulation ui m ρ" and step:"(ui m, ui (Suc m)) ∈ par_rstep UR"
shows "complete_R_step_simulation ui (Suc m) ρ"
proof-
let ?usteps = "λ m j σi. (∀i. 0 ≤ i ∧ i ≤ length (snd ρ) ⟶
j i < m ∧ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i))"
let ?isteps = "λ j ni. ∀i. 0 ≤ i ∧ i < length (snd ρ) ⟶
(ui (Suc (j i)), ui (j (Suc i))) ∈ par_urstep_below_root ^^ ni i"
let ?sum = "λ j ni. j 0 + sum_list (map (Suc ∘ ni) [0..<length (snd ρ)]) = j (length (snd ρ))"
from sim[unfolded complete_R_step_simulation_def] obtain j ni σi where sim: "?usteps m j σi" "?isteps j ni" "?sum j ni" by force
from sim(1) have 1:"?usteps (Suc m) j σi" by force
with sim show ?thesis unfolding complete_R_step_simulation_def by blast
qed
lemma first_root_step:
assumes ui:"∀i< n. (ui i, ui (Suc i)) ∈ par_rstep UR"
and root_step:"∃ i < n. ∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR"
and m0:"m0 = (LEAST i. i < n ∧ (∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR))"
and first:"sig_F (ui 0)"
shows "∃ ρ ∈ R. (∃ σ. (ui m0, ui (Suc m0)) ∈ rstep_r_p_s UR (lhs_n ρ 0,rhs_n ρ 0) ε σ)"
proof-
let ?root_step_at = "λi. i < n ∧ (∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR)"
have m0':"m0 < n ∧ (∃ l r σ. ui m0 = l ⋅ σ ∧ (ui (Suc m0)) = r ⋅ σ ∧ (l, r) ∈ UR)" unfolding m0
by (rule LeastI_ex, insert root_step, auto)
then obtain l r σ where m0':"m0 < n" "ui m0 = l ⋅ σ" "ui (Suc m0) = r ⋅ σ" "(l, r) ∈ UR" by auto
hence step:"(ui m0, ui (Suc m0)) ∈ rstep_r_p_s UR (l,r) ε σ" unfolding rstep_r_p_s_def by auto
{ assume "is_Var (ui 0)"
then obtain x where ui0:"ui 0 = Var x" by auto
{fix i
have "i ≤ m0 ⟹ ui i = Var x" proof(induct i, simp add:ui0)
case (Suc i)
hence uii:"ui i = Var x" by auto
from Suc have "i < m0" by auto
from not_less_Least[OF this[unfolded m0]] have rs:"¬ ?root_step_at i" by simp
from Suc m0' have "i < n" by auto
with ui[rule_format, OF this, unfolded par_rstep.simps[of "ui i"]] uii rs show ?case by force
qed
hence "i ≤ m0 ⟹ is_Var (ui i)" by auto
} note vars = this
from vars[OF le_refl] ur_step_exhaust[OF step] step have ?thesis by auto
} note var = this
{ assume "is_Fun (ui 0)"
then obtain f us where ui0:"ui 0 = Fun f us" by auto
{ fix j
assume "j ≤ m0"
hence "∃ vs. ui j = Fun f vs" proof(induct j, simp add:ui0)
case (Suc j)
then obtain ws where uii:"ui j = Fun f ws" by auto
from Suc have "j < m0" by auto
from not_less_Least[OF this[unfolded m0]] have rs:"¬ ?root_step_at j" by simp
from Suc m0' have "j < n" by auto
with ui[rule_format, OF this, unfolded par_rstep.simps[of "ui j"]] uii rs show ?case by force
qed
}
hence uim0:"∃ vs. ui m0 = Fun f vs" by simp
from ui0 first[unfolded sig_F_def] have "f ∈ F" by auto
with uim0 ur_step_exhaust[OF step] step have ?thesis by auto
}
with var show ?thesis by blast
qed
lemma Lemma_16:
assumes ui:"∀i< n. (ui i, ui (Suc i)) ∈ par_rstep UR"
and root_step:"∃ i < n. ∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR"
and first:"sig_F (ui 0)"
shows "∃ ρ k. ρ ∈ R ∧ (complete_R_step_simulation ui n ρ ∨ partial_R_step_simulation ui n ρ k)"
proof-
let ?ucstep = "∀ i l r σ. i < n ∧ ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR ⟶ ((l, r), []) ∉ R"
show ?thesis proof(cases ?ucstep)
case False
then obtain i l r σ where *:"i < n ∧ ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR ∧ ((l, r), []) ∈ R" by blast
hence **:"(ui i, ui (Suc i)) ∈ rstep_r_p_s UR (l, r) ε σ" unfolding rstep_r_p_s_def by simp
have "complete_R_step_simulation ui n ((l, r), [])" unfolding complete_R_step_simulation_def
by (rule exI[of _ "λj. i"], rule exI[of _"λj. 0"],rule exI[of _ "λj. σ"], insert * **, auto)
with * show?thesis by blast
next
case True
note root_step_not_R = this
let ?root_step_at = "λi. i < n ∧ (∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR)"
def n0 ≡ "LEAST i.?root_step_at i"
have "n0 < n ∧ (∃ l r σ. ui n0 = l ⋅ σ ∧ (ui (Suc n0)) = r ⋅ σ ∧ (l, r) ∈ UR)" unfolding n0_def
by (rule LeastI_ex, insert root_step, auto)
hence n0n:"n0 < n" by auto
let ?rule0_step = "λi. (n - i) < n ∧ (∃ρ∈R. ∃σ. (ui (n-i), ui (Suc (n-i))) ∈ rstep_r_p_s UR (lhs_n ρ 0, rhs_n ρ 0) ε σ)"
from first_root_step[OF ui root_step _ first] n0_def n0n have first_rule0_step:"?rule0_step (n - n0)" by auto
def mm0 ≡ "LEAST i. ?rule0_step i"
def m0 ≡ "n - mm0"
have " n - mm0 < n ∧ (∃ρ∈R. ∃σ. (ui (n-mm0), ui (Suc (n-mm0))) ∈ rstep_r_p_s UR (lhs_n ρ 0, rhs_n ρ 0) ε σ)" unfolding mm0_def
by (rule LeastI_ex, insert first_rule0_step, auto)
then obtain ρ0 σ1 where rhoR:"ρ0 ∈ R" and x:"n -mm0 < n""(ui (n-mm0), ui (Suc (n-mm0))) ∈ rstep_r_p_s UR (lhs_n ρ0 0, rhs_n ρ0 0) ε σ1" by blast
hence first_step:"(ui m0, ui (Suc m0)) ∈ rstep_r_p_s UR (lhs_n ρ0 0, rhs_n ρ0 0) ε σ1" unfolding m0_def by auto
from x have m0n:" m0 < n" unfolding m0_def by auto
{ fix j
assume a:"m0 < j" "j < n"
with m0n have "n - j < mm0" unfolding m0_def by linarith
from not_less_Least[of "n-j" ?rule0_step,OF this[unfolded mm0_def]] x(1) have "¬?rule0_step (n - j)" by blast
with a have "∀ρ∈R. ∀σ. (ui j, ui (Suc j)) ∉ rstep_r_p_s UR (lhs_n ρ 0, rhs_n ρ 0) ε σ" by simp
} note no_more_rule0 = this
let ?l = "lhs_n ρ0 0" and ?r = "rhs_n ρ0 0"
def l ≡ ?l
from first_step[unfolded rstep_r_p_s_def] have i:"ui m0 = ?l ⋅ σ1" "ui (Suc m0) = ?r ⋅ σ1" "(?l, ?r) ∈ UR" by auto
with root_step_not_R[rule_format, of m0] m0n have notR:"((?l,?r),[]) ∉ R" by blast
with lhs_n.simps(1) obtain rr cs where rho:"ρ0 = ((l,rr),cs)" unfolding l_def by (metis prod.collapse)
from notR[unfolded rhs_n.simps] rhoR rho have lcs:"0 < length cs" by fastforce
from lcs rho rhs_n.simps have r:"?r = (U ρ0 0)⟨fst (cs ! 0)⟩" by force
from U_cond[OF rhoR] lcs obtain U0 where U0:"U_fun ρ0 0 U0" unfolding rho by fastforce
with r i(2) obtain ts where uiSm0:"ui (Suc m0) = Fun U0 ts" by force
let ?uterm_at = "λρ n k. ∃ Uk ts. ui n = Fun Uk ts ∧ U_fun ρ k Uk ∧ k < length (snd ρ)"
let ?sim = "λρ n k. complete_R_step_simulation ui n ρ ∨ (partial_R_step_simulation ui n ρ k ∧ ?uterm_at ρ n k)"
{ fix m k Uk ts
let ?ustep = "λ ρ m j σi i. j i < m ∧ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i)"
let ?usteps = "λ ρ m k j σi. (∀i. 0 ≤ i ∧ i ≤ k ⟶ ?ustep ρ m j σi i)"
let ?istep = "λ j ni i. (ui (Suc (j i)), ui (j (Suc i))) ∈ par_urstep_below_root ^^ ni i"
let ?isteps = "λ k j ni. ∀i. 0 ≤ i ∧ i < k ⟶ ?istep j ni i"
let ?suffix = "λ m k j nm. (ui (Suc (j k)), ui m) ∈ par_urstep_below_root ^^ nm"
let ?sum = "λ m k j ni nm. j 0 + sum_list (map (Suc ∘ ni) [0..<k]) + Suc nm = m"
assume "m0 < m" and "m ≤ n"
hence "∃ρ k. ρ ∈ R ∧ ?sim ρ m k" proof (induct m)
case 0
thus ?case unfolding sig_F_def by simp
next
case (Suc m) note ih = this
show ?case proof (cases "m = m0")
case True
from uiSm0 lcs U0 have uterm:"?uterm_at ρ0 (Suc m) 0" unfolding True rho by simp
from first_step rhoR have 1:"?usteps ρ0 (Suc m) 0 (λi. m) (λi. σ1)" unfolding True by fastforce
have "?suffix (Suc m) 0 (λi. m) 0" by auto
with 1 i(3)[unfolded r] lcs have "partial_R_step_simulation ui (Suc m) ρ0 0" unfolding partial_R_step_simulation_def True rho by fastforce
with uterm rhoR show ?thesis by blast
next
case False
with Suc have lt:"m0 < m" and mn':"m ≤n" by auto
with Suc(1)[OF lt mn'] Suc(3) obtain ρ k where rhoR:"ρ ∈ R" and k:"?sim ρ m k" by blast
show ?thesis proof (cases "complete_R_step_simulation ui m ρ")
case True
from ui[rule_format, of m] Suc have "(ui m, ui (Suc m)) ∈ par_rstep UR" by auto
with extend_complete_R_step_sim[OF True this] rhoR show ?thesis by blast
next
case False
with k have part:"partial_R_step_simulation ui m ρ k" and uterm:"?uterm_at ρ m k" by auto
from part[unfolded partial_R_step_simulation_def] obtain j ni nm σi where
sim:"?usteps ρ m k j σi" "?isteps k j ni" "?suffix m k j nm" "?sum m k j ni nm" by blast
from uterm obtain Uk ts where Uk:"ui m = Fun Uk ts" "U_fun ρ k Uk" "k < length (snd ρ)" by auto
show ?thesis proof (cases "(ui m, ui (Suc m)) ∈ par_urstep_below_root")
case True
from this[unfolded par_urstep_below_root_def] Uk have uterm:"?uterm_at ρ (Suc m) k" by force
with extend_partial_R_step_sim[OF part True] rhoR show ?thesis by blast
next
case False
from ui[rule_format, of m] Suc have last_step:"(ui m, ui (Suc m)) ∈ par_rstep UR" by auto
from this[unfolded par_rstep.simps[of "ui m"]] False[unfolded par_urstep_below_root_def] obtain l r σk where
last_step':"ui m = l ⋅ σk" "ui (Suc m) = r ⋅ σk" "(l, r) ∈ UR" unfolding Uk by blast
hence last_step:"(ui m, ui (Suc m)) ∈ rstep_r_p_s UR (l,r) ε σk" unfolding rstep_r_p_s_def by auto
from Suc(3) have "m < n" by force
from no_more_rule0[OF lt this] last_step' rhoR have "¬(∃ρ∈R. (l, r) = (lhs_n ρ 0, rhs_n ρ 0))"
unfolding rstep_r_p_s_def by auto
with ur_step_urule[OF last_step[unfolded Uk] rhoR Uk(3) Uk(2)] have
"(∃ρ'. ρ' ∈ R ∧ prefix_equivalent ρ ρ' k ∧ U ρ k = U ρ' k ∧ (Fun Uk ts, ui (Suc m)) ∈ rstep_r_p_s UR (lhs_n ρ' (Suc k), rhs_n ρ' (Suc k)) ε σk)"
by blast
then obtain ρ' where rhoR':"ρ' ∈ R" and pe:"prefix_equivalent ρ ρ' k" and uks:"U ρ k = U ρ' k" and
lstep:"(Fun Uk ts, ui (Suc m)) ∈ rstep_r_p_s UR (lhs_n ρ' (Suc k), rhs_n ρ' (Suc k)) ε σk" by blast
from pe have krho':"k < length (snd ρ')" unfolding prefix_equivalent_def by blast
let ?ni = "λi. if i < k then ni i else nm"
let ?j = "λi. if i ≤ k then j i else m"
let ?σi = "λi. if i ≤ k then σi i else σk"
{ fix i
assume a:"0 ≤ i" "i ≤ Suc k"
have "?ustep ρ' (Suc m) ?j ?σi i"
proof(cases "i=Suc k")
case True
with lstep Uk(1) show ?thesis by auto
next
case False
with a sim(1) have ji:"j i < m" "(ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i)" by auto
with same_U_same_rules[OF rhoR rhoR' uks pe, rule_format, of i] a(2) False
have "(ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ' i, rhs_n ρ' i) ε (σi i)" by force
with ji(1) a False show ?thesis by auto
qed
} note 1 = this
{ fix i
assume a:"0 ≤ i" "i < Suc k"
have "?istep ?j ?ni i" by (cases "i = k", insert sim(2)[rule_format, of i] sim(3) a, auto)
} note 2 = this
have l:"(map (Suc ∘ ni) [0..<k]) @ [Suc nm] = map (Suc ∘ ?ni) [0..<Suc k]" by (induct k, auto)
have "sum_list (map (Suc ∘ ni) [0..<k]) + Suc nm = sum_list ((map (Suc ∘ ni) [0..<k]) @ [Suc nm])" by simp
from this[unfolded l] sim(4) have 3:"?sum (Suc m) (Suc k) ?j ?ni 0" by force
show ?thesis proof(cases "Suc k = length (snd ρ')")
case True
have "complete_R_step_simulation ui (Suc m) ρ'" unfolding complete_R_step_simulation_def
by (rule exI[of _ ?j], rule exI[of _ ?ni], rule exI[of _ ?σi], insert 1 2 3 True krho', auto)
with rhoR' show ?thesis by blast
next
case False
with krho' have kcs:"Suc k < length (snd ρ')" unfolding rho by auto
have 4:"?suffix (Suc m) (Suc k) ?j 0" by auto
from U_cond[OF rhoR'] kcs obtain Uk where Uk:"U_fun ρ' (Suc k) Uk" unfolding rho by fastforce
obtain lr' cs' where rho':"ρ' = (lr', cs')" by (cases ρ', auto)
from kcs Uk rhs_n.simps obtain ts' where r:"rhs_n ρ' (Suc k) = Fun Uk ts'" unfolding rho' by auto
with lstep obtain ts'' where "ui (Suc m) = Fun Uk ts''" unfolding rstep_r_p_s_def by force
with Uk kcs rho' have uterm:"?uterm_at ρ' (Suc m) (Suc k)" by simp
have "partial_R_step_simulation ui (Suc m) ρ' (Suc k)" unfolding partial_R_step_simulation_def
by (rule exI[of _ ?j], rule exI[of _ ?ni], rule exI[of _ 0], rule exI[of _ ?σi], insert 1 2 3 4 kcs rho, auto)
with uterm rhoR' show ?thesis by blast
qed
qed
qed
qed
qed
}
from this[OF m0n] show ?thesis by auto
qed
qed
lemma par_rstep_pow_imp_args_par_rstep_pow:
"(Fun f xs, Fun f ys) ∈ par_urstep_below_root ^^ n = ((∀i<length xs. (xs ! i, ys ! i) ∈ par_rstep UR ^^ n) ∧ length xs = length ys)"
proof
assume "(Fun f xs, Fun f ys) ∈ par_urstep_below_root ^^ n"
thus "((∀i<length xs. (xs ! i, ys ! i) ∈ par_rstep UR ^^ n) ∧ length xs = length ys)"
proof(induct n arbitrary:ys)
case 0
then show ?case unfolding par_urstep_below_root_def by auto
next
case (Suc n)
from relpow_Suc_E[OF Suc(2)] par_rstep_below_root_pow_same_root1 obtain zs where
steps:"(Fun f xs, Fun f zs) ∈ par_urstep_below_root ^^ n" "(Fun f zs, Fun f ys) ∈ par_urstep_below_root" by metis
from steps(1) par_rstep_below_root_pow_same_length have len:"length xs = length zs" by auto
from CollectD[OF steps(2)[unfolded par_urstep_below_root_def], unfolded split] have len':"length ys = length zs" by fastforce
{fix i
assume i:"i<length xs"
from Suc(1) steps(1) this have xs:"(xs ! i, zs ! i) ∈ par_rstep UR ^^ n" by auto
from CollectD[OF steps(2)[unfolded par_urstep_below_root_def], unfolded split] i[unfolded len]
have "(zs ! i, ys ! i) ∈ par_rstep UR" by fastforce
with xs have "(xs ! i, ys ! i) ∈ par_rstep UR ^^ (Suc n)" by auto
} with len len' show ?case by auto
qed
next
assume "(∀i<length xs. (xs ! i, ys ! i) ∈ par_rstep UR ^^ n) ∧ length xs = length ys"
thus "(Fun f xs, Fun f ys) ∈ par_urstep_below_root ^^ n"
proof(induct n arbitrary:ys)
case 0
hence "∀i<length xs. xs ! i = ys ! i" by simp
with 0 list_eq_iff_nth_eq have "xs = ys" by blast
with 0 show ?case unfolding par_urstep_below_root_def by simp
next
case (Suc n)
{fix i
assume i:"i<length xs"
from conjunct1[OF Suc(2), rule_format, OF i] relpow_Suc_E have
"∃z. (xs ! i, z) ∈ par_rstep UR ^^ n ∧ (z, ys ! i) ∈ par_rstep UR" by auto
}
then obtain fz where fz:"(∀i < length xs. (xs ! i, fz i) ∈ par_rstep UR ^^ n ∧ (fz i, ys ! i) ∈ par_rstep UR )" by metis
let ?zs = "map fz [0..<length xs]"
from Suc have len:"length ?zs = length ys" by simp
from fz have zs:"(∀i < length xs. (xs ! i, ?zs ! i) ∈ par_rstep UR ^^ n ∧ (?zs ! i, ys ! i) ∈ par_rstep UR)" by force
with Suc have n:"(Fun f xs, Fun f ?zs) ∈ par_urstep_below_root ^^ n" by fastforce
from zs len have "(Fun f ?zs, Fun f ys) ∈ par_urstep_below_root" unfolding par_urstep_below_root_def by force
with n show ?case by auto
qed
qed
lemma f_in_R_not_U_fun: "f ∈ F ⟹ ¬(∃ ρ i. ρ ∈ R ∧ i < length (snd ρ) ∧ U_fun ρ i f)"
proof
assume fR:"f ∈ F" and "∃ ρ i. ρ ∈ R ∧ i < length (snd ρ) ∧ U_fun ρ i f"
then obtain ρ i where a:"ρ ∈ R" "i < length (snd ρ)" "U_fun ρ i f" by auto
from U_cond[OF a(1-2)] a(3) have "f ∉ F" by force
with fR show False by auto
qed
abbreviation is_U_symbol :: "'f ⇒ bool"
where "is_U_symbol f ≡ (∃ ρ ∈ R. ∃ i < length (snd ρ). U_fun ρ i f)"
lemma sig_F_not_U:
assumes sR:"sig_F t" shows "¬(∃ Ui zs. is_U_symbol Ui ∧ (∃zs. t = Fun Ui zs))"
proof (cases t, simp)
case (Fun f us)
from sR[unfolded sig_F_def Fun] have "f ∈ F" by auto
from f_in_R_not_U_fun[OF this] Fun this show ?thesis by blast
qed
definition partial_aux :: "('f,'v) term ⇒ ('f,'v) term ⇒ (('f,'v) crule × nat) ⇒ bool"
where "partial_aux s t ρk ≡ ∃ σi τ1 τ2.
case ρk of (ρ,k) ⇒
k < length (snd ρ) ∧
(s = (lhs_n ρ 0) ⋅ τ1) ∧
(∃ti Uk. t = Fun Uk (ti # (map τ2 (Z ρ k))) ∧ U_fun ρ k Uk) ∧
(∀x ∈ vars_term (lhs_n ρ 0). (τ1 x,(σi 0) x) ∈ (par_rstep UR) ^*) ∧
(∀i. 0 ≤ i ∧ i < k ⟶ (∀x ∈ set (Z ρ i). (σi i x,(σi (Suc i)) x) ∈ (par_rstep UR) ^*)) ∧
(∀x ∈ set (Z ρ k). (σi k x, τ2 x) ∈ (par_rstep UR) ^*)"
lemma soundness_key_lemma:
assumes ll:"left_linear_trs UR"
and s:"sig_F s"
and t:"sig_F t" "linear_term t"
and seq:"(s,t⋅σ) ∈ (par_rstep UR) ^^ n"
shows "∃ θ. (s, t⋅θ) ∈ (cstep R)^* ∧ sig_F_subst θ (vars_term t) ∧
(∀ x ∈ vars_term t. (Var x⋅θ, Var x⋅σ) ∈ (par_rstep UR) ^^ n) ∧ (sig_F (t⋅σ) ⟶ t⋅θ = t⋅σ)
∧ (non_LV ∧ source_preserving R Z ∧ (∃ Ui zs. is_U_symbol Ui ∧ t⋅σ = Fun Ui zs) ⟶
(∃ ρ τ1 τ2 k u. ρ ∈ R ∧ k < length (snd ρ) ∧ t⋅θ = (clhs ρ)⋅τ1 ∧ t⋅σ = ((U ρ k) ⋅⇩c τ2)⟨u⟩ ∧ (∀x ∈ vars_term (clhs ρ). (τ1 x, τ2 x) ∈ (par_rstep UR)^*)))"
proof-
def t_U_cond ≡ "λ t θ σ. (non_LV ∧ source_preserving R Z ∧ (∃ Ui zs. is_U_symbol Ui ∧ (t ::('f,'v) term)⋅σ = Fun Ui zs)) ⟶
(∃ ρ τ1 τ2 k u. ρ ∈ R ∧ k < length (snd ρ) ∧ t⋅θ = (clhs ρ)⋅τ1 ∧ t⋅σ =((U ρ k) ⋅⇩c τ2)⟨u⟩ ∧ (∀x ∈ vars_term (clhs ρ). (τ1 x, τ2 x) ∈ (par_rstep UR)^*))"
let ?A = "λ n s t σ .sig_F s ∧ sig_F t ∧ linear_term t ∧ (s,t ⋅ σ) ∈ (par_rstep UR) ^^ n"
let ?G = "λ n s t σ . ∃ θ. (s, t⋅θ) ∈ (cstep R)^* ∧ sig_F_subst θ (vars_term t) ∧
(∀ x ∈ vars_term t. (Var x⋅θ, Var x⋅σ) ∈ (par_rstep UR) ^^ n) ∧ (sig_F (t⋅σ) ⟶ t⋅θ = t⋅σ) ∧ (t_U_cond t θ σ)"
let ?P = "λ (n,s). ∀ t σ. (?A n s t σ ⟶ ?G n s t σ)"
from sig_F_not_U have sig_F_not_U:"⋀t θ σ. sig_F (t⋅σ) ⟹ t_U_cond t θ σ" unfolding t_U_cond_def by fast
have "?P (n,s)" proof(induct rule: wf_induct[OF wf_measures, of "[fst, size ∘ snd]" ?P])
case (1 nt) note ind = this
obtain n s where ns: "nt = (n,s)" by force
show ?case unfolding ns split proof(rule, rule, rule)
fix t σ
assume a:"sig_F s ∧ sig_F t ∧ linear_term t ∧ (s, t ⋅ σ) ∈ par_rstep UR ^^ n"
hence sR:"sig_F s" and tR:"sig_F t" and lint:"linear_term t" and seq:"(s, t ⋅ σ) ∈ par_rstep UR ^^ n" by auto
{ assume eq:"s = t⋅σ"
hence 0:"(s, t⋅σ) ∈ (cstep R)^*" by auto
from a have t:"sig_F t" and s:"sig_F s" by auto
have 1:"sig_F_subst σ (vars_term t)" proof
fix x
assume xt:"x ∈ vars_term t"
hence "t ⋅ σ ⊵ Var x ⋅ σ" by (metis supteq_subst vars_term_supteq)
from supteq_imp_funs_term_subset [OF this] s[unfolded eq]
show "sig_F (σ x)" unfolding sig_F_def aux by auto
qed
from par_rstep_refl relpow_refl_mono[OF _ le0 relpow_0_I] have
2:"∀ x ∈ vars_term t. (Var x⋅σ, Var x⋅σ) ∈ (par_rstep UR) ^^ n" by metis
have "?G n s t σ" by (rule exI[of _ σ], insert 0 1 2 sig_F_not_U[OF sR[unfolded eq]], auto)
} note equal_terms = this
show "?G n s t σ" proof (cases n)
case 0
with a equal_terms show ?thesis by auto
next
case (Suc m) note Suc_m = this
from seq[unfolded Suc relpow_fun_conv] obtain ui where
ui:"ui 0 = s" "ui (Suc m) = t ⋅ σ" "∀i<Suc m. (ui i, ui (Suc i)) ∈ par_rstep UR" by blast
show ?thesis proof(cases "∃ i < Suc m. ∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR")
case False note no_root_step = this
show ?thesis proof (cases "∃x. s = Var x")
case True
then obtain x where sx:"s = Var x" by blast
{fix i
have "i ≤ Suc m ⟹ ui i = Var x" proof(induct i, insert ui(1) sx, simp)
case (Suc i)
hence ix:"ui i = Var x" by auto
from Suc have "i < Suc m" by auto
with ix ui(3)[rule_format, OF this, unfolded par_rstep.simps[of "ui i"], unfolded ix] no_root_step
show "ui (Suc i) = Var x" by fastforce
qed}
from this[OF order_refl] ui(2) sx have "s = t⋅σ" by auto
from equal_terms[OF this] show ?thesis by auto
next
case False note s_no_var = this
from no_root_step ui(1) have "¬ (∃ l r σ. s = l ⋅ σ ∧ (ui (Suc 0)) = r ⋅ σ ∧ (l, r) ∈ UR)" by auto
with s_no_var ui(3)[rule_format, OF zero_less_Suc, unfolded ui(1) par_rstep.simps[of s]]
obtain f ss where sf:"s = Fun f ss" by blast
let ?k = "length ss"
{fix i
let ?ps = "λ ts i. ∀x<length ts.(ss ! x, ts ! x) ∈ par_rstep UR ^^ i"
have "i ≤ Suc m ⟹ ∃ ts. ui i = Fun f ts ∧ ?ps ts i ∧ length ss = length ts"
proof(induct i)
case 0
from par_rstep_refl relpow_refl_mono[OF _ le0 relpow_0_I] have "?ps ss 0" by metis
with ui(1)[unfolded sf] exI[of _ ss] show ?case by blast
next
case (Suc i)
hence im:"i ≤ Suc m" "i < Suc m" by auto
from Suc(1)[OF this(1)] obtain ts where ih:"ui i = Fun f ts" "?ps ts i" "?k = length ts" by blast
from im no_root_step Suc have "¬ (∃ l r σ. ui i = l ⋅ σ ∧ (ui (Suc i)) = r ⋅ σ ∧ (l, r) ∈ UR)" by blast
with ih(1) ui(3)[rule_format, OF im(2), unfolded par_rstep.simps[of "ui i"]] s_no_var
obtain ts' where x:"ui (Suc i) = Fun f ts' ∧ (∀x<length ts'. (ts ! x, ts' ! x) ∈ par_rstep UR) ∧ length ts' = length ts" by force
from conjunct1[OF conjunct2[OF this]] ih(2) have "?ps ts' (Suc i)" by (metis relpow_Suc_I x)
with Suc ih(3) x show "∃ts. ui (Suc i) = Fun f ts ∧ ?ps ts (Suc i) ∧ ?k = length ts" by force
qed} note sequence_f_rooted = this
from sequence_f_rooted[OF order_refl] ui(2) obtain tss where tσ:"t ⋅ σ = Fun f tss" "length tss =?k" by auto
from nth_mem supt.arg have ssj:"⋀ j. j < length ss ⟹ s ⊳ ss ! j" unfolding sf by fast
from supt_size ssj have ms:"⋀ j. j < length ss ⟹((n,ss ! j), nt) ∈ measures [fst, size ∘ snd]" unfolding ns sf by force
show ?thesis proof (cases "∃ x. t = Var x")
case False note t_no_var = this
from t_no_var subst_apply_term.elims[OF tσ(1)] tσ(2) term.inject(2)[of f tss] obtain ts where t:"t = Fun f ts""length ts =?k"
by (metis length_map)
with tσ have sub:"∀x < ?k. tss ! x = ts ! x ⋅ σ" by auto
let ?θj_cond = "λ j θj. (ss ! j, (ts ! j)⋅θj) ∈ (cstep R)^* ∧ sig_F_subst θj (vars_term (ts ! j)) ∧
(∀ x ∈ vars_term (ts ! j). (Var x⋅θj, Var x⋅σ) ∈ (par_rstep UR) ^^ n) ∧
(sig_F ((ts ! j) ⋅σ) ⟶ (ts ! j)⋅θj = (ts ! j)⋅σ) ∧ (non_LV ⟶ t_U_cond (ts ! j) θj σ)"
let ?exj = "λ j. (∃ θj. ?θj_cond j θj)"
have "∀j<length ts. (?exj j)"
proof(rule, rule)
fix j
assume j:"j < length ts"
let ?tj = "ts ! j" and ?sj = "ss ! j"
from nth_mem[OF j] supt.arg have ttj:"t ⊳ ?tj" unfolding t by fast
from j lint[unfolded t] have lin:"linear_term ?tj" by force
from sR supteq_imp_funs_term_subset[OF supt_imp_supteq[OF ssj[OF j[unfolded t(2)]]]]
have sigs:"sig_F ?sj" unfolding sig_F_def by fast
from tR supteq_imp_funs_term_subset[OF supt_imp_supteq[OF ttj]]
have sigt:"sig_F ?tj" unfolding sig_F_def by fast
from sub sequence_f_rooted[OF order_refl] ui(2) term.inject(2)[of f tss] t(2) tσ(1) j
have step:"(?sj, ?tj ⋅ σ) ∈ par_rstep UR ^^ Suc m" by force
from ind[rule_format, OF ms[OF j[unfolded t(2)]], unfolded split, rule_format] sigs sigt lin step Suc
show "?exj j" by blast
qed
from this[unfolded choice_iff'] obtain θf where θcond:"∀j<length ts. (?θj_cond j (θf j))" by fast
let ?θs = "map θf [0..<length ts]" and ?vs = "map vars_term ts"
from lint[unfolded t linear_term.simps(2)] have p:"is_partition ?vs" by auto
let ?θ = "fun_merge ?θs ?vs"
have xequiv:"⋀ j x . j < length ts ⟹ x ∈ vars_term (ts ! j) ⟹ ?θ x = (θf j) x" unfolding length_upt
proof-
fix j x
assume j:"j < length ts" and x:"x ∈ vars_term (ts ! j)"
with j have xt:"x ∈ vars_term t" unfolding t(1) by fastforce
with fun_merge_part[OF p, unfolded length_map, OF j, unfolded nth_map[OF j], OF x, of ?θs, unfolded nth_map[OF j]
nth_map[of _ "[0..<length ts]", unfolded length_upt minus_nat.diff_0, OF j]
nth_upt[of 0 j, unfolded add_0, OF j] in_subst_restrict[OF x]]
show "?θ x = (θf j) x" unfolding in_subst_restrict[OF xt] by blast
qed
from term_subst_eq this have equiv:"⋀ j. j < length ts ⟹ (ts ! j) ⋅ ?θ = (ts ! j) ⋅ (θf j)" unfolding length_upt
proof-
fix j
assume "j < length ts"
from term_subst_eq[of "ts ! j" ?θ "θf j", OF xequiv[OF this]] show "(ts ! j) ⋅ ?θ = (ts ! j) ⋅ (θf j)" by fast
qed
let ?θts = "map (λ t. t⋅?θ) ts"
from t(2) have len:"length ss = length ?θts" unfolding length_map by auto
have "∀j<length ss. (ss ! j, ?θts ! j) ∈ (cstep R)⇧*"
proof(rule,rule)
fix j
assume j:"j < length ss"
with t(2) have j:"j < length ts" by auto
from θcond[rule_format, OF j] equiv[OF j] have "(ss ! j, ts ! j ⋅ θf j) ∈ (cstep R)⇧*" by blast
with equiv[OF j] show "(ss ! j, ?θts ! j) ∈ (cstep R)⇧*" unfolding nth_map[OF j] by fastforce
qed
from args_steps_imp_steps[OF cstep_ctxt_closed len this]
have 0:"(s, t⋅?θ) ∈ (cstep R)^*" unfolding sf t by force
have 12:"∀ x ∈ (vars_term t). (Var x⋅?θ, Var x⋅σ) ∈ (par_rstep UR) ^^ n ∧ sig_F (?θ x)"
proof
fix x
assume xt:"x ∈ vars_term t"
from var_imp_var_of_arg[OF this[unfolded t(1)]] obtain j where j:"j < length ts" "x ∈ vars_term (ts ! j)" by force
from θcond[rule_format, OF j(1)] j(2) xequiv[OF j(1) j(2)] show "(Var x⋅?θ, Var x⋅σ) ∈ (par_rstep UR) ^^ n ∧ sig_F (?θ x)" by auto
qed
{assume tR:"sig_F (t ⋅σ)"
{ fix j
assume j':"j < length ts"
with tσ(2) t(2) have j:"j < length tss" by auto
from tR[unfolded tσ] supteq_imp_funs_term_subset[OF supt_imp_supteq, OF supt.arg[OF nth_mem[OF j]]] have
"sig_F (tss ! j)" unfolding sig_F_def by fast
with θcond[rule_format, OF j'] sub[rule_format,OF j'[unfolded t(2)]] equiv[OF j']
have "ts ! j ⋅?θ = ts ! j ⋅ σ" by presburger
}
with nth_map_conv[OF refl, of ts] t(2) have "t⋅?θ = t⋅σ" unfolding t(1) subst_apply_term.simps(2) term.simps(2)
by (metis (poly_guards_query, lifting))
} note 3 = this
from f_in_R_not_U_fun[of f] tR[unfolded sig_F_def t] t have 4:"t_U_cond t ?θ σ" unfolding t_U_cond_def by force
show ?thesis by (rule exI[of _ ?θ], insert 0 12 3 4, auto)
next
assume "∃x. t = Var x"
with tσ obtain x where x:"t = Var x""σ x = Fun f tss" by force
let ?xs = "dvars (length tss)"
from distinct_vars[of "length tss"] have fresh:"distinct ?xs""length ?xs = length tss" by auto
let ?τ = "mk_subst Var (zip ?xs tss)"
{ fix j assume "j < length tss"
from mk_subst_distinct[OF fresh(1), unfolded fresh(2), OF refl this] have "?τ (?xs ! j) = tss ! j" by fast
} note τequiv = this
with fresh(2) nth_map have
tσ':"t⋅σ = Fun f (map ?τ ?xs)" unfolding tσ term.inject(2)[of f tss] list_eq_iff_nth_eq length_map by simp
let ?θj_cond = "λ j θj. (ss ! j, θj (?xs ! j)) ∈ (cstep R)^* ∧ sig_F_subst θj {?xs ! j} ∧
(θj (?xs ! j), tss ! j) ∈ (par_rstep UR) ^^ n ∧ (sig_F (tss ! j) ⟶ θj (?xs ! j) = tss ! j)
∧ (non_LV ⟶ t_U_cond (Var (?xs ! j)) θj ?τ)"
let ?exj = "λ j. (∃ θj. ?θj_cond j θj)"
{ fix j
assume j:"j < length tss"
let ?sj = "ss ! j"
let ?x = "?xs ! j"
from τequiv[OF j] sequence_f_rooted[OF order_refl, unfolded ui(2)] tσ term.inject(2)[of f tss] j have
0:"(ss ! j,?τ ?x) ∈ par_rstep UR ^^ Suc m" by simp
have 1:"linear_term (Var ?x)" by simp
from sR supteq_imp_funs_term_subset[OF supt_imp_supteq[OF ssj[OF j[unfolded tσ(2)]]]]
have 2:"sig_F ?sj""sig_F (Var ?x)" unfolding sig_F_def by auto
from ind[rule_format, OF ms[OF j[unfolded tσ(2)]], unfolded split, rule_format, of "Var ?x" ?τ] 0 1 2 have "?exj j"
unfolding term.simps Ball_def singleton_iff simp_thms(41) subst_apply_term.simps(1) Suc τequiv[OF j] by blast
}
hence "∀ j < length tss. ?exj j" by auto
from this[unfolded choice_iff'] obtain θf where θcond:"∀j<length tss. (?θj_cond j (θf j))" by presburger
let ?θs = "map θf [0..<length tss]" and ?vs = "map (λ x. {x}) ?xs"
have p:"is_partition ?vs" unfolding is_partition_def length_map fresh(2)
proof(rule, rule, rule, rule)
fix i j
assume j:"j < length tss" and i:"i < j"
hence i':"i < length tss" by auto
from i fresh(1)[unfolded distinct_conv_nth, rule_format, unfolded fresh(2), OF j i'] have "?xs ! i ≠ ?xs ! j" by auto
thus "map (λx. {x}) ?xs ! i ∩ map (λx. {x}) ?xs ! j = {}"
unfolding nth_map[of i ?xs, unfolded fresh(2), OF i'] nth_map[of j ?xs, unfolded fresh(2), OF j] by fast
qed
def θ' ≡ "fun_merge ?θs ?vs"
have xequiv:"⋀ j. j < length tss ⟹ θ' (?xs ! j) = (θf j) (?xs ! j)"
proof-
fix j
assume j:"j < length tss"
from fun_merge_part[OF p, unfolded length_map fresh(2), OF j, unfolded nth_map[of _ ?xs, unfolded fresh(2), OF j] singleton_iff, of _ ?θs,
unfolded nth_map[of _ "[0..<length tss]", unfolded length_upt minus_nat.diff_0, OF j]] nth_upt[of 0 j, unfolded add_0, OF j]
show "θ'(?xs ! j) = (θf j) (?xs ! j)" unfolding θ'_def by auto
qed
let ?θts = "map θ' ?xs"
from tσ(2) fresh(2) have len:"length ss = length ?θts" unfolding length_map by auto
have "∀j<length ss. (ss ! j, ?θts ! j) ∈ (cstep R)⇧*"
proof(rule,rule)
fix j
assume "j < length ss"
with tσ(2) have j:"j < length tss" by auto
from θcond[rule_format, OF j, unfolded xequiv[OF j, symmetric]]
show "(ss ! j, ?θts ! j) ∈ (cstep R)⇧*" unfolding nth_map[of j ?xs, unfolded fresh(2), OF j] by blast
qed
from args_steps_imp_steps[OF cstep_ctxt_closed len this]
have 0:"(s, Fun f ?θts) ∈ (cstep R)^*" unfolding sf t by force
let ?θ = "subst x (Fun f ?θts)"
have z:"Var x ⋅ ?θ = Fun f ?θts" by auto
from 0 have 0:"(s, Var x ⋅ ?θ) ∈ (cstep R)^*" by fastforce
{ fix j
assume j:"j < length tss"
with fresh(2) have j':"j < length ?xs" by auto
from θcond[rule_format, OF j] xequiv[OF j]
have "(?θts ! j, tss ! j) ∈ (par_rstep UR) ^^ n ∧ sig_F (?θts ! j)" unfolding nth_map[OF j'] by simp
} note aux = this
hence "∀ j < length tss.(?θts ! j, tss ! j) ∈ (par_rstep UR) ^^ n" by auto
with args_par_rstep_pow_imp_par_rstep_pow[of ?θts "map ?τ ?xs", unfolded length_map fresh(2)]
have 1:"(Var x⋅?θ, Var x⋅σ) ∈ (par_rstep UR) ^^ n" unfolding z tσ'[unfolded x]
by (metis term.inject(2) tσ' tσ(1))
from a[unfolded sf sig_F_def] term.simps(16) have fR:"{f} ⊆ F " by fast
from aux len tσ(2) have aux':"∀ j < length ?θts. sig_F (?θts ! j)" by presburger
from this[unfolded all_set_conv_all_nth[symmetric, of ?θts sig_F]] fR
sig_F_def have 2:"sig_F (Var x ⋅ ?θ)" unfolding subst_simps(2) z by auto
{
assume tR:"sig_F (σ x)"
{ fix j
assume j:"j < length tss"
from tR[unfolded x[symmetric] tσ, unfolded tσ[unfolded x, unfolded subst_apply_term.simps(1)]]
supteq_imp_funs_term_subset[OF supt_imp_supteq, OF supt.arg[OF nth_mem[OF j]]] have
"sig_F (tss ! j)" unfolding sig_F_def by fast
with θcond[rule_format, OF j, unfolded τequiv[OF j]] xequiv[OF j] have "θ' (?xs ! j) = tss ! j" by auto
}
with fresh(2) have "(Fun f (map θ' ?xs)) = t⋅σ"
unfolding tσ(1) subst_apply_term.simps(2) term.simps(2) by (metis map_nth_eq_conv)
with x have "(Fun f (map θ' ?xs)) = Var x ⋅σ" by auto
} note 3 = this
from f_in_R_not_U_fun[of f] x fR have 4:"t_U_cond (Var x) ?θ σ" unfolding sig_F_def t_U_cond_def by force
show ?thesis unfolding x term.simps(17) by (rule exI[of _ ?θ], insert 0 1 2 3 4, simp)
qed
qed
next
case True note there_is_root_step = this
from all_ctxt_closed_relpow[OF all_ctxt_closed_par_rstep] have acc:"⋀ i. all_ctxt_closed UNIV (par_rstep UR ^^ i)" by auto
from relpow_refl_mono[of "par_rstep UR"] par_rstep_refl have
par_rstep_mono:"⋀ m n a b. m ≤ n ⟹ (a, b) ∈ par_rstep UR ^^ m ⟹ (a, b) ∈ par_rstep UR ^^ n" by blast
from Lemma_16[OF ui(3) there_is_root_step sR[unfolded ui(1)[symmetric]]]
have "∃ ρ k. ρ ∈ R ∧ (complete_R_step_simulation ui (Suc m) ρ ∨ partial_R_step_simulation ui (Suc m) ρ k)" by auto
then obtain ρ k where sim:"ρ ∈ R"
"complete_R_step_simulation ui (Suc m) ρ ∨ partial_R_step_simulation ui (Suc m) ρ k" (is "?complete ∨ ?partial") by blast
obtain l rr cs where rho:"ρ = ((l,rr), cs)" by (cases ρ, auto)
let ?ustep = "λ s t k σ . (s, t) ∈ rstep_r_p_s UR (lhs_n ρ k, rhs_n ρ k) ε σ"
let ?usteps' = "λ ji. (∀x. ∃σ. 0 ≤ x ∧ x ≤ length cs ⟶ ?ustep (ui (ji x)) (ui (Suc (ji x))) x σ)"
let ?usteps = "λ cs σi ji. (∀x. 0 ≤ x ∧ x ≤ length cs ⟶ ?ustep (ui (ji x)) (ui (Suc (ji x))) x (σi x))"
let ?isteps = "λ cs ji ni. ∀k. 0 ≤ k ∧ k < length cs ⟶ (ui (Suc (ji k)), ui (ji (Suc k))) ∈ par_urstep_below_root ^^ ni k"
let ?domi = "λi. case i of 0 ⇒ vars_term l | Suc j ⇒ vars_term (ti ρ j) ∪ XY ρ j"
let ?result = "λ m0 σ1 θ1. (s, l ⋅ θ1) ∈ (cstep R)⇧* ∧ sig_F_subst θ1 (vars_term l) ∧
(∀x∈vars_term l ∪ set (Z ρ 0). (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0) ∧ (sig_F (l ⋅ σ1) ⟶ l ⋅ θ1 = l ⋅ σ1) ∧
sig_F_subst θ1 (?domi 0) ∧ (non_LV ⟶ t_U_cond l θ1 σ1)"
{ fix m0 r σ1
assume i:"m0 < Suc m" "ui m0 = l ⋅ σ1" "ui (Suc m0) = (rhs_n ρ 0) ⋅ σ1"
from ui(3) i(1) have "∀ i' < m0. (ui i', ui (Suc i')) ∈ par_rstep UR" by auto
with ui(1) i(2) have 1:"(s, l ⋅ σ1) ∈ par_rstep UR ^^ m0" unfolding relpow_fun_conv by blast
from sim(1) rho rules_def have "∃r'. (l,r') ∈ rules ρ" unfolding rules_def by force
then obtain r' where " (l,r') ∈ rules ρ" by blast
with ll[unfolded left_linear_trs_def, rule_format, of "(l,r')"] sim(1) have 2:"linear_term l"
unfolding left_linear_trs_def rho UR_def by blast
from sig_F_l[OF sim(1)] have 3:"sig_F l" unfolding rho by force
from i(1) ns Suc_m have "((m0, s), nt) ∈ measures [fst, size ∘ snd]" unfolding ns by auto
from ind[rule_format, OF this, unfolded split, rule_format, of l σ1] 1 2 3 sR obtain θ1 where
theta1:"(s, l ⋅ θ1) ∈ (cstep R)⇧*" "sig_F_subst θ1 (vars_term l)" "(∀x∈vars_term l. (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0)"
"(sig_F (l ⋅ σ1) ⟶ l ⋅ θ1 = l ⋅ σ1)" "non_LV ⟶ t_U_cond l θ1 σ1"
by blast
let ?θ1 = "λx. if x ∈ vars_term l then θ1 x else Var x ⋅ σ1"
have lθ:"∀x∈vars_term l. ?θ1 x = θ1 x" by fastforce
from theta1(2) l_vars_X0_vars[OF sim(1)] sim(2) rho have substR1:"sig_F_subst ?θ1 (?domi 0)" by auto
from theta1(1) lθ[unfolded term_subst_eq_conv[symmetric]] have 1:"(s, l ⋅ ?θ1) ∈ (cstep R)⇧*" by simp
from theta1(2) lθ have 2:"sig_F_subst ?θ1 (vars_term l)" by force
{ fix x assume "x ∈ vars_term l ∪ set (Z ρ 0)"
with theta1(3) lθ par_rstep_mono[OF le0] have " (Var x ⋅ ?θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0" by auto
} note 4 = this
{ assume nlv:non_LV
from rho lhs_n.simps(1) have "lhs_n ρ 0 = l" by force
with nlv[unfolded non_LV_def UR_def] rules_def sim(1)[unfolded rho] have "is_Fun l" by fastforce
then obtain f zs where "l = Fun f zs" by auto
with f_in_R_not_U_fun[of f] 3[unfolded sig_F_def] have "t_U_cond l ?θ1 σ1" unfolding t_U_cond_def by force
} note 5 = this
note facts = theta1 lθ lθ[unfolded term_subst_eq_conv[symmetric]] 4 5
have "∃ θ1. ?result m0 σ1 θ1" by (rule exI[of _ ?θ1], insert facts, simp)
} note prefix = this
show ?thesis proof(cases "?complete")
case True
note complete = this
let ?theta_prop_with = "λ σ m s t θ' i. (s, t ⋅ θ') ∈ (cstep R)⇧* ∧ (sig_F_subst θ' (vars_term t ∩ ?domi i)) ∧
(∀x∈vars_term t. (Var x ⋅ θ', Var x ⋅ σ) ∈ par_rstep UR ^^ m)"
let ?theta_prop_with' = "λ σ m s t θ' i. (s, t ⋅ θ') ∈ (cstep R)⇧* ∧ (sig_F_subst θ' (vars_term t)) ∧
(∀x∈vars_term t. (Var x ⋅ θ', Var x ⋅ σ) ∈ par_rstep UR ^^ m) ∧ (sig_F (t ⋅ σ) ⟶ t ⋅ θ' = t ⋅ σ) ∧ t_U_cond t θ' σ"
have up2r:"∃θ j0. (s, rr ⋅ θ) ∈ (cstep R)⇧+ ∧ sig_F (rr ⋅ θ) ∧ (rr ⋅ θ, ui (Suc j0)) ∈ par_rstep UR ^^ j0 ∧ j0 ≤ m"
proof (cases "length cs = 0")
case True
with complete[unfolded complete_R_step_simulation_def rho snd_conv] rho obtain j0 σ0 where
j0:"j0 < Suc m" "(ui j0, ui (Suc j0)) ∈ rstep_r_p_s UR (l, rr) ε σ0" by auto
hence lr:"ui j0 = l ⋅ σ0" "ui (Suc j0) = rr ⋅ σ0" unfolding rstep_r_p_s_def by (simp,simp)
from prefix[OF j0(1) lr(1), unfolded rho] rhs_n.simps True lr(2) obtain θ1 where
cs:"(s, l ⋅ θ1) ∈ (cstep R)⇧*" " sig_F_subst θ1 (vars_term l)" "∀x∈vars_term l. (Var x ⋅ θ1, Var x ⋅ σ0) ∈ par_rstep UR ^^ j0" by auto
have "(l⋅θ1, rr⋅θ1) ∈ (cstep_n R (Suc 0))"
by (rule cstep_n_SucI[of l rr "[]" _ _ _ _ Hole], insert True sim(1) rho, auto)
from this cstep_iff rtrancl_into_trancl1[OF cs(1), of "rr⋅θ1"] have 1:"(s, rr ⋅ θ1) ∈ (cstep R)⇧+" by fast
from type3[unfolded type3_def, rule_format, OF sim(1)] True
have vs:"vars_term rr ⊆ vars_term l" unfolding vars_trs_def rho by auto
with cs(3) have "∀x∈vars_term rr. (Var x ⋅ θ1, Var x ⋅ σ0) ∈ par_rstep UR ^^ j0" by auto
with all_ctxt_closed_subst_step[OF acc] lr(2) have 2:"(rr ⋅ θ1, ui (Suc j0)) ∈ par_rstep UR ^^ j0" by simp
from cs(2) vs have "(∀x∈vars_term rr. sig_F (θ1 x))" by auto
with sim(1) funs_crule_def[of ρ, unfolded funs_rule_def] F have 3:"sig_F (rr⋅θ1)"
unfolding sig_F_def funs_term_subst funs_ctrs_def rho by auto
show ?thesis by (rule exI[of _ θ1], insert 1 2 3 j0(1), auto)
next
case False
let ?sum = "λ cs j ni. j 0 + sum_list (map (Suc ∘ ni) [0..< (length cs)]) = j (length (snd ρ))"
let ?ji = "λ cs ji. (∀x. 0 ≤ x ∧ x ≤ length cs ⟶ ji x < Suc m)"
let ?ustep' = "λ j σi i. j i < Suc m ∧ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i)"
let ?usteps' = "λ j σi. (∀i. 0 ≤ i ∧ i ≤ length cs ⟶ ?ustep' j σi i)"
from complete[unfolded complete_R_step_simulation_def] obtain ji ni σi where
dec:"?usteps' ji σi" "?isteps cs ji ni" "?sum cs ji ni" unfolding rho by force
hence dec:"?ji cs ji" "?usteps cs σi ji" "?isteps cs ji ni" "?sum cs ji ni" by (blast, auto)
def m0 ≡ "ji 0" def n0 ≡ "ni 0" def σ1 ≡ "σi 0"
from dec(2)[rule_format, of 0] have step:"(ui m0, ui (Suc m0)) ∈ rstep_r_p_s UR (lhs_n ρ 0, rhs_n ρ 0) ε σ1" unfolding m0_def σ1_def by auto
from this[unfolded rstep_r_p_s_def] have uim0:"ui m0 = l ⋅ σ1" "ui (Suc m0) = (rhs_n ρ 0) ⋅ σ1" unfolding rho lhs_n.simps(1) by (force,force)
from uim0 False rho have u1:"ui (Suc m0) = (U ρ 0)⟨si ρ 0⟩ ⋅ σ1" by auto
from U_cond[OF sim(1), of 0] False rho obtain U0 where U0:"U_fun ρ 0 U0" by auto
from dec(1)[rule_format, of 0] have m0m:"m0 < Suc m" unfolding m0_def by simp
from prefix[OF this uim0] obtain θ1 where theta1:"?result m0 σ1 θ1" by presburger
from dctrs[unfolded dctrs_def, rule_format, OF sim(1), of 0] False rho l_vars_X0_vars[OF sim(1)] sim
have vs0:"vars_term (si ρ 0) ⊆ vars_term l" by simp
with theta1 have "⋀ x. x ∈ vars_term (si ρ 0) ⟹ (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0" by auto
with all_ctxt_closed_subst_step[OF acc] have sstep:"(si ρ 0 ⋅ θ1, si ρ 0 ⋅ σ1) ∈ par_rstep UR ^^ m0" by fastforce
from theta1 have substR1:"sig_F_subst θ1 (?domi 0)" by auto
from theta1 have theta1:"(s, l ⋅ θ1) ∈ (cstep R)⇧*" "sig_F_subst θ1 (vars_term l)"
"(∀x∈ set (Z ρ 0). (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0)" "(sig_F (l ⋅ σ1) ⟶ l ⋅ θ1 = l ⋅ σ1)" by (fast+)
from dec(1) rho have j_last:"ji (length (snd ρ)) < Suc m" by auto
let ?mi = "λ i. ji 0 + sum_list (map ni [0..< i])"
let ?θcond = "λ θs cs cs'. (length θs = Suc (length cs) ∧ (θs ! 0 = θ1) ∧(∀ i < Suc (length cs). sig_F_subst (θs ! i) (?domi i)) ∧
(s, l ⋅ (θs ! 0)) ∈ (cstep R)⇧* ∧
(∀ i < length cs. (si ρ i ⋅ (θs ! i), ti ρ i ⋅ (θs ! (Suc i))) ∈ (cstep R)⇧*) ∧
(∀ i < length cs. ∀ j < length (Z ρ i) . (((θs ! i) (Z ρ i ! j), (θs ! Suc i) (Z ρ i ! j)) ∈ (cstep R)^*) ∧
((θs ! Suc i) (Z ρ i ! j), (σi (Suc i)) (Z ρ i ! j)) ∈ par_rstep UR ^^ ?mi (Suc i)) ∧
(∀ i < length cs. (∀x∈vars_term (ti ρ i). ((θs ! Suc i) x, (σi (Suc i)) x) ∈ par_rstep UR ^^ ?mi (Suc i))))"
let ?theta_prop = "λ s t θ' i. ?theta_prop_with (σi i) (?mi i) s t θ' i"
{ fix cs cs'
assume "ρ = ((l,rr),cs @ cs')" "?ji cs ji" "?usteps cs σi ji" "?isteps cs ji ni"
"?sum (cs @ cs') ji ni"
hence "∃ θs. ?θcond θs cs cs'"
proof(induct "length cs" arbitrary:cs cs')
case 0
from 0(1) 0(2) False rho have l:"length cs' > 0" by simp
show ?case by (rule exI[of _ "[θ1]"], insert 0 l theta1, simp)
next
case (Suc k)
note Suck=this
note U_cond = U_cond[OF sim(1), unfolded Suc(3) snd_conv]
note inR = sim(1) and rho = Suc(3)
from Suc(2) Suc(3) have kl:"k < length cs" by auto
hence kl':"k < length (cs @ cs')" by auto
from U_cond[OF kl'] rho obtain Uk where Uk:"U_fun ρ k Uk" unfolding Suc(3) snd_conv by blast
let ?cs = "butlast cs" and ?cs' = "last cs # cs'"
from append_butlast_last_id[of cs] Suc(2) have app:"cs @ cs' = ?cs @ ?cs'" by fastforce
from length_butlast[of cs] Suc(2) have 0:"length ?cs = k" by auto
from Suc(3) app have 2:"ρ = ((l,rr), ?cs @ ?cs')" unfolding rho by force
from Suc(4) have 3:"?ji ?cs ji" by force
from Suc(5) have 4:"?usteps ?cs σi ji" by force
from Suc(6) have 5:"?isteps ?cs ji ni" by force
from Suc(7) app have 6:"?sum (?cs @ ?cs') ji ni" by simp
from Suc(1)[OF 0[symmetric] 2 3 4 5 6] obtain θs' where θs':"?θcond θs' ?cs ?cs'" by auto
let ?k = "Suc k"
let ?θk = "λ x. case k of 0 ⇒ (θs' ! k) x | Suc m ⇒ if x ∈ ?domi k ∪ set (Z ρ m) then (θs' ! k) x else (σi k) x"
note θ1=conjunct1[OF conjunct2[OF θs']]
have thetak:"⋀t m. k = Suc m ⟹ vars_term t ⊆ ?domi k ∪ set (Z ρ m) ⟹ t ⋅ (θs' ! k) = t ⋅ ?θk"
by (cases k, insert term_subst_eq[of _ "θs' ! k" ?θk] nat.case(2), fastforce+)
from vars_si_subset_ti_XY[OF inR] rho Suc(2) have
vs:"⋀m. k = Suc m ⟹ vars_term (si ρ k) ⊆ vars_term (ti ρ m) ∪ XY ρ m" by simp
from θs' 0 have vt:"⋀m. k = Suc m ⟹∀x∈vars_term (ti ρ m). (?θk x, σi k x) ∈ par_rstep UR ^^ ?mi k" by auto
from θs' 0 have vz':"⋀m. k = Suc m ⟹ ∀j < length (Z ρ m). (?θk (Z ρ m ! j), σi k (Z ρ m ! j)) ∈ par_rstep UR ^^ ?mi k" by auto
hence vz:"⋀m. k = Suc m ⟹ ∀z ∈ set (Z ρ m). (?θk z, σi k z) ∈ par_rstep UR ^^ ?mi k" unfolding all_set_conv_all_nth by blast
from X_Y_imp_Z[OF inR] Suc(2) Suc(3) rho have xyz:"⋀m. k = Suc m ⟹ XY ρ m ⊆ set (Z ρ m)" by force
have si_k_steps:"((si ρ k) ⋅ ?θk,(si ρ k) ⋅ (σi k)) ∈ par_rstep UR ^^ ?mi k"
proof (cases k)
case 0
from θ1 sstep show ?thesis unfolding σ1_def 0 nat.case m0_def by simp
next
case (Suc m) note k = this
let ?σk = "σi (Suc m)"
from vs[OF k] vt[OF k] vz[OF k] 0 xyz[OF k] have "∀x∈vars_term (si ρ k). (?θk x, σi k x) ∈ par_rstep UR ^^ ?mi k" unfolding k by fast
from this all_ctxt_closed_subst_step[OF acc] show ?thesis by fast
qed
from kl Suc(5)[rule_format, of k] have x:"(ui (ji k), ui (Suc (ji k))) ∈ rstep_r_p_s UR (lhs_n ρ k, rhs_n ρ k) ε (σi k)" by auto
from rhs_n.simps[of _ "cs @ cs'" k] Suc(2) have "rhs_n ρ k = (U ρ k)⟨si ρ k⟩" unfolding rho by simp
with x[unfolded rho ] rho rstep_r_p_s_def Suc(2) have
u1:"ui (Suc (ji k)) = (U ρ k)⟨si ρ k⟩ ⋅ (σi k)" by force
from Suc(2) Suc(5)[rule_format, of "?k"] have
"(ui (ji ?k), ui (Suc (ji ?k))) ∈ rstep_r_p_s UR (lhs_n ρ ?k, rhs_n ρ ?k) ε (σi ?k)" by force
from this[unfolded rho lhs_n.simps(2)] rstep_r_p_s_def rho have
u2:" ui (ji ?k) = (U ρ k)⟨ti ρ k⟩ ⋅ (σi ?k)" by force
from u1 u2 kl Suc(6)[rule_format, of k] have
u:"((U ρ k)⟨si ρ k⟩ ⋅ (σi k),(U ρ k)⟨ti ρ k⟩ ⋅ (σi ?k)) ∈ par_urstep_below_root ^^ ni k" by auto
from this[unfolded Uk ctxt_apply_term.simps append_Nil] par_urstep_below_root_def par_rstep_pow_imp_args_par_rstep_pow
have si_k_steps':"(si ρ k ⋅ (σi k), ti ρ k ⋅ (σi ?k)) ∈ par_rstep UR ^^ ni k" by auto
from kl have sum:"?mi ?k = ?mi k + ni k" by simp
from si_k_steps si_k_steps' relpow_add have
step:"((si ρ k) ⋅ ?θk, ti ρ k ⋅ (σi ?k)) ∈ par_rstep UR ^^ ?mi ?k" unfolding sum by fast
from sig_F_si[OF inR] kl rho have sig_F:"sig_F (si ρ k)" by auto
note sigRs = conjunct1[OF conjunct2[OF conjunct2[OF θs']]]
from vs have 1:"sig_F ((si ρ k) ⋅ ?θk)" proof (cases k)
case 0
from vs0 theta1(2) sig_F show ?thesis unfolding 0 nat.case θ1 sig_F_def funs_term_subst by blast
next
case (Suc m)
from vs[OF Suc] have vs:"vars_term (si ρ k) ⊆ ?domi k" unfolding Suc by simp
from term_subst_eq[of _ "θs' ! k" ?θk] have thetak:"⋀t. vars_term t ⊆ ?domi k ∪ set (Z ρ m) ⟹ t ⋅ (θs' ! k) = t ⋅ ?θk"
unfolding Suc nat.case(2) by fastforce
with sigRs[ rule_format, of k] vs have eq:"si ρ k ⋅ θs' ! Suc m = si ρ (Suc m) ⋅ ?θk" unfolding 0 Suc by blast
from sigRs[ rule_format, of k] vs
have "⋀x. x ∈ vars_term (si ρ k) ⟹ sig_F ((θs' ! Suc m) x)" unfolding 0 Suc by blast
with vs sig_F show ?thesis unfolding sig_F_def funs_term_subst 0 Suc nat.case(2) by fastforce
qed
from linear_term_ti[OF ll inR, unfolded rho, simplified] kl rho have 2:"linear_term (ti ρ k)" by simp
from sig_F_ti[OF inR] kl rho have 3:"sig_F (ti ρ k)" by auto
have "⋀j. Suc 0 ≤ j ∧ j < Suc k ⟹ ni j ≤ (Suc ∘ ni) j" by force
have "sum_list (map ni [0..<Suc k]) < sum_list (map (Suc ∘ ni) [0..<Suc k])" by (induct k, auto)
with Suc(7) have m':"?mi ?k < ji (length (snd ρ))" unfolding length_append Suc(2)[symmetric]
upt_add_eq_append[OF le0] map_append sum_list_append by linarith
with j_last have m:"((?mi ?k, si ρ k ⋅ ?θk), nt) ∈ measures [fst, size ∘ snd]" unfolding ns Suc_m by auto
from ind[rule_format, OF m, unfolded split, rule_format] 1 2 3 step obtain θ' where
θ':"?theta_prop (si ρ k ⋅ ?θk) (ti ρ k) θ' ?k" by blast
from X_Y_imp_Z[OF inR] Suc(2) rho have xyz':"XY ρ k ⊆ set (Z ρ k)" by force
{ fix j
assume jl:"j < length (Z ρ k)"
let ?z = "(Z ρ k) ! j"
from set_conv_nth jl have zZ:"?z ∈ set (Z ρ k)" by auto
from u[unfolded Uk ctxt_apply_term.simps append_Nil subst_apply_term.simps(2)] par_rstep_pow_imp_args_par_rstep_pow
have "(∀i< length (Z ρ k). (map (σi k) (Z ρ k) ! i, map (σi ?k) (Z ρ k) ! i) ∈ par_rstep UR ^^ ni k)" by auto
from this[rule_format, OF jl] nth_map[of j] jl have z_step:"((σi k) ?z, σi ?k ?z) ∈ par_rstep UR ^^ ni k" by force
from m' j_last have m:"((?mi ?k, ?θk ?z), nt) ∈ measures [fst, size ∘ snd]" unfolding ns Suc_m by auto
have "∃ θz. ?theta_prop (?θk ?z) (Var ?z) θz ?k" proof (cases k)
case 0
from theta1(3)[rule_format, of ?z] jl have i:"(Var ?z ⋅ θ1, Var ?z ⋅ σ1) ∈ par_rstep UR ^^ m0"
unfolding set_conv_nth 0 by blast
from Suc(6)[rule_format, of 0] Suc(2)
have m0_step:"((U ρ 0)⟨si ρ 0⟩ ⋅ σ1, (U ρ 0)⟨ti ρ 0⟩ ⋅ (σi (Suc 0))) ∈ par_urstep_below_root ^^ n0"
unfolding 0 n0_def m0_def u1[unfolded m0_def 0] u2[unfolded 0] σ1_def by fastforce
from m0_step[unfolded U0 ctxt_apply_term.simps(2)] iffD1[OF par_rstep_pow_imp_args_par_rstep_pow] jl
have "(Var ?z ⋅ σ1, Var ?z ⋅ (σi (Suc 0))) ∈ par_rstep UR ^^ n0" unfolding 0 by fastforce
with i have steps:"(Var ?z ⋅ θ1, Var ?z ⋅ (σi (Suc 0))) ∈ par_rstep UR ^^ (m0 + n0)" unfolding relpow_add by blast
show ?thesis proof (cases "?z ∈ XY ρ 0" )
case True
with l_vars_X0_vars[OF inR] Suc(2) rho have "?z ∈ vars_term l" unfolding 0 by force
with jl theta1(2) have 1:"sig_F (θ1 ?z)" unfolding sig_F_def funs_term_subst by force
have 2:"linear_term (Var ?z)" and 3:"sig_F (Var ?z)" unfolding sig_F_def by auto
have m0n0:"?mi (Suc 0) = m0 + n0" unfolding Suc(2)[symmetric] m0_def n0_def by simp
note m0 = m[unfolded 0 nat.case θ1 m0n0]
from ind[rule_format, OF m, unfolded split, rule_format, of "Var ?z" "σi (Suc 0)"] steps 1 2 3
show ?thesis unfolding 0 nat.case m0n0 θ1 by force
next
case False
from Z_ti_disjoint[OF inR _ ll, of 0] kl rho jl have "vars_term (ti ρ 0) ∩ set (Z ρ 0) = {}" unfolding 0 by force
from this[unfolded set_conv_nth] jl have ti:"?z ∉ vars_term (ti ρ 0)" unfolding 0 by blast
with False have ti:"Z ρ 0 ! j ∉ (vars_term (ti ρ 0) ∪ (X_vars ρ 0 ∩ Y_vars ρ 0))" unfolding 0 by blast
show ?thesis unfolding 0 nat.case by (rule exI[of _ ?θk, unfolded 0 nat.case], insert steps[unfolded 0 m0_def n0_def] ti θ1, auto)
qed
next
case (Suc m) note k = this
with kl have ml:"m < length cs + length cs'" by auto
show ?thesis proof(cases "?z ∈ vars_term (ti ρ m) ∪ XY ρ m")
case True
with xyz[OF Suc] vz[OF k] vt[OF k] have "(?θk ?z, σi k ?z) ∈ par_rstep UR ^^ ?mi k" by blast
with z_step relpow_add have step:"(?θk ?z, σi ?k ?z) ∈ par_rstep UR ^^ ?mi ?k" unfolding sum by fast
have sig_F:"sig_F (Var ?z)" unfolding sig_F_def by simp
from U_cond[unfolded rho snd_conv length_append, OF ml] ml rho obtain Um where
Um:"U_fun ρ m Um" unfolding k by blast
from True xyz have "?z ∈ vars_term (U ρ m)⟨ti ρ m⟩" unfolding k Um ctxt_apply_term.simps by auto
with sig_F sigRs[rule_format, of k] xyz True
have 1:"sig_F (?θk ?z)" unfolding sig_F_def funs_term_subst 0 k by simp
from m' j_last have m:"((?mi ?k, ?θk ?z), nt) ∈ measures [fst, size ∘ snd]" unfolding ns Suc_m by auto
from ind[rule_format, OF m, unfolded split, rule_format, of "Var ?z" "σi ?k"] 1 sig_F step show ?thesis by auto
next
case False note dom = this
with XYi_subset_ti_XY[OF inR, of m] k rho Suck(2) have mem:"?z ∉ XY ρ (Suc m)" by auto
from Z_ti_disjoint[OF inR _ ll, of k] Suck(2) rho zZ have "?z ∉ vars_term (ti ρ (Suc m))" unfolding k by auto
with mem have sig:"sig_F_subst ?θk ({?z} ∩ ?domi (Suc k))" unfolding k by simp
show ?thesis proof (cases "?z ∈ set (Z ρ m)")
case True
from vz[OF k, rule_format, OF True] have "(?θk ?z, σi k ?z) ∈ par_rstep UR ^^ ?mi k" unfolding k by blast
with z_step relpow_add have steps:"(?θk ?z, σi (Suc k) ?z) ∈ par_rstep UR ^^ ?mi ?k" unfolding sum by fast
show ?thesis by (rule exI[of _ ?θk], insert sig True steps, auto)
next
case False
with dom have eq:"?θk ?z = σi k ?z" unfolding k nat.case(2) by auto
with par_rstep_mono[of 0 "?mi k"] have steps:"(?θk ?z, σi k ?z) ∈ par_rstep UR ^^ ?mi k" unfolding k by simp
with z_step relpow_add have steps:"(?θk ?z, σi (Suc k) ?z) ∈ par_rstep UR ^^ ?mi ?k" unfolding sum by fast
from sig steps dom False eq k have " ?theta_prop (?θk ?z) (Var ?z) ?θk ?k" unfolding k nat.case(2) by auto
thus ?thesis unfolding k nat.case by blast
qed
qed
qed
} with choice[of "λ j θz. j < length (Z ρ k) ⟶ ?theta_prop (?θk ((Z ρ k) ! j)) (Var ((Z ρ k) ! j)) θz ?k"]
obtain θz where zsteps:"∀j < length (Z ρ k). ?theta_prop (?θk ((Z ρ k) ! j)) (Var ((Z ρ k) ! j)) (θz j) ?k" by auto
let ?θs = "θ' # map θz [0..<length (Z ρ k)]" and ?vs = "vars_term (ti ρ k) # map (λ z. {z}) (Z ρ k)"
from Z_part'[OF inR _ ll, of k] Suc(2) rho have p:"is_partition ?vs" by auto
have l0:"0 < length ?vs" by auto
def θSk ≡ "fun_merge ?θs ?vs"
from fun_merge_part[OF p l0, of _ ?θs] have vt:"⋀x. x ∈ vars_term (ti ρ k) ⟹ θ' x = θSk x" unfolding θSk_def by fastforce
with θ' term_subst_eq[of "ti ρ k" θ' θSk, OF this] have st_prop:"?theta_prop (si ρ k ⋅ ?θk) (ti ρ k) θSk ?k" by simp
{ fix j
let ?z = "(Z ρ k) ! j"
assume j:"j < length (Z ρ k)"
hence j':"Suc j < length ?vs" by auto
with j have jth:"?vs ! (Suc j) = {?z}" by simp
from fun_merge_part[OF p j', unfolded jth, of _ ?θs] j have z:"θz j ?z = θSk ?z" "Var ?z ⋅ (θz j) = θSk ?z" unfolding θSk_def by auto
have aux:"⋀P. ∀x∈{Z ρ 0 ! j}.P x = P (Z ρ 0 ! j)" by fast
have p:"?theta_prop (?θk ?z) (Var ?z) θSk ?k" proof (cases k)
case 0 from zsteps[rule_format, OF j] z show ?thesis unfolding 0 nat.case subst_apply_term.simps term.set z by force
next
case (Suc m) from zsteps[rule_format, OF j] z show ?thesis unfolding Suc nat.case subst_apply_term.simps term.set z by force
qed
} note z_prop = this
def θs ≡ "butlast θs' @ (?θk # [θSk])"
from θs' 0 Suc(2) have f1:"length θs = Suc ?k" unfolding θs_def by auto
with 0 Suc(2) last_snoc last_conv_nth[of θs] have last:"θs ! ?k = θSk" unfolding θs_def by fastforce
from conjunct1[OF θs'] 0 nth_append_length have lb:"length (butlast θs') = k" by auto
from nth_append_length[of "butlast θs'"] have butlast:"θs ! k = ?θk" unfolding θs_def lb by blast
from nth_append[of "butlast θs'"] nth_butlast[of _ "θs'"] have nth:"⋀i. i < k ⟹ θs' ! i = θs ! i" unfolding θs_def lb by simp
from f1 0 have aux:"⋀P. P ?θk θSk k ⟹ (∀ i < k. P (θs ! i) (θs ! Suc i) i) ⟹ ∀i< ?k. P (θs ! i) (θs ! (Suc i)) i"
unfolding butlast[symmetric] last[symmetric] by (metis less_Suc_eq)
from f1 0 have aux':"⋀P m. k = Suc m ⟹ P (θs ! m) ?θk m ⟹ (∀ i < m. P (θs ! i) (θs ! Suc i) i) ⟹ ∀i< k. P (θs ! i) (θs ! (Suc i)) i"
unfolding butlast[symmetric] last[symmetric] by (metis less_Suc_eq)
with aux have aux':"⋀P m. k = Suc m ⟹ P ?θk θSk k ⟹ P (θs ! m) ?θk m ⟹ (∀ i < m. P (θs ! i) (θs ! Suc i) i) ⟹ ∀i< ?k. P (θs ! i) (θs ! (Suc i)) i"
unfolding butlast[symmetric] last[symmetric] by metis
{ fix i
assume i:"i < Suc ?k"
have a1:"vars_term ((U ρ k)⟨ti ρ k⟩) = vars_term (ti ρ k) ∪ set (Z ρ k)" unfolding Uk by simp
from z_prop xyz' have "sig_F_subst θSk (XY ρ k)" unfolding set_conv_nth[of "Z ρ k"] by auto
with st_prop a1 have 1:"sig_F_subst (θs ! ?k) (?domi ?k)" unfolding True last nat.case(2) by blast
from sigRs[rule_format, of k] vs0 have 2:"sig_F_subst (θs ! k) (?domi k)"
unfolding butlast unfolding nat.case(2) 0 by (cases k, auto)
{ assume "i < k"
with conjunct1[OF conjunct2[OF conjunct2[OF θs']], rule_format, unfolded 0, of i] nth
have "sig_F_subst (θs ! i) (?domi i)" by force
} note less = this
from i have "i < k ∨ i = k ∨ i = ?k" by linarith
with less 1 2 have "sig_F_subst (θs ! i) (?domi i)" by blast
} note f2 = this
from θs' have st:"∀i<k. (si ρ i ⋅ θs' ! i, ti ρ i ⋅ θs' ! Suc i) ∈ (cstep R)⇧*" unfolding 0 by auto
have f4:"∀i < ?k. (si ρ i ⋅ θs ! i, ti ρ i ⋅ θs ! Suc i) ∈ (cstep R)⇧*" proof(cases k)
case 0
from conjunct1[OF st_prop[unfolded 0 nat.case]] last butlast show ?thesis unfolding 0 by auto
next
case (Suc m) note k = this
from st[rule_format, of m, unfolded k, OF lessI] thetak[of m "ti ρ m"] have f41:"(si ρ m ⋅ θs ! m, ti ρ m ⋅ ?θk) ∈ (cstep R)⇧*"
unfolding 0 k nat.case unfolding nth[unfolded k, OF lessI] by fastforce
{ fix i assume "i < m"
with st[rule_format, of i] nth have "(si ρ i ⋅ θs ! i, ti ρ i ⋅ θs ! Suc i) ∈ (cstep R)⇧*" unfolding 0 k by simp
} note f43 = this
show ?thesis by (rule aux', insert f41 st_prop f43 k, auto)
qed
from θs' have "(s, l ⋅ θs' ! 0) ∈ (cstep R)⇧*" by auto
with nth[of 0] butlast have f3:"(s, l ⋅ θs ! 0) ∈ (cstep R)⇧*" by (cases k, auto)
{ fix i j
assume i:"i< ?k" and j:"j < length (Z ρ i)"
let ?z = "Z ρ i ! j"
have "(((θs ! i) ?z, (θs ! Suc i) ?z) ∈ (cstep R)⇧* ∧
((θs ! Suc i) ?z, σi (Suc i) ?z) ∈ par_rstep UR ^^ ?mi (Suc i))"
proof (cases "i = k")
case True
from z_prop[OF j[unfolded True]] show ?thesis unfolding True last butlast by auto
next
case False note ltk = this
with i not0_implies_Suc[of k] obtain m where k:"k=Suc m" by fastforce
show ?thesis proof (cases "i = m")
case False
with ltk i have im:"i < m" "Suc i < k" "i < k" unfolding k by auto
with θs' j i have "((θs' ! i) ?z, (θs' ! Suc i) ?z) ∈ (cstep R)⇧* ∧ ((θs' ! Suc i) ?z, σi (Suc i) ?z) ∈ par_rstep UR ^^ ?mi (Suc i)" unfolding 0 by auto
with conjunct1[OF θs', unfolded 0] nth[OF im(2)] nth[OF im(3)] show ?thesis unfolding k by simp
next
case True
with nth have x1:"θs' ! i = θs ! i" unfolding k by auto
from thetak[OF k, of "Var ?z"] j have x2:"Var ?z ⋅ θs' ! k = Var ?z ⋅ ?θk" unfolding set_conv_nth k True by fastforce
from θs' j i have "((θs' ! i) ?z, (θs' ! Suc i) ?z) ∈ (cstep R)⇧* ∧ ((θs' ! Suc i) ?z, σi (Suc i) ?z) ∈ par_rstep UR ^^ ?mi (Suc i)" unfolding 0 True k by auto
from this[unfolded x1] x2 j butlast show ?thesis unfolding True k by simp
qed
qed
} note f5 = this
{ fix i
assume i:"i < ?k"
have "∀x∈vars_term (ti ρ i). ((θs ! Suc i) x, σi (Suc i) x) ∈ par_rstep UR ^^ ?mi (Suc i)"
proof(cases "i = k")
case True
from st_prop last show ?thesis unfolding True by simp
next
case False note f1 = this
with i gr0_implies_Suc[of k] obtain m where k:"k = Suc m" by blast
show ?thesis proof(cases "i = m")
case True
from θs' have "∀x∈vars_term (ti ρ m). ((θs' ! k) x, σi k x) ∈ par_rstep UR ^^ ?mi k" unfolding 0 True k by blast
with butlast thetak show ?thesis unfolding k True by force
next
case False
with i f1 have im:"i < m" unfolding k by auto
with θs' have "∀x∈vars_term (ti ρ i). ((θs' ! (Suc i)) x, σi (Suc i) x) ∈ par_rstep UR ^^ ?mi (Suc i)" unfolding 0 True k by auto
with nth im show ?thesis unfolding k True by force
qed
qed
} note f6 = this
from θs' nth butlast have f7:"θs ! 0 = θ1" by (cases k, auto)
from f1 f2 f3 f4 f5 f6 f7 have c:"?θcond θs cs cs'" unfolding Suc(2)[symmetric] by auto
show "∃ θs. ?θcond θs cs cs'" by (rule exI[of _ θs], insert c, auto)
qed
} note key = this
from False rho have lcs:"0 < length cs" by auto
from key[of cs "[]", unfolded append_Nil2, OF rho dec(1) dec(2) dec(3) dec(4)] obtain θs where θs:"?θcond θs cs []" by presburger
let ?k = "length (snd ρ)"
from θs rho have 1:"∀i < ?k. ∀z∈set (Z ρ i). (Var z ⋅ θs ! i, Var z ⋅ θs ! Suc i) ∈ (cstep R)⇧*" unfolding all_set_conv_all_nth by auto
with Lemma_17[OF sim(1) ll, of θs] lcs 1 rho θs have "(l ⋅ θs ! 0, rr ⋅ θs ! ?k) ∈ (cstep R)⇧+" by auto
with θs have ssteps:"(s, rr ⋅ θs ! length (snd ρ)) ∈ (cstep R)⇧+" by auto
from lcs gr0_conv_Suc rho obtain k' where k:"?k = Suc k'""length cs = Suc k'" unfolding rho by auto
from U_cond[unfolded rho snd_conv length_append, OF sim(1), of k'] rho lcs obtain Uk where
Uk:"U_fun ρ k' Uk" unfolding k by force
hence vs:"vars_term (U ρ k')⟨ti ρ k'⟩ = vars_term (ti ρ k') ∪ set (Z ρ k')" by auto
from sig_F_r[OF sim(1)] have sig_F_r:"sig_F rr" unfolding rho by force
from X_Y_imp_Z[OF sim(1), of k'] k rho have xyz:"XY ρ k' ⊆ set (Z ρ k')" by force
with vars_r_subset_tk_Z[OF sim(1)[unfolded rho] lcs] rho k have
vr:"vars_term rr ⊆ vars_term (ti ρ k') ∪ set (Z ρ k')" by auto
from θs have z_steps:"∀j<length (Z ρ k'). ((θs ! ?k) (Z ρ k' ! j), σi ?k (Z ρ k' ! j)) ∈ par_rstep UR ^^ ?mi ?k" unfolding k by blast
from θs have t_steps:"∀x∈vars_term (ti ρ k'). ((θs ! ?k) x, σi ?k x) ∈ par_rstep UR ^^ ?mi ?k" unfolding k by blast
with vr z_steps have "∀x∈vars_term rr. ((θs ! ?k) x, σi ?k x) ∈ par_rstep UR ^^ ?mi ?k" unfolding set_conv_nth by blast
with all_ctxt_closed_subst_step[OF acc] have rsteps:"(rr ⋅ (θs ! ?k), rr ⋅ (σi ?k)) ∈ par_rstep UR ^^ ?mi ?k" by fast
note sig_r = conjunct1[OF conjunct2[OF conjunct2[OF θs]]]
from sig_r[ rule_format, of "length cs", OF lessI] lcs rho vars_r_subset_tk_Z[OF sim(1)[unfolded rho] lcs] Uk
have "⋀x. x ∈ vars_term rr ⟹ sig_F ((θs ! ?k) x)" unfolding k by auto
with sig_F_r have 11:"sig_F (rr ⋅ θs ! ?k)" unfolding sig_F_def funs_term_subst by blast
from dec(2)[rule_format, of ?k, unfolded k] rhs_n.simps[of "(l,rr)" cs "Suc k'"] have usq_r:"ui (Suc (ji (Suc k'))) = rr ⋅ (σi ?k)"
unfolding k rho rstep_r_p_s_def ctxt_of_pos_term.simps Let_def ctxt_apply_term.simps snd_conv by auto
let ?j = "ji ?k"
from dec(2)[rule_format, of ?k] have
last_step:"(ui ?j, ui (Suc ?j)) ∈ rstep_r_p_s UR (lhs_n ρ ?k, rhs_n ρ ?k) ε (σi ?k)" unfolding rho by fastforce
from ui(3) j_last have aux:"∀i<Suc m - Suc ?j. (ui (i + Suc ?j), ui (Suc i + Suc ?j)) ∈ par_rstep UR" by simp
from last_step have usq_j:"ui (Suc ?j) = rr ⋅ (σi ?k)" unfolding rstep_r_p_s_def rho rhs_n.simps by simp
have ls:"sum_list (map (Suc ∘ ni) [0..<Suc k']) > sum_list (map ni [0..<Suc k'])" by (induct k', auto)
with dec(4) j_last k have m':"?mi ?k ≤ ?j" unfolding rho by simp
from rsteps par_rstep_mono[OF this] usq_j have rsteps':"(rr ⋅ (θs ! ?k), ui (Suc ?j)) ∈ par_rstep UR ^^ ?j" by auto
from dec(1)[rule_format, of ?k] have jm:"?j ≤ m" unfolding rho by auto
show ?thesis by(rule exI[of _ "θs ! ?k"], rule exI[of _ "?j"], insert ssteps 11 rsteps' jm, auto)
qed
then obtain θ' m' where up2r:"(s, rr ⋅ θ') ∈ (cstep R)⇧+" "sig_F (rr ⋅ θ')"
"(rr ⋅ θ', ui (Suc m')) ∈ par_rstep UR ^^ m'" "m' ≤ m" by auto
have "(ui (Suc m'), ui (Suc m)) ∈ par_rstep UR ^^ (Suc m - (Suc m'))" unfolding relpow_fun_conv
by (rule exI[of _ "λ i. ui (i + Suc m')"], insert up2r(4) ui(3), auto)
with ui(2) have steps:"(ui (Suc m'), t ⋅ σ) ∈ par_rstep UR ^^ (Suc m - Suc m')" by fastforce
let ?m = "m' + (Suc m - Suc m')"
from steps up2r(3) have steps:"(rr ⋅ θ', t ⋅ σ) ∈ par_rstep UR ^^ ?m" unfolding relpow_add by fastforce
from up2r(4) have m':"?m = m" by linarith
hence m:"((m, rr ⋅ θ'), nt) ∈ measures [fst, size ∘ snd]" unfolding ns Suc_m by auto
from up2r(2) tR lint steps ind[rule_format, OF m, unfolded split, rule_format, of t σ] obtain θ where
θ:"?theta_prop_with' σ ?m (rr ⋅ θ') t θ ?k" unfolding m' by blast
with m' par_rstep_mono[of ?m n]
have 1:"∀x∈vars_term t. (Var x ⋅ θ, Var x ⋅ σ) ∈ par_rstep UR ^^ n" unfolding Suc_m by simp
from θ up2r(1) have 2:"(s, t⋅ θ) ∈ (cstep R)⇧*" by force
show ?thesis by (rule exI[of _ θ], insert θ 1 2, auto)
next
case False
with sim have part:"?partial" by auto
let ?sum = "λ k j ni nm. j 0 + sum_list (map (Suc ∘ ni) [0..< k]) + Suc nm = Suc m"
let ?ji = "λ k ji. (∀x. 0 ≤ x ∧ x ≤ k ⟶ ji x < Suc m)"
let ?ustep' = "λ j σi i. j i < Suc m ∧ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i)"
let ?usteps' = "λ k j σi. (∀i. 0 ≤ i ∧ i ≤ k ⟶ ?ustep' j σi i)"
let ?usteps = "λ k j σi. ∀i. 0 ≤ i ∧ i ≤ k ⟶ (ui (j i), ui (Suc (j i))) ∈ rstep_r_p_s UR (lhs_n ρ i, rhs_n ρ i) ε (σi i)"
let ?isteps = "λ k ji ni. ∀i. 0 ≤ i ∧ i < k ⟶ (ui (Suc (ji i)), ui (ji (Suc i))) ∈ par_urstep_below_root ^^ ni i"
let ?suffix = "λ k j nm. (ui (Suc (j k)), ui (Suc m)) ∈ par_urstep_below_root ^^ nm"
from part[unfolded partial_R_step_simulation_def] obtain ji ni σi nm where
"k < length cs" "?usteps' k ji σi" "?isteps k ji ni" "?suffix k ji nm" "?sum k ji ni nm" unfolding rho by force
hence dec:"k < length cs" "?ji k ji" "?usteps k ji σi" "?isteps k ji ni" "?suffix k ji nm" "?sum k ji ni nm" by (blast, auto)
def m0 ≡ "ji 0" def σ1 ≡ "σi 0"
from dec(3)[rule_format, of 0] have uim0:"ui m0 = l ⋅ σ1" "ui (Suc m0) = (rhs_n ρ 0) ⋅ σ1"
unfolding m0_def σ1_def rho rstep_r_p_s_def lhs_n.simps(1) by (force,force)
from dec(2) have m0m:"m0 < Suc m" unfolding m0_def by auto
from prefix[OF this uim0] obtain θ1 where theta1:"?result m0 σ1 θ1" by presburger
hence vars:"∀x∈vars_term l ∪ set (Z ρ 0). (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0"
and substR1:"sig_F_subst θ1 (?domi 0)" by auto
from dec(1) rho have lpos:"0 < length (snd ρ)" by auto
from dctrs[unfolded dctrs_def, rule_format, OF sim(1) lpos] rho l_vars_X0_vars[OF sim(1) lpos] sim
have vs:"vars_term (si ρ 0) ⊆ vars_term l" by simp
with vs vars have "⋀ x. x ∈ vars_term (si ρ 0) ⟹ (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0" by auto
with all_ctxt_closed_subst_step[OF acc] have sstep:"(si ρ 0 ⋅ θ1, si ρ 0 ⋅ σ1) ∈ par_rstep UR ^^ m0" by fastforce
from theta1[unfolded nat.case(1)] have theta1:"(s, l ⋅ θ1) ∈ (cstep R)⇧*" "sig_F_subst θ1 (vars_term l)"
"(∀x∈vars_term l. (Var x ⋅ θ1, Var x ⋅ σ1) ∈ par_rstep UR ^^ m0)" "(sig_F (l ⋅ σ1) ⟶ l ⋅ θ1 = l ⋅ σ1)" by (fast+)
from sig_F_l[OF sim(1)] have 3:"sig_F l" unfolding rho by force
from U_cond[OF sim(1), of k] dec(1) obtain Uk where Uk:"U_fun ρ k Uk" "Uk ∉ F" unfolding rho by auto
from dec(3)[rule_format, of k, unfolded rstep_r_p_s_def rho rhs_n.simps] dec(1) Uk
obtain ts where Uk_last:"ui (Suc (ji k)) = Fun Uk ts" unfolding rho by force
from dec(5)[unfolded this] par_rstep_below_root_pow_same_root1 obtain ys where Uk':"ui (Suc m) = Fun Uk ys" by blast
from Uk(2) ui(2)[unfolded this] tR[unfolded sig_F_def] funs_term_subst[of t σ] obtain x where tx:"t = Var x" by (cases t, auto)
with Uk Uk' ui(2) have 4:"¬ sig_F (σ x)" unfolding sig_F_def by force
let ?θ = "λ x. l ⋅ θ1"
from theta1(3) all_ctxt_closed_subst_step[OF acc] have lsteps:"(l ⋅ θ1, l ⋅ σ1) ∈ par_rstep UR ^^ m0" by simp
have "(ui m0, ui (Suc m)) ∈ par_rstep UR ^^ (Suc m - m0)" unfolding relpow_fun_conv
by (rule exI[of _ "λ i. ui (i + m0)"], insert ui(3) m0m, auto)
from this[unfolded uim0 ui(2) tx] have "(l ⋅ σ1, σ x) ∈ par_rstep UR ^^ (Suc m - m0)" by force
with lsteps m0m relpow_add[of m0 "Suc m - m0" "par_rstep UR"]
have steps:"(t ⋅ ?θ, σ x) ∈ par_rstep UR ^^ n" unfolding Suc tx by auto
from theta1(1) tx have 1:"(s, t ⋅ ?θ) ∈ (cstep R)⇧*" by force
from sig_F_subst[OF theta1(2) 3] have 2:"sig_F_subst ?θ (vars_term t)" unfolding tx by blast
{ assume nlv:"non_LV" and zd:"source_preserving R Z"
have 1:"t⋅?θ = (clhs ρ)⋅θ1" unfolding tx rho by auto
def τ2 ≡ "mk_subst Var (zip (Z ρ k) (tl ys))"
let ?v = "Fun Uk (si ρ k # (map Var (Z ρ k))) ⋅ (σi k)"
from dec(3)[rule_format, of k, unfolded rstep_r_p_s_def] a have t':"ui (Suc (ji k)) = rhs_n ρ k ⋅ (σi k)" by simp
from Uk t'[unfolded rho rhs_n.simps] a rho dec(1) have t':"ui (Suc (ji k)) = ?v" by auto
from Z[unfolded Z_vars_def] sim(1) dec(1) rho have d:"distinct (Z ρ k)" by force
from dec(5)[unfolded t' Uk' subst_apply_term.simps par_rstep_pow_imp_args_par_rstep_pow length_map] have
"length (si ρ k # map Var (Z ρ k)) = length ys" by simp
hence ll:"length (tl ys) = length (Z ρ k)" and lys: "length ys > 0" by auto
with mk_subst_distinct[OF d this(1)] have tys:"tl ys = map (λt. t ⋅ τ2) (map Var (Z ρ k))"
unfolding list_eq_iff_nth_eq τ2_def by force
from tys lys have 2:"t⋅σ =((U ρ k) ⋅⇩c τ2)⟨hd ys⟩"
unfolding Uk subst_apply_ctxt.simps ctxt_apply_term.simps Uk'[unfolded ui(2)] list.map append_Nil tys[symmetric] by auto
have 3:"∀x ∈ vars_term (clhs ρ). (θ1 x, τ2 x) ∈ (par_rstep UR)^*"
proof
fix x
assume xl:"x ∈ vars_term (clhs ρ)"
with rho have xl:"x ∈ vars_term l" by simp
with vars relpow_imp_rtrancl have s0:"(Var x ⋅ θ1, Var x ⋅ σ1) ∈ (par_rstep UR) ^*" by blast
{ fix i
assume ik:"i ≤ k"
hence "(Var x ⋅ θ1, Var x ⋅ (σi i)) ∈ (par_rstep UR) ^*" proof(induct i)
case 0
from s0 show ?case unfolding σ1_def by auto
next
case (Suc i)
hence *:"(Var x ⋅ θ1, Var x ⋅ σi i) ∈ (par_rstep UR)⇧*" by auto
from Suc have i:"Suc i < length cs" using dec(1) by auto
from zd[unfolded source_preserving_def, rule_format, OF sim(1), of i] Suc(2) xl dec(1) have "x ∈ set (Z ρ i)"
unfolding rho by force
from this[unfolded set_conv_nth] obtain j where xj:"x = (Z ρ i) ! j" "j < length (Z ρ i)" by blast
from U_cond[OF sim(1), of i] i obtain Ui where Ui:"U_fun ρ i Ui" unfolding rho by auto
from U_cond[OF sim(1), of "Suc i"] i obtain USi where USi:"U_fun ρ (Suc i) USi" unfolding rho by auto
from dec(3)[rule_format, of "i", unfolded rho rhs_n.simps] dec(1) Suc(2) have
u1:"ui (Suc (ji i)) = (U ρ i)⟨si ρ i⟩ ⋅ σi i" unfolding rho rstep_r_p_s_def ctxt_of_pos_term.simps(1)
Let_def ctxt_apply_term.simps i by simp
from dec(3)[rule_format, of "Suc i", unfolded rho lhs_n.simps] dec(1) Suc(2) have
u2:"ui (ji (Suc i)) = (U ρ i)⟨ti ρ i⟩ ⋅ σi (Suc i)" unfolding rho rstep_r_p_s_def ctxt_of_pos_term.simps(1)
Let_def ctxt_apply_term.simps i by simp
let ?zs = "map Var (Z ρ i)"
let ?ss = "map (λt. t ⋅ σi i) (si ρ i # ?zs)"
let ?ts = "map (λt. t ⋅ σi (Suc i)) (ti ρ i # ?zs)"
from dec(4)[rule_format, of i, unfolded rho u1 u2 Ui[unfolded rho] ctxt_apply_term.simps append_Nil] Suc(2) rho have
"(Fun Ui (si ρ i # map Var (Z ρ i)) ⋅ σi i, Fun Ui (ti ρ i # map Var (Z ρ i)) ⋅ σi (Suc i)) ∈ par_urstep_below_root ^^ ni i"
by simp
from this[unfolded subst_apply_term.simps par_rstep_pow_imp_args_par_rstep_pow length_map] Suc(2)
have "∀x<length (si ρ i # ?zs). (?ss ! x, ?ts ! x) ∈ par_rstep UR ^^ ni i" by blast
from this[rule_format, of "Suc j"] xj(2) have "(?ss ! (Suc j), ?ts ! (Suc j)) ∈ par_rstep UR ^^ ni i" by fastforce
from xj this[unfolded list.map(2) nth_Cons_Suc map_map] have "(σi i x, σi (Suc i) x) ∈ par_rstep UR ^^ ni i" by simp
with relpow_imp_rtrancl have "(σi i x, σi (Suc i) x) ∈ (par_rstep UR)^*" by blast
with * show ?case by simp
qed
} hence k:"(Var x ⋅ θ1, Var x ⋅ σi k) ∈ (par_rstep UR)⇧*" by auto
let ?ss = "map (λt. t ⋅ σi k) (local.si ρ k # map Var (Z ρ k))"
from dec(5)[unfolded t' Uk' subst_apply_term.simps par_rstep_pow_imp_args_par_rstep_pow] have
ss:"(∀i<length ?ss. (?ss ! i, ys ! i) ∈ par_rstep UR ^^ nm)" by blast
from zd[unfolded source_preserving_def, rule_format, OF sim(1), of k] dec(1) xl dec(1) have "x ∈ set (Z ρ k)"
unfolding rho by force
from this[unfolded set_conv_nth] obtain j where xj:"x = (Z ρ k) ! j" "j < length (Z ρ k)" by blast
from ss[rule_format, unfolded length_map list.map(2) nth_Cons_Suc , of "Suc j"] xj have
"(σi k x, ys ! (Suc j)) ∈ par_rstep UR ^^ nm" by auto
with relpow_imp_rtrancl have "(σi k x, ys ! (Suc j)) ∈ (par_rstep UR)^*" by auto
with nth_tl[of j ys, unfolded ll, OF xj(2)] have *:"(σi k x, tl ys ! j) ∈ (par_rstep UR)^*" by auto
from tys xj have "tl ys ! j = τ2 x" by force
with k * show "(θ1 x, τ2 x) ∈ (par_rstep UR)⇧*" by simp
qed
have "∃ ρ τ1 τ2 k u. ρ ∈ R ∧ k < length (snd ρ) ∧ t ⋅ (λx. l ⋅ θ1) = clhs ρ ⋅ τ1 ∧ t ⋅ σ = ((U ρ k) ⋅⇩c τ2)⟨u⟩ ∧
(∀x ∈ vars_term (clhs ρ). (τ1 x, τ2 x) ∈ (par_rstep UR)^*)" unfolding rho
by (rule exI[of _ ρ],rule exI[of _ θ1], rule exI[of _ τ2],rule exI[of _ k], insert 1 2 3 sim(1) dec(1) rho, auto)
}
hence 5:"t_U_cond t ?θ σ" unfolding t_U_cond_def tx by fast
show ?thesis by (rule exI[of _ ?θ], insert 1 2 steps 4 5, simp add: tx)
qed
qed
qed
qed
qed
from this[unfolded split, rule_format] s t seq show ?thesis unfolding t_U_cond_def split by presburger
qed
lemma soundness:
assumes ll:"left_linear_trs UR"
and sig_F_s:"sig_F s"
and sig_F_t:"sig_F t"
and seq:"(s,t) ∈ (rstep UR)^*"
shows "(s, t) ∈ (cstep R)^*"
proof-
fix x :: 'v
have sig_F_x:"sig_F (Var x)" unfolding sig_F_def by simp
have lin:"linear_term (Var x)" by simp
from seq rtrancl_mono[OF rstep_par_rstep] have "(s, t) ∈ (par_rstep UR)⇧*" by blast
with rtrancl_imp_relpow obtain n where "(s,Var x ⋅ (λy. t)) ∈ (par_rstep UR) ^^ n" by auto
from soundness_key_lemma[OF ll sig_F_s sig_F_x lin this] sig_F_t show ?thesis by force
qed
lemma join_cstep:
assumes sseq:"(s,u) ∈ (rstep UR)^*"
and tseq:"(t,u) ∈ (rstep UR)^*"
and u:"funs_term u ⊆ funs_trs UR ∪ F" (is "_ ⊆ ?FUR")
and sp:"source_preserving R Z"
and nlv:"non_LV"
and ll:"left_linear_trs UR"
and s:"sig_F s"
and t:"sig_F t"
shows "(s,t) ∈ (cstep R)⇧↓"
proof-
have "⋀s t. (s,u) ∈ (rstep UR)^* ⟹ (t,u) ∈ (rstep UR)^* ⟹ sig_F s ⟹ sig_F t ⟹ funs_term u ⊆ ?FUR ⟹ (s,t) ∈ (cstep R)⇧↓"
proof(induct u rule:term.induct)
case (Var x)
hence x:"sig_F (Var x)" unfolding sig_F_def by simp
from soundness[OF ll Var(3) x Var(1)] have *:"(s, Var x) ∈ (cstep R)⇧*" by auto
from soundness[OF ll Var(4) x Var(2)] have "(t, Var x) ∈ (cstep R)⇧*" by auto
with * show ?case by blast
next
case (Fun f us)
from rtrancl_imp_relpow[OF Fun(2)[unfolded par_rsteps_rsteps[symmetric]]] obtain m
where sseq':"(s, Fun f us) ∈ par_rstep UR ^^ m" by blast
from rtrancl_imp_relpow[OF Fun(3)[unfolded par_rsteps_rsteps[symmetric]]] obtain n
where tseq':"(t, Fun f us) ∈ par_rstep UR ^^ n" by blast
{ assume fR:"f ∈ F"
let ?xs = "dvars (length us)"
from distinct_vars[of "length us"] have fresh:"distinct ?xs""length ?xs = length us" by auto
let ?u = "Fun f (map Var ?xs)"
from fR have u1:"sig_F ?u" unfolding sig_F_def by auto
let ?vs = "map (λ x. {x}) ?xs"
have "?vs = map vars_term (map Var ?xs)" by auto
have p:"is_partition ?vs" unfolding is_partition_def length_map fresh(2)
proof(rule, rule, rule, rule)
fix i j
assume j:"j < length us" and i:"i < j"
hence i':"i < length us" by auto
from i fresh(1)[unfolded distinct_conv_nth, rule_format, unfolded fresh(2), OF j i'] have "?xs ! i ≠ ?xs ! j" by auto
thus "map (λx. {x}) ?xs ! i ∩ map (λx. {x}) ?xs ! j = {}"
unfolding nth_map[of i ?xs, unfolded fresh(2), OF i'] nth_map[of j ?xs, unfolded fresh(2), OF j] by fast
qed
have ls:"⋀x. x ∈ set (map Var ?xs) ⟹ linear_term x" by auto
have "map (λx. {x}) (dvars (length us)) = map vars_term (map Var (dvars (length us)))" unfolding map_map by auto
with ls fresh p have lin:"linear_term ?u" unfolding linear_term.simps(2)[of f "map Var ?xs"] unfolding map_map by metis
let ?σ = "mk_subst Var (zip ?xs us)"
{ fix j assume "j < length us"
from mk_subst_distinct[OF fresh(1), unfolded fresh(2), OF refl this] have "?σ (?xs ! j) = us ! j" by fast
} note σequiv = this
with fresh(2) nth_map[of] have usσ:"us = map ?σ ?xs" unfolding list_eq_iff_nth_eq length_map by simp
then have uσ:"Fun f us = ?u ⋅ ?σ" unfolding subst_apply_term.simps(2)
term.inject(2)[of f us] list_eq_iff_nth_eq by simp
from soundness_key_lemma[OF ll Fun(4) u1, unfolded uσ[symmetric], OF lin] sseq'[unfolded uσ] obtain θs where
sseq:"(s, ?u ⋅ θs) ∈ (cstep R)⇧*""sig_F_subst θs (vars_term ?u)"
"∀x∈vars_term ?u. (Var x ⋅ θs, Var x ⋅ ?σ) ∈ par_rstep UR ^^ m" by meson
from soundness_key_lemma[OF ll Fun(5) u1, unfolded uσ[symmetric], OF lin] tseq'[unfolded uσ] obtain θt where
tseq:"(t, ?u ⋅ θt) ∈ (cstep R)⇧*""sig_F_subst θt (vars_term ?u)"
"∀x∈vars_term ?u. (Var x ⋅ θt, Var x ⋅ ?σ) ∈ par_rstep UR ^^ n" by meson
let ?t = "(Fun f (map Var ?xs)) ⋅ θt" let ?s = "(Fun f (map Var ?xs)) ⋅ θs"
{ fix j
assume j: "j < length us"
let ?x = "?xs ! j"
from j have xv:"?x ∈ vars_term ?u" unfolding term.simps(18)
using dvars_def distinct_vars by auto
from sseq(3)[rule_format, OF xv] relpow_imp_rtrancl par_rsteps_rsteps have m:"(Var ?x ⋅ θs, Var ?x ⋅ ?σ) ∈ (rstep UR)^*" by blast
from tseq(3)[rule_format, OF xv] relpow_imp_rtrancl par_rsteps_rsteps have n:"(Var ?x ⋅ θt, Var ?x ⋅ ?σ) ∈ (rstep UR)^*" by blast
from j xv have "Var ?x ⋅ ?σ ∈ set (map ?σ ?xs)" by force
with usσ have xus:"Var ?x ⋅ ?σ ∈ set us" by force
with usσ Fun(6) term.set(2) have funs: "funs_term (Var ?x ⋅ ?σ) ⊆ ?FUR" by auto
from xv sseq(2) have sigs:"sig_F (θs ?x)" by blast
from xv tseq(2) have sigt:"sig_F (θt ?x)" by blast
from Fun(1)[OF xus m n] sigs sigt funs have "(θs ?x, θt ?x) ∈ (cstep R)⇧↓" by auto
} note xsteps = this
have "(?u ⋅ θs, ?u ⋅ θt) ∈ (cstep R)⇧↓" unfolding subst_apply_term.simps
by (rule all_ctxt_closedD, insert xsteps join_csteps_all_ctxt_closed fresh(2), auto)
from join_rtrancl_join[OF rtrancl_join_join tseq(1), OF sseq(1) this] have "(s, t) ∈ (cstep R)⇧↓" by auto
} note case1 = this
{ assume fR:"∃ ρ i. ρ ∈ R ∧ i < length (snd ρ) ∧ U_fun ρ i f"
then obtain ρ i where *:"ρ ∈ R" "i < length (snd ρ)" "U_fun ρ i f" by auto
fix x :: 'v
obtain l r cs where rho:"ρ = ((l,r),cs)" by (cases ρ, auto)
have u:"Fun f us = (Var x) ⋅ (λx. Fun f us)" by simp
have x:"sig_F (Var x)" "linear_term (Var x)" unfolding sig_F_def by auto
let ?rseq = "λu θu. (u, (Var x) ⋅ θu) ∈ (cstep R)⇧*"
let ?vars = "λθu n. (Var x ⋅ θu, Fun f us) ∈ par_rstep UR ^^ n"
let ?cond = "non_LV ∧ source_preserving R Z ∧ (∃Ui zs. (∃ρ∈R. ∃i<length (snd ρ). U_fun ρ i Ui) ∧ Fun f us = Fun Ui zs)"
let ?cons = "λθ. (∃ρ τ1 τ2 k u. ρ ∈ R ∧ k < length (snd ρ) ∧ Var x ⋅ θ = clhs ρ ⋅ τ1 ∧ Fun f us = ((U ρ k) ⋅⇩c τ2)⟨u⟩ ∧
(∀x∈vars_term (clhs ρ). (τ1 x, τ2 x) ∈ (par_rstep UR)⇧*))"
from nlv assms(4) fR have c:"?cond" by blast
from soundness_key_lemma[OF ll Fun(5) x, of "λx. Fun f us", unfolded u[symmetric],OF tseq'] obtain θt where
tseq:"?rseq t θt ∧ sig_F (θt x) ∧ ?vars θt n ∧ (?cond⟶ ?cons θt)" by force
with c have tseq:"?rseq t θt" "sig_F (θt x)" "?vars θt n" "?cons θt" by auto
from soundness_key_lemma[OF ll Fun(4) x, of "λx. Fun f us", unfolded u[symmetric],OF sseq'] obtain θs where
sseq:"?rseq s θs ∧ sig_F (θs x) ∧ ?vars θs m ∧ (?cond⟶ ?cons θs)" by force
with c have sseq:"?rseq s θs" "sig_F (θs x)" "?vars θs m" "?cons θs" by auto
from sseq(4) obtain ρs σf σl ks u_s where ps:"ρs ∈ R" "ks < length (snd ρs)""Var x ⋅ θs = clhs ρs ⋅ σf" "Fun f us = ((U ρs ks) ⋅⇩c σl)⟨u_s⟩"
"∀x∈vars_term (clhs ρs). (σf x, σl x) ∈ (par_rstep UR)⇧*" by blast
from tseq(4) obtain ρt τf τl kt u_t where pt:"ρt ∈ R" "kt < length (snd ρt)" "Var x ⋅ θt = clhs ρt ⋅ τf" "Fun f us = ((U ρt kt) ⋅⇩c τl)⟨u_t⟩"
"∀x∈vars_term (clhs ρt). (τf x, τl x) ∈ (par_rstep UR)⇧*" by blast
from U_cond[OF ps(1-2)] ps(4) have fs:"U_fun ρs ks f" by fastforce
from U_cond[OF pt(1-2)] pt(4) have ft:"U_fun ρt kt f" by fastforce
from U_cond[OF ps(1-2)] obtain f' where
pe:"U_fun ρs ks f' ∧ (∀ρ' n' g b c a. ρ' ∈ R ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a ⟶
f' ≠ g ∨ ks = n' ∧ (∀i≤ks. U ρs i = U ρ' i) ∧ prefix_equivalent ρs ρ' ks)" by blast
with fs have "f' = f" by simp
from pe[unfolded this] ft pt(1) pt(2) have pe:"ks = kt ∧ (∀i≤ks. U ρs i = U ρt i) ∧ prefix_equivalent ρs ρt ks" by blast
from this[unfolded prefix_equivalent_def] have ll':"clhs ρs = clhs ρt" by blast
from U_cond[OF ps(1-2)] * fs ctxt.inject[of f "[]" □]
have "prefix_equivalent ρs ρ ks" by metis
from this[unfolded prefix_equivalent_def] have ll:"clhs ρs = l" unfolding rho by simp
from ps(4) pt(4) have u:" ((U ρs ks) ⋅⇩c σl)⟨u_s⟩ = ((U ρt kt) ⋅⇩c τl)⟨u_t⟩" by auto
have aux:"⋀σ.((λt. t ⋅ σ) ∘ Var) = σ" by force
from conjunct2[OF u[unfolded fs ft subst_apply_ctxt.simps ctxt_apply_term.simps term.simps(2) append_Nil list.map(2) map_map]]
have zs:"map σl (Z ρs ks) = map τl (Z ρt kt)" unfolding aux by simp
note acc = all_ctxt_closed_subst_step[OF all_ctxt_closed_par_rsteps]
from ps(5) ll acc have "(l⋅σf, l⋅σl) ∈ (par_rstep UR)⇧*" by simp
from pt(5) ll ll' acc have "(l⋅τf, l⋅τl) ∈ (par_rstep UR)⇧*" by simp
from pe have uu:"U ρs ks = U ρt kt" by auto
from term.inject(1) inj_on_def have "inj Var" by auto
from uu[unfolded fs ft ctxt.inject, simplified] inj_map_eq_map[OF this] have zzz:"Z ρs ks = Z ρt kt" by blast
note vlz = sp[unfolded source_preserving_def, rule_format, OF pt(1-2)]
{ fix x
assume "x ∈ vars_term l"
with vlz ll ll' have vlk:"x ∈ set (Z ρt kt)" by auto
from this[unfolded set_conv_nth] obtain j where j:"j < length (Z ρt kt)" "x = (Z ρt kt) ! j" by auto
from j(1) zs[unfolded list_eq_iff_nth_eq] have "σl x = τl x" unfolding j(2) zzz by simp
} note vl = this
have eq:"l⋅ σl = l ⋅ τl" by (rule term_subst_eq, insert zs[unfolded zzz] vl, auto)
from ps(4)[unfolded fs] have useq:"us ≠ []" "tl us = map σl (Z ρs ks)" by (simp,simp)
{ fix z
assume z:"z ∈ vars_term l"
with vlz have zz:"z ∈ set (Z ρt kt)" using ll' ll by auto
from this[unfolded set_conv_nth] obtain j where j:"j < length (Z ρt kt)" "z = (Z ρt kt) ! j" by blast
from vl z have xeq:"σl z = τl z" by simp
with useq[unfolded zzz] j have xtl:"σl z ∈ set (tl us)" by (metis length_map nth_map nth_mem)
from sig_F_l[OF *(1)] have sigl:"sig_F l" unfolding rho by fastforce
from sseq(2)[unfolded ps(3)[unfolded subst_apply_term.simps(1)] ll] z funs_term_subst
have sR1:"sig_F (σf z)" unfolding sig_F_def by fast
from tseq(2)[unfolded pt(3)[unfolded subst_apply_term.simps(1)] ll'[symmetric] ll] z funs_term_subst
have tR1:"sig_F (τf z)" unfolding sig_F_def by fast
with list.set_sel(2)[OF useq(1) xtl] Fun(6) term.set(2) have funs: "funs_term (τl z) ⊆ ?FUR" unfolding xeq by auto
note steps = ps(5)[rule_format, unfolded ll, OF z] pt(5)[rule_format, unfolded ll'[symmetric] ll, OF z]
from steps vl[OF z] have steps:"(σf z, σl z) ∈ (rstep UR)⇧*" "(τf z, σl z) ∈ (rstep UR)⇧*" unfolding par_rsteps_rsteps by auto
from Fun(1)[OF list.set_sel(2)[OF useq(1) xtl] steps sR1 tR1] funs vl[OF z] have "(σf z, τf z) ∈ (cstep R)⇧↓" by auto
}
with all_ctxt_closed_subst_step[OF join_csteps_all_ctxt_closed] have "(l ⋅ σf, l ⋅ τf) ∈ (cstep R)⇧↓" by blast
with join_rtrancl_join[OF rtrancl_join_join sseq(1), OF tseq(1)] ps(3) pt(3) ll ll' have "(s, t) ∈ (cstep R)⇧↓" by auto
} note case2 = this
from Fun(6) funs_UR F
have "f ∈ F ∨ (∃ ρ i. ρ ∈ R ∧ i < length (snd ρ) ∧ U_fun ρ i f)" by auto
with case1 case2 show "(s, t) ∈ (cstep R)⇧↓" by auto
qed
from this[OF sseq tseq s t u] show ?thesis by simp
qed
lemma wf_ctrs_non_LV: "wf_ctrs R ⟹ non_LV" unfolding non_LV_def
proof
fix l r
assume wf:"wf_ctrs R" and lr:"(l,r) ∈ UR"
from lr[unfolded UR_def] rules_def obtain n ρ where n:"ρ ∈ R" "(l,r) = (lhs_n ρ n, rhs_n ρ n)" "n ≤ length (snd ρ)" by blast
obtain l' r' cs where rho:"ρ = ((l',r'), cs)" by (cases ρ, auto)
from wf[unfolded wf_ctrs_def, rule_format] n(1)[unfolded rho] have l':"is_Fun l'" by fast
show "is_Fun l" proof (cases n)
case 0
from n(2)[unfolded rho 0 lhs_n.simps] l' show ?thesis by auto
next
case (Suc k)
from n(3) Suc have k:"k < length (snd ρ)" by auto
from U_cond[OF n(1) k] obtain f where U:"U_fun ρ k f" by fast
from n(2)[unfolded Suc rho lhs_n.simps U[unfolded rho] ctxt_apply_term.simps] show "is_Fun l" by fast
qed
qed
lemma CR_imp_CR_on:
assumes sp:"source_preserving R Z"
and ll:"left_linear_trs UR"
and cr:"CR (rstep UR)"
and wf:"wf_ctrs R"
shows "CR_on (cstep R) {t. funs_term t ⊆ F}"
proof (cases "R = {}")
case False
then obtain ρ where "ρ ∈ R" by auto
then obtain l r cs where lr: "((l,r),cs) ∈ R" by (cases ρ) auto
with wf[unfolded wf_ctrs_def] obtain g ls where "l = Fun g ls" by (cases l) auto
with lr have "g ∈ funs_ctrs R"
unfolding funs_ctrs_def funs_crule_def[abs_def] funs_rule_def by force
with funs_UR have g: "g ∈ funs_trs UR" by simp
show ?thesis
proof
fix u :: "('f,'v) term"
fix s t
assume u:"u ∈ {t. funs_term t ⊆ F}"
assume usc:"(u, s) ∈ (cstep R)⇧*"
assume utc:"(u, t) ∈ (cstep R)⇧*"
from u have u:"funs_term u ⊆ F" by auto
from completeness have *:"cstep R ⊆ (rstep UR)⇧+" by auto
from rtrancl_mono[OF *, unfolded trancl_rtrancl_absorb] usc have us:"(u, s) ∈ (rstep UR)⇧*" by blast
from rtrancl_mono[OF *, unfolded trancl_rtrancl_absorb] utc have ut:"(u, t) ∈ (rstep UR)⇧*" by blast
from cr[unfolded CR_defs] us ut have "(s, t) ∈ (rstep UR)⇧↓" by auto
then obtain v where v:"(s, v) ∈ (rstep UR)⇧*" "(t, v) ∈ (rstep UR)⇧*" by blast
from funs_term_funas_term have funs_rule:"⋀ rl. funs_rule rl = fst ` funas_rule rl"
unfolding funs_rule_def funas_rule_def image_Un by metis
note unf = sig_F_def funs_term_funas_term funs_ctrs_funas_ctrs
let ?F = "funas_trs UR ∪ F × UNIV"
let ?h = "λ f. if f ∈ funs_trs UR ∪ F then f else g"
let ?ren = "map_funs_term ?h"
from wf_ctrs_steps_preserves_funs[OF wf u F usc] have sR: "sig_F s" and sR': "funas_term s ⊆ ?F"
unfolding sig_F_def funs_term_funas_term by auto
from wf_ctrs_steps_preserves_funs[OF wf u F utc] have tR: "sig_F t" unfolding sig_F_def .
{
fix s
assume "sig_F s"
hence "?ren s = s" unfolding sig_F_def
by (intro funs_term_map_funs_term_id, auto)
} note id = this
from us v(1) have uv:"(u, v) ∈ (rstep UR)⇧*" by auto
note map = rtrancl_map[of "rstep UR" ?ren, OF rstep_map_funs_term[of UR ?h]]
have "(?ren s, ?ren v) ∈ (rstep UR)^*"
by (rule map[OF _ _ v(1)], auto)
hence sv: "(s, ?ren v) ∈ (rstep UR)^*" unfolding id[OF sR] .
have "(?ren t, ?ren v) ∈ (rstep UR)^*"
by (rule map[OF _ _ v(2)], auto)
hence tv: "(t, ?ren v) ∈ (rstep UR)^*" unfolding id[OF tR] .
have "funs_term (?ren v) ⊆ funs_trs UR ∪ F"
using funs_term_map_funs_term[of ?h v] g by auto
from join_cstep[OF sv tv this sp wf_ctrs_non_LV[OF wf] ll sR tR]
show "(s, t) ∈ (cstep R)⇧↓" .
qed
qed (simp add: CR_on_def join_def)
end
hide_const si ti
lemma (in unraveling) CR_imp_CR:
assumes U_cond: "U_cond U R (funs_ctrs R) Z"
and Z:"Z_vars Z"
and dctrs:"dctrs R"
and type3:"type3 R"
and inf_var: "infinite (UNIV :: 'v set)"
and inf_fun: "infinite (UNIV :: 'f set)"
and sp: "source_preserving R Z"
and ll:"left_linear_trs UR"
and fin: "finite R"
and cr:"CR (rstep UR)"
and wf:"wf_ctrs R"
shows "CR (cstep R)"
proof
fix s t u
assume ts: "(t, s) ∈ (cstep R)⇧*" and tu: "(t, u) ∈ (cstep R)⇧*"
def FU ≡ "funs_trs UR"
from finite_funas_trs[OF finite_UR[OF fin]] have "finite (funs_trs UR)"
unfolding funs_trs_funas_trs by auto
hence FU: "finite FU" unfolding FU_def funs_term_funas_term using finite_funas_term by auto
from infinite_inj_on_finite_remove_finite[OF inf_fun _ FU, of id UNIV]
obtain h where inj: "inj (h :: 'f ⇒ 'f)" and disj: "range h ∩ FU = {}" by auto
def g ≡ "λ f. if f ∈ funs_ctrs R then f else h f"
def g' ≡ "λ f. if f ∈ funs_ctrs R then f else (the_inv h f)"
let ?ren = "map_funs_term g"
let ?ren' = "map_funs_term g'"
let ?t = "?ren t"
let ?FR = "funs_ctrs R"
have g: "⋀ f. f ∈ funs_ctrs R ⟹ g f = f" unfolding g_def by auto
have g': "⋀ f. f ∈ funs_ctrs R ⟹ g' f = f" unfolding g'_def by auto
have ts: "(?ren t, ?ren s) ∈ (cstep R)⇧*"
by (rule rtrancl_map[OF cstep_map_funs_term[OF g] ts])
have tu: "(?ren t, ?ren u) ∈ (cstep R)⇧*"
by (rule rtrancl_map[OF cstep_map_funs_term[OF g] tu])
def F ≡ "funs_ctrs R ∪ funs_term ?t"
let ?cond = "λ ρ n f. (∀ ρ' n' g b c a. (ρ' ∈ R ∧ n' < length (snd ρ') ∧ U ρ' n' = More g b c a) ⟶ f ≠ g ∨ (n = n' ∧ (∀i ≤n. U ρ i = U ρ' i) ∧ prefix_equivalent ρ ρ' n))"
interpret opt: standard_unraveling R U "funs_ctrs R" Z
by (unfold_locales, rule subset_refl, rule U_cond,
insert F_def Z dctrs inf_var type3, auto)
have U_cond: "U_cond U R F Z"
proof (rule U_condI)
fix ρ n
assume rho: "ρ ∈ R" and n: "n < length (snd ρ)"
from opt.U_cond[OF this] obtain f where U: "U ρ n = More f [] □ (map Var (Z ρ n))"
and f: "f ∉ funs_ctrs R" and cond: "?cond ρ n f" by auto
obtain l r cs where rule: "ρ = ((l,r),cs)" by (cases ρ, auto)
have f: "f ∉ F"
proof
assume "f ∈ F"
with f have "f ∈ funs_term (?ren t)" unfolding F_def by auto
with funs_term_map_funs_term[of g] have "f ∈ range g" by auto
with disj f have "f ∉ FU" unfolding g_def by auto
from this[unfolded FU_def opt.funs_UR] rho rule U n show False
by auto
qed
show "∃ f. (U ρ n = (More f Nil Hole (map Var (Z ρ n))) ∧ f ∉ F ∧ ?cond ρ n f)"
by (intro exI conjI, rule U, rule f, rule cond)
qed
interpret standard_unraveling R U F Z
by (unfold_locales, insert U_cond F_def Z dctrs inf_var type3, auto)
from CR_onD[OF CR_imp_CR_on[OF sp ll cr wf] _ ts tu]
have "(?ren s, ?ren u) ∈ (cstep R)⇧↓" unfolding F_def by auto
then obtain v where sv: "(?ren s, v) ∈ (cstep R)^*" and uv: "(?ren u, v) ∈ (cstep R)^*" by auto
have sv: "(?ren' (?ren s), ?ren' v) ∈ (cstep R)⇧*"
by (rule rtrancl_map[OF cstep_map_funs_term[OF g'] sv])
have uv: "(?ren' (?ren u), ?ren' v) ∈ (cstep R)⇧*"
by (rule rtrancl_map[OF cstep_map_funs_term[OF g'] uv])
from sv uv have su: "(?ren' (?ren s), ?ren' (?ren u)) ∈ (cstep R)⇧↓" by auto
{
fix t :: "('f,'v)term"
have "?ren' (?ren t) = map_funs_term (g' o g) t" by (rule map_funs_term_comp)
also have "g' o g = id"
proof -
{
fix f
have "g' (g f) = f"
proof (cases "f ∈ funs_ctrs R")
case True
thus ?thesis unfolding g'_def g_def by auto
next
case False
hence "g f = h f" unfolding g_def by simp
moreover have "h f ∉ funs_ctrs R" using disj
unfolding FU_def funs_UR by auto
ultimately have "g' (g f) = the_inv h (h f)" unfolding g'_def by auto
with the_inv_f_f[OF inj] show ?thesis by simp
qed
}
thus ?thesis by auto
qed
also have "map_funs_term id t = t" by simp
finally have "?ren' (?ren t) = t" .
} note ren_ren = this
from su
show "(s, u) ∈ (cstep R)⇧↓" unfolding ren_ren .
qed
end