theory Generic_Reduction_Pair_Processor
imports
Generic_Usable_Rules
QTRS.QDP_Framework
begin
lemma generic_redtriple_proc:
assumes checker: "usable_rules_checker checker"
and U: "set U ⊆ NS"
and oP: "P ⊆ NST ∪ S"
and redtriple: "ce_af_redtriple S NS NST π"
and check: "checker nfs m (wwf_qtrs Q (set R)) π Q R U_opt P = Some U"
shows "¬ min_ichain (nfs,m,S ∩ P, P - S, Q, {}, set R) s t σ"
proof
assume chain: "min_ichain (nfs,m,S ∩ P, P - S, Q, {}, set R) s t σ"
let ?Q = "NF_terms Q"
let ?R = "qrstep nfs Q (set R)"
interpret ce_af_redtriple S NS NST π by fact
have redpair: "ce_af_redpair S NS π" ..
note checker = checker[unfolded usable_rules_checker_def, rule_format, OF check redpair U]
from checker obtain f where f: "⋀ s t u σ τ. (s,t) ∈ P ⟹ s ⋅ σ ∈ ?Q ⟹ NF_subst nfs (s,t) σ Q ⟹ (t ⋅ σ, u ⋅ τ) ∈ ?R^* ⟹ (m ⟹ SN_on ?R {t ⋅ σ}) ⟹ (t ⋅ f σ, u ⋅ f τ) ∈ NS^*" by blast
note chain = chain[unfolded min_ichain.simps ichain.simps minimal_cond_def]
from chain have P: "⋀ i. (s i, t i) ∈ P" by auto
from chain have Q: "⋀ i. s i ⋅ σ i ∈ ?Q" by auto
from chain have nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q" by auto
from chain have steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?R^*" by auto
from chain have SNt: "⋀ i. m ⟹ SN_on ?R {t i ⋅ σ i}" by auto
let ?s = "λ i. s i ⋅ f (σ i)"
let ?t = "λ i. t i ⋅ f (σ i)"
let ?next = "λ i. (s (Suc i), t (Suc i))"
from f[OF P Q nfs steps SNt] have stepsNS: "⋀ i. (?t i, ?s (Suc i)) ∈ NS^*" by simp
from oP P have allP: "⋀ i. (s i, t i) ∈ NST ∪ S" by (auto simp: ichain.simps)
from chain have inf: "INFM i. (s i, t i) ∈ S ∩ P" by simp
have piece1: "∀ i. (?t i, ?t (Suc i)) ∈ S ∨ (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* ∧ (?next i) ∉ S"
proof
fix i
show "(?t i, ?t (Suc i)) ∈ S ∨ (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* ∧ (?next i) ∉ S"
proof (cases "?next i ∈ S")
case True
hence "(?s (Suc i), ?t (Suc i)) ∈ S" using subst_S by (auto simp: subst.closed_def)
with stepsNS NS.trCompat show ?thesis by auto
next
case False
with stepsNS allP[of "Suc i"]
have one: "?next i ∈ NST" and two: "?next i ∉ S" by auto
from one have "(?s (Suc i), ?t (Suc i)) ∈ NST" using subst_NST by (auto simp: subst.closed_def)
with stepsNS[of i] have steps: "(?t i, ?t (Suc i)) ∈ NS^* O NST" by auto
have "(?t i, ?t (Suc i)) ∈ (NS ∪ NST)^*"
by (rule set_mp[OF _ steps], regexp)
with two show ?thesis by simp
qed
qed
hence infSeq: "∀ i. (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* ∪ S" by auto
from SN have "SN_on S {?t 0}" by best
from infSeq both.trCompat this have "∃ j. ∀ i ≥ j. (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* - S" by (rule non_strict_ending)
from this obtain j where one: "∀ i ≥ j. (?t i, ?t (Suc i)) ∈ (NS ∪ NST)^* - S" ..
with piece1 have ns: "∀ i ≥ j. ?next i ∉ S" by blast
from inf[unfolded INFM_nat] obtain n where n: "n > j" and s: "(s n, t n) ∈ S" by auto
from n obtain m where n: "n = Suc m" and m: "m ≥ j" by (cases n, auto)
from ns[THEN spec[of _ m]] s show False unfolding n using m by auto
qed
lemma generic_root_redtriple_proc:
assumes checker: "usable_rules_checker (checker :: ('f,'v)usable_rules_checker)"
and U: "set U ⊆ NS"
and oP: "P ⊆ NST ∪ S"
and Pcond: "⋀ s t. (s,t) ∈ P ⟹ is_Fun s ∧ is_Fun t"
and redtriple: "ce_af_root_redtriple S NS NST π π'"
and check: "checker nfs m (wwf_qtrs Q (set R)) π Q R U_opt
{(s,ts ! i) | s f ts i. (s,Fun f ts) ∈ P ∧ i < length ts ∧ i ∈ π' (f,length ts)} = Some U"
(is "checker nfs m _ π Q R U_opt ?P = Some U")
shows "¬ nr_min_ichain (nfs,m,S ∩ P, P - S, Q, set R) s t σ"
proof
assume chain: "nr_min_ichain (nfs,m,S ∩ P, P - S, Q, set R) s t σ"
let ?Q = "NF_terms Q"
let ?R = "qrstep nfs Q (set R)"
let ?N = "nrqrstep nfs Q (set R)"
interpret ce_af_root_redtriple S NS NST π π' by fact
have redpair: "ce_af_redpair S NS π" ..
note checker = checker[unfolded usable_rules_checker_def, rule_format, OF check redpair U]
from checker obtain f where f: "⋀ s t u σ τ. (s,t) ∈ ?P ⟹ s ⋅ σ ∈ ?Q ⟹ NF_subst nfs (s,t) σ Q ⟹ (t ⋅ σ, u ⋅ τ) ∈ ?R^* ⟹ (m ⟹ SN_on ?R {t ⋅ σ}) ⟹ (t ⋅ f σ, u ⋅ f τ) ∈ NS^*" by blast
note chain = chain[unfolded nr_min_ichain.simps nr_ichain.simps minimal_cond_def]
from chain have P: "⋀ i. (s i, t i) ∈ P" by auto
from chain have Q: "⋀ i. s i ⋅ σ i ∈ ?Q" by auto
from chain have nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q" by auto
from chain have steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ ?N^*" by auto
from chain have SNt: "⋀ i. m ⟹ SN_on ?R {t i ⋅ σ i}" by auto
let ?s = "λ i. s i ⋅ f (σ i)"
let ?t = "λ i. t i ⋅ f (σ i)"
let ?next = "λ i. (s (Suc i), t (Suc i))"
{
fix i
note P = P[of i] P[of "Suc i"]
from Pcond[OF P(1)] obtain g ts where ti: "t i = Fun g ts" by force
from Pcond[OF P(2)] obtain h ss where si: "s (Suc i) = Fun h ss" by force
let ?ts = "map (λ t. t ⋅ σ i) ts"
let ?ss = "map (λ t. t ⋅ σ (Suc i)) ss"
let ?fts = "map (λ t. t ⋅ f (σ i)) ts"
let ?fss = "map (λ t. t ⋅ f (σ (Suc i))) ss"
have id: "t i ⋅ σ i = Fun g ?ts" "s (Suc i) ⋅ σ (Suc i) = Fun h ?ss" unfolding si ti by auto
from nrqrsteps_preserve_root[OF steps[of i], unfolded id] have hg: "h = g" "length ts = length ss" by auto
note arg_steps = nrqrsteps_imp_arg_qrsteps[OF steps[of i], unfolded id term.sel]
{
fix j
assume j: "j < length ts" and "j ∈ π' (g,length ts)"
with P have s: "(s i, ts ! j) ∈ ?P" unfolding ti by auto
note f = f[OF this Q[of i]]
from ti j have "ts ! j ∈ set (args (t i))" by auto
hence "vars_term (ts ! j) ⊆ vars_term (t i)" unfolding ti by auto
with nfs[of i] have "NF_subst nfs (s i, ts ! j) (σ i) Q" unfolding NF_subst_def vars_rule_def by auto
note f = f[OF this]
from arg_steps[of j] j hg have "(ts ! j ⋅ σ i, ss ! j ⋅ σ (Suc i)) ∈ ?R^*" by auto
note f = f[OF this]
{
assume m
have "SN_on ?R {ts ! j ⋅ σ i}"
by (rule SN_imp_SN_arg_gen[OF ctxt_closed_qrstep SNt[of i, unfolded id, OF ‹m›]], insert j, auto)
}
note f = f[OF this]
from f have "(?fts ! j, ?fss ! j) ∈ NS^*" using j hg by auto
} note NS = this
let ?rel = "λ i. if i ∈ π' (g,length ts) then NS^* else UNIV"
note cong = args_steps_imp_steps_gen[of ?rel]
note af = af_compat'[unfolded af_compatible_def, rule_format, of _ g]
have "(t i ⋅ f (σ i), s (Suc i) ⋅ f (σ (Suc i))) ∈ NST^*" unfolding ti si hg subst_apply_term.simps
proof (rule cong, unfold length_map hg(2)[symmetric])
fix s t and bef aft :: "('f,'v)term list"
assume st: "(s,t) ∈ ?rel (length bef)" and len: "length ts = Suc (length bef + length aft)"
show "(Fun g (bef @ s # aft), Fun g (bef @ t # aft)) ∈ NST^*"
proof (cases "length bef ∈ π' (g,length ts)")
case False
with af[of bef aft s t, unfolded len[symmetric]] show ?thesis by auto
next
case True
with st have st: "(s,t) ∈ NS^*" by simp
show ?thesis
by (rule compat_NSs_root[OF st])
qed
qed (insert NS, auto)
}
hence stepsNS: "⋀ i. (?t i, ?s (Suc i)) ∈ NST^*" .
from oP P have allP: "⋀ i. (s i, t i) ∈ NST ∪ S" by (auto simp: ichain.simps)
from chain have inf: "INFM i. (s i, t i) ∈ S ∩ P" by simp
have piece1: "∀ i. (?t i, ?t (Suc i)) ∈ S ∨ (?t i, ?t (Suc i)) ∈ NST^* ∧ (?next i) ∉ S"
proof
fix i
show "(?t i, ?t (Suc i)) ∈ S ∨ (?t i, ?t (Suc i)) ∈ NST^* ∧ (?next i) ∉ S"
proof (cases "?next i ∈ S")
case True
hence "(?s (Suc i), ?t (Suc i)) ∈ S" using subst_S by (auto simp: subst.closed_def)
with stepsNS compat_NSTs show ?thesis by auto
next
case False
with stepsNS allP[of "Suc i"]
have one: "?next i ∈ NST" and two: "?next i ∉ S" by auto
from one have "(?s (Suc i), ?t (Suc i)) ∈ NST" using subst_NST by (auto simp: subst.closed_def)
with stepsNS[of i] have steps: "(?t i, ?t (Suc i)) ∈ NST^*" by auto
with two show ?thesis by simp
qed
qed
hence infSeq: "∀ i. (?t i, ?t (Suc i)) ∈ NST^* ∪ S" by auto
from compat_NSTs have compat: "NST^* O S ⊆ S" by auto
from SN have "SN_on S {?t 0}" by best
from non_strict_ending[OF infSeq compat, OF this]
obtain j where one: "∀ i ≥ j. (?t i, ?t (Suc i)) ∈ NST^* - S" ..
with piece1 have ns: "∀ i ≥ j. ?next i ∉ S" by blast
from inf[unfolded INFM_nat] obtain n where n: "n > j" and s: "(s n, t n) ∈ S" by auto
from n obtain m where n: "n = Suc m" and m: "m ≥ j" by (cases n, auto)
from ns[THEN spec[of _ m]] s show False unfolding n using m by auto
qed
lemma root_redtriple_sound:
assumes checker: "usable_rules_checker checker"
and check: "checker nfs m (wwf_qtrs Q (set R)) π Q R U_opt
{(s,ts ! i) | s f ts i. (s,Fun f ts) ∈ P ∧ i < length ts ∧ i ∈ π' (f,length ts)} = Some U"
and U: "set U ⊆ NS"
and oP: "P ⊆ NST ∪ S"
and Pcond: "⋀ s t. (s,t) ∈ P ⟹ is_Fun s ∧ is_Fun t"
and Rcond: "⋀ l r. (l,r) ∈ set R ⟹ is_Fun l"
and ndef: "∀ (s,t) ∈ P. ¬ defined (set R) (the (root t))"
and redtriple: "ce_af_root_redtriple S NS NST π π'"
shows "¬ min_ichain (nfs,m,S ∩ P, P - S, Q, {}, (set R)) s t σ"
proof
assume ichain: "min_ichain (nfs,m,S ∩ P, P - S, Q, {}, (set R)) s t σ"
have "nr_min_ichain (nfs,m,S ∩ P, P - S, Q, (set R)) s t σ"
by (rule min_ichain_imp_nr_min_ichain[OF ichain], insert ndef Pcond Rcond, auto)
with generic_root_redtriple_proc[OF checker U oP Pcond redtriple, OF _ check]
show False ..
qed
end