theory SCNP
imports
QTRS.Term_Order
QTRS.Lexicographic_Extension
QTRS.List_Order
begin
fun proja :: "('f,'v)term ⇒ nat ⇒ ('f,'v)term"
where "proja (Fun f ts) i = (if i < length ts then ts ! i else Fun f ts)"
definition lterms :: "(('f × nat) ⇒ (nat × nat)list) ⇒ ('f,'v)term ⇒ (('f,'v)term × nat)list"
where "lterms π ≡ λ t. case t of Fun f ts ⇒ map (λ(i,n). (proja (Fun f ts) i, n)) (π (f,length ts))"
locale scnp = redtriple_order S NS NST + list_order_extension s_ext ns_ext
for S NS NST :: "('f,'v)trs" and
s_ext ns_ext :: "(('f,'v)term × nat) list_ext" +
fixes π :: "('f × nat) ⇒ (nat × nat)list"
begin
abbreviation gt :: "nat rel" where "gt ≡ {(a,b). a > b}"
abbreviation ge :: "nat rel" where "ge ≡ {(a,b). a ≥ b}"
definition label_s :: "(('f, 'v) term × nat) rel"
where "label_s ≡ lex_two S NS gt"
definition label_ns :: "(('f, 'v) term × nat) rel"
where "label_ns ≡ lex_two S NS ge"
lemma trans_S_O: "S O S ⊆ S" using trans_S_point by auto
lemma trans_NS_O: "NS O NS ⊆ NS" using trans_NS_point by auto
lemmas trans_compat = compat_NS_S compat_S_NS trans_S_O trans_NS_O
lemma label_s_ns_order_pair: "SN_order_pair label_s label_ns"
proof(unfold_locales)
{
fix s t u
assume st: "(s,t) ∈ label_s" and tu: "(t,u) ∈ label_s"
from st[unfolded label_s_def] have st: "(s,t) ∈ lex_two S NS gt" .
from tu[unfolded label_s_def] have tu: "(t,u) ∈ lex_two S NS gt" by blast
have "(s,u) ∈ lex_two S NS gt"
by (rule lex_two_compat[of NS S gt gt, OF trans_compat _ st tu], auto)
hence "(s,u) ∈ label_s" unfolding label_s_def by blast
}
thus "trans label_s" unfolding trans_def by blast
next
{
fix s t u
assume st: "(s,t) ∈ label_ns" and tu: "(t,u) ∈ label_ns"
from st[unfolded label_ns_def] have st: "(s,t) ∈ lex_two S NS ge" .
from tu[unfolded label_ns_def] have tu: "(t,u) ∈ lex_two S NS ge" .
have "(s,u) ∈ lex_two S NS ge"
by (rule lex_two_compat[of NS S ge ge, OF trans_compat _ st tu], auto)
hence "(s,u) ∈ label_ns" unfolding label_ns_def by blast
}
thus "trans label_ns" unfolding trans_def by blast
next
{
fix s t u
assume st: "(s,t) ∈ label_ns" and tu: "(t,u) ∈ label_s"
from st[unfolded label_ns_def] have st: "(s,t) ∈ lex_two S NS ge" .
from tu[unfolded label_s_def] have tu: "(t,u) ∈ lex_two S NS gt" .
have "(s,u) ∈ lex_two S NS gt"
by (rule lex_two_compat[of NS S ge gt, OF trans_compat _ st tu], auto)
hence "(s,u) ∈ label_s" unfolding label_s_def by blast
}
thus "label_ns O label_s ⊆ label_s" by blast
next
{
fix s t u
assume st: "(s,t) ∈ label_s" and tu: "(t,u) ∈ label_ns"
from st[unfolded label_s_def] have st: "(s,t) ∈ lex_two S NS gt" .
from tu[unfolded label_ns_def] have tu: "(t,u) ∈ lex_two S NS ge" .
have "(s,u) ∈ lex_two S NS gt"
by (rule lex_two_compat'[of NS S gt ge, OF trans_compat _ st tu], auto)
hence "(s,u) ∈ label_s" unfolding label_s_def by blast
}
thus "label_s O label_ns ⊆ label_s" by blast
next
show "SN label_s" unfolding label_s_def
by (rule lex_two[OF compat_NS_S], insert SN SN_nat_gt, auto)
next
show "refl label_ns" unfolding refl_on_def label_ns_def using refl_NS
unfolding refl_on_def by auto
qed
definition NST_label_mul :: "('f,'v)trs" where
"NST_label_mul ≡ {(Fun f ts, Fun g ss) | f g ts ss. (lterms π (Fun f ts), lterms π (Fun g ss)) ∈ ns_ext label_s label_ns}"
definition S_label_mul :: "('f,'v)trs" where
"S_label_mul ≡ {(Fun f ts, Fun g ss) | f g ts ss. (lterms π (Fun f ts), lterms π (Fun g ss)) ∈ s_ext label_s label_ns}"
lemma scnp_mul: "root_redtriple_order S_label_mul NS NST_label_mul"
(is "root_redtriple_order ?S _ ?NST")
proof -
note S = S_label_mul_def
note NST = NST_label_mul_def
let ?ml = "λ f ts. lterms π (Fun f ts)"
let ?S' = "s_ext label_s label_ns"
let ?NS' = "ns_ext label_s label_ns"
from subst_S[unfolded subst.closed_def]
have subS: "⋀ σ s t. (s,t) ∈ S ⟹ (s ⋅ σ, t ⋅ σ) ∈ S" by auto
from subst_NS[unfolded subst.closed_def]
have subNS: "⋀ σ s t. (s,t) ∈ NS ⟹ (s ⋅ σ, t ⋅ σ) ∈ NS" by auto
let ?σ = "(λ (σ :: ('f,'v)subst) s. s ⋅ σ)"
let ?σn = "(λ σ (t,n). (?σ σ t, n)) :: ('f,'v)subst ⇒ ('f,'v)term × nat ⇒ ('f,'v)term × nat"
{
fix f ss σ
have "?ml f (map (?σ σ) ss) = map (?σn σ) (?ml f ss)"
unfolding lterms_def term.simps map_map o_def length_map
unfolding map_eq_conv
by (clarify, rule conjI[OF _ refl], auto)
} note idsub = this
interpret list: SN_order_pair ?S' ?NS'
by (rule extension[OF label_s_ns_order_pair])
show ?thesis
proof
show "ctxt.closed NS" by (rule wm_NS)
next
show "subst.closed NS" by (rule subst_NS)
next
show "refl NS" by (rule refl_NS)
next
show "trans NS" by (rule trans_NS)
next
show "SN S_label_mul" unfolding S
by (rule SN_subset[OF SN_inv_image[OF list.SN]], auto)
next
show "trans S_label_mul" unfolding S using list.trans_S unfolding trans_def
by blast
next
show "trans NST_label_mul" unfolding NST using list.trans_NS unfolding trans_def by blast
next
show "?NST O ?S ⊆ ?S" unfolding S NST using list.compat_NS_S by blast
next
fix s t f bef aft u
assume st: "(s,t) ∈ NS"
let ?ts = "bef @ t # aft"
let ?t = "Fun f ?ts"
let ?ss = "bef @ s # aft"
let ?s = "Fun f ?ss"
obtain n where n: "n = Suc (length bef + length aft)" by auto
let ?pt = "proja (Fun f (bef @ t # aft))"
let ?ps = "proja (Fun f (bef @ s # aft))"
let ?ts' = "map (λ (i,y). (?pt i, y)) (π (f,n))"
let ?ss' = "map (λ (i,y). (?ps i, y)) (π (f,n))"
have "(?ss', ?ts') ∈ ?NS'"
proof (rule all_ns_imp_ns, simp)
fix i
assume i': "i < length ?ts'"
hence i: "i < length (π (f,n))" by auto
then obtain j m where pi: "π (f,n) ! i = (j,m)" by force
show "(?ss' ! i, ?ts' ! i) ∈ label_ns" unfolding nth_map[OF i] pi prod.simps
proof (cases "j = length bef")
case True
thus "((?ps j, m), (?pt j, m)) ∈ label_ns" using st unfolding label_ns_def by auto
next
case False
hence id: "?ss ! j = ?ts ! j" unfolding nth_append by auto
show "((?ps j, m), (?pt j, m)) ∈ label_ns"
proof (cases "j < Suc (length bef + length aft)")
case True
thus ?thesis using id refl_NS unfolding label_ns_def refl_on_def by auto
next
case False
thus ?thesis
using ctxt_closed_one[OF wm_NS st, of f bef aft]
unfolding label_ns_def by auto
qed
qed
qed
hence S': "(?ml f ?ss, ?ml f ?ts) ∈ ?NS'" unfolding n lterms_def term.simps by auto
thus "(Fun f ?ss, Fun f ?ts) ∈ ?NST" unfolding NST by auto
next
show "subst.closed ?S" unfolding subst.closed_def
proof
fix ss ts
assume "(ss,ts) ∈ subst.closure ?S"
thus "(ss,ts) ∈ ?S"
proof (induct)
fix s t and σ :: "('f,'v)subst"
assume mem: "(s,t) ∈ ?S"
from mem obtain f ss where s: "s = Fun f ss" unfolding S by auto
from mem obtain g ts where t: "t = Fun g ts" unfolding S by auto
from mem[unfolded s t S] have S': "(?ml f ss,?ml g ts) ∈ ?S'" by simp
show "(s ⋅ σ, t ⋅ σ) ∈ ?S" unfolding s t S
by (rule, intro exI conjI, unfold subst_apply_term.simps, rule refl,
unfold idsub, rule s_map[OF _ _ S'],
unfold label_s_def label_ns_def, insert subS subNS, auto)
qed
qed
next
show "subst.closed ?NST" unfolding subst.closed_def
proof
fix ss ts
assume "(ss,ts) ∈ subst.closure ?NST"
thus "(ss,ts) ∈ ?NST"
proof (induct)
fix s t and σ :: "('f,'v)subst"
assume mem: "(s,t) ∈ ?NST"
from mem obtain f ss where s: "s = Fun f ss" unfolding NST by auto
from mem obtain g ts where t: "t = Fun g ts" unfolding NST by auto
from mem[unfolded s t NST] have S': "(?ml f ss,?ml g ts) ∈ ?NS'" by simp
show "(s ⋅ σ, t ⋅ σ) ∈ ?NST" unfolding s t NST
by (rule, intro exI conjI, unfold subst_apply_term.simps, rule refl,
unfold idsub, rule ns_map[OF _ _ S'],
unfold label_s_def label_ns_def, insert subS subNS, auto)
qed
qed
qed
qed
end
definition scnp_af_to_af :: "(('f × nat) ⇒ (nat × nat)list) ⇒ 'f af ⇒ 'f af" where
"scnp_af_to_af π π' ≡ λ(f, n).
let is = map fst (π (f, n)) in
if (∃i∈set is. i ≥ n)
then π' (f, n) ∪ set is
else set is"
locale ce_af_scnp = scnp S NS NST s_ext ns_ext π + ce_af_redtriple S NS NST π'
for S NS NST :: "('f, 'v) trs" and π and s_ext ns_ext and π'
begin
lemma ce_af_scnp_mul: "ce_af_root_redtriple_order S_label_mul NS NST_label_mul π' (scnp_af_to_af π π')"
(is "ce_af_root_redtriple_order ?S _ ?NST _ ?pi")
proof -
from scnp_mul interpret root_redtriple_order S_label_mul NS NST_label_mul .
show ?thesis
proof (unfold_locales, rule NS_ce_compat, rule af_compat)
show "af_compatible ?pi ?NST"
unfolding af_compatible_def
proof (intro allI)
fix f bef s t aft
show "length bef ∈ ?pi (f, Suc (length bef + length aft)) ∨
(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ?NST" (is "?i ∈ (scnp_af_to_af π π') (f, ?n) ∨ (?s,?t) ∈ ?NST")
proof -
{
assume not: "?i ∉ ?pi (f, ?n)"
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
note not = not[unfolded scnp_af_to_af_def Let_def, unfolded Product_Type.split]
have "(?s,?t) ∈ ?NST" unfolding NST_label_mul_def
proof (rule, intro exI conjI, rule refl, rule all_ns_imp_ns)
show "length (lterms π ?s) = length (lterms π ?t)" unfolding lterms_def by auto
next
fix i
assume i: "i < length (lterms π ?t)"
hence i: "i < length (π (f,?n))" unfolding lterms_def by auto
obtain a b where pi: "π (f, ?n) ! i = (a,b)" by force
have id: "(lterms π ?s ! i, lterms π ?t ! i) = ((proja ?s a,b), (proja ?t a, b))" (is "_ = ((?ps,b),(?pt,b))")
unfolding lterms_def term.simps using i pi by auto
from pi i have mem: "(a,b) ∈ set (π (f,?n))" unfolding set_conv_nth by force
hence mem': "a ∈ set (map fst (π (f,?n)))" by force
let ?cond = "Bex (set (map fst (π (f, ?n)))) (op ≤ ?n)"
have "(?ps, ?pt) ∈ NS"
proof (cases "a < ?n")
case True
have "a ≠ ?i"
proof (cases ?cond)
case True
hence c: "?cond = True" by simp
from not[unfolded c] mem' show ?thesis by force
next
case False
hence c: "?cond = False" by simp
from not[unfolded c] mem' show ?thesis by force
qed
with True have "?ps = ?pt" by (simp add: nth_append)
thus ?thesis using refl_NS unfolding refl_on_def by auto
next
case False
hence a: "a ≥ ?n" by simp
with mem' have c: "?cond = True" by auto
from a have id: "?ps = ?s" "?pt = ?t" by auto
from not[unfolded c] have not: "?i ∉ π' (f, ?n)" by auto
show ?thesis unfolding id
proof (rule af_steps_imp_orient[where p = "λ i. i ∈ π' (f, ?n)", OF trans_NS refl_NS wm_NS, rule_format])
fix i
assume "i < length ?ss" and "i ∈ π' (f, ?n)"
with not have "i ≠ ?i" by auto
hence "?ss ! i = ?ts ! i" unfolding nth_append by auto
thus "(?ss ! i, ?ts ! i) ∈ NS" using refl_NS[unfolded refl_on_def] by auto
qed (insert af_compat[unfolded af_compatible_def], auto)
qed
thus "(lterms π ?s ! i, lterms π ?t ! i) ∈ label_ns" unfolding id label_ns_def by auto
qed
}
thus ?thesis by blast
qed
qed
qed
qed
end
end