theory Flat_Context_Closure
imports
"Check-NT.Name"
QTRS.QDP_Framework
TA.Signature_Extension
begin
definition
root_altering :: "('f, 'v) trs ⇒ ('f, 'v) trs" ("'(_')a" 1000)
where
"(R)a ≡ {(l, r) | l r. (l, r) ∈ R ∧ root l ≠ root r}"
text ‹The following function creates a flat context with root @{text f}
and a hole at position @{text i}. All variables are taken from the list
@{text xs}.›
definition
flat_ctxt_i :: "('f, 'v) term list ⇒ 'f ⇒ nat ⇒ ('f, 'v) ctxt"
where
"flat_ctxt_i xs f i ≡ More f (take i xs) □ (drop (Suc i) xs)"
definition
fresh_vars :: "nat ⇒ string set ⇒ string list"
where
"fresh_vars n tabus ≡ fresh_strings ''x'' 0 tabus n"
lemma fresh_vars_fresh:
assumes "finite V"
shows "set (fresh_vars n V) ∩ V = {}"
using assms fresh_name_gen_for_strings[of "''x''" 0]
unfolding fresh_vars_def fresh_name_gen_def by auto
lemma fresh_vars_length:
assumes "finite V" shows "length (fresh_vars n V) = n"
using assms fresh_name_gen_for_strings[of "''x''" 0]
unfolding fresh_name_gen_def fresh_vars_def by simp
lemma Var_inj: "inj_on Var (set vs)" unfolding inj_on_def by auto
lemma fresh_vars_distinct:
assumes "finite V"
shows "distinct (fresh_vars n V)"
using assms Var_inj[of "fresh_strings ''x'' 0 V n"]
fresh_name_gen_for_strings[of "''x''" 0]
distinct_map[of Var "fresh_strings ''x'' 0 V n"]
unfolding fresh_name_gen_def fresh_vars_def by auto
definition
flat_ctxts :: "string set ⇒ ('f × nat) set ⇒ ('f, string) ctxt set"
where
"flat_ctxts tabus fs ≡ (⋃(f, n)∈fs.
{flat_ctxt_i (map Var (fresh_vars n tabus)) f i | i. i ∈ {0..<n}})"
definition
flat_ctxt_closure :: "('f × nat) set ⇒ ('f, string) trs ⇒ ('f, string) trs" ("FC")
where
"FC F R ≡ (⋃(l, r)∈(R)a. {(C⟨l⟩, C⟨r⟩) | C. C ∈ flat_ctxts (vars_trs R) F}) ∪ (R - (R)a)"
lemma flat_ctxts_empty[simp]: "flat_ctxts xs {} = {}" unfolding flat_ctxts_def by simp
lemma root_altering_list[simp]:
"set (fst (partition (λ(l, r). root l ≠ root r) trs)) = (set trs)a"
unfolding partition_filter_conv root_altering_def by auto
lemma root_altering_list_aux[simp]:
"set (snd (partition (λ(l, r). root l ≠ root r) trs)) = set trs - (set trs)a"
unfolding partition_filter_conv root_altering_def by auto
lemma fccE[elim]:
fixes R::"('f, string) trs"
assumes "(s, t) ∈ FC F R"
and ra: "(s, t) ∈ R - (R)a ⟹ P"
and rp: "∃(l, r)∈(R)a. ∃C∈flat_ctxts (vars_trs R) F. s = C⟨l⟩ ∧ t = C⟨r⟩ ⟹ P"
shows "P"
using assms unfolding flat_ctxts_def flat_ctxt_closure_def by force
lemma fccI_altering[intro]:
fixes R::"('f, string) trs"
assumes "C ∈ flat_ctxts (vars_trs R) F"
and "(l, r) ∈ (R)a"
shows "(C⟨l⟩, C⟨r⟩) ∈ FC F R"
using assms unfolding flat_ctxt_closure_def by auto
lemma fccI_preserving[intro]:
fixes R::"('f, string) trs"
assumes "(l, r) ∈ R - (R)a"
shows "(l, r) ∈ FC F R"
using assms unfolding flat_ctxt_closure_def by simp
lemma partial_fcc_preserves_SN:
assumes SN: "SN (qrstep nfs Q R)"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
and refl: "∀(l, r)∈R'. ∃(u, v)∈R. ∃C. l = C⟨u⟩ ∧ r = C⟨v⟩"
shows "SN (qrstep nfs Q R')"
using SN
proof (rule contrapos_pp)
let ?r = "qrstep nfs Q R"
let ?c = "qrstep nfs Q R'"
from wwf_qtrs_imp_nfs_False_switch[OF wwf] have switch: "qrstep nfs Q R = qrstep False Q R" .
assume "¬ SN ?c"
then obtain t where chain: "chain ?c t" unfolding SN_defs by auto
have "chain ?r t"
proof
fix i
from chain have "(t i, t (Suc i)) ∈ ?c" by simp
then obtain C σ l r where R': "(l, r) ∈ R'" and NF: "∀s⊲l ⋅ σ. s ∈ NF_terms Q"
and s: "t i = C⟨l ⋅ σ⟩" and t: "t (Suc i) = C⟨r ⋅ σ⟩" by auto
from R' refl have "∃(u, v) ∈ R. ∃C. l = C⟨u⟩ ∧ r = C⟨v⟩" by auto
then obtain u v C' where R: "(u, v) ∈ R" and l: "l = C'⟨u⟩" and r: "r = C'⟨v⟩" by auto
from ctxt_supteq[OF l] have "l ⊵ u" .
hence "l ⋅ σ ⊵ u ⋅ σ" by auto
hence NF': "∀s⊲u ⋅ σ. s ∈ NF_terms Q"
unfolding supteq_supt_conv using NF by (auto intro: supt_trans)
from qrstep.subst[OF NF' R] have "(u ⋅ σ, v ⋅ σ) ∈ qrstep nfs Q R" unfolding switch by auto
from qrstep.ctxt[OF this] show "(t i, t (Suc i)) ∈ ?r"
unfolding s t l r by auto
qed
thus "¬ SN ?r" unfolding SN_defs by auto
qed
lemma fcc_imp_refl:
"∀(l, r) ∈ FC F R. (∃(u, v)∈R. ∃C. l = C⟨u⟩ ∧ r = C⟨v⟩)"
proof -
{
fix l r assume "(l, r) ∈ FC F R"
hence "∃(u,v)∈R. ∃C. l = C⟨u⟩ ∧ r = C⟨v⟩"
proof
assume "(l, r) ∈ R - (R)a"
hence "(l, r) ∈ R" by simp
moreover have "l = □⟨l⟩" by simp
moreover have "r = □⟨r⟩" by simp
ultimately show ?thesis by best
next
assume "∃(x, y)∈(R)a. ∃C∈flat_ctxts (vars_trs R) F. l = C⟨x⟩ ∧ r = C⟨y⟩"
moreover have "(R)a ⊆ R" unfolding root_altering_def by auto
ultimately show ?thesis by auto
qed
}
thus ?thesis by auto
qed
lemma fcc_imp_pres:
fixes R::"('f, string) trs"
and F::"('f × nat) set"
defines "fcs ≡ flat_ctxts (vars_trs R) F"
shows "∀(l, r)∈R. (l, r) ∈ FC F R ∨ (∀C∈fcs. (C⟨l⟩, C⟨r⟩) ∈ FC F R)"
proof (intro ballI2)
fix l r assume "(l, r) ∈ R"
hence "(l, r) ∈ (R)a ∨ (l, r) ∈ R - (R)a" by auto
thus "(l, r) ∈ FC F R ∨ (∀C∈fcs. (C⟨l⟩, C⟨r⟩) ∈ FC F R)"
proof
assume Ra: "(l, r) ∈ (R)a"
thus ?thesis unfolding fcs_def using fccI_altering[of _ R F l r] by auto
next
assume "(l, r) ∈ R - (R)a" thus ?thesis using fccI_preserving by best
qed
qed
lemma fcc_preserves_SN:
assumes "SN (qrstep nfs Q R)" and "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R" shows "SN (qrstep nfs Q (FC F R))"
using partial_fcc_preserves_SN[OF assms, of "FC F R"] fcc_imp_refl[of F R] by simp
lemma fresh_vars_subst:
assumes "finite V" and "x ∈ set (fresh_vars n V)" shows "Var x⋅(σ |s V) = Var x"
using fresh_vars_fresh[OF ‹finite V›] assms by (auto simp: subst_restrict_def)
lemma flat_ctxt_subst_apply[simp]:
assumes "finite V" and "C ∈ flat_ctxts V F"
shows "C⟨t⟩⋅(σ |s V) = C⟨t⋅(σ |s V)⟩"
proof -
from assms obtain f n i
where i:"i<n" and fn: "(f,n)∈F" and C: "C = flat_ctxt_i (map Var (fresh_vars n V)) f i" (is "_ = flat_ctxt_i ?V f i")
unfolding flat_ctxts_def by auto
have fresh: "map (λt. t⋅(σ |s V)) ?V = ?V"
using map_idI[of "?V" "λt. t⋅(σ |s V)"] fresh_vars_subst[OF ‹finite V›] by auto
from C have C: "C = More f (take i ?V) □ (drop (Suc i) ?V)"
unfolding flat_ctxt_i_def by simp
show ?thesis unfolding C
unfolding ctxt_apply_term.simps subst_apply_term.simps unfolding map_append
unfolding take_map[symmetric]
unfolding list.simps
unfolding drop_map[symmetric]
unfolding fresh by simp
qed
lemma flat_ctxt_has_fresh_vars:
assumes finite: "finite V"
and FC: "C ∈ flat_ctxts V F"
shows "vars_ctxt C ∩ V = {}"
proof -
from FC obtain f n i where "(f,n) ∈ F"
and "i < n" and "C = flat_ctxt_i (map Var (fresh_vars n V)) f i"
(is "_ = flat_ctxt_i ?V _ _")
unfolding flat_ctxts_def by auto
hence C: "C = More f (take i ?V) □ (drop (Suc i) ?V)" unfolding flat_ctxt_i_def by simp
have vC: "vars_ctxt C = ⋃(set (map vars_term (take i ?V @ drop (Suc i) ?V)))" by (simp add: C)
have"vars_ctxt C ⊆ ⋃(set (map vars_term ?V))"
using fresh_vars_length[OF finite,of n] and ‹i < n› unfolding vC
using set_take_subset[of i ?V] set_drop_subset[of "Suc i" ?V] by auto
hence "{Var x | x. x ∈ vars_ctxt C} ⊆ set ?V" unfolding fresh_vars_def by auto
with fresh_vars_fresh[OF finite,of n] show ?thesis by auto
qed
lemma wwf_FC:
assumes "wwf_qtrs Q R"
shows "wwf_qtrs Q (FC F R)"
unfolding wwf_qtrs_def
proof (intro ballI2 impI)
fix l r assume 1: "(l, r) ∈ FC F R" and applicable: "applicable_rule Q (l, r)"
from 1 show "is_Fun l ∧ vars_term r ⊆ vars_term l"
proof
assume "(l, r) ∈ R - (R)a" with assms show ?thesis by (auto simp: applicable wwf_qtrs_def)
next
assume "∃(l', r')∈(R)a. ∃C∈flat_ctxts (vars_trs R) F. l = C⟨l'⟩ ∧ r = C⟨r'⟩"
then obtain l' r' C where "(l',r') ∈ (R)a"
and C: "C ∈ flat_ctxts (vars_trs R) F" and l: "l = C⟨l'⟩" and r: "r = C⟨r'⟩" by best
hence R: "(l', r') ∈ R" unfolding root_altering_def by auto
from C obtain f n i where "(f,n) ∈ F" and "i < n"
and "C = flat_ctxt_i (map Var (fresh_vars n (vars_trs R))) f i"
(is "C = flat_ctxt_i ?V f i") unfolding flat_ctxts_def by auto
hence C: "C = More f (take i ?V) □ (drop (Suc i) ?V)" unfolding flat_ctxt_i_def by simp
hence "l = Fun f (take i ?V@l'#drop (Suc i) ?V)" unfolding l by simp
hence "is_Fun l" by auto
moreover have "vars_term r ⊆ vars_term l"
proof -
from applicable have "applicable_rule Q (l', r')" unfolding l r applicable_rule_def
using NF_terms_ctxt[of C l' Q] by simp
with R and assms have "vars_term r' ⊆ vars_term l'" by (auto simp: wwf_qtrs_def)
with l r show ?thesis unfolding C by auto
qed
ultimately show ?thesis by simp
qed
qed
lemma wf_FC:
assumes "wf_trs R"
shows "wf_trs (FC F R)"
using assms wwf_FC[of "{}", unfolded wwf_qtrs_empty] by blast
lemma fc_flat:
assumes C: "C ∈ flat_ctxts V F"
and finite: "finite V"
shows "vars_ctxt C ∩ V = {} ∧ (∃f ss1 ss2. C = More f ss1 □ ss2
∧ (f, Suc (length (ss1 @ ss2))) ∈ F
∧ (∀t∈set (ss1 @ ss2). is_Var t)
∧ distinct (ss1 @ ss2))"
proof -
from C obtain g i m where "i < m" and "(g,m) ∈ F"
and C': "C = More g (take i (map Var (fresh_vars m V))) □ (drop (Suc i) (map Var (fresh_vars m V)))" (is "C = More g ?ss1 □ ?ss2")
unfolding flat_ctxts_def flat_ctxt_i_def by auto
from flat_ctxt_has_fresh_vars[OF finite C] have fresh: "vars_ctxt C ∩ V = {}" .
from fresh_vars_length[OF finite] have len: "length(fresh_vars m V) = m" by simp
from fresh_vars_distinct[OF finite] have dist: "distinct(fresh_vars m V)" by simp
from length_take[of i "fresh_vars m V"] ‹i < m› have take: "length(?ss1) = i" unfolding len by simp
from length_drop[of "Suc i" "fresh_vars m V"] have drop: "length(?ss2) = length(fresh_vars m V) - Suc i" by simp
from take drop have m: "Suc(length(?ss1@?ss2)) = m" unfolding len using ‹i < m› by simp
have F:"(g,Suc(length(?ss1@?ss2))) ∈ F" using ‹(g,m) ∈ F› unfolding m .
have "∀t∈set ?ss1. is_Var t" unfolding take_map by auto
moreover have "∀t∈set ?ss2. is_Var t" unfolding drop_map by auto
ultimately have is_Var: "∀t∈set (?ss1@?ss2). is_Var t" by auto
have dist: "distinct(?ss1@?ss2)" using distinct_take_drop[OF dist,unfolded len,OF ‹i < m›]
unfolding take_map drop_map map_append[symmetric] by (rule distinct_map_Var)
with fresh C' F is_Var dist show ?thesis by auto
qed
fun is_flat_ctxt :: "'v set ⇒ ('f × nat) set ⇒ ('f, 'v) ctxt ⇒ bool" where
"is_flat_ctxt V F (More f ss1 □ ss2) = (
(f, Suc (length (ss1 @ ss2))) ∈ F
∧ (∀s∈set (ss1 @ ss2). is_Var s)
∧ distinct (ss1 @ ss2)
∧ vars_ctxt (More f ss1 □ ss2) ∩ V = {}
)"
| "is_flat_ctxt V F _ = False"
lemma is_flat_ctxt_union: "is_flat_ctxt (V ∪ W) F C = (is_flat_ctxt V F C ∧ is_flat_ctxt W F C)"
proof (cases C)
case Hole
show ?thesis unfolding Hole by simp
next
case (More f bef D aft)
show ?thesis unfolding More by (cases D, auto)
qed
lemma is_flat_ctxt_cases[consumes 1,case_names True]:
assumes "is_flat_ctxt V F C"
and "⋀f ss1 ss2. C = More f ss1 □ ss2 ⟹ P"
shows "P"
using assms(1) proof (cases rule: is_flat_ctxt.cases[of "(V,F,C)"])
case (1 V' F' f ss1 ss2)
hence "C = More f ss1 □ ss2" by simp
with assms(2) show ?thesis by auto
next
case ("2_1" V' F') with assms(1) show ?thesis by simp
next
case ("2_2" V' F' f ss1 g ts1 D ts2 ss2) with assms(1) show ?thesis by simp
qed
lemma is_flat_ctxt_imp_flat_ctxt:
assumes "is_flat_ctxt V F C"
shows "vars_ctxt C ∩ V = {} ∧ (∃f ss1 ss2. C = More f ss1 □ ss2
∧ (f, Suc (length(ss1 @ ss2))) ∈ F
∧ (∀s∈set (ss1 @ ss2). is_Var s)
∧ distinct (ss1 @ ss2))"
using assms by (cases rule: is_flat_ctxt_cases, auto)
lemma subst_extend_flat_ctxt':
assumes dist: "distinct(vs1@vs2)"
and len1: "length vs1 = length ss1"
and len2: "length vs2 = length ss2"
shows "More f (map Var vs1) □ (map Var vs2) ⋅⇩c subst_extend σ (zip (vs1@vs2) (ss1@ss2)) = More f ss1 □ ss2"
proof -
let ?V = "map Var (vs1@vs2)"
let ?vs1 = "vs1" and ?vs2 = "vs2"
let ?ss1 = "map Var vs1" and ?ss2 = "map Var vs2"
let ?σ = "subst_extend σ (zip (?vs1@?vs2) (ss1@ss2))"
from len1 and len2 have len: "length(?vs1@?vs2) = length(ss1@ss2)" by simp
from subst_extend_absorb[OF dist len,of "σ"] have map: "map (λt. t⋅?σ) (?ss1@?ss2) = ss1@ss2" unfolding map_append .
from len1 and map have "map (λt. t⋅?σ) ?ss1 = ss1" by auto
moreover from len2 and map have "map (λt. t⋅?σ) ?ss2 = ss2" by auto
ultimately show ?thesis by simp
qed
lemma partial_fcc_sig_step:
assumes flat_ctxts: "∀C∈fcs. is_flat_ctxt (vars_trs R) F C"
and complete: "∀(f, n)∈F. ∀i<n. ∃ss1 ss2. (More f ss1 □ ss2) ∈ fcs ∧ length ss1 = i ∧
length ss2 = n - i - 1"
and subset: "funas_trs R ⊆ F"
and C: "C ∈ fcs"
and pres: "∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀C∈fcs. Bex R' (instance_rule (C⟨l⟩, C⟨r⟩)))"
and step: "(s,t) ∈ sig_step F (rstep R)"
shows "(C⟨s⟩,C⟨t⟩) ∈ rstep R'"
proof -
let ?r = "sig_step F (rstep R)"
let ?c = "rstep R'"
from sig_stepE[OF step] subset
have rstep: "(s,t) ∈ rstep R" and wfs: "funas_term s ⊆ F"
and wft: "funas_term t ⊆ F" by auto
from rstep_imp_C_s_r[OF rstep] obtain D σ l r where R: "(l,r) ∈ R"
and s: "s = D⟨l⋅σ⟩" and t: "t = D⟨r⋅σ⟩" by auto
have vl: "vars_term l ⊆ vars_trs R"
using R unfolding vars_trs_def vars_rule_def [abs_def] by auto
have vr: "vars_term r ⊆ vars_trs R"
using R unfolding vars_trs_def vars_rule_def [abs_def] by auto
from flat_ctxts[THEN bspec[where x=C],OF C] have distinct: "vars_ctxt C ∩ vars_trs R = {}"
using is_flat_ctxt_imp_flat_ctxt by best
from R pres have "(Bex R' (instance_rule (l,r))) ∨ (∀C∈fcs. Bex R' (instance_rule (C⟨l⟩,C⟨r⟩)))" by auto
thus "(C⟨s⟩,C⟨t⟩) ∈ ?c"
proof
assume bex: "Bex R' (instance_rule (l,r))"
have "(D⟨l⋅σ⟩,D⟨r⋅σ⟩) ∈ rstep {(l,r)}" by auto
hence "(D⟨l⋅σ⟩,D⟨r⋅σ⟩) ∈ ?c"
by (rule instance_rule_rstep[OF _ bex])
from rstep.ctxt[OF this] show ?thesis unfolding s t by simp
next
assume closed: "∀C∈fcs. Bex R' (instance_rule (C⟨l⟩,C⟨r⟩))"
show ?thesis
proof (cases D rule: ctxt_exhaust_rev)
case Hole
let ?σ = "σ |s (vars_trs R)"
from C and closed have inst: "Bex R' (instance_rule (C⟨l⟩,C⟨r⟩))" by auto
have "(C⟨l⟩⋅?σ,C⟨r⟩⋅?σ) ∈ ?c"
by (rule instance_rule_rstep[OF _ inst], blast)
hence mem: "((C ⋅⇩c ?σ)⟨l⋅?σ⟩, (C ⋅⇩c ?σ)⟨r⋅?σ⟩) ∈ ?c" by simp
have "l ⋅ ?σ = l ⋅ σ" and "r ⋅ ?σ = r ⋅ σ"
unfolding term_subst_eq_conv using vl vr unfolding subst_restrict_def
by auto
with mem have "((C ⋅⇩c ?σ)⟨l⋅σ⟩, (C ⋅⇩c ?σ)⟨r⋅σ⟩) ∈ ?c" by auto
thus ?thesis unfolding subst_apply_ctxt_id[OF distinct] unfolding s t Hole by simp
next
case (More E f ss1 ss2)
from wfs[unfolded s]
have D: "funas_ctxt D ⊆ F" and "funas_term (l⋅σ) ⊆ F" by auto
from D[unfolded More]
have "funas_ctxt E ⊆ F" and "funas_ctxt (More f ss1 □ ss2) ⊆ F" by auto
hence F: "(f,Suc(length(ss1@ss2))) ∈ F" (is "(f,?n) ∈ _")
by auto
have len: "length ss1 < ?n" (is "?i < _") by simp
from complete[THEN bspec[where x="(f,?n)"],OF F] len
obtain ts1 ts2 where C': "More f ts1 □ ts2 ∈ fcs" (is "?C' ∈ fcs")
and "length ts1 = ?i" and "length ts2 = ?n - ?i - 1" by best
note inst = instance_rule_rstep[OF _ closed[THEN bspec[OF _ C']]]
have len_ss1: "length ss1 = length ts1" using ‹length ts1 = ?i› by simp
have len_ss2: "length ss2 = length ts2" using ‹length ts2 = ?n - ?i - 1› by simp
have len_ss1ss2: "length(ss1@ss2) = length(ts1@ts2)" using len_ss1 len_ss2 by simp
let ?V = "map the_Var (ts1@ts2)"
let ?σ = "subst_extend σ (zip ?V (ss1@ss2))"
from is_flat_ctxt_imp_flat_ctxt[OF flat_ctxts[THEN bspec,OF C']]
have is_Var: "∀t∈set (ts1 @ ts2). is_Var t"
and fresh: "vars_ctxt ?C' ∩ vars_trs R = {}" by auto
have vars_C': "vars_ctxt ?C' = set ?V" using terms_to_vars[OF is_Var] by simp
from fresh have fresh: "vars_trs R ∩ set ?V = {}" unfolding vars_C' by auto
from is_flat_ctxt_imp_flat_ctxt[OF flat_ctxts[THEN bspec,OF C']]
have "∀t∈set (ts1 @ ts2). is_Var t" and "distinct(ts1@ts2)" by auto
hence "distinct ?V" by (rule distinct_the_vars)
hence dist: "distinct(map the_Var ts1 @ map the_Var ts2)" by simp
have len1: "length(map the_Var ts1) = length ss1" unfolding len_ss1 by simp
have len2: "length(map the_Var ts2) = length ss2" unfolding len_ss2 by simp
from is_Var have "∀t∈set ts1. is_Var t" by simp
hence id1: "map Var (map the_Var ts1) = ts1" by (rule Var_the_Var_id)
from is_Var have "∀t∈set ts2. is_Var t" by simp
hence id2: "map Var (map the_Var ts2) = ts2" by (rule Var_the_Var_id)
have Cl: "(?C'⟨l⟩)⋅?σ = (More f ss1 □ ss2)⟨l⋅σ⟩"
unfolding subst_apply_term_ctxt_apply_distrib subst_extend_id[OF fresh vl,of σ]
unfolding map_append subst_extend_flat_ctxt'[OF dist len1 len2,unfolded id1 id2] by simp
have Cr: "(?C'⟨r⟩)⋅?σ = (More f ss1 □ ss2)⟨r⋅σ⟩"
unfolding subst_apply_term_ctxt_apply_distrib subst_extend_id[OF fresh vr,of σ]
unfolding map_append subst_extend_flat_ctxt'[OF dist len1 len2,unfolded id1 id2] by simp
let ?C'' = "More f ss1 □ ss2"
have "(?C''⟨l⋅σ⟩,?C''⟨r⋅σ⟩) ∈ ?c"
by (rule inst, unfold Cl[symmetric] Cr[symmetric], blast)
from ctxt.closure.intros[OF this,of E] have "(E⟨?C''⟨l⋅σ⟩⟩,E⟨?C''⟨r⋅σ⟩⟩) ∈ ?c" by simp
from ctxt.closure.intros[OF this,of C] have "(C⟨E⟨?C''⟨l⋅σ⟩⟩⟩,C⟨E⟨?C''⟨r⋅σ⟩⟩⟩) ∈ ?c" by simp
thus ?thesis unfolding s t More by simp
qed
qed
qed
lemma partial_fcc_reflects_SN_rel: fixes R S R' S' :: "('f,'v)trs"
assumes flat_ctxts: "∀C∈fcs. is_flat_ctxt (vars_trs (R ∪ S)) F C"
and complete: "∀(f, n)∈F. ∀i<n. ∃ss1 ss2. (More f ss1 □ ss2) ∈ fcs ∧ length ss1 = i ∧
length ss2 = n - i - 1"
and F: "funas_trs (R ∪ S) ⊆ F"
and ne: "fcs ≠ {}"
and presR: "∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀C∈fcs. Bex R' (instance_rule (C⟨l⟩, C⟨r⟩)))"
and presS: "∀(l, r)∈S. (Bex (R' ∪ S') (instance_rule (l, r))) ∨ (∀C∈fcs. Bex (R' ∪ S') (instance_rule (C⟨l⟩, C⟨r⟩)))"
and SN: "SN_rel (rstep R') (rstep S')"
shows "SN_rel (rstep R) (rstep S)"
proof -
from ne obtain C where C: "C ∈ fcs" by auto
let ?r = "sig_step F (rstep R)"
let ?s = "sig_step F (rstep S)"
let ?r' = "rstep R'"
let ?s' = "rstep S'"
let ?c = "λ t. C⟨t⟩"
note fcc = partial_fcc_sig_step[OF _ complete _ C]
from F have FR: "funas_trs R ⊆ F" and FS: "funas_trs S ⊆ F" by auto
have relSN: "SN_rel (?r) (?s)"
proof (rule SN_rel_map[OF SN, of _ ?c])
fix s t
assume step: "(s,t) ∈ ?r"
from flat_ctxts have flat_ctxt: "∀ C ∈ fcs. is_flat_ctxt (vars_trs R) F C"
unfolding vars_trs_union is_flat_ctxt_union by auto
from F have F: "funas_trs R ⊆ F" by auto
have "(?c s, ?c t) ∈ ?r'"
by (rule fcc[OF flat_ctxt F presR step])
thus "(?c s, ?c t) ∈ (?r' ∪ ?s')^* O ?r' O (?r' ∪ ?s')^*" by auto
next
fix s t
assume "(s,t) ∈ ?s"
hence step: "(s,t) ∈ sig_step F (rstep (R ∪ S))" unfolding rstep_union sig_step_def by auto
have "(?c s, ?c t) ∈ rstep (R' ∪ S')"
by (rule fcc[OF flat_ctxts F _ step], insert presR presS, force)
thus "(?c s, ?c t) ∈ (?r' ∪ ?s')^*" unfolding rstep_union by auto
qed
show ?thesis
proof (cases "R = {}")
case True
thus ?thesis by (simp add: SN_rel_defs)
next
case False
with presR C have ne: "R' ≠ {}" by auto
with SN_rel_imp_wf_reltrs[OF SN] have
varcond: "⋀ l r. (l,r) ∈ R' ∪ S' ⟹ vars_term r ⊆ vars_term l" by (force simp: wf_trs_def)
show ?thesis
proof (rule sig_ext_relative_rewriting_var_cond[OF _ FR FS relSN])
fix l r
assume lr: "(l,r) ∈ S"
from presS[rule_format, OF lr, unfolded split]
show "vars_term r ⊆ vars_term l"
proof
assume "Bex (R' ∪ S') (instance_rule (l, r))"
then obtain l' r' σ where mem: "(l',r') ∈ R' ∪ S'" and lr: "l = l' ⋅ σ" "r = r' ⋅ σ"
by (force simp: instance_rule_def)
from varcond[OF mem] show ?thesis unfolding lr by (auto simp: vars_term_subst)
next
assume "∀C∈fcs. Bex (R' ∪ S') (instance_rule (C⟨l⟩, C⟨r⟩))"
with C obtain l' r' where mem: "(l',r') ∈ R' ∪ S'"
and inst: "instance_rule (C⟨l⟩, C⟨r⟩) (l',r')" by force
from inst[unfolded instance_rule_def] obtain σ where id: "C⟨l⟩ = l' ⋅ σ" "C⟨r⟩ = r' ⋅ σ" by auto
from varcond[OF mem] have vars: "vars_term r' ⊆ vars_term l'" .
from flat_ctxts[rule_format,OF C] have distinct: "vars_ctxt C ∩ vars_trs (R ∪ S) = {}"
using is_flat_ctxt_imp_flat_ctxt by best
show ?thesis
proof
fix x
assume x: "x ∈ vars_term r"
hence "x ∈ vars_term C⟨r⟩" unfolding vars_term_ctxt_apply by auto
with vars id have "x ∈ vars_term C⟨l⟩" by (auto simp: vars_term_subst)
hence xx: "x ∈ vars_ctxt C ∪ vars_term l" unfolding vars_term_ctxt_apply .
from x lr have "x ∈ vars_trs (R ∪ S)"
unfolding vars_trs_def vars_rule_def [abs_def] by force
with distinct xx show "x ∈ vars_term l" by auto
qed
qed
qed
qed
qed
lemma flat_ctxt_is_flat:
assumes fin: "finite V" and fc: "C ∈ flat_ctxts V F"
shows "is_flat_ctxt V F C"
using fc_flat[OF fc fin] by auto
lemma fcc_reflects_SN_rel:
assumes finite: "finite (R ∪ S)"
and subset: "funas_trs (R ∪ S) ⊆ G"
and ne: "flat_ctxts (vars_trs (R ∪ S)) G ≠ {}" (is "?fcs ≠ {}")
and SN: "SN_rel (rstep(FC G R)) (rstep (FC G S))"
shows "SN_rel (rstep R) (rstep S)"
proof -
from finite have fin: "finite(vars_trs (R ∪ S))"
unfolding vars_trs_def vars_rule_def [abs_def] by auto
have fcs: "∀C∈?fcs. is_flat_ctxt (vars_trs (R ∪ S)) G C" using flat_ctxt_is_flat[OF fin] by best
have complete: "∀(f,n)∈G.∀i<n.∃ss1 ss2. More f ss1 □ ss2 ∈ ?fcs ∧ length ss1 = i ∧ length ss2 = n - i - 1"
proof (intro ballI2 allI impI)
fix f n i
let ?V = "map Var (fresh_vars n (vars_trs (R ∪ S)))"
assume "(f,n) ∈ G" and "i < n"
hence "flat_ctxt_i ?V f i ∈ ?fcs" unfolding flat_ctxts_def by auto
hence "More f (take i ?V) □ (drop (Suc i) ?V) ∈ ?fcs" (is "More f ?ss1 □ ?ss2 ∈ _") unfolding flat_ctxt_i_def by auto
moreover have "length ?ss1 = i" using fresh_vars_length[OF fin,of n] ‹i < n› by simp
moreover have "length ?ss2 = n - i - 1" using fresh_vars_length[OF fin,of n] ‹i < n› by simp
ultimately show "∃ss1 ss2. More f ss1 □ ss2 ∈ ?fcs ∧ length ss1 = i ∧ length ss2 = n - i - 1" by best
qed
from partial_fcc_reflects_SN_rel[OF fcs complete subset ne _ _ SN]
fcc_imp_pres show ?thesis oops
lemma fcc_ne_imp_funs_ne:
assumes ne: "flat_ctxts V (funas_trs R) ≠ {}"
shows "funs_trs R ≠ {}"
proof -
from ne have "funas_trs R ≠ {}" unfolding flat_ctxts_def by auto
then obtain l r where R: "(l,r) ∈ R" and "funas_term l ∪ funas_term r ≠ {}"
unfolding funas_rule_def [abs_def] funas_trs_def by force
hence "funas_term l ≠ {} ∨ funas_term r ≠ {}" by simp
thus "funs_trs R ≠ {}"
proof
assume "funas_term l ≠ {}"
then obtain f ss where "l = Fun f ss" by (induct l) auto
hence "f ∈ funs_term l" by simp
with R show ?thesis unfolding funs_trs_def funs_rule_def [abs_def] by force
next
assume "funas_term r ≠ {}"
then obtain f ss where "r = Fun f ss" by (induct r) auto
hence "f ∈ funs_term r" by simp
with R show ?thesis unfolding funs_trs_def funs_rule_def [abs_def] by force
qed
qed
fun hole_at where
"hole_at n i f (More g ss1 □ ss2) = (g = f ∧ length ss1 = i ∧ length ss2 = n - i - 1)"
| "hole_at n i f _ = False"
fun has_unary_root :: "'f ⇒ ('f, 'v) term ⇒ bool" where
"has_unary_root f (Fun g [t]) = (f = g)"
| "has_unary_root f t = False"
fun strip_unary_root :: "'f ⇒ ('f, 'v) term ⇒ ('f, 'v) term" where
"strip_unary_root f (Fun g [t]) = (if f = g then t else Fun g [t])"
| "strip_unary_root f t = t"
fun block_term :: "'f ⇒ ('f, 'v) term ⇒ ('f, 'v) term" where
"block_term f (Var x) = Var x"
| "block_term f (Fun g ts) = Fun g (map (λt. Fun f [t]) ts)"
definition block_rule :: "'f ⇒ ('f, 'v) rule ⇒ ('f, 'v) rule" where
"block_rule f r = (block_term f (fst r), block_term f (snd r))"
fun unblock_term :: "'f ⇒ ('f, 'v) term ⇒ ('f, 'v) term" where
"unblock_term f (Fun g ts) = (if ∀t∈set ts. has_unary_root f t
then Fun g (map (strip_unary_root f) ts)
else Fun g ts)"
| "unblock_term f t = t"
lemma [simp]: "strip_unary_root f ∘ (λt. Fun f [t]) = id"
by (rule ext) (simp add: o_def)
lemma unblock_block_term_ident[simp]: "unblock_term f (block_term f t) = t"
by (cases t) (simp_all)
definition unblock_rule :: "'f ⇒ ('f, 'v) rule ⇒ ('f, 'v) rule" where
"unblock_rule f r ≡ (unblock_term f (fst r), unblock_term f (snd r))"
lemma subst_apply_term_block_term_distrib[simp]:
assumes "is_Fun t"
shows "block_term f t ⋅ σ = block_term f (t ⋅ σ)"
using assms by (cases t) simp_all
lemma blocked_rstep_imp_rstep:
assumes refl: "∀(l, r)∈R'. ∃(u, v)∈R. ∃C∈set (□ # fcs). l = C⟨u⟩ ∧ r = C⟨v⟩"
and rstep: "(s, t) ∈ rstep R'"
shows "(s, t) ∈ rstep R"
proof -
from rstep obtain C l r σ where "(l, r) ∈ R'"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by auto
from refl and ‹(l, r) ∈ R'›
have "(l, r) ∈ R ∨ (∃(u, v)∈R. ∃C∈set fcs. l = C⟨u⟩ ∧ r = C⟨v⟩)" by auto
thus ?thesis
proof
assume "(l, r) ∈ R" thus "(s, t) ∈ rstep R" unfolding s t by auto
next
assume "∃(u, v)∈R. ∃C∈set fcs. l = C⟨u⟩ ∧ r = C⟨v⟩"
then obtain u v D where "(u, v) ∈ R" and "D ∈ set fcs" and l: "l = D⟨u⟩" and r: "r = D⟨v⟩" by auto
let ?C = "C ∘⇩c (D ⋅⇩c σ)"
have s': "s = ?C⟨u⋅σ⟩" unfolding s l by simp
have t': "t = ?C⟨v⋅σ⟩" unfolding t r by simp
from ‹(u, v) ∈ R› show "(s, t) ∈ rstep R" unfolding s' t' by best
qed
qed
lemma unary_flat_ctxts:
assumes "(f, Suc 0) ∈ F"
shows "More f [] □ [] ∈ flat_ctxts V F"
proof -
let ?xs = "map Var (fresh_vars (Suc 0) V)"
have "flat_ctxt_i ?xs f 0 = More f [] □ []"
unfolding flat_ctxt_i_def fresh_vars_def fresh_strings_def by simp
with assms show ?thesis unfolding flat_ctxts_def by force
qed
lemma flat_ctxts_funas:
fixes n::nat and V::"string set"
defines "xs ≡ map Var (fresh_vars n V)"
assumes "(f, n) ∈ F"
shows "∀i<n. More f (take i xs) □ (drop (Suc i) xs) ∈ flat_ctxts V F"
proof (intro allI impI)
fix i assume "i < n"
hence "flat_ctxt_i xs f i = More f (take i xs) □ (drop (Suc i) xs)"
unfolding flat_ctxt_i_def xs_def by simp
with ‹i < n›
have "More f (take i xs) □ (drop (Suc i) xs) ∈ {flat_ctxt_i xs f i | i. i ∈ {0..<n}}"
unfolding xs_def by force
with assms show "More f (take i xs) □ (drop (Suc i) xs) ∈ flat_ctxts V F"
unfolding flat_ctxts_def xs_def by force
qed
lemma rstep_imp_blocked_rstep_union:
assumes "wf_trs (R ∪ Rw)"
and flat_ctxts: "∀C∈fcs. is_flat_ctxt (vars_trs (R ∪ Rw)) F C"
and complete: "∀(f, n)∈F. ∀i<n. ∃ss1 ss2.
(More f ss1 □ ss2) ∈ fcs ∧ length ss1 = i ∧ length ss2 = n - i - 1"
and "funas_args_term s ⊆ funas_trs (R ∪ Rw) ∪ funas_args_trs P"
and "funas_trs (R ∪ Rw) ∪ funas_args_trs P ⊆ F"
and "(f, Suc 0) ∈ F"
and "¬ defined (R ∪ Rw) (the(root s))"
and "(s, t) ∈ rstep R"
and pres: "∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀E∈fcs. Bex R' (instance_rule (E⟨l⟩, E⟨r⟩)))"
shows "¬ defined (R ∪ Rw) (the(root t)) ∧ funas_args_term t ⊆ funas_trs (R ∪ Rw) ∪ funas_args_trs P
∧ (block_term f s, block_term f t) ∈ rstep R'" (is "_ ∧ _ ∧ (?s, ?t) ∈ rstep R'")
proof -
let ?R = "R ∪ Rw"
from ‹(s, t) ∈ rstep R› obtain C l r σ where "(l, r) ∈ R"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
from ‹wf_trs ?R› and ‹(l, r) ∈ R› obtain g ls
where l: "l = Fun g ls" by (cases l) (auto simp: wf_trs_def)
show ?thesis
proof (cases C)
case Hole
have "the(root s) = (g, length ls)" by (simp add: s l Hole)
with ‹(l, r) ∈ R› l Hole s have "defined ?R (the(root s))" by (auto simp: defined_def l)
with assms show ?thesis by simp
next
case (More h ss1 D ss2)
note C = this
let ?block_list = "map (λt. Fun f [t])"
let ?ss1 = "?block_list ss1"
let ?ss2 = "?block_list ss2"
let ?D = "More h ?ss1 (More f [] D []) ?ss2"
have s': "?s = ?D⟨l⋅σ⟩" by (simp add: s More)
have t': "?t = ?D⟨r⋅σ⟩" by (simp add: t More)
have "the (root s) = (h, num_args s)" unfolding s More by simp
moreover have "the(root t) = (h, num_args t)" unfolding t More by simp
moreover have "num_args s = num_args t" unfolding s t More by simp
ultimately have no_def: "¬ defined ?R (the (root t))" using assms by simp
have funas_args: "funas_args_term t ⊆ funas_trs ?R ∪ funas_args_trs P"
proof -
have "funas_args_term t = ⋃(set (map funas_term (ss1 @ (D⟨r ⋅ σ⟩) # ss2 )))"
unfolding t More funas_args_term_def by simp
moreover have "funas_term (D⟨r ⋅ σ⟩) ⊆ funas_trs ?R ∪ funas_args_trs P"
proof -
from ‹funas_args_term s ⊆ funas_trs ?R ∪ funas_args_trs P›
have fs: "funas_term (D⟨l ⋅ σ⟩) ⊆ funas_trs ?R ∪ funas_args_trs P"
unfolding s C funas_args_term_def by simp
from fs
have "(⋃x∈vars_term l. funas_term (Var x ⋅ σ)) ⊆ funas_trs ?R ∪ funas_args_trs P"
unfolding funas_term_subst funas_term_ctxt_apply by simp
moreover from ‹(l, r) ∈ R› and ‹wf_trs ?R›
have "vars_term r ⊆ vars_term l" unfolding wf_trs_def by simp
ultimately
have "(⋃x∈vars_term r. funas_term (Var x ⋅ σ)) ⊆ funas_trs ?R ∪ funas_args_trs P"
by auto
moreover from ‹(l, r) ∈ R› have "funas_term r ⊆ funas_trs ?R"
unfolding funas_defs [abs_def] by auto
ultimately have "funas_term (r ⋅ σ) ⊆ funas_trs ?R ∪ funas_args_trs P"
unfolding funas_term_subst by auto
moreover from fs have "funas_ctxt D ⊆ funas_trs ?R ∪ funas_args_trs P"
unfolding s More funas_term_ctxt_apply by simp
ultimately show ?thesis unfolding funas_term_ctxt_apply by simp
qed
ultimately show ?thesis using ‹funas_args_term s ⊆ funas_trs ?R ∪ funas_args_trs P›
unfolding s C funas_args_term_def by simp
qed
from bspec[OF pres ‹(l, r) ∈ R›, unfolded split_def fst_conv snd_conv] show ?thesis
proof
assume inst: "Bex R' (instance_rule (l, r))"
have "(block_term f s, block_term f t) ∈ rstep {(l,r)}"
unfolding s' t' by best
from instance_rule_rstep[OF this inst]
show ?thesis using no_def funas_args by auto
next
assume flat_ctxt: "∀E∈fcs. Bex R' (instance_rule (E⟨l⟩, E⟨r⟩))"
show ?thesis
proof (cases D rule: ctxt_exhaust_rev)
case Hole
let ?E = "More f [] □ []"
let ?F = "More h ?ss1 □ ?ss2"
from ‹(f, Suc 0) ∈ F› and complete
have "More f [] □ [] ∈ fcs" by auto
with flat_ctxt
have inst: "Bex R' (instance_rule (?E⟨l⟩, ?E⟨r⟩))" by best
have "((?E⟨l⟩)⋅σ, (?E⟨r⟩)⋅σ) ∈ rstep R'"
by (rule instance_rule_rstep[OF _ inst], blast)
hence "(?E⟨l⋅σ⟩, ?E⟨r⋅σ⟩) ∈ rstep R'" by simp
from rstep.ctxt[OF this]
have "(?F⟨?E⟨l⋅σ⟩⟩, ?F⟨?E⟨r⋅σ⟩⟩) ∈ rstep R'" .
hence "(?s, ?t) ∈ rstep R'" unfolding s' t' Hole by simp
with no_def and funas_args show ?thesis by simp
next
case (More D' f' ss1' ss2')
let ?n = "Suc (length (ss1' @ ss2'))"
let ?i = "length ss1'"
from ‹(l, r) ∈ R›
have vl: "vars_term l ⊆ vars_trs R"
and vr: "vars_term r ⊆ vars_trs R"
unfolding vars_defs [abs_def] by auto
from vl have l_subst_R: "l ⋅ (σ |s vars_trs R) = l ⋅ σ"
unfolding term_subst_eq_conv subst_restrict_def by auto
from vr have r_subst_R: "r ⋅ (σ |s vars_trs R) = r ⋅ σ"
unfolding term_subst_eq_conv subst_restrict_def by auto
from ‹funas_args_term s ⊆ funas_trs ?R ∪ funas_args_trs P›
and ‹funas_trs ?R ∪ funas_args_trs P ⊆ F›
have "funas_args_term s ⊆ F" by blast
hence in_F: "(f', ?n) ∈ F"
unfolding funas_args_term_def s C More by simp
have "?i < ?n" by simp
with in_F and complete obtain ss1 ss2 where "More f' ss1 □ ss2 ∈ fcs" (is "?G ∈ _")
and "length ss1 = ?i" and "length ss2 = ?n - ?i - 1" by best
with flat_ctxt have in_R': "Bex R' (instance_rule (?G⟨l⟩, ?G⟨r⟩))" by best
from flat_ctxts and ‹?G ∈ fcs› have "is_flat_ctxt (vars_trs ?R) F ?G" by best
from is_flat_ctxt_imp_flat_ctxt[OF this]
have dist_vars: "vars_ctxt ?G ∩ vars_trs ?R = {}"
and "(f', Suc (length (ss1 @ ss2))) ∈ F"
and all_vars: "∀s∈set (ss1 @ ss2). is_Var s"
and "distinct (ss1 @ ss2)" by auto
let ?ss1' = "map the_Var ss1"
let ?ss2' = "map the_Var ss2"
from all_vars have "∀s∈set ss1. is_Var s" by simp
from all_vars have "∀s∈set ss2. is_Var s" by simp
from dist_vars have "⋃(set (map vars_term ss1)) ∩ vars_trs ?R = {}" by auto
with ‹∀s∈set ss1. is_Var s› have "set ?ss1' ∩ vars_trs ?R = {}" by (induct ss1) auto
moreover from dist_vars have "⋃(set (map vars_term ss2)) ∩ vars_trs ?R = {}" by auto
with ‹∀s∈set ss2. is_Var s› have "set ?ss2' ∩ vars_trs ?R = {}" by (induct ss2) auto
ultimately have fresh: "vars_trs ?R ∩ set(?ss1' @ ?ss2') = {}" by auto
hence fresh: "vars_trs R ∩ set(?ss1' @ ?ss2') = {}" unfolding vars_trs_def by auto
from Var_the_Var_id[OF all_vars]
have "map Var (map the_Var (ss1 @ ss2)) = ss1 @ ss2" .
from distinct_the_vars[OF all_vars ‹distinct (ss1 @ ss2)›]
have "distinct (map the_Var (ss1 @ ss2))" .
hence dist: "distinct (?ss1' @ ?ss2')" by simp
have len1: "length ?ss1' = length ss1'" using ‹length ss1 = ?i› by simp
have len2: "length ?ss2' = length ss2'" using ‹length ss2 = ?n - ?i - 1› by simp
let ?σ = "subst_extend σ (zip (?ss1' @ ?ss2') (ss1' @ ss2'))"
let ?E' = "More f' ss1' □ ss2'"
have G_l_substex: "?E'⟨l ⋅ σ⟩ = (?G⟨l⟩) ⋅ ?σ"
unfolding subst_apply_term_ctxt_apply_distrib
unfolding subst_extend_id[OF fresh vl]
using subst_extend_flat_ctxt'[OF dist len1 len2]
unfolding Var_the_Var_id[OF ‹∀s∈set ss1. is_Var s›]
unfolding Var_the_Var_id[OF ‹∀s∈set ss2. is_Var s›] by simp
have G_r_substex: "?E'⟨r ⋅ σ⟩ = (?G⟨r⟩) ⋅ ?σ"
unfolding subst_apply_term_ctxt_apply_distrib
unfolding subst_extend_id[OF fresh vr]
using subst_extend_flat_ctxt'[OF dist len1 len2]
unfolding Var_the_Var_id[OF ‹∀s∈set ss1. is_Var s›]
unfolding Var_the_Var_id[OF ‹∀s∈set ss2. is_Var s›] by simp
have "(?E'⟨l ⋅ σ⟩, ?E'⟨r ⋅ σ⟩) ∈ rstep R'"
unfolding G_l_substex G_r_substex
by (rule instance_rule_rstep[OF _ in_R'], blast)
from rstep.ctxt[OF this, of D']
have "(D⟨l ⋅ σ⟩, D⟨r ⋅ σ⟩) ∈ rstep R'"
unfolding More by simp
from rstep.ctxt[OF this, of "More h ?ss1 (More f [] □ []) ?ss2"]
have "(?s, ?t) ∈ rstep R'" unfolding s t C by simp
with no_def and funas_args show ?thesis by simp
qed
qed
qed
qed
lemma rstep_imp_blocked_rstep:
assumes "wf_trs R"
and flat_ctxts: "∀C∈fcs. is_flat_ctxt (vars_trs R) F C"
and complete: "∀(f, n)∈F. ∀i<n. ∃ss1 ss2.
(More f ss1 □ ss2) ∈ fcs ∧ length ss1 = i ∧ length ss2 = n - i - 1"
and "funas_args_term s ⊆ funas_trs R ∪ funas_args_trs P"
and "funas_trs R ∪ funas_args_trs P ⊆ F"
and "(f, Suc 0) ∈ F"
and "¬ defined R (the(root s))"
and "(s, t) ∈ rstep R"
and pres: "∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀E∈fcs. Bex R' (instance_rule (E⟨l⟩, E⟨r⟩)))"
shows "¬ defined R (the(root t)) ∧ funas_args_term t ⊆ funas_trs R ∪ funas_args_trs P
∧ (block_term f s, block_term f t) ∈ rstep R'"
using assms rstep_imp_blocked_rstep_union[of R "{}" fcs F s P f t R']
by auto
lemma rseq_imp_blocked_rseq:
assumes "wf_trs R"
and flat_ctxts: "∀C∈fcs. is_flat_ctxt (vars_trs R) F C"
and complete: "∀(f, n)∈F. ∀i<n. ∃ss1 ss2.
(More f ss1 □ ss2) ∈ fcs ∧ length ss1 = i ∧ length ss2 = n - i - 1"
and "funas_args_term s ⊆ funas_trs R ∪ funas_args_trs P"
and "funas_trs R ∪ funas_args_trs P ⊆ F"
and "(f, Suc 0) ∈ F"
and "¬ defined R (the (root s))"
and "(s, t) ∈ (rstep R)^*"
and pres: "∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀E∈fcs. Bex R' (instance_rule (E⟨l⟩, E⟨r⟩)))"
shows "¬ defined R (the (root t)) ∧ funas_args_term t ⊆ funas_trs R ∪ funas_args_trs P
∧ (block_term f s, block_term f t) ∈ (rstep R')^*"
using ‹(s, t) ∈ (rstep R)^*›
and ‹funas_args_term s ⊆ funas_trs R ∪ funas_args_trs P›
and ‹¬ defined R (the (root s))›
proof (induct rule: rtrancl_induct)
case base thus ?case by simp
next
case (step y z)
with rstep_imp_blocked_rstep[OF ‹wf_trs R› flat_ctxts complete
_ ‹funas_trs R ∪ funas_args_trs P ⊆ F› ‹(f, Suc 0) ∈ F› _ _ pres, of y z]
have "¬ defined R (the (root z)) ∧ funas_args_term z ⊆ funas_trs R ∪ funas_args_trs P
∧ (block_term f y, block_term f z) ∈ rstep R'
∧ (block_term f s, block_term f y) ∈ (rstep R')^*" by simp
thus ?case by auto
qed
lemma funas_args_term_Fun:
"funas_args_term (Fun f ts ⋅ σ) = (⋃t∈set ts. funas_term (t ⋅ σ))"
unfolding funas_args_term_def by auto
lemma funas_args_term_subst_apply:
assumes "is_Fun t"
shows "funas_args_term (t ⋅ σ) = (⋃t∈set (args t). funas_term (t ⋅ σ))"
proof -
from assms obtain f ts where t: "t = Fun f ts" by (cases t) auto
show ?thesis using funas_args_term_Fun unfolding t by simp
qed
lemma block_subst_Fun:
"block_term f (Fun g us ⋅ σ) = (block_term f (Fun g us)) ⋅ σ"
by simp
lemma num_args_block_term[simp]:
"num_args (block_term f t) = num_args t"
by (induct t) simp_all
lemma blocked_rstep_imp_rstep':
assumes "wf_trs R"
and "¬ defined R (f, 1)"
and "¬ defined R (the (root s))"
and "(block_term f s, block_term f t) ∈ rstep R" (is "(?s, ?t) ∈ _")
shows "¬ defined R (the (root t)) ∧ (s, t) ∈ rstep R"
proof -
from NF_Var[OF ‹wf_trs R›] and assms obtain g ss where s: "s = Fun g ss" by (induct s) auto
hence s': "?s = Fun g (map (λt. Fun f [t]) ss)" by simp
from assms have "¬ defined R (g, length ss)" unfolding s by simp
from ‹wf_trs R› and ‹(?s, ?t) ∈ rstep R›[unfolded s'] show ?thesis
proof (cases rule: rstep_cases_Fun')
case (root ls r σ)
from arg_cong[where f = length, OF this(2)]
have id: "length ss = length ls" by auto
from ‹¬ defined R (g, length ss)› show ?thesis unfolding defined_def id using root by force
next
case (nonroot i u)
from ‹i < length (map (λt. Fun f [t]) ss)› have "i < length ss" by simp
from id_take_nth_drop[OF this] have ss: "take i ss @ (ss!i) # drop (Suc i) ss = ss" ..
let ?C = "More g (take i ss) □ (drop (Suc i) ss)"
from nonroot have "(Fun f [ss!i], u) ∈ rstep R" by simp
with ‹wf_trs R› have "∃v. u = Fun f [v] ∧ (ss!i, v) ∈ rstep R"
proof (cases rule: rstep_cases_Fun')
case (root ls' r' σ')
with ‹¬ defined R (f, 1)› have False unfolding defined_def by force
thus ?thesis ..
next
case (nonroot j v)
thus ?thesis by auto
qed
then obtain v where u: "u = Fun f [v]" and rstep: "(ss!i, v) ∈ rstep R" by auto
from rstep.ctxt[OF rstep] have "(?C⟨ss!i⟩, ?C⟨v⟩) ∈ rstep R" .
moreover have "s = ?C⟨ss!i⟩" by (simp add: s ss)
moreover have u: "unblock_term f ?t = ?C⟨v⟩"
proof -
let ?ss = "take i ss @ v # drop (Suc i) ss"
let ?ss' = "map (λt. Fun f [t]) ?ss"
have map_simp_aux: "Fun f [v] # map (λt. Fun f [t]) (drop (Suc i) ss) = map (λt. Fun f [t]) (v # drop (Suc i) ss)" by simp
have "∀s∈set ?ss'. has_unary_root f s" by auto
hence "unblock_term f (Fun g ?ss') = Fun g ?ss" by simp
thus ?thesis unfolding nonroot
unfolding take_map u drop_map
unfolding list.map[symmetric]
unfolding nonroot u
unfolding take_map drop_map
unfolding map_simp_aux
unfolding map_append by simp
qed
moreover have "¬ defined R (the (root t))"
proof -
have id: "num_args t = length ss" using u unfolding unblock_block_term_ident using ‹i < length ss› by auto
have "the (root (unblock_term f ?t)) = (g, num_args ?t)" unfolding nonroot by simp
with ‹¬ defined R (g, length ss)›
show ?thesis unfolding unblock_block_term_ident by (simp add: id)
qed
ultimately show ?thesis by simp
qed
qed
lemma rstep_imp_blocked_rstep':
assumes "wf_trs R"
and "¬ defined R (f, 1)"
and "¬ defined R (the (root s))"
and "(block_term f s, t) ∈ rstep R"
shows "∃u. ¬ defined R (the (root u)) ∧ t = block_term f u"
proof -
let ?s = "block_term f s"
from assms and NF_Var[OF ‹wf_trs R›] have "is_Fun s" by auto
then obtain g ss where s: "s = Fun g ss" by (induct s) auto
let ?ss = "map (λt. Fun f [t]) ss"
have s': "?s = Fun g ?ss" by (simp add: s)
from assms have "¬ defined R (g, length ?ss)" unfolding s by simp
from rstep_preserves_undefined_root[OF ‹wf_trs R› this ‹(?s, t) ∈ rstep R›[unfolded s']]
obtain ts where "length ts = length ?ss" and t: "t = Fun g ts" by auto
hence "¬ defined R (the (root t))" unfolding t using ‹¬ defined R (g, length ?ss)› by simp
from ‹wf_trs R› and ‹(?s, t) ∈ rstep R›[unfolded s'] show ?thesis
proof (cases rule: rstep_cases_Fun')
case (root ls r σ)
from arg_cong[where f = length,OF root(2)] have "length ss = length ls" by auto
with assms and root have "¬ defined R (g, length ls)" unfolding root s by auto
with ‹(Fun g ls, r) ∈ R› show ?thesis unfolding defined_def by force
next
case (nonroot i u)
hence i: "i < length ss" by auto
hence "length (take i ?ss @ u # drop (Suc i) ?ss) = length ss" by auto
with assms have "¬ defined R (the (root t))" using nonroot by (simp add: s)
from nonroot have "(Fun f [ss!i], u) ∈ rstep R" by simp
from rstep_preserves_undefined_root[OF ‹wf_trs R› _ this] ‹¬ defined R (f, 1)›
obtain ts where "length ts = length [ss!i]" and "u = Fun f ts" by auto
then obtain v where u: "u = Fun f [v]" by (induct ts) simp_all
let ?u = "Fun g (take i ss @ v # drop (Suc i) ss)"
have ss1: "map (λt. Fun f [t]) (take i ss) = take i ?ss" unfolding take_map ..
have ss2: "map (λt. Fun f [t]) (drop (Suc i) ss) = drop (Suc i) ?ss" unfolding drop_map ..
have "map (λt. Fun f [t]) (take i ss @ v # drop (Suc i) ss) = take i ?ss @ (Fun f [v]) # drop (Suc i) ?ss" unfolding map_append by (simp add: ss1 ss2)
hence "t = block_term f ?u" unfolding nonroot u by simp
moreover have "¬ defined R (the (root ?u))" using ‹¬ defined R (the (root t))›
unfolding nonroot by simp
ultimately show ?thesis by best
qed
qed
lemma SN_on_imp_blocked_SN_on:
assumes "wf_trs R"
and "¬ defined R (f, 1)"
and "¬ SN_on (rstep R') {block_term f t}"
and "¬ defined R (the (root t))"
and refl: "∀(l, r)∈R'. ∃(u, v)∈R. ∃C∈set (□ # fcs). l = C⟨u⟩ ∧ r = C⟨v⟩"
shows "¬ SN_on (rstep R) {t}"
proof -
from assms(3) obtain S where "S 0 = block_term f t"
and chain: "chain (rstep R') S" by auto
from chain and blocked_rstep_imp_rstep[OF refl]
have R_chain: "chain (rstep R) S" by auto
have "∀i. ∃u. ¬ defined R (the (root u)) ∧ S i = block_term f u"
proof
fix i show "∃u. ¬ defined R (the (root u)) ∧ S i = block_term f u"
proof (induct i)
case 0
from ‹S 0 = block_term f t› and assms show ?case by auto
next
case (Suc i)
then obtain u where "¬ defined R (the (root u))" and Si: "S i = block_term f u" by auto
from R_chain have "(S i, S (Suc i)) ∈ rstep R" by simp
hence "(block_term f u, S (Suc i)) ∈ rstep R" unfolding Si by simp
from rstep_imp_blocked_rstep'[OF ‹wf_trs R› ‹¬ defined R (f, 1)›
‹¬ defined R (the (root u))› this]
show ?case .
qed
qed
from choice[OF this] obtain T
where "∀i. ¬ defined R (the (root (T i))) ∧ S i = block_term f (T i)"
(is "∀i. _ ∧ S i = ?T i") by auto
with R_chain have blocked_chain: "chain (rstep R) ?T" by auto
let ?T' = "λi. unblock_term f (S i)"
have "?T' 0 = t" unfolding ‹S 0 = block_term f t› by simp
moreover have "∀i. (?T' i, ?T' (Suc i)) ∈ rstep R"
proof
fix i show "(?T' i, ?T' (Suc i)) ∈ rstep R"
proof -
from ‹∀i. ¬ defined R (the (root (T i))) ∧ S i = ?T i›
have "¬ defined R (the (root (T i)))"
and si: "S i = block_term f (T i)"
and ssi: "S (Suc i) = block_term f (T (Suc i))" by auto
from blocked_chain have "(?T i, ?T (Suc i)) ∈ rstep R" ..
from blocked_rstep_imp_rstep'[OF ‹wf_trs R› ‹¬ defined R (f, 1)› ‹¬ defined R (the (root (T i)))› this]
show ?thesis unfolding si ssi by simp
qed
qed
ultimately show ?thesis unfolding SN_defs by auto
qed
lemma block_map_funs_term [simp]:
"(map_funs_term h (block_term f (Fun g ts))) = block_term (h f) (map_funs_term h (Fun g ts))"
by (simp)
lemma block_map_funs_term_pow [simp]:
fixes h :: "'a ⇒ 'a"
shows "((map_funs_term h)^^n) (block_term f (Fun g ts)) = block_term ((h ^^ n) f) (((map_funs_term h)^^n) (Fun g ts))"
proof (induct n arbitrary: g ts f)
case (Suc n g ts f)
have "(map_funs_term h ^^ Suc n) (block_term f (Fun g ts)) = (map_funs_term h ^^ n) (map_funs_term h (block_term f (Fun g ts)))"
by (simp add: funpow_swap1)
also have "… = (map_funs_term h ^^ n) (block_term (h f) (Fun (h g) (map (map_funs_term h) ts)))" by (simp only: block_map_funs_term, simp)
also have "… = block_term ((h ^^ n) (h f)) ((map_funs_term h ^^ n) (Fun (h g) (map (map_funs_term h) ts)))" unfolding Suc by simp
also have "… = block_term ((h ^^ (Suc n)) f) ((map_funs_term h ^^ (Suc n)) (Fun g ts))" by (simp add: funpow_swap1)
finally
show ?case .
qed simp
abbreviation block_trs where "block_trs f R ≡ block_rule f ` R"
lemma superset_of_blocked:
assumes "∀rule∈R. block_rule f rule ∈ R'"
shows "block_trs f R ⊆ R'"
proof (rule subrelI)
fix s t assume "(s, t) ∈ block_trs f R"
then obtain r where st: "block_rule f r = (s, t)" and "r ∈ R" by auto
with assms have "block_rule f r ∈ R'" by blast
thus "(s, t) ∈ R'" unfolding st .
qed
definition fcc_tt_cond :: "('f, 'v) ctxt set ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool" where
"fcc_tt_cond fcs R R' S S' = (
let F = funas_trs (R ∪ S) in
let vs = vars_trs (R ∪ S) in
fcs ≠ {} ∧
(∀C∈fcs. is_flat_ctxt vs F C) ∧
(∀(g, n)∈F. ∀i<n. ∃ss1 ss2.
More g ss1 □ ss2 ∈ fcs ∧ length ss1 = i ∧ length ss2 = n - i - 1) ∧
(∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀E∈fcs. Bex R' (instance_rule (E⟨l⟩, E⟨r⟩)))) ∧
(∀(l, r)∈S. (Bex (R' ∪ S') (instance_rule (l, r))) ∨ (∀E∈fcs. Bex (R' ∪ S') (instance_rule (E⟨l⟩, E⟨r⟩)))))"
fun
fcc_tt :: "('f, 'v) ctxt set ⇒ ('f, 'v) qreltrs ⇒ ('f, 'v) qreltrs ⇒ bool"
where
"fcc_tt fcs (nfs,Q, R, S) (nfs',Q', R', S') = (
fcc_tt_cond fcs R R' S S' ∧
Q' = {})"
theorem fcc_tt_sound:
assumes tt: "fcc_tt fcs (nfs,Q, R, S) (nfs',Q', R', S')"
and sn: "SN_qrel (nfs',Q', R', S')"
shows "SN_qrel (nfs,Q, R, S)"
proof -
note cond = tt[unfolded fcc_tt.simps fcc_tt_cond_def Let_def]
from sn have "SN_rel (rstep R') (rstep S')" using cond by simp
from partial_fcc_reflects_SN_rel[OF _ _ _ _ _ _ this] and cond
have relSN: "SN_rel (rstep R) (rstep S)" by auto
show ?thesis unfolding SN_qrel_def split
by (rule SN_rel_mono[OF _ _ relSN], auto)
qed
definition
fcc_cond ::
"'f ⇒ ('f, 'v) ctxt list ⇒
('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒
('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒
bool"
where
"fcc_cond f fcs P Pw R Rw P' Pw' R' Rw' ≡
let F = funas_trs (R ∪ Rw) ∪ funas_args_trs (P ∪ Pw);
Cf = More f [] □ [] in
wf_trs (R ∪ Rw) ∧ ¬ defined (R ∪ Rw) (f, 1) ∧
(∀C∈set (Cf#fcs). is_flat_ctxt (vars_trs (R ∪ Rw)) ({(f, 1)} ∪ F) C) ∧
(∀(g, n)∈F. ∀i<n. ∃ss1 ss2.
More g ss1 □ ss2 ∈ set (Cf # fcs) ∧ length ss1 = i ∧ length ss2 = n - i - 1) ∧
(∀(l, r)∈R. (Bex R' (instance_rule (l, r))) ∨ (∀C∈set (Cf#fcs). (Bex R' (instance_rule (C⟨l⟩, C⟨r⟩))))) ∧
(∀(l, r)∈Rw. (Bex (R' ∪ Rw') (instance_rule (l, r))) ∨ (∀C∈set (Cf#fcs). Bex (R' ∪ Rw') (instance_rule (C⟨l⟩, C⟨r⟩)))) ∧
(∀(l', r')∈R' ∪ Rw'. ∃(l, r)∈R ∪ Rw. ∃C∈set (□ # Cf # fcs). l' = C⟨l⟩ ∧ r' = C⟨r⟩) ∧
block_rule f ` P ⊆ P' ∧
block_rule f ` Pw ⊆ Pw' ∧
(∀(s, t)∈P ∪ Pw. is_Fun s ∧ is_Fun t) ∧
(∀(s, t)∈P ∪ Pw. ¬ defined (R ∪ Rw) (the (root t)))"
fun
fcc_proc ::
"'f ⇒ ('f, 'v) ctxt list ⇒ ('f, 'v) dpp ⇒ ('f, 'v) dpp ⇒ bool"
where
"fcc_proc f fcs (nfs,m,P, Pw, Q, R, Rw) (nfs',m',P', Pw', Q', R', Rw') = (
fcc_cond f fcs P Pw R Rw P' Pw' R' Rw')"
theorem fcc_proc_chain: fixes P Pw R Rw :: "('f,'v)trs"
defines F: "F ≡ funas_trs (R ∪ Rw) ∪ funas_args_trs (P ∪ Pw)"
assumes proc: "fcc_proc f fcs (nfs,m,P, Pw, {}, R, Rw) (nfs,m,P', Pw', {}, R', Rw')"
and michain: "min_ichain_sig (nfs,m,P,Pw,{},R,Rw) F s t σ"
shows "∃ s t. min_ichain (nfs,m,P',Pw',{},R',Rw') s t σ"
proof -
note cond = proc[unfolded fcc_proc.simps fcc_cond_def Let_def]
let ?P = "P ∪ Pw"
let ?P' = "P' ∪ Pw'"
let ?R = "R ∪ Rw"
let ?R' = "R' ∪ Rw'"
let ?Cf = "More f [] □ []"
let ?F' = "funas_trs ?R ∪ funas_args_trs ?P"
let ?F = "{(f, 1)} ∪ ?F'"
from michain proc have mchain: "min_ichain (nfs,m,P,Pw,{},R,Rw) s t σ" and F: "funas_ichain s t σ ⊆ ?F'" unfolding F by auto
from cond have flat_ctxts: "∀C∈set (?Cf # fcs). is_flat_ctxt (vars_trs ?R) ?F C" by auto
from cond have complete: "∀(g, n)∈?F. ∀i<n. ∃ss1 ss2.
More g ss1 □ ss2 ∈ set (?Cf # fcs) ∧ length ss1 = i ∧ length ss2 = n - i - 1" by simp
from cond have wfR: "wf_trs ?R" by simp
from cond have pres: "∀(l, r)∈R. (Bex R' (instance_rule (l, r)))
∨ (∀C∈set (?Cf # fcs). (Bex R' (instance_rule (C⟨l⟩, C⟨r⟩))))"
"∀(l, r)∈Rw. (Bex ?R' (instance_rule (l, r)))
∨ (∀C∈set (?Cf # fcs). Bex ?R' (instance_rule (C⟨l⟩, C⟨r⟩)))" by auto
from pres have pres': "∀(l, r)∈ ?R. (Bex ?R' (instance_rule (l, r)))
∨ (∀C∈set (?Cf # fcs). Bex ?R' (instance_rule (C⟨l⟩, C⟨r⟩)))" by blast
from cond
have refl: "∀(l', r')∈ ?R'. ∃(l, r)∈ ?R. ∃C∈set (□ # ?Cf # fcs). l' = C⟨l⟩ ∧ r' = C⟨r⟩"
by simp
from mchain have P_steps: "∀i. (s i, t i) ∈ ?P" by (auto simp add: ichain.simps)
hence "∀i. is_Fun (s i) ∧ is_Fun (t i)" using cond by best
hence si_Fun: "∀i. is_Fun (s i)" and ti_Fun: "∀i. is_Fun (t i)" by auto
have funas_args: "funas_trs ?R ∪ funas_args_trs ?P ⊆ ?F" by blast
from cond have nd: "¬ defined ?R (f, 1)" by simp
have inP: "⋀ s t. (s, t) ∈ ?P ⟹ is_Fun s ∧ is_Fun t ∧ ¬ defined ?R (the (root t))"
using cond by blast
let ?s = "λi. block_term f (s i)"
let ?t = "λi. block_term f (t i)"
let ?RR = "(rstep ?R)^* O rstep R O (rstep ?R)^*"
let ?RR' = "(rstep ?R')^* O rstep R' O (rstep ?R')^*"
{
fix t u :: "('f,'v)term"
let ?Rc = "(if rstep ?R = rstep R then rstep R' else rstep ?R')"
have Rc: "?Rc ⊆ rstep ?R'" unfolding rstep_union by auto
hence Rc: "?Rc^* ⊆ (rstep ?R')^*" by (rule rtrancl_mono)
assume t: "¬ defined ?R (the (root t)) ∧ funas_args_term t ⊆ ?F'"
have " ((t, u) ∈ (rstep ?R)⇧* ⟶
(block_term f t, block_term f u)
∈ ?Rc^*) ∧
((t, u) ∈ ?RR ⟶
(block_term f t, block_term f u)
∈ ?Rc^* O
rstep R' O
?Rc^*)"
proof (rule steps_map[where Q = "λ S. S = rstep R ∨ S = rstep ?R" and P = "λ t. ¬ defined ?R (the (root t)) ∧ funas_args_term t ⊆ ?F'" and f = "block_term f" and g = "λ S. if S = rstep R then rstep R' else rstep ?R'", of _ "rstep ?R" "rstep R", unfolded HOL.simp_thms if_True, OF _ t])
fix t u S
assume t: "¬ defined ?R (the (root t)) ∧ funas_args_term t ⊆ ?F'"
and S: "S = rstep R ∨ S = rstep ?R"
and step: "(t,u) ∈ S"
from step S have step': "(t, u) ∈ rstep ?R" unfolding rstep_union by auto
from t have ndef: "¬ defined ?R (the (root t))"
and funas: "funas_args_term t ⊆ ?F'" by auto
from rstep_imp_blocked_rstep[OF wfR flat_ctxts complete funas _ _ ndef step' pres', of f]
have one: "¬ defined ?R (the (root u)) ∧ funas_args_term u ⊆ ?F'" and
step': "(block_term f t, block_term f u) ∈ rstep ?R'" by auto
let ?S = "(if S = rstep R then rstep R' else rstep ?R')"
show "(¬ defined ?R (the (root u)) ∧ funas_args_term u ⊆ ?F') ∧
(block_term f t, block_term f u) ∈ ?S"
proof (rule conjI[OF one])
show "(block_term f t, block_term f u) ∈ ?S"
proof (cases "?S = rstep ?R'")
case True
show ?thesis unfolding True using step' .
next
case False
hence "?S = rstep R' ∧ S = rstep R"
by (cases "S = rstep R", auto)
hence S: "?S = rstep R'" "S = rstep R" by auto
with step have step: "(t,u) ∈ rstep R" by auto
from rstep_imp_blocked_rstep_union[OF wfR flat_ctxts complete funas _ _ ndef step pres(1), of f]
show ?thesis unfolding S(1) by auto
qed
qed
qed auto
with Rc have " ((t, u) ∈ (rstep ?R)⇧* ⟶
(block_term f t, block_term f u)
∈ (rstep ?R')^*) ∧
((t, u) ∈ ?RR ⟶
(block_term f t, block_term f u)
∈ ?RR')" by auto
} note main = this
{
fix i
let ?σ = "σ i"
let ?t = "t i ⋅ ?σ"
let ?σ' = "σ (Suc i)"
let ?s = "s (Suc i) ⋅ ?σ'"
let ?bt = "block_term f (t i) ⋅ σ i"
let ?bs = "block_term f (s (Suc i)) ⋅ σ (Suc i)"
from P_steps have t_in_P: "(s i, t i) ∈ ?P" by simp
from P_steps have s_in_P: "(s (Suc i), t (Suc i)) ∈ ?P" by simp
from mchain have R_seq: "(?t, ?s) ∈ (rstep ?R)^*" by (simp add: ichain.simps)
from ti_Fun have "is_Fun (t i)" by simp
then obtain gs ts where ti: "t i = Fun gs ts" by best
from si_Fun have "is_Fun (s (Suc i))" by simp
then obtain hs us where si: "s (Suc i) = Fun hs us" by best
from inP[OF t_in_P]
have "¬ defined ?R (the (root (t i)))" by (auto)
hence not_def_t: "¬ defined ?R (the (root ?t))" unfolding ti by simp
have t_funas_args: "funas_args_term ?t ⊆ funas_trs ?R ∪ funas_args_trs ?P"
proof -
from t_in_P
have funas_ti: "funas_args_term (t i) ⊆ ?F'"
unfolding funas_args_trs_def funas_args_rule_def [abs_def] by auto
moreover have "funas_args_term ?t = (⋃t∈set ts. funas_term (t ⋅ ?σ))"
unfolding funas_args_term_subst_apply[OF ‹is_Fun (t i)›]
unfolding ti by auto
moreover
have "∀t∈set ts. funas_term (t ⋅ ?σ) ⊆ ?F'"
proof
fix u assume "u ∈ set ts"
from funas_ti[unfolded ti funas_args_term_def]
have "⋃(set (map funas_term ts))
⊆ ?F'" by simp
with ‹u ∈ set ts› have "funas_term u
⊆ ?F'" by auto
hence "funas_term (u ⋅ ?σ) ⊆ ?F' ∪ funas_ichain s t σ"
unfolding funas_term_subst funas_ichain_def by auto
thus "funas_term (u ⋅ ?σ)
⊆ ?F'" using F by auto
qed
ultimately show ?thesis by auto
qed
from not_def_t t_funas_args have precond: "¬ defined ?R (the (root ?t)) ∧ funas_args_term ?t ⊆ ?F'" by auto
note main = main[OF this, of ?s]
from ti have bti: "block_term f ?t = ?bt" by simp
from si have bsi: "block_term f ?s = ?bs" by simp
note main = main[unfolded bti bsi]
from main[THEN conjunct1, rule_format, OF R_seq]
have steps: "(?bt, ?bs) ∈ (rstep ?R')^*" by simp
{
assume "(?t,?s) ∈ ?RR"
hence "(?bt,?bs) ∈ ?RR'"
using main[THEN conjunct2] by auto
}
note steps this
} note main = this
note steps = main(1)
note strict_steps = main(2)
have "∀i. (?s i, ?t i) ∈ ?P'"
proof
fix i
from mchain have "(s i, t i) ∈ ?P" by (simp add: ichain.simps)
hence "block_rule f (s i, t i) ∈ block_rule f ` ?P" by simp
hence "(?s i, ?t i) ∈ block_rule f ` ?P" unfolding block_rule_def by simp
moreover from cond
have "block_rule f ` ?P ⊆ ?P'"
using superset_of_blocked by auto
ultimately show "(?s i, ?t i) ∈ ?P'" by blast
qed
moreover {
assume m
have "∀i. SN_on (rstep ?R') {?t i ⋅ σ i}"
proof
fix i
from ti_Fun obtain k vs where ti: "t i = Fun k vs" by best
have "the (root (t i)) = (k, length vs)" unfolding ti by simp
hence k: "(k, length vs) = the (root (t i ⋅ σ i))" unfolding ti by simp
from P_steps have inP': "(s i, t i) ∈ ?P" by simp
let ?tsi = "(t i ⋅ σ i)"
let ?bti = "block_term f ?tsi"
from cond and ‹(s i, t i) ∈ ?P›
have "¬ defined ?R (the (root (t i)))" by auto
hence not_def_t: "¬ defined ?R (the (root ?tsi))"
unfolding ti by auto
from block_subst_Fun[of f k vs "σ i"]
have block_ti: "?t i ⋅ σ i = ?bti" unfolding ti by auto
from refl have ci: "?R' ⊆ci ?R" unfolding ci_subset_def by blast
have subset: "rstep ?R' ⊆ rstep ?R"
using qrstep_ci_mono[OF ci, of False "{}", unfolded qrstep_rstep_conv] by auto
show "SN_on (rstep ?R') {?t i ⋅ σ i}"
proof (rule SN_on_subset1[OF _ subset], rule ccontr)
assume "¬ SN_on (rstep ?R) {?t i ⋅ σ i}"
hence not_SN: "¬ SN_on (rstep ?R) {?bti}" unfolding block_ti .
let ?tmp = "Fun f [t 0]"
from nd have a: "is_Fun ?tmp"
and b: "¬ defined ?R (the (root ?tmp))" by auto
have nSN: "¬ SN_on (rstep ?R) {?tsi}"
using SN_on_imp_blocked_SN_on[OF ‹wf_trs ?R› nd not_SN not_def_t, of "[]"] by auto
with mchain ‹m›
show False by (simp add: minimal_cond_def)
qed
qed
}
moreover have "∀i. (?t i ⋅ σ i, ?s (Suc i) ⋅ σ (Suc i)) ∈ (rstep ?R')^*"
(is "∀i. ?Prop i")
using steps by simp
moreover have "(INFM i. (?s i, ?t i) ∈ P') ∨ (INFM i. (?t i ⋅ σ i, ?s (Suc i) ⋅ σ (Suc i)) ∈ ?RR')"
proof -
let ?orig = "λ i. (s i, t i) ∈ P ∨ (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?RR"
let ?new = "λ i. (?s i, ?t i) ∈ P' ∨ (?t i ⋅ σ i, ?s (Suc i) ⋅ σ (Suc i)) ∈ ?RR'"
from mchain[unfolded min_ichain.simps ichain.simps]
have inf: "(INFM i. ?orig i)" unfolding INFM_disj_distrib by simp
show ?thesis unfolding INFM_disj_distrib[symmetric]
unfolding INFM_nat_le
proof
fix i :: nat
from inf[unfolded INFM_nat_le, rule_format, of i]
obtain j where j: "j ≥ i" and orig: "?orig j" by auto
show "∃ j ≥ i. ?new j"
proof (rule exI, rule conjI[OF j])
from ‹?orig j› show "?new j"
proof
assume "(s j, t j) ∈ P"
hence "block_rule f (s j, t j) ∈ block_rule f ` P" by simp
hence "(?s j, ?t j) ∈ block_rule f ` P" unfolding block_rule_def by simp
moreover from cond
have "block_rule f ` P ⊆ P'"
using superset_of_blocked by auto
ultimately have "(?s j, ?t j) ∈ P'" by blast
thus "?new j" ..
next
assume "(t j ⋅ σ j, s (Suc j) ⋅ σ (Suc j)) ∈ ?RR"
from strict_steps[OF this] show "?new j" ..
qed
qed
qed
qed
ultimately have "min_ichain (nfs,m,P', Pw', {}, R', Rw') ?s ?t σ"
unfolding min_ichain.simps ichain.simps minimal_cond_def
by simp
thus ?thesis by blast
qed
theorem fcc_proc_sound: fixes P :: "('f,'v)trs"
assumes proc: "fcc_proc f fcs (nfs,m,P, Pw, {}, {}, R) (nfs,m,P', Pw', {}, {}, R')"
and left: "left_linear_trs R"
and finite: "finite_dpp (nfs,m,P', Pw', {}, {}, R')"
shows "finite_dpp (nfs,m,P, Pw, {}, {}, R)"
proof (rule ccontr)
let ?D = "(nfs,m,P,Pw,{},{},R) :: ('f,'v)dpp"
let ?F = "(funas_args_trs (P ∪ Pw) ∪ funas_trs R)"
let ?F' = "(funas_trs ({} ∪ R) ∪ funas_args_trs (P ∪ Pw))"
assume "¬ ?thesis"
then obtain s t σ where chain: "min_ichain ?D s t σ" unfolding finite_dpp_def by auto
from proc[unfolded fcc_proc.simps fcc_cond_def Let_def] have "wf_trs R" by auto
hence nvar: " ∀(l, r)∈ R. is_Fun l" unfolding wf_trs_def by auto
have "∃ σ. min_ichain_sig ?D ?F s t σ"
by (rule left_linear_min_ichain_imp_min_ichain_sig[OF left subset_refl _ chain nvar], insert proc[unfolded fcc_proc.simps fcc_cond_def Let_def], auto)
then obtain σ where chain: "min_ichain_sig ?D ?F' s t σ" by auto
from finite fcc_proc_chain[OF proc chain] show False unfolding finite_dpp_def by auto
qed
theorem fcc_split_proc_sound: fixes P :: "('f,'v)trs"
assumes proc: "fcc_proc f fcs (nfs,m,Ps ∩ (P ∪ Pw), (P ∪ Pw) - Ps, {}, Rw ∩ Rs, Rw - Rs) (nfs,m,P', Pw', {}, R', Rw')"
and left: "left_linear_trs Rw"
and finite1: "finite_dpp (nfs,m,P', Pw', {}, R', Rw')"
and finite2: "finite_dpp (nfs,m,P - Ps, Pw - Ps,{},{},Rw - Rs)"
shows "finite_dpp (nfs,m,P, Pw, {}, {}, Rw)"
proof (rule ccontr)
let ?D = "(nfs,m,P,Pw,{},{},Rw) :: ('f,'v)dpp"
let ?D' = "(nfs,m,Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, {}, Rs ∩ ({} ∪ Rw), {} ∪ Rw - Rs)"
assume "¬ ?thesis"
then obtain s t σ where chain: "min_ichain ?D s t σ" unfolding finite_dpp_def by auto
let ?F = "(funas_args_trs (P ∪ Pw) ∪ funas_trs Rw)"
let ?F' = "(funas_trs ({} ∪ Rw) ∪ funas_args_trs (P ∪ Pw))"
from proc[unfolded fcc_proc.simps fcc_cond_def Let_def]
have Pcond: " (∀(s, t)∈Ps ∩ (P ∪ Pw) ∪ (P ∪ Pw - Ps). is_Fun s ∧ is_Fun t) ∧
(∀(s, t)∈Ps ∩ (P ∪ Pw) ∪ (P ∪ Pw - Ps).
¬ defined (Rw ∩ Rs ∪ (Rw - Rs)) (the (root t)))"
and wf: "wf_trs (Rw ∩ Rs ∪ (Rw - Rs))" by auto
have id: "Ps ∩ (P ∪ Pw) ∪ (P ∪ Pw - Ps) = P ∪ Pw" "(Rw ∩ Rs) ∪ (Rw - Rs) = Rw" by blast+
from Pcond[unfolded this]
have Pcond: "⋀s t. (s, t) ∈ P ∪ Pw ⟹
is_Fun s ∧ is_Fun t ∧ ¬ defined Rw (the (root t))" by auto
have "∃ σ. min_ichain_sig ?D ?F s t σ"
by (rule left_linear_min_ichain_imp_min_ichain_sig[OF left subset_refl Pcond chain],
insert wf[unfolded wf_trs_def], force+)
then obtain σ where chain: "min_ichain_sig ?D ?F' s t σ" by auto
have no_chain: "¬ min_ichain_sig ?D' ?F' s t σ"
proof
assume chain: "min_ichain_sig ?D' ?F' s t σ"
have "∃ s t. min_ichain (nfs,m,P',Pw',{},R',Rw') s t σ"
by (rule fcc_proc_chain[OF proc, unfolded id, of s t σ],
insert chain, simp add: Int_commute[of Rs])
with finite1 show False unfolding finite_dpp_def by blast
qed
from min_ichain_split_sig[OF chain no_chain] obtain i where
"min_ichain (nfs,m,P - Ps, Pw - Ps, {}, {}, Rw - Rs) (shift s i) (shift t i) (shift σ i)" by auto
with finite2 show False unfolding finite_dpp_def by blast
qed
end