theory Term_Order_Extension
imports
QTRS.Term_Order
TA.Signature_Extension
Argument_Filter
RPO
"Check-NT.Reduction_Pair"
begin
lift_definition only_unary_afs :: "('f × nat) set ⇒ 'f afs" is
"λ F. ((λ (f :: 'f, n). if n = 0 then AFList [] else
if (f,n) ∈ F then Collapse 0 else AFList [0 ..< n]), UNIV)"
by auto
lemma only_unary_afs: "afs (only_unary_afs F) =
(λ (f :: 'f, n). if n = 0 then AFList [] else
if (f,n) ∈ F then Collapse 0 else AFList [0 ..< n])"
by (transfer, auto)
context redtriple_order
begin
lemma sig_mono_imp_SN_rel:
fixes R Rw :: "('f, 'v) trs"
assumes sig_mono:
"⋀ s t f bef aft. ⟦(s, t) ∈ S; (f, Suc (length bef + length aft)) ∈ F⟧ ⟹
(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ S"
and orient: "R ⊆ S" "Rw ⊆ NS"
and var_cond: "⋀ l r. (l, r) ∈ NS ∩ Rw ⟹ vars_term r ⊆ vars_term l"
and F: "funas_trs R ⊆ F" "funas_trs Rw ⊆ F"
shows "SN_rel (rstep R) (rstep Rw)"
proof -
let ?R = "rstep R"
let ?FR = "sig_step F ?R"
let ?S = "rstep Rw"
let ?FS = "sig_step F ?S"
have S: "?FR ⊆ S"
proof
fix s t
assume st: "(s, t) ∈ ?FR"
hence st: "(s, t) ∈ ?R" and sF: "funas_term s ⊆ F" and tF: "funas_term t ⊆ F" using sig_stepE[OF st] by auto
from st obtain C l r σ where lr: "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by auto
from orient lr have lr: "(l, r) ∈ S" by auto
from subst.closedD[OF subst_S lr] have gt: "(l ⋅ σ, r ⋅ σ) ∈ S" .
from sF[unfolded s] have "funas_ctxt C ⊆ F" by auto
hence "(C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∈ S"
proof (induction C)
case Hole
show ?case using gt by simp
next
case (More f bef C aft)
from More.prems have C: "funas_ctxt C ⊆ F" and f: "(f, Suc (length bef + length aft)) ∈ F" by auto
from sig_mono[OF More.IH[OF C] f] show ?case by simp
qed
thus st: "(s, t) ∈ S" unfolding s t .
qed
from rstep_subset[OF wm_NS subst_NS orient(2)]
have NS: "?S ⊆ NS" .
hence NS_sig: "?FS ⊆ NS" by auto
from relto_mono[OF S NS_sig]
have subset: "relto (?FR) (?FS) ⊆ S" by (simp add: order_simps)
have "SN (relto (?FR) (?FS))"
by (rule SN_subset[OF SN subset])
hence relSN: "SN_rel (?FR) (?FS)" unfolding SN_rel_defs .
{
fix l r
assume lr: "(l, r) ∈ Rw"
with orient have "(l, r) ∈ NS ∩ Rw" by auto
from var_cond[OF this]
have "vars_term r ⊆ vars_term l" .
} note var_cond = this
show ?thesis
by (rule sig_ext_relative_rewriting_var_cond[OF var_cond F relSN])
qed
lemma manna_ness_relative:
assumes orient: "R ⊆ S" "Rw ⊆ NS"
and mono: "ctxt.closed S"
shows "SN_rel (rstep R) (rstep Rw)"
proof -
from rstep_subset[OF wm_NS subst_NS orient(2)] have NS: "rstep Rw ⊆ NS" .
from rstep_subset[OF mono subst_S orient(1)] have S: "rstep R ⊆ S" .
from SN_subset[OF SN relto_mono[OF S NS, unfolded order_simps]]
show ?thesis unfolding SN_rel_defs .
qed
lemma sig_mono_imp_SN_rel_subterm:
assumes sig_mono:
"⋀ s t f bef aft. ⟦(s, t) ∈ S; (f, Suc (length bef + length aft)) ∈ F⟧ ⟹
(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ S"
and F_unary: "⋀ fn. fn ∈ F ⟹ snd fn ≤ Suc 0"
and orient: "R ⊆ S" "Rw ⊆ NS"
and var_cond: "⋀ l r. (l, r) ∈ NS ∩ Rw ⟹ vars_term r ⊆ vars_term l"
and F: "funas_trs R ⊆ F" "funas_trs Rw ⊆ F"
and ST: "ST ⊆ {(Fun f ts, t) | f ts t. t ∈ set ts ∧ (f,length ts) ∉ F}"
shows "SN_rel (rstep (R ∪ ST)) (rstep (Rw ∪ ST))"
proof -
let ?c = ST
from sig_mono_imp_SN_rel[OF sig_mono orient var_cond F]
have SN_rel_R_Rw: "SN_rel (rstep R) (rstep Rw)" .
hence SN: "SN_qrel (False, {}, R, Rw)" unfolding SN_qrel_def by simp
have "SN_qrel (False, {}, R ∪ ?c, Rw ∪ ?c)"
proof (rule SN_qrel_split[where D = ?c])
show "SN_qrel (False, {}, R ∪ ?c - ?c, Rw ∪ ?c - ?c)"
by (rule SN_qrel_mono[OF _ _ _ SN], auto)
next
show "SN_qrel (False, {}, ?c ∩ (R ∪ ?c ∪ (Rw ∪ ?c)), R ∪ ?c ∪ (Rw ∪ ?c) - ?c)"
proof (rule SN_qrel_mono[where Q = "{}" and Q' = "{}"], unfold SN_qrel_def split qrstep_rstep_conv)
obtain prc :: "'f filtered × nat ⇒ nat" where prc: "prc = (λ _ . 0)" by auto
obtain c :: "'f filtered × nat ⇒ order_tag" where c: "c = (λ _ . Lex)" by auto
obtain n :: nat where True by auto
interpret rpo_pr "prc_nat prc" "prl_nat prc" c ..
let ?af = "only_unary_afs F"
let ?S = "RPO_S prc c n"
let ?NS = "RPO_NS prc c n"
interpret mono_ce_af_redtriple ?S ?NS ?NS full_af ..
interpret afs_redtriple ?af ?S ?NS ?NS ..
let ?pi = "afs_rel ?af"
show "SN_rel (rstep ?c) (rstep (R ∪ Rw))"
proof (rule manna_ness_relative[OF _ _ ctxt_closed[OF _ rpo_pr_prc.RPO_S_pr_ctxt_closed]])
show "mono_afs ?af" unfolding mono_afs_def using F_unary
by (auto simp: only_unary_afs)
show "?c ⊆ ?pi ?S"
proof
fix s t
assume st: "(s, t) ∈ ?c"
with ST obtain f ts where s: "s = Fun f ts" and t: "t ∈ set ts" and f: "(f,length ts) ∉ F" by auto
show "(s, t) ∈ ?pi ?S" unfolding afs_rel_def
proof(rule, rule exI, rule conjI[OF refl])
let ?s = "afs_term ?af s"
let ?t = "afs_term ?af t"
have pi: "afs ?af (f, length ts) = AFList [0 ..< length ts]"
using f by (auto simp: only_unary_afs)
have "?t ∈ set (args ?s)" unfolding s using t[unfolded set_conv_nth]
by (force simp: Let_def pi)
hence "?s ⊳ ?t" by (cases ?s, auto)
from rpo_pr_prc.supt_imp_rpo_stri[OF this, of prc c n]
have "(?s, ?t) ∈ ?S" unfolding rpo_pr_prc.RPO_S_pr_def by auto
thus "afs_rule ?af (s, t) ∈ ?S"
unfolding afs_rule_def fst_conv snd_conv .
qed
qed
show "R ∪ Rw ⊆ ?pi ?NS"
proof
fix l r
assume lr: "(l, r) ∈ R ∪ Rw"
with F have F: "funas_term l ⊆ F" "funas_term r ⊆ F"
unfolding funas_trs_def funas_rule_def [abs_def] by force+
from SN_rel_imp_wf_reltrs[OF SN_rel_R_Rw]
have "wf_reltrs (R) (Rw)" .
with var_cond[of l r] lr orient(2) have vars: "vars_term r ⊆ vars_term l"
unfolding wf_reltrs.simps wf_trs_def by auto
let ?pi = "afs_term ?af"
{ fix t :: "('f, 'v) term" and x
assume "funas_term t ⊆ F" and "x ∈ vars_term t"
hence "?pi t = Var x"
proof (induction t)
case (Var y)
thus ?case by simp
next
case (Fun f ts)
from Fun.prems(1) have f: "(f, length ts) ∈ F" by auto
from F_unary[OF this] obtain t where ts: "ts = [t]"
using Fun.prems(2) by (cases ts, auto)
from Fun.prems[unfolded ts] have F: "funas_term t ⊆ F"
and x: "x ∈ vars_term t" by auto
from Fun.IH[OF _ F x] f show ?case unfolding ts
by (auto simp: only_unary_afs)
qed }
note var = this
have "(?pi l, ?pi r) ∈ ?NS"
proof (cases "vars_term r = {}")
case False
then obtain x where xr: "x ∈ vars_term r" by auto
with vars have xl: "x ∈ vars_term l" by auto
show ?thesis
unfolding var[OF F(1) xl] var[OF F(2) xr]
by (rule rpo_pr_prc.RPO_refl)
next
case True
with F(2) have "∃ c. ?pi r = Fun c []"
proof (induction r)
case (Fun f ts)
from Fun.prems(1) have f: "(f, length ts) ∈ F" by auto
from F_unary[OF this] obtain t where ts: "ts = [t] ∨ ts = []"
using Fun.prems(2) by (cases ts, auto)
thus ?case
proof
assume ts: "ts = [t]"
from Fun.prems[unfolded ts] have F: "funas_term t ⊆ F"
and vars: "vars_term t = {}" by auto
from Fun.IH[OF _ F vars] f show ?case unfolding ts
by (simp add: only_unary_afs)
next
assume ts: "ts = []"
show ?case unfolding ts
by (simp add: only_unary_afs)
qed
qed auto
then obtain f where pir: "?pi r = Fun f []" by auto
have f: "prl_nat prc (f,0)" unfolding prc prl_nat_def by simp
show ?thesis unfolding pir
using rpo_pr_prc.RPO_least_Var[OF f]
using rpo_pr_prc.RPO_least_Fun[OF f]
by (cases "?pi l", auto)
qed
thus "(l, r) ∈ afs_rel ?af ?NS"
unfolding afs_rel_def afs_rule_def by auto
qed
qed
qed auto
qed
thus ?thesis unfolding SN_qrel_def by simp
qed
end
lemma ce_SN_rel_imp_redtriple:
fixes R Rw :: "('f, 'v) trs"
assumes SN_rel: "SN_rel (rstep R) (rstep Rw)"
and ce: "⋃(ce_trs ` UNIV) ⊆ R ∩ Rw"
and pi: "⋀ f n. pi (f, n) = {0 ..< n}"
shows "mono_ce_af_redtriple_order ((relto (rstep R) (rstep Rw))⇧+) ((rstep R ∪ rstep Rw)⇧*) ((rstep R ∪ rstep Rw)⇧*) pi"
proof -
let ?R = "relto (rstep R) (rstep Rw)"
let ?Rw = "rstep R ∪ rstep Rw"
from SN_rel have SN: "SN (?R^+)" unfolding SN_rel_defs
by (rule SN_imp_SN_trancl)
note conv = relto_trancl_conv
note subst = subst.closed_rtrancl subst.closed_Un subst.closed_comp subst_closed_rstep
let ?ce = "⋃(range ce_trs) :: ('f, 'v)trs"
from ce have "?ce ⊆ rstep R ∩ rstep Rw" by auto
also have "... ⊆ ?R^+ ∩ ?Rw^*" unfolding conv by auto
finally have ce: "?ce ⊆ ?R^+ ∩ ?Rw^*" .
{
fix c d m
have "ce_trs (c, m) ⊆ ?ce" by auto
also have "... ⊆ ?R^+ ∩ ?Rw^*" by (rule ce)
finally have "ce_trs (c, m) ⊆ ?R^+ ∩ ?Rw^*" .
} note ce = this
show ?thesis
proof(unfold_locales, rule SN)
show "ctxt.closed (?Rw^*)" by blast
show "subst.closed (?R^+)" unfolding conv by (blast)
show "subst.closed (?Rw^*)" by (blast)
show "refl (?Rw^*)" by (auto intro: refl_rtrancl)
show "trans (?Rw^*)" by (auto intro: trans_rtrancl)
show "?Rw^* O ?R^+ ⊆ ?R^+" unfolding conv by regexp
show "?R^+ O ?Rw^* ⊆ ?R^+" unfolding conv by regexp
show "af_compatible pi (?Rw^*)" unfolding af_compatible_def using pi by auto
have "?R^+ O ?R^+ ⊆ ?R^+" unfolding conv by regexp
thus "trans (?R^+)" by auto
show "?R^+ ⊆ ?Rw^*" by regexp
qed (insert ce, blast+)
qed
end