theory Generalized_Usable_Rules
imports
QTRS.QDP_Framework
"Check-NT.Name"
"../Proof_Checker/Countables"
"../Orderings/Non_Inf_Order"
TA.Signature_Extension
"Check-NT.Dependency_Graph"
begin
section ‹generalized usable rules›
fun compat_root where
"compat_root _ (Var _) = False"
| "compat_root (Var _) l = False"
| "compat_root fls gts = (root fls = root gts)"
locale fixed_trs_dep =
fixes π :: "'f dep"
and R :: "('f,'v)trs"
and Q :: "('f,'v)terms"
and nfs :: bool
begin
abbreviation NFQ where "NFQ ≡ NF_terms Q"
text ‹same definition as in CADE07 "Bounded Increase" paper, except that we define
the usable rules of a term as a predicate instead of a set.›
inductive gen_usable_rule :: "('f,'v)term ⇒ ('f,'v)rule ⇒ bool"
where in_R: "(l,r) ∈ R ⟹ compat_root l t ⟹ gen_usable_rule t (l,r)"
| in_U: "(l,r) ∈ R ⟹ compat_root l t ⟹ gen_usable_rule r lr ⟹ gen_usable_rule t lr"
| in_arg: "i < length ts ⟹ gen_usable_rule (ts ! i) lr ⟹ lr' ∈ {lr} ^^^ π (f,length ts) i ⟹ gen_usable_rule (Fun f ts) lr'"
definition gen_usable_rules :: "('f, 'v) term ⇒ ('f, 'v) trs" where
"gen_usable_rules t = {lr. gen_usable_rule t lr}"
definition gen_usable_rules_pairs :: "('f, 'v) trs ⇒ ('f, 'v) trs" where
"gen_usable_rules_pairs P = ⋃(gen_usable_rules ` snd ` P)"
lemma gen_usable_rulesI[intro]: "gen_usable_rule t lr ⟹ lr ∈ gen_usable_rules t"
unfolding gen_usable_rules_def by auto
lemma gen_usable_rulesE[elim]: "lr ∈ gen_usable_rules t ⟹ gen_usable_rule t lr"
unfolding gen_usable_rules_def by auto
text ‹a recursive version of usable rules
(easier to use, but does not reflect that inductive sets correspond to \emph{least} fixpoint)›
lemma gen_usable_rules_Fun: "gen_usable_rules (Fun f ts) =
{(Fun f ls,r) | ls r. (Fun f ls,r) ∈ R ∧ length ls = length ts} ∪
⋃ { gen_usable_rules r | ls r. (Fun f ls,r) ∈ R ∧ length ls = length ts} ∪
⋃ { gen_usable_rules (ts ! i) ^^^ π (f,length ts) i | i. i < length ts}" (is "?L = ?R1 ∪ ?R2 ∪ ?R3")
proof (rule equalityI)
let ?R = "?R1 ∪ ?R2 ∪ ?R3"
{
fix l r
assume "(l,r) ∈ ?L"
hence "gen_usable_rule (Fun f ts) (l,r)" by auto
hence "(l,r) ∈ ?R"
proof(cases)
case in_R
from in_R(2) obtain ls where l: "l = Fun f ls" by (cases l, auto)
with in_R show ?thesis by auto
next
case (in_U l2 r2)
from in_U(2) obtain ls where l2: "l2 = Fun f ls" by (cases l2, auto)
with in_U show ?thesis by auto
next
case (in_arg i lr)
hence "(l, r) ∈ {lr. gen_usable_rule (ts ! i) lr} ^^^ π (f, length ts) i"
by (cases "π (f,length ts) i", auto)
thus ?thesis using in_arg(1) unfolding gen_usable_rules_def by auto
qed
}
thus "?L ⊆ ?R" ..
moreover
{
fix l r
assume "(l,r) ∈ ?R"
hence "(l,r) ∈ ?R1 ∨ (l,r) ∈ ?R2 ∨ (l,r) ∈ ?R3" by blast
hence "(l,r) ∈ ?L"
proof
assume "(l,r) ∈ ?R1"
with in_R[of l r] show "(l,r) ∈ ?L" by auto
next
assume "(l,r) ∈ ?R2 ∨ (l,r) ∈ ?R3"
thus ?thesis
proof
assume "(l,r) ∈ ?R2"
then obtain ls r2 where U: "(l,r) ∈ gen_usable_rules r2"
and R: "(Fun f ls, r2) ∈ R" and l: "length ls = length ts" by auto
from in_U[OF R _ gen_usable_rulesE[OF U]] l
show ?thesis by auto
next
assume "(l,r) ∈ ?R3"
then obtain i where i: "i < length ts"
and lr: "(l,r) ∈ gen_usable_rules (ts ! i) ^^^ π (f,length ts) i" by auto
then obtain lr' where u: "gen_usable_rule (ts ! i) lr'" and lr: "(l,r) ∈ {lr'} ^^^ π (f,length ts) i"
unfolding gen_usable_rules_def by (cases "π (f,length ts) i", auto)
show "(l,r) ∈ ?L"
by (intro gen_usable_rulesI, rule in_arg[OF i u lr])
qed
qed
}
thus "?R ⊆ ?L" ..
qed
lemma gen_usable_rules_Var: "gen_usable_rules (Var x) = {}"
proof -
{
fix l r
assume "(l,r) ∈ gen_usable_rules (Var x)"
hence "gen_usable_rule (Var x) (l,r)" ..
hence False by (cases, auto)
}
thus ?thesis by auto
qed
lemma gen_usable_rules_subst: "gen_usable_rules t ⊆ gen_usable_rules (t ⋅ σ)"
proof (induct t)
case (Var x)
thus ?case by (simp add: gen_usable_rules_Var)
next
case (Fun f ts)
{
fix i
assume i: "i < length ts"
hence "ts ! i ∈ set ts" by auto
from Fun[OF this] i
have "gen_usable_rules (ts ! i) ^^^ π (f, length ts) i ⊆
gen_usable_rules (map (λt. t ⋅ σ) ts ! i) ^^^ π (f, length ts) i" (is "?l ⊆ _")
by (intro rel_dep_mono, auto)
also have "... ⊆ ⋃{gen_usable_rules (map (λt. t ⋅ σ) ts ! i) ^^^ π (f, length ts) i |i. i < length ts}"
(is "_ ⊆ ?r")
using i by auto
finally have "?l ⊆ ?r" .
} note main = this
show ?case unfolding subst_apply_term.simps gen_usable_rules_Fun
by (insert main, auto)
qed
text ‹
a helpful lemma to be used in an induction on the term structure, to show
that the usable rules of the one term are a subset of those of another term.
›
lemma gen_usable_rules_split: "∃ k. ∀ s t. gen_usable_rules s ^^^ k ⊆ gen_usable_rules t ^^^ k ⟶
gen_usable_rules (Fun f (b @ s # a)) ⊆ gen_usable_rules (Fun f (b @ t # a))"
proof -
let ?i = "length b"
let ?n = "Suc (?i + length a)"
let ?π = "π (f,?n) ?i"
let ?all = "λ t. gen_usable_rules (Fun f (b @ t # a))"
let ?coll = "λ t. ⋃((λ i. gen_usable_rules ((b @ t # a) ! i) ^^^ π (f,?n) i) ` {i . i < ?n})"
let ?single = "λ t. gen_usable_rules t ^^^ π (f,?n) ?i"
have id: "{i. i < ?n} = {i. i < ?i} ∪ {?i} ∪ {Suc ?i + k | k. Suc ?i + k < ?n}" (is "_ = ?ib ∪ ?ii ∪ ?ia") by (auto, presburger)
{
fix s t
have "?all s - ?all t ⊆ ?coll s - ?coll t"
unfolding gen_usable_rules_Fun by auto
also have "… ⊆ ?single s - ?single t" unfolding id by (auto simp: nth_append)
finally have "?all s - ?all t ⊆ ?single s - ?single t" .
} note sub = this
have "∃ k. ∀ s t. gen_usable_rules s ^^^ k ⊆ gen_usable_rules t ^^^ k ⟶ ?single s - ?single t = {}"
proof (cases ?π)
case Ignore
thus ?thesis by auto
next
case Increase
show ?thesis
by (rule exI[of _ Increase], insert Increase, auto)
next
case Decrease
show ?thesis
by (rule exI[of _ Decrease], insert Decrease, auto)
next
case Wild
show ?thesis
by (rule exI[of _ Wild], insert Wild, auto)
qed
then obtain k where "⋀ s t. gen_usable_rules s ^^^ k ⊆ gen_usable_rules t ^^^ k ⟹ ?single s - ?single t = {}" by auto
with sub have "⋀ s t. gen_usable_rules s ^^^ k ⊆ gen_usable_rules t ^^^ k ⟹ ?all s ⊆ ?all t" by blast
thus "∃ k. ∀ s t. gen_usable_rules s ^^^ k ⊆ gen_usable_rules t ^^^ k ⟶ ?all s ⊆ ?all t" by auto
qed
end
locale fixed_trs_dep_order = fixed_trs_dep π R Q nfs + non_inf_order_trs S NS F π
for π :: "('f :: countable) dep"
and R :: "('f,'v :: countable)trs"
and Q :: "('f,'v)terms"
and F :: "'f sig"
and S :: "('f,'v)trs"
and NS :: "('f,'v)trs"
and nfs :: bool
and m :: bool
+ fixes const :: 'f
assumes wwf: "wwf_qtrs Q R"
and NFQ: "NF_terms Q ⊆ NF_trs R"
and infinite_V: "infinite (UNIV :: 'v set)"
and RF: "funas_trs R ⊆ F"
and QF: "⋃(funas_term ` Q) ⊆ F"
begin
lemma main_technical_lemma:
assumes step: "(t ⋅ σ,v) ∈ qrstep nfs Q R"
and σ: "σ ` vars_term t ⊆ NFQ"
and tsigF: "funas_term (t ⋅ σ) ⊆ F ∨ funas_args_term (t ⋅ σ) ⊆ F ∧ ¬ defined (applicable_rules Q R) (the (root (t ⋅ σ)))"
shows "(gen_usable_rules t ^^^ k ⊆ NS ⟶ {(t ⋅ σ, v)} ^^^ k ⊆ NS) ∧ (∃ u σ'. v = u ⋅ σ'
∧ gen_usable_rules u ^^^ k ⊆ gen_usable_rules t ^^^ k ∧ σ' ` vars_term u ⊆ NFQ)"
using step σ tsigF
proof (induction t arbitrary: v k)
case (Var x v k)
from Var.prems(2) NFQ have "Var x ⋅ σ ∈ NF_trs R" by auto
moreover from Var.prems(1) have "(Var x ⋅ σ, v) ∈ rstep R" by auto
ultimately have False by auto
thus ?case by auto
next
case (Fun f ts v k)
note switch = wwf_qtrs_imp_nfs_switch[OF wwf]
from qrstepE[OF Fun.prems(1)[unfolded switch[of nfs True]]]
obtain C σ' l r where
nf: "∀u⊲l ⋅ σ'. u ∈ NFQ" and
lr: "(l, r) ∈ R" and
t: "Fun f ts ⋅ σ = C⟨l ⋅ σ'⟩" and
v: "v = C⟨r ⋅ σ'⟩" and
nfs: "NF_subst True (l, r) σ' Q" .
let ?σ' = "map (λ t. t ⋅ σ')"
let ?σ = "map (λ t. t ⋅ σ)"
from wwf_qtrs_imp_left_fun[OF wwf lr] obtain g ls where l: "l = Fun g ls" by auto
from wwf only_applicable_rules[OF nf] lr
have vars_lr: "vars_term r ⊆ vars_term l" unfolding wwf_qtrs_def by auto
from RF lr have rF: "funas_term r ⊆ F"
unfolding funas_trs_def funas_rule_def [abs_def] by force
show ?case
proof (cases C)
case Hole
from t Hole have t: "Fun f ts ⋅ σ = l ⋅ σ'" by simp
from only_applicable_rules[OF nf, of r] lr l
have defg: "defined (applicable_rules Q R) (g,length ls)" unfolding defined_def applicable_rules_def
by force
from v Hole have v: "v = r ⋅ σ'" by simp
from l t have gf: "g = f" and id: "?σ ts = ?σ' ls" by auto
from arg_cong[OF id, of length] have len: "length ts = length ls" by simp
with l t gf have compat: "compat_root l (Fun f ts)" by simp
from gf defg len have "defined (applicable_rules Q R) (f,length ts)" by simp
with Fun(4) have "funas_term (Fun f ts ⋅ σ) ⊆ F" by auto
with t have "funas_term (l ⋅ σ') ⊆ F" by simp
hence σ'F: "⋃(funas_term ` σ' ` vars_term l) ⊆ F" unfolding funas_term_subst by blast
let ?σ' = "λ x. if x ∈ vars_term l then σ' x else Var x"
have l_id: "l ⋅ σ' = l ⋅ ?σ'" by (rule term_subst_eq, simp)
have r_id: "r ⋅ σ' = r ⋅ ?σ'" by (rule term_subst_eq, insert vars_lr, auto)
have σ'F: "⋃(funas_term ` range ?σ') ⊆ F" using σ'F by auto
{
assume ns: "gen_usable_rules (Fun f ts) ^^^ k ⊆ NS"
have "(l,r) ∈ gen_usable_rules (Fun f ts)"
by (rule gen_usable_rulesI[OF in_R[OF lr compat]])
hence "{(l,r)} ⊆ gen_usable_rules (Fun f ts)" by auto
from subset_trans[OF rel_dep_mono[OF this] ns]
have "{(l,r)} ^^^ k ⊆ NS" .
hence "{(l ⋅ σ', r ⋅ σ')} ^^^ k ⊆ (λ (s,t). (s ⋅ ?σ', t ⋅ ?σ')) ` NS"
unfolding l_id r_id by (cases k, auto)
also have "(λ (s,t). (s ⋅ ?σ', t ⋅ ?σ')) ` NS ⊆ NS" using F_subst_closedD[OF stable_NS σ'F] by auto
finally have "{(Fun f ts ⋅ σ, v)} ^^^ k ⊆ NS" using t v by simp
}
hence NS: "gen_usable_rules (Fun f ts) ^^^ k ⊆ NS ⟶ {(Fun f ts ⋅ σ, v)} ^^^ k ⊆ NS" ..
show ?thesis
proof (rule conjI[OF NS], intro exI conjI)
show "v = r ⋅ ?σ'" using v r_id by simp
show "gen_usable_rules r ^^^ k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
by (rule rel_dep_mono, insert in_U[OF lr compat], auto simp: gen_usable_rules_def)
show "?σ' ` vars_term r ⊆ NFQ" using vars_lr nfs unfolding NF_subst_def vars_rule_def by auto
qed
next
case (More g bef D aft)
let ?i' = "length bef"
let ?tsi' = "ts ! ?i'"
let ?dl = "D ⟨ l ⋅ σ' ⟩"
let ?dr = "D ⟨ r ⋅ σ' ⟩"
let ?n' = "Suc (?i' + length aft)"
from t More have t: "Fun f ts ⋅ σ = Fun f (bef @ ?dl # aft)" and gf: "g = f" by auto
with v More have v: "v = Fun f (bef @ ?dr # aft)" by auto
from t have "map (λ t. t ⋅ σ) ts = bef @ ?dl # aft" by simp
from arg_cong[OF this, of length] have len: "length ts = ?n'" by simp
hence i': "?i' < length ts" by auto
from id_take_nth_drop[OF i'] obtain tbef taft where ts: "Fun f ts = Fun f (tbef @ ?tsi' # taft)" and tbef: "tbef = take ?i' ts" by auto
let ?i = "length tbef" let ?n = "Suc (?i + length taft)"
let ?tsi = "ts ! ?i"
from tbef i' have llen: "?i' = ?i" by auto
note ts = ts[unfolded llen]
note tbef = tbef[unfolded llen]
note i = i'[unfolded llen]
from i have mem: "?tsi ∈ set ts" by auto
from Fun.prems(2) mem have vars: "σ ` vars_term ?tsi ⊆ NFQ" by auto
from t[unfolded ts] have "?σ tbef @ (?tsi ⋅ σ) # ?σ taft = bef @ ?dl # aft" by auto
from this[unfolded append_eq_append_conv_if]
have bef: "bef = ?σ tbef" and tsi: "?tsi ⋅ σ = ?dl"
and aft: "aft = ?σ taft" using llen by auto
from Fun(4) have tF: "⋀ t. t ∈ set ts ⟹ funas_term (t ⋅ σ) ⊆ F"
by (auto simp: funas_args_term_def) (blast)+
from tF[OF mem] have dlF: "funas_term ?dl ⊆ F" unfolding tsi .
with vars_lr rF have drF: "funas_term ?dr ⊆ F" by (force simp: funas_term_subst)
have "(?tsi ⋅ σ,?dr) ∈ qrstep True Q R" unfolding tsi
by (rule qrstepI[OF nf lr _ _ nfs], auto)
note IH = Fun.IH[OF mem this[unfolded switch[of True nfs]] vars disjI1[OF tF[OF mem]]]
from Fun(4)[unfolded t bef aft] dlF have fdlF: "funas_args_term (Fun f (?σ tbef @ ?dl # ?σ taft)) ⊆ F" by (auto simp: funas_args_term_def)
from Fun(4)[unfolded t bef aft] drF have fdrF: "funas_args_term (Fun f (?σ tbef @ ?dr # ?σ taft)) ⊆ F" by (auto simp: funas_args_term_def)
note compat' = dep_compatE[OF dep_compat_NS, of f "?σ tbef" _ "?σ taft"]
note compat_lr = compat'[OF fdlF drF]
note compat_rl = compat'[OF fdrF dlF]
note v = v[unfolded bef aft]
have t: "Fun f ts ⋅ σ = Fun f (?σ tbef @ ?dl # ?σ taft)" unfolding ts tsi[symmetric]
by simp
{
assume pi: "π (f,?n) ?i = Increase ∨ π (f,?n) ?i = Wild"
have "gen_usable_rules ?tsi ^^^ k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
proof (rule rel_dep_mono, rule, intro gen_usable_rulesI)
fix l r
assume "(l, r) ∈ gen_usable_rules ?tsi"
note lr = gen_usable_rulesE[OF this]
show "gen_usable_rule (Fun f ts) (l, r)" unfolding ts
by (rule in_arg[of ?i _ "(l,r)"], insert lr pi, auto)
qed
} note inc = this
{
assume pi: "π (f,?n) ?i = Decrease ∨ π (f,?n) ?i = Wild"
have "gen_usable_rules ?tsi ^^^ invert_dep k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
proof (rule rel_dep_invert_mono, rule, intro gen_usable_rulesI)
fix l r
assume "(l, r) ∈ (gen_usable_rules ?tsi)^-1"
hence "(r,l) ∈ gen_usable_rules ?tsi" by auto
note lr = gen_usable_rulesE[OF this]
show "gen_usable_rule (Fun f ts) (l, r)" unfolding ts
by (rule in_arg[of ?i _ "(r,l)"], insert lr pi, auto)
qed
} note dec = this
{
assume prems: "gen_usable_rules (Fun f ts) ^^^ k ⊆ NS"
note us = this[unfolded ts]
have orient: "{(Fun f ts ⋅ σ, v)} ^^^ k ⊆ NS"
proof (cases "π (f,?n) ?i")
case Ignore
with compat_lr compat_rl
show ?thesis unfolding t v by (cases k, auto)
next
case Increase
have "gen_usable_rules ?tsi ^^^ k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
by (rule inc, insert Increase, auto)
from subset_trans[OF this prems] have "gen_usable_rules ?tsi ^^^ k ⊆ NS" .
from IH this have "{(?dl,?dr)} ^^^ k ⊆ NS" unfolding tsi by simp
with compat_lr compat_rl Increase show ?thesis unfolding t v
by (cases k, auto)
next
case Decrease
have "gen_usable_rules ?tsi ^^^ invert_dep k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
by (rule dec, insert Decrease, auto)
from subset_trans[OF this prems] have "gen_usable_rules ?tsi ^^^ invert_dep k ⊆ NS" .
from IH this have "{(?dl,?dr)} ^^^ invert_dep k ⊆ NS" unfolding tsi by simp
with compat_lr compat_rl Decrease show ?thesis unfolding t v
by (cases k, auto)
next
case Wild
have one: "gen_usable_rules ?tsi ^^^ invert_dep k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
by (rule dec, insert Wild, auto)
have two: "gen_usable_rules ?tsi ^^^ k ⊆ gen_usable_rules (Fun f ts) ^^^ k"
by (rule inc, insert Wild, auto)
from one two have "k = Ignore ∨ gen_usable_rules ?tsi ^^^ Wild ⊆ gen_usable_rules (Fun f ts) ^^^ k"
by (cases k, auto)
thus ?thesis
proof
assume "k = Ignore"
thus ?thesis by auto
next
assume "gen_usable_rules ?tsi ^^^ Wild ⊆ gen_usable_rules (Fun f ts) ^^^ k"
from subset_trans[OF this prems] have "gen_usable_rules ?tsi ^^^ Wild ⊆ NS" .
from IH[THEN conjunct1, rule_format, OF this] have "{(?dl,?dr)} ^^^ Wild ⊆ NS" unfolding tsi by auto
with compat_lr compat_rl Wild show ?thesis unfolding t v
by (cases k, auto)
qed
qed
}
hence orient: "gen_usable_rules (Fun f ts) ^^^ k ⊆ NS ⟶ {(Fun f ts ⋅ σ, v)} ^^^ k ⊆ NS" ..
let ?ts = "λ t. tbef @ t # taft"
let ?C = "λ t. Fun f (?ts t)"
{
fix j
from IH[THEN conjunct2]
obtain u μ where dr: "?dr = u ⋅ μ"
and us: "gen_usable_rules u ^^^ j ⊆ gen_usable_rules ?tsi ^^^ j"
and nf: "μ ` vars_term u ⊆ NFQ"
by blast
have "finite (vars_term (?C u))" by auto
from finite_fresh_names_infinite_univ[OF this infinite_V]
obtain ren ren' where
ren: "⋀ x. x ∈ vars_term (?C u) ⟹ ren x ∉ vars_term (?C u)"
and ren': "⋀ x. x ∈ vars_term (?C u) ⟹ ren' (ren x) = x" by blast
let ?ren = "(λ x. Var (ren x)) :: ('f,'v)subst"
let ?ren' = "(λ x. Var (ren' x)) :: ('f,'v)subst"
let ?u = "u ⋅ ?ren"
let ?μ = "λ x. if (x ∈ vars_term (?C u)) then σ x else (?ren' ∘⇩s μ) x"
have "∃u μ. v = ?C u ⋅ μ ∧ gen_usable_rules u ^^^ j ⊆ gen_usable_rules ?tsi ^^^ j ∧ μ ` vars_term (?C u) ⊆ NFQ"
proof (intro exI conjI)
have "?dr = u ⋅ (?ren ∘⇩s ?μ)" unfolding dr
by (rule term_subst_eq,
unfold subst_compose_def,
insert ren ren', auto)
also have "... = ?u ⋅ ?μ" by simp
finally have "?dr = ?u ⋅ ?μ" .
moreover
have "?σ (tbef @ taft) = map (λ t. t ⋅ ?μ) (tbef @ taft)"
proof (rule map_cong[OF refl])
fix t
assume t: "t ∈ set (tbef @ taft)"
show "t ⋅ σ = t ⋅ ?μ"
by (rule term_subst_eq, insert t, auto)
qed
ultimately
show "v = ?C ?u ⋅ ?μ" unfolding v by simp
next
have "gen_usable_rules ?u ⊆ gen_usable_rules (?u ⋅ ?ren')"
by (rule gen_usable_rules_subst)
also have "?u ⋅ ?ren' = u ⋅ (?ren ∘⇩s ?ren')" by simp
also have "... = u ⋅ Var"
by (rule term_subst_eq, unfold subst_compose_def, insert ren ren', auto)
finally have us': "gen_usable_rules ?u ⊆ gen_usable_rules u" by simp
show "gen_usable_rules ?u ^^^ j ⊆ gen_usable_rules ?tsi ^^^ j"
by (rule subset_trans[OF rel_dep_mono[OF us'] us])
next
{
fix x
assume "x ∈ vars_term (?C ?u)"
hence "x ∈ vars_term (Fun f (tbef @ taft)) ∨ x ∈ vars_term ?u" by auto
hence "?μ x ∈ NFQ"
proof
assume "x ∈ vars_term (Fun f (tbef @ taft))"
with Fun.prems(2) show ?thesis unfolding ts by auto
next
assume "x ∈ vars_term ?u"
then obtain y where y: "y ∈ vars_term u" and x: "x = ren y"
unfolding vars_term_subst by auto
with nf ren ren' show ?thesis unfolding subst_compose_def by auto
qed
}
thus "?μ ` vars_term (?C ?u) ⊆ NFQ" by blast
qed
}
note IH = this
show ?thesis
proof (rule conjI[OF orient])
from gen_usable_rules_split[of f tbef taft] obtain j where
usi: "⋀ s t. gen_usable_rules s ^^^ j ⊆ gen_usable_rules t ^^^ j ⟹ gen_usable_rules (Fun f (tbef @ s # taft)) ⊆ gen_usable_rules (Fun f (tbef @ t # taft))"
by auto
from IH[of j] obtain u μ where v: "v = ?C u ⋅ μ"
and usi_prem: "gen_usable_rules u ^^^ j ⊆ gen_usable_rules ?tsi ^^^ j"
and nf: "μ ` vars_term (?C u) ⊆ NFQ" by auto
note usi = usi[OF usi_prem]
show "∃u μ. v = u ⋅ μ ∧ gen_usable_rules u ^^^ k ⊆ gen_usable_rules (Fun f ts) ^^^ k ∧ μ ` vars_term u ⊆ NFQ"
by (rule exI[of _ "?C u"], rule exI[of _ μ], intro conjI[OF v conjI[OF _ nf]], unfold ts,
rule rel_dep_mono[OF usi])
qed
qed
qed
lemma gen_usable_rules_lemma:
assumes step: "(t ⋅ σ,v) ∈ (qrstep nfs Q R)^*"
and usable: "gen_usable_rules t ⊆ NS"
and σ: "σ ` vars_term t ⊆ NFQ"
and σF: "⋀ x. funas_term (σ x) ⊆ F"
and tsigF: "funas_args_term t ⊆ F"
and ndef: "¬ defined (applicable_rules Q R) (the (root (t ⋅ σ)))"
shows "(t ⋅ σ, v) ∈ NS"
proof -
let ?R = "qrstep nfs Q R"
have tsigF: "funas_args_term (t ⋅ σ) ⊆ F"
proof (cases t)
case (Var x) thus ?thesis using σF[of x] by (cases "σ x", auto simp: funas_args_term_def)
next
case (Fun f ts) thus ?thesis using σF tsigF
by (auto simp: funas_args_term_def funas_term_subst) (blast)+
qed
from rtrancl_imp_relpow[OF step] obtain n
where "(t ⋅ σ, v) ∈ ?R^^n" ..
from this σ usable tsigF ndef
show ?thesis
proof (induction n arbitrary: t σ v)
case 0
thus ?case using refl_NS unfolding refl_on_def by simp
next
case (Suc n)
from Suc.prems(1)
have "(t ⋅ σ, v) ∈ ?R^^(1 + n)" by auto
from this[unfolded relpow_add] obtain u where
one: "(t ⋅ σ, u) ∈ ?R" and n: "(u,v) ∈ ?R ^^ n" by auto
from Suc.prems(4-5) have "funas_args_term (t ⋅ σ) ⊆ F ∧ ¬ defined (applicable_rules Q R) (the (root (t ⋅ σ)))" by auto
from main_technical_lemma[OF one Suc.prems(2) disjI2[OF this], of Increase] Suc.prems(3)
obtain s μ where ns: "(t ⋅ σ, u) ∈ NS" and u: "u = s ⋅ μ"
and us: "gen_usable_rules s ⊆ gen_usable_rules t"
and nf: "μ ` vars_term s ⊆ NFQ"
by auto
from qrstep_imp_nrqrstep[OF _ Suc.prems(5) one[unfolded u]]
have one: "(t ⋅ σ, s ⋅ μ) ∈ nrqrstep nfs Q R" using wwf_qtrs_imp_left_fun[OF wwf] by force
from nrqrstep_preserves_root[OF one] Suc.prems(5) have ndef: "¬ defined (applicable_rules Q R) (the (root (s ⋅ μ)))" by simp
from nrqrstep_funas_args_term[OF wwf RF Suc.prems(4) one] have Fs: "funas_args_term (s ⋅ μ) ⊆ F" .
from Suc.IH[OF n[unfolded u] nf _ Fs ndef] us Suc.prems(3) have "(s ⋅ μ, v) ∈ NS" by auto
with ns trans_NS show ?case unfolding u trans_def by blast
qed
qed
end
section ‹processors using generalized usable rules›
text ‹directly use conditional contraints to define conditional reduction
pair processor. Since the conditional constraints allow us to express unconditional
constraints as well, we also get the generalized reduction pair processor without
conditions as consequence.›
datatype ('f,'v)cond_constraint
= CC_cond bool "('f,'v)rule"
| CC_rewr "('f,'v)term" "('f,'v)term"
| CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint"
| CC_all 'v "('f,'v)cond_constraint"
lemma
fixes P :: "('f, 'v) cond_constraint ⇒ bool"
assumes "⋀ ct s t. P(CC_cond ct (s,t))" and
"⋀ s t. P(CC_rewr s t)" and
"⋀cs c. (⋀c. c ∈ set cs ⟹ P c) ⟹ P c ⟹ P(CC_impl cs c)" and
"⋀ x c. P c ⟹ P(CC_all x c)"
shows cond_constraint_induct[case_names cond rewr impl all, induct type: cond_constraint]:
"P c"
by (induct c, insert assms, auto)
definition disjoint_variant :: "('f,'v)rule list ⇒ ('f,'v)rule list ⇒ bool"
where "disjoint_variant sts uvs ≡
length sts = length uvs ∧
(∀ i < length sts. sts ! i =⇩v uvs ! i) ∧
is_partition (map vars_rule uvs)"
text ‹define, which constraints must be present, where the two nats specify how many pairs
we take as predecessors and successofs (BEFore and AFTer)›
definition initial_conditions_gen :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ nat ⇒ 'a set ⇒ 'a ⇒ 'a list set" where
"initial_conditions_gen p bef_len aft_len P st ≡ let
pairs = (λ n. { sts. length sts = n ∧ set sts ⊆ P});
all = { bef @ st # aft | bef aft. bef ∈ pairs bef_len ∧ aft ∈ pairs aft_len}
in { bef_st_aft . bef_st_aft ∈ all ∧ (∀ i < bef_len + aft_len. p (bef_st_aft ! i) (bef_st_aft ! Suc i))}"
lemma initial_conditions_gen_mono: assumes "⋀ s t. p s t ⟹ q s t"
shows "initial_conditions_gen p bef_len aft_len P st ⊆ initial_conditions_gen q bef_len aft_len P st"
using assms unfolding initial_conditions_gen_def Let_def by auto
text ‹datatype to represent atomic constraints on the orders›
datatype condition_type = Bound | Strict | Non_Strict
fun condition_of :: "'f ⇒ condition_type ⇒ ('f,'v)rule ⇒ ('f,'v)cond_constraint" where
"condition_of c Bound (s,_) = CC_cond False (s,Fun c [])"
| "condition_of c Strict st = CC_cond True st"
| "condition_of c Non_Strict st = CC_cond False st"
definition constraint_of :: "'f ⇒ condition_type ⇒ ('f,'v)rule list ⇒ nat ⇒ ('f,'v)cond_constraint" where
"constraint_of c ctype uvs bef ≡
CC_impl
(map (λ i. CC_rewr (snd (uvs ! i)) (fst (uvs ! Suc i))) [0 ..< length uvs - 1])
(condition_of c ctype (uvs ! bef))"
context fixed_trs_dep_order
begin
definition rel_of :: "bool ⇒ ('f,'v)trs" where
"rel_of ct ≡ if ct then S else NS"
definition normal_F_subst :: "('f, 'v) subst ⇒ bool" where
"normal_F_subst σ ⟷ (⋃(funas_term ` range σ) ⊆ F) ∧ range σ ⊆ NF_trs R"
text ‹if we have minimality (m is true), then demand strong normalization›
definition m_SN :: "('f, 'v) term ⇒ bool" where
"m_SN t ⟷ m ⟶ SN_on (qrstep nfs Q R) {t}"
fun cc_models :: "('f,'v)subst ⇒ ('f,'v)cond_constraint ⇒ bool" (infix "⊨" 51) where
"σ ⊨ CC_cond ct (s,t) = ((s ⋅ σ,t ⋅ σ) ∈ rel_of ct)"
| "σ ⊨ CC_impl c1 c2 = (Ball (set c1) (cc_models σ) ⟶ σ ⊨ c2)"
| "σ ⊨ CC_rewr s t = (m_SN (s ⋅ σ) ∧ (s ⋅ σ, t ⋅ σ) ∈ (qrstep nfs Q R)^* ∧ t ⋅ σ ∈ NF_terms Q)"
| "σ ⊨ CC_all x c = (∀ (t :: ('f,'v)term). funas_term t ⊆ F ⟶ t ∈ NF_trs R ⟶ (σ (x := t)) ⊨ c)"
definition cc_valid :: "('f,'v)cond_constraint ⇒ bool" where
"cc_valid c ≡ ∀ σ. normal_F_subst σ ⟶ σ ⊨ c"
lemma cc_validE[elim]: "cc_valid c ⟹ normal_F_subst σ ⟹ σ ⊨ c" unfolding cc_valid_def by blast
lemma cc_validI[intro!]: "⟦⋀ σ. normal_F_subst σ ⟹ σ ⊨ c⟧ ⟹ cc_valid c" unfolding cc_valid_def by blast
definition cc_equiv :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint ⇒ bool" (infix "=cc" 49) where
"c =cc d ≡ ∀ σ. σ ⊨ c = σ ⊨ d"
definition cc_implies :: "('f,'v)cond_constraint ⇒ ('f,'v)cond_constraint ⇒ bool" (infix "⟶cc" 49) where
"c ⟶cc d ≡ ∀ σ. σ ⊨ c ⟶ σ ⊨ d"
lemma cc_equiv_substE: "c =cc d ⟹ σ ⊨ c = σ ⊨ d" unfolding cc_equiv_def by auto
lemma cc_equivI[intro]: "⟦⋀ σ. σ ⊨ c = σ ⊨ d⟧ ⟹ c =cc d" unfolding cc_equiv_def by auto
lemma cc_impliesI[intro]: "⟦⋀ σ. σ ⊨ c ⟹ σ ⊨ d⟧ ⟹ c ⟶cc d" unfolding cc_implies_def by auto
lemma cc_impliesE[elim]: "c ⟶cc d ⟹ cc_valid c ⟹ cc_valid d" unfolding cc_implies_def cc_valid_def by auto
lemma cc_implies_substE[elim]: "c ⟶cc d ⟹ σ ⊨ c ⟹ σ ⊨ d" unfolding cc_implies_def cc_valid_def by auto
lemma cc_equiv_validE: "c =cc d ⟹ cc_valid c = cc_valid d" unfolding cc_valid_def cc_equiv_def by auto
lemma cc_equiv_refl[simp]: "c =cc c" by auto
lemma cc_implies_refl[simp]: "c ⟶cc c" by auto
text ‹we do not have to consider all preceeding / succeeding pairs, but only those which are
connected in the dependency graph. This optimization is also integrated in AProVE›
definition initial_conditions :: "nat ⇒ nat ⇒ ('f,'v)trs ⇒ ('f,'v)rule ⇒ ('f,'v)rule list set" where
"initial_conditions bef aft P ≡ initial_conditions_gen (λ st uv. (st,uv) ∈ DG nfs m P Q R) bef aft P"
text ‹main test, whether all required constraints are present to ensure that some pair is bounded/decreasing›
definition constraint_present :: "nat ⇒ nat ⇒ ('f,'v)trs ⇒
condition_type ⇒ ('f,'v)cond_constraint set ⇒ ('f,'v)rule ⇒ bool" where
"constraint_present bef aft P ctype ccs st ≡
(∀ sts. sts ∈ initial_conditions bef aft P st ⟶
(∃ c uvs. disjoint_variant sts uvs ∧ c ∈ ccs ∧ c ⟶cc constraint_of const ctype uvs bef))"
fun tcondition_of :: "condition_type ⇒ ('f,'v)rule ⇒ bool" where
"tcondition_of Bound (s,t) = ((s,Fun const []) ∈ NS)"
| "tcondition_of Strict st = (st ∈ S)"
| "tcondition_of Non_Strict st = (st ∈ NS)"
lemma tcondition_of:
assumes model: "σ ⊨ condition_of const ctype (s,t)"
shows "tcondition_of ctype (s ⋅ σ,t ⋅ σ)"
using assms by (cases ctype, auto simp: rel_of_def)
text ‹the conditional reduction pair processor, as it is formulated on chains,
where here we already assume that the chains respect the signature F›
lemma conditional_general_reduction_pair_chains:
assumes U_NS: "gen_usable_rules_pairs (P ∪ Pw) ⊆ NS"
and chain: "min_ichain_sig (nfs,m,P,Pw,Q,Rs,Rw) F s t σ"
and nvar: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ is_Fun s ∧ is_Fun t"
and var_cond: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ vars_term t ⊆ vars_term s"
and ndef: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ ¬ defined (applicable_rules Q (Rs ∪ Rw)) (the (root t))"
and PF: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ funas_args_term t ⊆ F"
and orient: "P ∪ Pw ⊆ Ps ∪ Pns"
and cS: "Ball Ps (constraint_present bef aft (P ∪ Pw) Strict ccs)"
and cNS: "Ball Pns (constraint_present bef aft (P ∪ Pw) Non_Strict ccs)"
and cB: "Ball Pb (constraint_present bef aft (P ∪ Pw) Bound ccs)"
and ccs: "Ball ccs cc_valid"
and R: "Rs ∪ Rw = R"
shows "∃ i. min_ichain_sig (nfs,m,P - Ps, Pw - Ps,Q,Rs,Rw) F (shift s i) (shift t i) (shift σ i)
∨ min_ichain_sig (nfs,m,P - Pb, Pw - Pb,Q,Rs,Rw) F (shift s i) (shift t i) (shift σ i)"
proof -
let ?DP = "(nfs,m,P,Pw,Q,Rs,Rw)"
let ?DPm = "λ S. (nfs,m,P - S,Pw - S,Q,Rs,Rw)"
let ?DP_Ps = "?DPm Ps"
let ?DP_Pb = "?DPm Pb"
show ?thesis
proof (cases "(INFM i. (s i, t i) ∈ Ps) ∧ (INFM i. (s i, t i) ∈ Pb)")
case False
then obtain i where disj: "(∀ j ≥ i. (s j, t j) ∉ Ps) ∨ (∀ j ≥ i. (s j, t j) ∉ Pb)"
unfolding INFM_nat_le by blast
let ?s = "shift s"
let ?t = "shift t"
let ?σ = "shift σ"
from disj
show ?thesis
proof
assume nS: "(∀ j ≥ i. (s j, t j) ∉ Ps)"
let ?DP = "(nfs, m, P - Ps, Pw - Ps, Q, Rs - {}, Rw - {})"
have "∃ i. min_ichain_sig ?DP F (?s i) (?t i) (?σ i)"
proof (rule min_ichain_split_sig[OF chain], rule)
assume "min_ichain_sig (nfs, m, Ps ∩ (P ∪ Pw), P ∪ Pw - Ps, Q, {} ∩ (Rs ∪ Rw), Rs ∪ Rw - {}) F s t σ"
hence "INFM i. (s i, t i) ∈ Ps ∩ (P ∪ Pw)" by (auto simp: ichain.simps)
with nS show False unfolding INFM_nat_le by blast
qed
thus ?thesis by auto
next
assume nB: "(∀ j ≥ i. (s j, t j) ∉ Pb)"
let ?DP = "(nfs, m, P - Pb, Pw - Pb, Q, Rs - {}, Rw - {})"
have "∃ i. min_ichain_sig ?DP F (?s i) (?t i) (?σ i)"
proof (rule min_ichain_split_sig[OF chain], rule)
assume "min_ichain_sig (nfs, m, Pb ∩ (P ∪ Pw), P ∪ Pw - Pb, Q, {} ∩ (Rs ∪ Rw), Rs ∪ Rw - {}) F s t σ"
hence "INFM i. (s i, t i) ∈ Pb ∩ (P ∪ Pw)" by (auto simp: ichain.simps)
with nB show False unfolding INFM_nat_le by blast
qed
thus ?thesis by auto
qed
next
case True
let ?QR = "qrstep nfs Q R"
let ?ndef = "λ t. ¬ defined (applicable_rules Q R) (the (root t))"
from chain have ichain: "ichain ?DP s t σ" and σF: "funas_ichain s t σ ⊆ F" by auto
{
fix i
from σF have "⋃(funas_term ` range (σ i)) ⊆ F" unfolding funas_ichain_def by auto
} note σF = this
let ?st = "λ i. (s i, t i)"
from ichain have P_Pw: "⋀ i. ?st i ∈ P ∪ Pw" unfolding ichain.simps by auto
from ichain have NF: "⋀ i. s i ⋅ σ i ∈ NFQ" unfolding ichain.simps by auto
{
fix ctype PP i
assume i_bef: "i ≥ bef" and mem: "(s i, t i) ∈ PP"
assume cp: "Ball PP (constraint_present bef aft (P ∪ Pw) ctype ccs)"
with mem have cp: "constraint_present bef aft (P ∪ Pw) ctype ccs (s i, t i)" by auto
def j ≡ "i - bef"
def n ≡ "Suc (bef + aft)"
let ?j = "λ i. i + j"
from i_bef j_def have i_j_bef: "i = ?j bef" by auto
let ?sts_gen = "λ j. map (λ i. ?st (i + j))"
let ?sts = "?sts_gen j [0 ..< n]"
let ?bef = "?sts_gen j [0 ..< bef]"
let ?aft = "?sts_gen (j + Suc bef) [0 ..< aft]"
have "?sts = ?sts_gen j [0 ..< bef + Suc 0 + aft]" unfolding n_def by auto
also have "... = ?bef @ ?st i # ?aft"
unfolding map_upt_add i_j_bef by (simp add: ac_simps)
finally have sts: "?sts = ?bef @ ?st i # ?aft" .
have sts_init: "?sts ∈ initial_conditions bef aft (P ∪ Pw) (s i, t i)"
unfolding initial_conditions_def initial_conditions_gen_def Let_def
proof (rule, rule, rule, intro exI conjI, rule sts, insert P_Pw, (auto)[2], intro allI impI)
fix i
assume "i < bef + aft"
with n_def have i: "i < n" "Suc i < n" by auto
hence sts: "(?sts ! i, ?sts ! Suc i) = (?st (?j i), ?st (Suc (?j i)))" by auto
show "(?sts ! i, ?sts ! Suc i) ∈ DG nfs m (P ∪ Pw) Q R" unfolding sts
by (rule DG_I[of _ _ _ _ _ "σ (?j i)" "σ (Suc (?j i))"],
insert chain R, auto simp: ichain.simps minimal_cond_def)
qed
from cp[unfolded constraint_present_def, rule_format, OF sts_init]
obtain c uvs where var: "disjoint_variant ?sts uvs" and c_ccs: "c ∈ ccs" and c_uvs: "c ⟶cc constraint_of const ctype uvs bef" by auto
def us ≡ "λ i. fst (uvs ! i)"
def vs ≡ "λ i. snd (uvs ! i)"
let ?uv = "λ i. (us i, vs i)"
from cc_impliesE[OF c_uvs] ccs c_ccs
have valid: "cc_valid (constraint_of const ctype uvs bef)" by auto
note var = var[unfolded disjoint_variant_def]
from var have part: "is_partition (map vars_rule uvs)" and ulen: "length uvs = n" by auto
{
fix i
assume "i < n"
with var have "?st (?j i) =⇩v ?uv i" unfolding us_def vs_def by auto
from eq_rule_mod_varsE[OF this] this have
"∃ τ. s (?j i) = us i ⋅ τ ∧ t (?j i) = vs i ⋅ τ ∧ range τ ⊆ range Var" "?st (?j i) =⇩v ?uv i" by auto
}
hence eq: "⋀ i. i < n ⟹ ?st (?j i) =⇩v ?uv i" and taus: "∀ i. (∃ τ. i < n ⟶ s (?j i) = us i ⋅ τ ∧ t (?j i) = vs i ⋅ τ ∧ range τ ⊆ range Var)" by blast+
from choice[OF taus] obtain τ where st_uv: "⋀ i. i < n ⟹ s (?j i) = us i ⋅ τ i" "⋀ i. i < n ⟹ t (?j i) = vs i ⋅ τ i"
and τ: "⋀ i. i < n ⟹ range (τ i) ⊆ range Var" by auto
let ?sigs = "map (λ i. τ i ∘⇩s σ (?j i)) [0 ..< n]"
def γ ≡ "λ x. if x ∈ ⋃(vars_rule ` ?uv ` {0 ..< n}) then fun_merge ?sigs (map vars_rule uvs) x else Var x"
{
fix i x
assume i: "i < n" and x: "x ∈ vars_rule (uvs ! i)"
hence "x ∈ ⋃(vars_rule ` ?uv ` {0 ..< n})" unfolding us_def vs_def by auto
hence "γ x = fun_merge ?sigs (map vars_rule uvs) x" unfolding γ_def by auto
also have "… = (?sigs ! i) x"
using part [unfolded is_partition_alt is_partition_alt_def]
by (intro fun_merge_part, insert i x ulen, auto simp: is_partition_def)
also have "… = (τ i ∘⇩s σ (?j i)) x" using i by simp
finally have "γ x = (τ i ∘⇩s σ (?j i)) x" .
} note γ = this
{
fix i
assume i: "i < n"
have "us i ⋅ γ = us i ⋅ (τ i ∘⇩s σ (?j i))"
by (rule term_subst_eq, rule γ[OF i], unfold us_def vars_rule_def, auto)
also have "… = s (?j i) ⋅ σ (?j i)" unfolding st_uv[OF i] by simp
finally have "us i ⋅ γ = s (?j i) ⋅ σ (?j i)" .
} note u_s = this
{
fix i
assume i: "i < n"
have "vs i ⋅ γ = vs i ⋅ (τ i ∘⇩s σ (?j i))"
by (rule term_subst_eq, rule γ[OF i], unfold vs_def vars_rule_def, auto)
also have "… = t (?j i) ⋅ σ (?j i)" unfolding st_uv[OF i] by simp
finally have "vs i ⋅ γ = t (?j i) ⋅ σ (?j i)" .
} note v_t = this
have gammaF: "normal_F_subst γ" unfolding normal_F_subst_def
proof -
{
fix x
have "funas_term (γ x) ⊆ F ∧ γ x ∈ NF_trs R"
proof (cases "x ∈ ⋃(vars_rule ` ?uv ` {0 ..< n})")
case False
hence x: "γ x = Var x" unfolding γ_def by auto
from NF_Var_is_Fun[of "lhss R" x] wwf_var_cond[OF wwf] have "Var x ∈ NF_trs R" by force
thus ?thesis using x by auto
next
case True
then obtain i where i: "i < n" and xx: "x ∈ vars_rule (?uv i)" by auto
from eq_rule_mod_vars_var_cond[OF eq[OF i] var_cond[OF P_Pw]] xx
have x: "x ∈ vars_term (us i)" unfolding vars_rule_def by auto
hence "us i ⊵ Var x" by auto
hence supt: "us i ⋅ γ ⊵ γ x" by auto
from u_s[OF i] NF[of "i+j"] NFQ have "us i ⋅ γ ∈ NF_trs R" by auto
from NF_subterm[OF this supt] have NF: "γ x ∈ NF_trs R" .
from τ[OF i] obtain y where τ: "τ i x = Var y" by auto
have "γ x = (τ i ∘⇩s σ (?j i)) x"
by (rule γ[OF i], insert xx us_def vs_def, auto)
also have "… = σ (?j i) y" unfolding subst_compose_def τ by simp
finally have "funas_term (γ x) ⊆ F" using σF by auto
with NF show ?thesis by auto
qed
}
thus "⋃(funas_term ` range γ) ⊆ F ∧ range γ ⊆ NF_trs R" by auto
qed
have bef: "bef < n" unfolding n_def by auto
from cc_validE[OF valid gammaF]
have model: "γ ⊨ constraint_of const ctype uvs bef" .
have rewr: "Ball (set (map (λi. CC_rewr (snd (uvs ! i)) (fst (uvs ! Suc i))) [0..<length uvs - 1])) (cc_models γ)"
proof
fix c
assume "c ∈ set (map (λi. CC_rewr (snd (uvs ! i)) (fst (uvs ! Suc i))) [0..<length uvs - 1])"
then obtain i where i: "i < n - 1" and c: "c = CC_rewr (vs i) (us (Suc i))" unfolding us_def vs_def ulen by auto
from i have i: "i < n" "Suc i < n" unfolding n_def by auto
show "γ ⊨ c" unfolding c cc_models.simps u_s[OF i(2)] v_t[OF i(1)] using chain
by (auto simp: minimal_cond_def R ichain.simps m_SN_def)
qed
from this model[unfolded constraint_of_def]
have "γ ⊨ condition_of const ctype (us bef, vs bef)" unfolding us_def vs_def by simp
from tcondition_of[OF this, unfolded u_s[OF bef] v_t[OF bef]]
have "tcondition_of ctype (s i ⋅ σ i, t i ⋅ σ i)" unfolding i_j_bef .
} note main_constraint = this
def cc ≡ "(Fun const []) :: ('f,'v)term"
def u ≡ "λ i. s (i + bef) ⋅ σ (i + bef)"
def v ≡ "λ i. t (i + bef) ⋅ σ (i + bef)"
let ?st = "λ i. (s (i + bef), t (i + bef))"
note uv = u_def v_def
{
fix i
assume i: "?st i ∈ Ps"
from main_constraint[OF _ this cS] have "(u i, v i) ∈ S" unfolding uv by simp
} note PS = this
{
fix i
assume i: "?st i ∈ Pns"
from main_constraint[OF _ this cNS] have "(u i, v i) ∈ NS" unfolding uv by simp
} note PNS = this
{
fix i
assume i: "?st i ∈ Pb"
from main_constraint[OF _ this cB] have "(u i, cc) ∈ NS" unfolding uv cc_def by simp
} note PB = this
{
fix i
from ichain have steps: "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?QR^*"
and P: "(s i, t i) ∈ P ∪ Pw"
and NF: "s i ⋅ σ i ∈ NFQ" unfolding ichain.simps R by auto
from P U_NS have orient: "gen_usable_rules (t i) ⊆ NS" unfolding gen_usable_rules_pairs_def by force
from nvar[OF P] obtain f ts where ti: "t i = Fun f ts" by (cases "t i", auto)
from PF[OF P] have tF: "funas_args_term (t i) ⊆ F" .
from ndef[OF P] have "?ndef (t i)" unfolding R .
with ti have ndef: "?ndef (t i ⋅ σ i)" by simp
{
fix x
assume "x ∈ vars_term (t i)"
with var_cond[OF P] have "x ∈ vars_term (s i)" by auto
hence "s i ⊵ Var x" by auto
from NF_subterm[OF NF supteq_subst[OF this, of "σ i"]] have "σ i x ∈ NFQ" by simp
}
hence NF: "σ i ` vars_term (t i) ⊆ NFQ" by auto
have NS: "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ NS"
by (rule gen_usable_rules_lemma[OF steps orient NF _ tF ndef], insert σF, auto)
} note NS = this
{
fix i
have "(v i, u (Suc i)) ∈ NS" unfolding uv using NS[of "i+bef"] by simp
} note NS = this
{
fix i
from P_Pw[of "i + bef"] have "?st i ∈ P ∪ Pw" .
with orient have "?st i ∈ Ps ∪ Pns" by auto
with PS PNS have "(u i, v i) ∈ NS ∪ S" by auto
with NS[of i]
trans_NS[unfolded trans_def] compat_S_NS have "(u i, u (Suc i)) ∈ NS ∪ S" by blast
} note orient = this
{
fix i
assume "?st i ∈ Ps"
from PS[OF this] NS[of i] compat_S_NS have "(u i, u (Suc i)) ∈ S" by auto
}
hence Ps: "{i. ?st i ∈ Ps} ⊆ {i. (u i, u (Suc i)) ∈ S}" by auto
from PB have "{i. ?st i ∈ Pb} ⊆ {i. (u i, cc) ∈ NS ∪ S}" by auto
from chain_split[of _ "λ i. i" u, OF Ps this orient]
have disj: "(∀⇩∞j. ?st j ∉ Ps) ∨ (∀⇩∞j. ?st j ∉ Pb)" by auto
note shift = Infm_double_shift[of "λ s t. (s,t) ∈ P" s bef t for P]
from True[folded shift[of Ps] shift[of Pb]]
have "(∃⇩∞i. ?st i ∈ Ps) ∧ (∃⇩∞i. ?st i ∈ Pb)" by auto
with disj have False unfolding INFM_nat_le MOST_nat_le by auto
thus ?thesis ..
qed
qed
text ‹the same processor again, but here the result on signature extensions is integrated›
lemma conditional_general_reduction_pair_proc:
assumes R: "Rs ∪ Rw = R"
and nvar: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ is_Fun s ∧ is_Fun t"
and var_cond: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ vars_term t ⊆ vars_term s"
and ndef: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ ¬ defined (applicable_rules Q R) (the (root t))"
and PF: "funas_args_trs (P ∪ Pw) ⊆ F"
and U_NS: "gen_usable_rules_pairs (P ∪ Pw) ⊆ NS"
and orient: "P ∪ Pw ⊆ Ps ∪ Pns"
and cS: "Ball Ps (constraint_present bef aft (P ∪ Pw) Strict ccs)"
and cNS: "Ball Pns (constraint_present bef aft (P ∪ Pw) Non_Strict ccs)"
and cB: "Ball Pb (constraint_present bef aft (P ∪ Pw) Bound ccs)"
and ccs: "Ball ccs cc_valid"
and finiteS: "finite_dpp (nfs,m,P - Ps, Pw - Ps,Q,Rs,Rw)"
and finiteB: "finite_dpp (nfs,m,P - Pb, Pw - Pb,Q,Rs,Rw)"
shows "finite_dpp (nfs,m,P, Pw,Q,Rs,Rw)"
proof (rule ccontr)
let ?D = "(nfs,m,P, Pw,Q,Rs,Rw)"
let ?Ds = "(nfs,m,P - Ps, Pw - Ps,Q,Rs,Rw)"
let ?Db = "(nfs,m,P - Pb, Pw - Pb,Q,Rs,Rw)"
{
from ex_inj obtain tn :: "('f,'v)term ⇒ nat" where tn: "inj tn" by auto
from infinite_countable_subset[OF infinite_V] obtain nv :: "nat ⇒ 'v" where nv: "inj nv" by blast
from inj_comp[OF nv tn] have "∃ c :: ('f,'v)term ⇒ 'v. inj c" by blast
}
then obtain c :: "('f,'v)term ⇒ 'v" where inj: "inj c" ..
interpret cleaning_innermost F c by (unfold_locales, rule inj)
assume "¬ ?thesis"
then obtain s t σ where chain: "min_ichain ?D s t σ" unfolding finite_dpp_def by auto
from R have RR: "R = Rs ∪ Rw" by simp
from QF have QF': "QF_cond F Q" unfolding QF_cond_def by auto
from PF have PF': "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ funas_args_term t ⊆ F"
unfolding funas_args_trs_def funas_args_rule_def [abs_def] by force
from clean_min_ichain_below[of Q Rs Rw, unfolded R, OF NFQ QF' RF PF wwf _ var_cond chain]
nvar ndef obtain σ where "min_ichain_sig ?D F s t σ" by blast
from conditional_general_reduction_pair_chains[where Pb = Pb, OF U_NS this nvar var_cond ndef[unfolded RR] PF' orient cS cNS cB ccs R]
have "∃ i. min_ichain_sig ?Ds F (shift s i) (shift t i) (shift σ i) ∨ min_ichain_sig ?Db F (shift s i) (shift t i) (shift σ i)" .
then obtain s t σ where "min_ichain_sig ?Ds F s t σ ∨ min_ichain_sig ?Db F s t σ" by blast
hence "min_ichain ?Ds s t σ ∨ min_ichain ?Db s t σ" unfolding min_ichain_sig.simps by blast
with finiteS finiteB show False unfolding finite_dpp_def by blast
qed
text ‹we can also derive the unconditional general reduction pair processor by taking bef = aft = 0›
lemma general_reduction_pair_proc:
assumes R: "Rs ∪ Rw = R"
and nvar: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ is_Fun s ∧ is_Fun t"
and var_cond: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ vars_term t ⊆ vars_term s"
and ndef: "⋀ s t. (s,t) ∈ P ∪ Pw ⟹ ¬ defined (applicable_rules Q R) (the (root t))"
and PF: "funas_args_trs (P ∪ Pw) ⊆ F"
and U_NS: "gen_usable_rules_pairs (P ∪ Pw) ⊆ NS"
and orient: "P ∪ Pw ⊆ Ps ∪ Pns"
and orientS: "Ps ⊆ S"
and orientNS: "Pns ⊆ NS"
and orientB: "⋀ s t. (s,t) ∈ Pb ⟹ (s,Fun const []) ∈ NS"
and finiteS: "finite_dpp (nfs,m,P - Ps, Pw - Ps,Q,Rs,Rw)"
and finiteB: "finite_dpp (nfs,m,P - Pb, Pw - Pb,Q,Rs,Rw)"
shows "finite_dpp (nfs,m,P, Pw,Q,Rs,Rw)"
proof (rule conditional_general_reduction_pair_proc[OF R nvar var_cond ndef PF U_NS orient _ _ _ _ finiteS finiteB])
let ?c = "λ ctype st. constraint_of const ctype [st] 0"
let ?cS = "(?c Strict) ` Ps"
let ?cNS = "(?c Non_Strict) ` Pns"
let ?cB = "(?c Bound) ` Pb"
let ?ccs = "?cS ∪ ?cNS ∪ ?cB"
{
fix ctype PP
have "Ball PP (constraint_present 0 0 (P ∪ Pw) ctype (?c ctype ` PP))"
proof (intro ballI, unfold constraint_present_def, intro allI impI)
fix st sts
assume mem: "st ∈ PP" and sts: "sts ∈ initial_conditions 0 0 (P ∪ Pw) st"
obtain s t where st: "st = (s,t)" by force
from sts[unfolded initial_conditions_def initial_conditions_gen_def Let_def] st have sts: "sts = [(s,t)]" by simp
have disj: "disjoint_variant sts [(s,t)]" unfolding sts disjoint_variant_def
by (auto simp: is_partition_def)
show "∃c uvs. disjoint_variant sts uvs ∧ c ∈ (?c ctype) ` PP ∧ c ⟶cc constraint_of const ctype uvs 0"
by (intro exI conjI, rule disj, insert st mem, auto)
qed
} note present = this
from present[of Ps Strict]
show "Ball Ps (constraint_present 0 0 (P ∪ Pw) Strict ?ccs)" by (force simp: constraint_present_def)
from present[of Pns Non_Strict]
show "Ball Pns (constraint_present 0 0 (P ∪ Pw) Non_Strict ?ccs)" by (force simp: constraint_present_def)
from present[of Pb Bound]
show "Ball Pb (constraint_present 0 0 (P ∪ Pw) Bound ?ccs)" by (force simp: constraint_present_def)
show "Ball ?ccs cc_valid"
proof
fix cc
assume cc: "cc ∈ ?ccs"
show "cc_valid cc"
proof
fix σ
assume "normal_F_subst σ"
hence σF: "⋃(funas_term ` range σ) ⊆ F" unfolding normal_F_subst_def by auto
note stable_S = F_subst_closedD[OF stable_S σF]
note stable_NS = F_subst_closedD[OF stable_NS σF]
{
assume "cc ∈ ?cS"
then obtain s t where st: "(s,t) ∈ Ps" and cc: "cc = ?c Strict (s,t)" by force
from st orientS have "(s,t) ∈ S" by auto
from stable_S[OF this]
have "σ ⊨ cc" unfolding cc constraint_of_def by (simp add: rel_of_def)
}
moreover
{
assume "cc ∈ ?cB"
then obtain s t where st: "(s,t) ∈ Pb" and cc: "cc = ?c Bound (s,t)" by force
from st orientB have "(s,Fun const []) ∈ NS" by auto
from stable_NS[OF this]
have "σ ⊨ cc" unfolding cc constraint_of_def by (simp add: rel_of_def)
}
moreover
{
assume "cc ∈ ?cNS"
then obtain s t where st: "(s,t) ∈ Pns" and cc: "cc = ?c Non_Strict (s,t)" by force
from st orientNS have "(s,t) ∈ NS" by auto
from stable_NS[OF this]
have "σ ⊨ cc" unfolding cc constraint_of_def by (simp add: rel_of_def)
}
ultimately show "σ ⊨ cc" using cc by blast
qed
qed
qed auto
end
end