theory Check_Termination
imports Check_Common
begin
fun collect_assms :: "('tp ⇒ ('f, 'l, 'v) assm list)
⇒ ('dpp ⇒ ('f, 'l, 'v) assm list)
⇒ ('fptp ⇒ ('f, 'l, 'v) assm list)
⇒ ('unk ⇒ ('f, 'l, 'v) assm list)
⇒ ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof ⇒ ('f, 'l, 'v) assm list"
where
"collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf"
| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf"
| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf"
| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf"
| "collect_assms _ _ _ _ _ = []"
lemma collect_assms_cong [fundef_cong]:
assumes "⋀ t p. i = SN_assm_proof t p ⟹ tp p = tp' p"
and "⋀ t p. i = Finite_assm_proof t p ⟹ dpp p = dpp' p"
and "⋀ t p. i = SN_FP_assm_proof t p ⟹ fptp p = fptp' p"
and "⋀ t p. i = Unknown_assm_proof t p ⟹ unk p = unk' p"
shows "collect_assms tp dpp fptp unk i = collect_assms tp' dpp' fptp' unk' i"
using assms by (cases i) (auto)
subsection ‹Proving finiteness in the QDP Framework›
fun
check_dpp_subsumes ::
"('d, ('f::{key,show}, 'l::{key,show}) lab, 'v::show) dpp_ops
⇒ ('f, 'l, 'v) dppLL ⇒ 'd ⇒ shows check"
where
"check_dpp_subsumes I (nfs', m', p', pw', q', r', rw') d = (do {
let p = dpp_ops.P I d;
let pw = dpp_ops.Pw I d;
let q = dpp_ops.Q I d;
let r = dpp_ops.R I d;
let rw = dpp_ops.Rw I d;
let nfs = dpp_ops.nfs I d;
let m = dpp_ops.minimal I d;
let pb' = p' @ pw';
let rb = r @ rw;
let rb' = r' @ rw';
check (m = m') (shows ''incompatible minimality flags'');
check (nfs = nfs') (shows ''incompatible substitutions-in-normal-form flags'');
check_subseteq p p' <+? (λr. toomuch ''pair'' (shows_rule r));
check_subseteq pw pb' <+? (λr. toomuch ''weak pair'' (shows_rule r));
check_NF_terms_eq q q' <+? (λr. shows ''NF(Q) differs due to term '' ∘ shows_term r);
check_subseteq r r' <+? (λr. toomuch ''strict rule'' (shows_rule r));
check_subseteq rb rb' <+? (λr. toomuch ''strict/weak rule'' (shows_rule r));
check_subseteq rb' rb <+? (λr. missing ''strict/weak rule'' (shows_rule r));
succeed
}) <+? (λs. shows ''finiteness of the problem'' ∘ shows_nl ∘ shows_dpp I d ∘ shows_nl
∘ shows ''may not be concluded from assuming finiteness of the problem'' ∘ shows_nl
∘ shows_dpp I (dpp_ops.mk I nfs' m' p' pw' q' r' rw') ∘ shows_nl
∘ s ∘ shows_nl)"
lemma check_dpp_subsumesD [dest]:
assumes 1: "dpp_spec I"
and 2: "isOK (check_dpp_subsumes I (nfs, m, p, pw, q, r, rw) d)"
shows
"dpp_ops.minimal I d = m"
"dpp_ops.nfs I d = nfs"
"set (dpp_ops.P I d) ⊆ set p"
"set (dpp_ops.Pw I d) ⊆ set p ∪ set pw"
"NF_terms (set (dpp_ops.Q I d)) = NF_terms (set q)"
"set (dpp_ops.R I d) ⊆ set r"
"set (dpp_ops.R I d) ∪ set (dpp_ops.Rw I d) = set r ∪ set rw"
by (insert 1 2, auto simp: Let_def)
lemma check_dpp_subsumes_sound:
assumes I: "dpp_spec I"
and ok: "isOK (check_dpp_subsumes I dpp' dpp)"
and fin: "finite_dpp (mk_dpp_set dpp')"
shows "finite_dpp (dpp_ops.dpp I dpp)"
proof -
obtain nfs m p pw q r rw where
dpp': "dpp' = (nfs, m, p, pw, q, r, rw)" by (cases dpp') force+
let ?m = "dpp_ops.minimal I dpp"
let ?nfs = "dpp_ops.nfs I dpp"
let ?P = "set (dpp_ops.P I dpp)"
let ?Pw = "set (dpp_ops.Pw I dpp)"
let ?Q = "set (dpp_ops.Q I dpp)"
let ?R = "set (dpp_ops.R I dpp)"
let ?Rw = "set (dpp_ops.Rw I dpp)"
let ?P' = "set p"
let ?Pw' = "set pw"
let ?Q' = "set q"
let ?R' = "set r"
let ?Rw' = "set rw"
from check_dpp_subsumesD [OF I ok [unfolded dpp']]
have flags: "?m = m" "?nfs = nfs"
and 1: "?P ⊆ ?P'"
"?P ∪ ?Pw ⊆ ?P' ∪ ?Pw'"
"NF_terms ?Q' = NF_terms ?Q"
"?R ⊆ ?R'"
"?R ∪ ?Rw = ?R' ∪ ?Rw'"
by auto
let ?dppg = "λ nfs m. (nfs, m, ?P', ?Pw', ?Q', ?R', ?Rw')"
show ?thesis
unfolding dpp_spec.dpp_sound [OF I]
proof (rule finite_dpp_mono [OF _ 1], rule ccontr)
assume "¬ finite_dpp (?dppg ?nfs ?m)"
then obtain s t σ where "min_ichain (?dppg ?nfs ?m) s t σ"
unfolding finite_dpp_def by auto
hence "min_ichain (?dppg ?nfs ?m) s t σ" by auto
hence "¬ finite_dpp (?dppg ?nfs ?m)"
unfolding finite_dpp_def by auto
with fin [unfolded dpp'] show False
unfolding flags by simp
qed
qed
definition check_compatible_nfs :: "bool ⇒ (('f :: show,'v :: show)term ⇒ bool) ⇒ ('f,'v)rules ⇒ bool ⇒ ('f,'v)term list ⇒ bool" where
"check_compatible_nfs nfs1 nf1 R1 nfs2 Q2 ≡ nfs1 = nfs2 ∨ Q2 = [] ∨
isOK(check_wwf_qtrs nf1 R1)"
lemma check_compatible_nfs: assumes compat: "check_compatible_nfs nfs1 (λ t. t ∈ NF_terms (set Q1)) R1 nfs2 Q2"
and R: "R ⊆ set R1"
shows "qrstep nfs1 (set Q1) R = qrstep nfs2 (set Q1) R ∨ qrstep nfs2 (set Q2) R2 = qrstep nfs1 (set Q2) R2"
proof (cases "nfs1 = nfs2 ∨ Q2 = []")
case False
from False compat[unfolded check_compatible_nfs_def] have "wwf_qtrs (set Q1) (set R1)" by auto
with R have "wwf_qtrs (set Q1) R" unfolding wwf_qtrs_def by auto
from wwf_qtrs_imp_nfs_switch[OF this, of nfs1 nfs2] show ?thesis by auto
qed auto
lemma check_compatible_nfs_SN_qrel: assumes compat: "check_compatible_nfs nfs1 (λ t. t ∈ NF_terms (set Q1)) (R @ Rw) nfs2 Q2"
shows "SN_qrel (nfs1, set Q1, set R, set Rw) = SN_qrel (nfs2, set Q1, set R, set Rw)
∨ SN_qrel (nfs2, set Q2, R', Rw') = SN_qrel (nfs1, set Q2, R', Rw')"
proof -
from check_compatible_nfs[OF compat]
have choice: "⋀ R1 R2. R1 ⊆ set (R @ Rw) ⟹
qrstep nfs1 (set Q1) R1 = qrstep nfs2 (set Q1) R1 ∨ qrstep nfs2 (set Q2) R2 = qrstep nfs1 (set Q2) R2" .
show ?thesis
proof (cases "qrstep nfs1 (set Q1) (set R) = qrstep nfs2 (set Q1) (set R) ∧
qrstep nfs1 (set Q1) (set Rw) = qrstep nfs2 (set Q1) (set Rw)")
case True
thus ?thesis unfolding SN_qrel_def split by auto
next
case False
{
fix R2
have "qrstep nfs2 (set Q2) R2 = qrstep nfs1 (set Q2) R2"
using choice[of "set R" R2] choice[of "set Rw" R2] using False by auto
}
thus ?thesis unfolding SN_qrel_def split by auto
qed
qed
fun
check_tp_subsumes ::
"('tp, ('f::show, 'l::show) lab, 'v::show) tp_ops ⇒ ('f, 'l, 'v) qreltrsLL ⇒
'tp ⇒ shows check"
where
"check_tp_subsumes I (nfs', q', r', rw') tp = (do {
let nfs = tp_ops.nfs I tp;
let q = tp_ops.is_QNF I tp;
let r = tp_ops.R I tp;
let rw = tp_ops.Rw I tp;
let rb' = r' @ rw';
let nf1 = tp_ops.is_QNF I tp;
check (check_compatible_nfs nfs nf1 (r @ rw) nfs' q') (shows ''incompatible substitutions-in-normal-form flags'');
check_NF_terms_subset q q' <+? (λr. shows ''problem with innermost strategy due to term '' ∘ shows_term r);
check_subseteq r r' <+? (λr. toomuch ''rule'' (shows_rule r));
check_subseteq rw rb' <+? (λr. toomuch ''relative rule'' (shows_rule r));
succeed
}) <+? (λs. shows ''termination of the problem'' ∘ shows_nl ∘ shows_tp I tp ∘ shows_nl
∘ shows ''may not be concluded from assuming termination of the problem'' ∘ shows_nl
∘ shows_tp I (tp_ops.mk I nfs' q' r' rw') ∘ shows_nl
∘ s ∘ shows_nl)"
lemma check_tp_subsumesE[elim]:
assumes 1: "tp_spec I"
and 2: "isOK (check_tp_subsumes I (nfs, q, r, rw) t)"
and 3: "check_compatible_nfs (tp_ops.nfs I t) (tp_ops.is_QNF I t) (tp_ops.R I t @ tp_ops.Rw I t) nfs q
⟹ NF_terms (set (tp_ops.Q I t)) ⊆ NF_terms (set q)
⟹ set (tp_ops.R I t) ⊆ set r
⟹ set (tp_ops.Rw I t) ⊆ set r ∪ set rw
⟹ P"
shows "P"
proof -
interpret tp_spec I by fact
show ?thesis
by (rule 3, insert 2) (auto simp: Let_def)
qed
lemma check_tp_subsumes_sound:
assumes I: "tp_spec I"
and ok: "isOK (check_tp_subsumes I tp' tp)"
and fin: "SN_qrel (mk_tp_set tp')"
shows "SN_qrel (tp_ops.qreltrs I tp)"
proof -
interpret tp_spec I by fact
obtain nfs q r rw where tp': "tp' = (nfs, q, r, rw)" by (cases tp') force+
let ?nfs = "tp_ops.nfs I tp"
let ?Q = "set (Q tp)"
let ?R = "set (R tp)"
let ?Rw = "set (Rw tp)"
let ?Q' = "set q"
let ?R' = "set r"
let ?Rw' = "set rw"
from I and ok
have compat: "check_compatible_nfs ?nfs (λ t. t ∈ NF_terms (set (Q tp))) (tp_ops.R I tp @ tp_ops.Rw I tp) nfs q"
and 1: "NF_terms ?Q ⊆ NF_terms ?Q'" "?R ⊆ ?R'" "?Rw ⊆ ?R' ∪ ?Rw'"
unfolding tp' by auto
note compat = check_compatible_nfs_SN_qrel[OF compat, of "set r" "set rw"]
thus ?thesis
proof
assume id: "SN_qrel (nfs, set q, set r, set rw) = SN_qrel (?nfs, set q, set r, set rw)"
show ?thesis unfolding tp_spec.qreltrs_sound[OF I]
by (rule SN_qrel_mono[OF 1], unfold id[symmetric], insert fin[unfolded tp'], auto)
next
assume id: "SN_qrel (?nfs, ?Q, ?R, ?Rw) = SN_qrel (nfs, ?Q, ?R, ?Rw)"
show ?thesis unfolding tp_spec.qreltrs_sound[OF I] id
by (rule SN_qrel_mono[OF 1], insert fin[unfolded tp'], auto)
qed
qed
fun mk_tp where
"mk_tp I (nfs, q, r, rw) = tp_ops.mk I nfs q r rw"
fun mk_dpp where
"mk_dpp I (nfs, m, p, pw, q, r, rw) = dpp_ops.mk I nfs m p pw q r rw"
lemma SN_rel_imp_finite_dpp: assumes SN: "SN_rel (qrstep nfs Q (P ∪ R)) (qrstep nfs Q (Pw ∪ Rw))"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof (rule SN_rel_ext_imp_finite_dpp[OF SN_rel_ext_mono[OF _ _ subset_refl subset_refl]])
show "rqrstep nfs Q P ∩ {(s, t). s ∈ NF_terms Q} ⊆ qrstep nfs Q P" by auto
show "rqrstep nfs Q Pw ∩ {(s, t). s ∈ NF_terms Q} ⊆ qrstep nfs Q Pw" by auto
show "SN_rel_ext (qrstep nfs Q P) (qrstep nfs Q Pw) (qrstep nfs Q R) (qrstep nfs Q Rw)
(λx. m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {x})"
unfolding SN_rel_ext_def
proof (clarify)
fix t k
assume strict: "∃⇩∞i. k (i :: nat) ∈ {top_s, normal_s}"
and steps: "∀ i. (t i, t (Suc i))
∈ SN_rel_ext_step (qrstep nfs Q P) (qrstep nfs Q Pw) (qrstep nfs Q R) (qrstep nfs Q Rw) (k i)"
{
fix i
have "(t i, t (Suc i)) ∈ qrstep nfs Q (P ∪ R) ∪ qrstep nfs Q (Pw ∪ Rw)"
using steps[rule_format, of i]
by (cases "k i", auto simp: qrstep_union)
}
with SN_rel_on_imp_SN_rel_on_alt[OF SN, unfolded SN_rel_on_alt_def, rule_format, of t]
have noninf: "¬ (∃⇩∞j. (t j, t (Suc j)) ∈ qrstep nfs Q (P ∪ R))" by auto
{
fix i
assume "k i ∈ {top_s, normal_s}"
with steps[rule_format, of i]
have "(t i, t (Suc i)) ∈ qrstep nfs Q (P ∪ R)"
by (cases "k i", auto simp: qrstep_union)
}
with strict noninf
show False unfolding INFM_nat by blast
qed
qed
datatype (dead 'f, dead 'l, dead 'v) dp_termination_proof =
P_is_Empty
| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Gen_Subterm_Criterion_Proc "('f, 'l) lab status_impl"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option × ('f, 'l, 'v) trsLL) list"
| Mono_Redpair_Proc "('f, 'l) lab redtriple_impl"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Mono_URM_Redpair_Proc "('f, 'l) lab redtriple_impl"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule × ((nat × nat) list × (nat × nat) list)) list"
| Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
"((('f, 'l) lab, 'v) rule × ((nat × nat) list × (nat × nat) list)) list"
| Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Split_Proc
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
"('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof"
| Semlab_Proc
"(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL"
"(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL"
"('f, 'l, 'v) dp_termination_proof"
| Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof"
| Rewriting_Proc
"('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL"
"('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof"
| Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Forward_Instantiation_Proc
"('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof"
| Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Assume_Finite
"('f, 'l, 'v) dppLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
| Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
| Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof"
| Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof"
| General_Redpair_Proc
"('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
"(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list"
| To_Trs_Proc "('f, 'l, 'v) trs_termination_proof"
and ('f, 'l, 'v) trs_termination_proof =
DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof"
| Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof"
| String_Reversal "('f, 'l, 'v) trs_termination_proof"
| Constant_String "(('f,'l)lab,'v)const_string_sound_proof" "('f,'l,'v) trs_termination_proof"
| Bounds "(('f, 'l) lab, 'v) bounds_info"
| Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
| Semlab
"(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
| R_is_Empty
| Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
| Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof"
| Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof"
| Drop_Equality "('f, 'l, 'v) trs_termination_proof"
| Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
| Permuting_AFS "('f,'l)lab afs_list" "('f, 'l, 'v) trs_termination_proof"
| Assume_SN "('f, 'l, 'v) qreltrsLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
and ('f, 'l, 'v) unknown_proof =
Assume_Unknown unknown_info "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
and ('f, 'l, 'v) fptrs_termination_proof =
Assume_FP_SN "('f,'l,'v)fptrsLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
fun dp_assms :: "bool ⇒ ('f, 'l, 'v) dp_termination_proof ⇒ ('f, 'l, 'v) assm list"
and sn_assms :: "bool ⇒ ('f,'l,'v) trs_termination_proof ⇒ ('f,'l,'v) assm list"
and sn_fp_assms :: "bool ⇒ ('f,'l,'v) fptrs_termination_proof ⇒ ('f,'l,'v) assm list"
and unknown_assms :: "bool ⇒ ('f,'l,'v) unknown_proof ⇒ ('f,'l,'v) assm list"
where
"dp_assms a P_is_Empty = []"
| "dp_assms a (Subterm_Criterion_Proc _ _ _ p) = dp_assms a p"
| "dp_assms a (Gen_Subterm_Criterion_Proc _ _ p) = dp_assms a p"
| "dp_assms a (Redpair_Proc _ _ p) = dp_assms a p"
| "dp_assms a (Redpair_UR_Proc _ _ _ p) = dp_assms a p"
| "dp_assms a (Usable_Rules_Proc _ p) = dp_assms a p"
| "dp_assms a (Dep_Graph_Proc ps) =
concat (concat (map (map (dp_assms a) ∘ option_to_list ∘ fst) ps))"
| "dp_assms a (Mono_Redpair_Proc _ _ _ p) = dp_assms a p"
| "dp_assms a (Mono_URM_Redpair_Proc _ _ _ p) = dp_assms a p"
| "dp_assms a (Mono_Redpair_UR_Proc _ _ _ _ p) = dp_assms a p"
| "dp_assms a (Size_Change_Subterm_Proc _) = []"
| "dp_assms a (Size_Change_Redpair_Proc _ _ _) = []"
| "dp_assms a (Uncurry_Proc _ _ _ _ p) = dp_assms a p"
| "dp_assms a (Fcc_Proc _ _ _ _ p) = dp_assms a p"
| "dp_assms a (Split_Proc _ _ p q) = dp_assms a p @ dp_assms a q"
| "dp_assms a (Semlab_Proc _ _ _ _ p) = dp_assms a p"
| "dp_assms a (Switch_Innermost_Proc _ p) = dp_assms a p"
| "dp_assms a (Rewriting_Proc _ _ _ _ _ _ p) = dp_assms a p"
| "dp_assms a (Narrowing_Proc _ _ _ p) = dp_assms a p"
| "dp_assms a (Instantiation_Proc _ _ p) = dp_assms a p"
| "dp_assms a (Forward_Instantiation_Proc _ _ _ p) = dp_assms a p"
| "dp_assms a (Unlab_Proc _ _ p) = dp_assms a p"
| "dp_assms a (Q_Reduction_Proc _ p) = dp_assms a p"
| "dp_assms a (General_Redpair_Proc _ _ _ _ ps) = concat (map (dp_assms a) ps)"
| "dp_assms a (Complex_Constant_Removal_Proc _ p) = dp_assms a p"
| "dp_assms a (To_Trs_Proc p) = sn_assms a p"
| "dp_assms a (Assume_Finite d dps) = (if a then Finite_assm (map assm_proof_to_problem dps) d
# concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) dps) else [])"
| "sn_assms a (DP_Trans _ _ _ p) = dp_assms a p"
| "sn_assms a (Rule_Removal _ _ p) = sn_assms a p"
| "sn_assms a (String_Reversal p) = sn_assms a p"
| "sn_assms a (Constant_String _ p) = sn_assms a p"
| "sn_assms a (Bounds _) = []"
| "sn_assms a (Uncurry _ _ p) = sn_assms a p"
| "sn_assms a (Semlab _ _ _ p) = sn_assms a p"
| "sn_assms a R_is_Empty = []"
| "sn_assms a (Fcc _ _ p) = sn_assms a p"
| "sn_assms a (Split _ p q) = sn_assms a p @ sn_assms a q"
| "sn_assms a (Switch_Innermost _ p) = sn_assms a p"
| "sn_assms a (Drop_Equality p) = sn_assms a p"
| "sn_assms a (Remove_Nonapplicable_Rules _ p) = sn_assms a p"
| "sn_assms a (Permuting_AFS _ p) = sn_assms a p"
| "sn_assms a (Assume_SN t tps) = (if a then SN_assm (map assm_proof_to_problem tps) t
# concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) tps) else [])"
| "sn_fp_assms a (Assume_FP_SN t tps) = (if a then SN_FP_assm (map assm_proof_to_problem tps) t
# concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) tps) else [])"
| "unknown_assms a (Assume_Unknown t tps) = (if a then Unknown_assm (map assm_proof_to_problem tps) t
# concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) tps) else [])"
lemma assms_False [simp]:
"dp_assms False (p :: ('f,'l,'v)dp_termination_proof) = []"
"sn_assms False (q :: ('f,'l,'v)trs_termination_proof) = []"
"sn_fp_assms False (r :: ('f,'l,'v)fptrs_termination_proof) = []"
"unknown_assms False (s :: ('f,'l,'v)unknown_proof) = []"
by (induct p and q and r and s
rule: dp_assms_sn_assms_sn_fp_assms_unknown_assms.induct[of
"λ a p. dp_assms False p = []"
"λ a q. sn_assms False q = []"
"λ a q. sn_fp_assms False q = []"
"λ a q. unknown_assms False q = []"], auto)
fun
get_fcc_option ::
"('f, 'l, 'v) dp_termination_proof ⇒
(('f, 'l) lab × (('f, 'l) lab, 'v) ctxt list × ('f, 'l, 'v) trsLL × ('f, 'l, 'v) trsLL × ('f, 'l, 'v) dp_termination_proof)option"
where
"get_fcc_option (Fcc_Proc f fcs Pb' Rb' prf) = Some (f, fcs, Pb', Rb', prf)" |
"get_fcc_option _ = None"
lemma (in tp_spec) mk_tp_set: "mk_tp_set t = tp_ops.qreltrs I (mk_tp I t)" by (cases t, auto)
lemma (in dpp_spec) mk_dpp_set: "mk_dpp_set t = dpp_ops.dpp I (mk_dpp I t)" by (cases t, auto)
hide_const (open) AC_Subterm_Criterion.proj_term
text ‹The parameter "assms" is a flag that specifies whether partial proofs
(i.e, containing assumptions) are accepted or not.›
context
fixes J :: "('tp, ('f::{show,key,countable}, label_type) lab, string) tp_ops"
and I :: "('dpp, ('f, label_type) lab, string) dpp_ops"
and assms :: bool
begin
fun check_assm :: "('tp ⇒ 'tp_prf ⇒ shows check)
⇒ ('dpp ⇒ 'dpp_prf ⇒ shows check)
⇒ (('f,label_type,string)fptrsLL ⇒ 'fptp_prf ⇒ shows check)
⇒ (unknown_info ⇒ 'unk_prf ⇒ shows check)
⇒ ('f,label_type,string, 'tp_prf, 'dpp_prf, 'fptp_prf, 'unk_prf) assm_proof ⇒ shows check" where
"check_assm tp_check dp_check fptp_check unk_check (SN_assm_proof t prf) = tp_check (mk_tp J t) prf"
| "check_assm tp_check dp_check fptp_check unk_check (Finite_assm_proof t prf) = dp_check (mk_dpp I t) prf"
| "check_assm tp_check dp_check fptp_check unk_check (Unknown_assm_proof t prf) = unk_check t prf"
| "check_assm tp_check dp_check fptp_check unk_check (SN_FP_assm_proof t prf) = fptp_check t prf"
| "check_assm _ _ _ _ _ = error (shows ''no support for non-termination assumptions in termination proof'')"
lemma check_assms_cong[fundef_cong]:
assumes
"⋀ t p. i = SN_assm_proof t p ⟹ tp (mk_tp J t) p = tp' (mk_tp J t) p"
"⋀ t p. i = Finite_assm_proof t p ⟹ dpp (mk_dpp I t) p = dpp' (mk_dpp I t) p"
"⋀ t p. i = SN_FP_assm_proof t p ⟹ fptp t p = fptp' t p"
"⋀ t p. i = Unknown_assm_proof t p ⟹ unk t p = unk' t p"
shows "check_assm tp dpp fptp unk i = check_assm tp' dpp' fptp' unk' i"
using assms
by (cases i, auto)
lemma check_assm:
assumes
"⋀ t p. i = SN_assm_proof t p ⟹ isOK(tp (mk_tp J t) p) ⟹ SN_qrel (mk_tp_set t)"
"⋀ d p. i = Finite_assm_proof d p ⟹ isOK(dpp (mk_dpp I d) p) ⟹ finite_dpp (mk_dpp_set d)"
"⋀ t p. i = SN_FP_assm_proof t p ⟹ isOK(fptp t p) ⟹ SN_fpstep (mk_fptp_set t)"
"⋀ d p. i = Unknown_assm_proof d p ⟹ isOK(unk d p) ⟹ unknown_satisfied d"
shows "isOK(check_assm tp dpp fptp unk i) ⟹ satisfied (assm_proof_to_problem i)"
using assms
by (cases i, auto)
function
check_dp_termination_proof_main ::
"shows ⇒ 'dpp ⇒
('f, label_type, string) dp_termination_proof ⇒
shows check"
and check_trs_termination_proof_main ::
"shows ⇒ 'tp ⇒
('f, label_type, string) trs_termination_proof ⇒
shows check"
and check_fptrs_termination_proof_main ::
"shows ⇒ ('f,label_type,string)fptrsLL ⇒
('f, label_type, string) fptrs_termination_proof ⇒
shows check"
and check_unknown_proof_main ::
"shows ⇒ unknown_info ⇒
('f, label_type, string) unknown_proof ⇒
shows check"
where
"check_dp_termination_proof_main i dpp P_is_Empty = debug (i []) ''P is empty''
(if dpp_ops.P I dpp = [] ∧ (dpp_ops.Pw I dpp = [] ∨ dpp_ops.R I dpp = [])
then succeed
else error (i ∘ shows '': P is not empty in the following DP-problem '' ∘
shows_nl ∘ shows_dpp I dpp))"
| "check_dp_termination_proof_main i dpp (Subterm_Criterion_Proc p rseq rP prf) =
debug (i []) ''Subterm_Criterion_Proc'' (do {
let P = dpp_ops.pairs I dpp;
let Pr = ceta_list_diff P rP;
dpp' ← subterm_criterion_proc I p rseq Pr dpp
<+? (λs. i ∘ shows '': error when applying the subterm criterion to the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows ''and trying to remove the pairs '' ∘ shows_nl ∘ shows_rules Pr
∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the subterm criterion'' ∘ shows_nl
∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Gen_Subterm_Criterion_Proc p Pr prf) =
debug (i []) ''Gen_Subterm_Criterion_Proc'' (do {
dpp' ← generalized_subterm_proc I p Pr dpp
<+? (λs. i ∘ shows '': error when applying the generalized subterm criterion to the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows ''and trying to remove the pairs '' ∘ shows_nl ∘ shows_rules Pr
∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the generalized subterm criterion'' ∘ shows_nl
∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Redpair_Proc redp rP prf) = debug (i []) ''Redpair_Proc'' (do {
let P = dpp_ops.pairs I dpp;
let Pr = ceta_list_diff P rP;
let Proc = (case redp of Inr rp ⇒ generic_ur_af_redtriple_proc I (get_redtriple rp) None
| Inl rrp ⇒ generic_ur_af_root_redtriple_proc I (get_root_redtriple rrp) None);
dpp' ← Proc Pr dpp
<+? (λs. i ∘ shows '': error when applying the reduction pair processor to remove from the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows '' the pairs '' ∘ shows_nl ∘ shows_rules Pr ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the reduction pair processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Usable_Rules_Proc U prf) = debug (i []) ''Usable_Rules_Proc'' (do {
dpp' ← usable_rules_proc I U dpp
<+? (λs. i ∘ shows '': error when applying the usable rules processor to restrict the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows '' to the usable rules '' ∘ shows_nl ∘ shows_rules U ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the usable rules processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Q_Reduction_Proc Q prf) = debug (i []) ''Q_Reduction_Proc'' (do {
dpp' ← q_reduction_proc I Q dpp
<+? (λs. i ∘ shows '': error when applying the Q-reduction processor'' ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the Q-reduction processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Mono_Redpair_Proc redp rP rR prf) = debug (i []) ''Mono_Redpair_Proc'' (do {
let P = dpp_ops.pairs I dpp;
let Pr = ceta_list_diff P rP;
let R = dpp_ops.rules I dpp;
let Rr = ceta_list_diff R rR;
dpp' ← mono_redpair_proc I (get_redtriple redp) Pr Rr dpp
<+? (λs. i ∘ shows '': error when applying the mono reduction pair processor to remove from the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows '' the pairs '' ∘ shows_nl ∘ shows_rules Pr ∘ shows_nl
∘ shows '' and the rules '' ∘ shows_nl ∘ shows_rules Rr ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the mono reduction pair processor''∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Mono_URM_Redpair_Proc redp Pr Rr prf) = debug (i []) ''Mono_URM_Redpair_Proc'' (do {
dpp' ← mono_urm_redpair_proc I (get_redtriple redp) Pr Rr dpp
<+? (λs. i ∘ shows '': error when applying the mono reduction pair processor with usable repl. map to remove from the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows '' the pairs '' ∘ shows_nl ∘ shows_rules Pr ∘ shows_nl
∘ shows '' and the rules '' ∘ shows_nl ∘ shows_rules Rr ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the mono reduction pair processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Dep_Graph_Proc edpts) =
debug (i []) ''Dep_Graph_Proc'' (do {
pdpps ← dep_graph_proc I dpp edpts
<+? (λs. i ∘ shows '': error while trying to perform Sctxt_closure-decomposition on '' ∘
shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s);
check_allm_index (λ (prof,dpp') j. check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) dpp' prof) pdpps
<+? (λs. i ∘ shows '': error below the dependency graph processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Redpair_UR_Proc redp rP ur prf) = debug (i []) ''Redpair_UR_Proc'' (do {
let P = dpp_ops.pairs I dpp;
let Pr = ceta_list_diff P rP;
let Proc = (case redp of Inr rp ⇒ generic_ur_af_redtriple_proc I (get_redtriple rp) (Some ur)
| Inl rrp ⇒ generic_ur_af_root_redtriple_proc I (get_root_redtriple rrp) (Some ur));
dpp' ← Proc Pr dpp
<+? (λs. i ∘ shows '': error when applying the reduction pair processor with usable rules to remove from the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows '' the pairs '' ∘ shows_nl ∘ shows_rules Pr ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the reduction pair processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Mono_Redpair_UR_Proc redp rP rR ur prf) = debug (i []) ''Mono_Redpair_UR_Proc'' (do {
let P = dpp_ops.pairs I dpp;
let Pr = ceta_list_diff P rP;
let R = dpp_ops.rules I dpp;
let Rr = ceta_list_diff R rR;
dpp' ← generic_mono_ur_redpair_proc I (get_redtriple redp) Pr Rr ur dpp
<+? (λs. i ∘ shows '': error when applying the mono reduction pair processor with usable rules to remove from the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl
∘ shows '' the pairs '' ∘ shows_nl ∘ shows_rules Pr ∘ shows_nl
∘ shows '' and the rules '' ∘ shows_nl ∘ shows_rules Rr ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the mono reduction pair processor with usable rules'' ∘ shows_nl
∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Uncurry_Proc mode u_info P' R' prf) =
debug (i []) ''Uncurry_Proc'' (do {
dpp' ← uncurry_proc_both I mode u_info P' R' dpp
<+? (λs. i ∘ shows '': error when applying the uncurrying processor on the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the uncurrying processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Size_Change_Subterm_Proc graphs) =
debug (i []) ''Size_Change_Subterm_Proc'' (sct_subterm_proc I graphs dpp
<+? (λs. i ∘ shows '': error when applying the size-change (subterm) processor on the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s))"
| "check_dp_termination_proof_main i dpp (Size_Change_Redpair_Proc redp U_opt graphs) =
debug (i []) ''Size_Change_Redpair_Proc'' (sct_ur_af_proc I (get_redtriple redp) graphs U_opt dpp
<+? (λs. i ∘ shows '': error when applying the size-change (redpair) processor on the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s))"
| "check_dp_termination_proof_main i dpp (Fcc_Proc f fcs Pb' R' prf) = debug (i []) ''Fcc_Proc'' (do {
dpp' ← fcc_proc I f fcs Pb' R' dpp
<+? (λs. i ∘
shows '': error when applying the flat context closure processor on the DP problem'' ∘
shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the flat context closure processor'' ∘ shows_nl
∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Split_Proc Prem Rrem prf1 prf2) = debug (i []) ''Split_Proc'' (case get_fcc_option prf1 of
Some (f,fcs,Pb',Rb',prf1') ⇒ debug (i []) ''Split_ProcFcc'' (do {
(dpp1,dpp2) ← fcc_split_proc I f fcs Pb' Rb' Prem Rrem dpp;
check_dp_termination_proof_main (i ∘ shows_string ''.1.1'') dpp1 prf1'
<+? (λs. i ∘ shows '': error below the split and fcc processor'' ∘ shows_nl ∘ indent s);
check_dp_termination_proof_main (i ∘ shows_string ''.2'') dpp2 prf2
<+? (λs. i ∘ shows '': error below the split processor'' ∘ shows_nl ∘ indent s)
})
| None ⇒ do {
let (dpp1,dpp2) = split_proc I dpp Prem Rrem;
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp1 prf1
<+? (λs. i ∘ shows '': error below the split processor'' ∘ shows_nl ∘ indent s);
check_dp_termination_proof_main (i ∘ shows_string ''.2'') dpp2 prf2
<+? (λs. i ∘ shows '': error below the split processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Semlab_Proc sli lP lQ lR prf) =
debug (i []) ''Semlab_Proc'' (do {
dpp' ← semlab_fin_proc I sli lP lQ lR dpp
<+? (λs. i ∘ shows '': error when applying the semlab processor on the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the semlab processor'' ∘ shows_nl
∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Switch_Innermost_Proc joins prf) =
debug (i []) ''Switch_Innermost_Proc'' (do {
dpp' ← switch_innermost_proc I joins dpp
<+? (λs. i ∘ shows '': error when applying the processor to switch to innermost on the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the switch to innermost processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Assume_Finite dpp' ass) =
debug (i []) ''Finiteness Assumption or Unknown Proof'' (
if assms
then (do {
check_dpp_subsumes I dpp' dpp
<+? (λs. i ∘ shows '': error in finiteness assumption or unknown proof'' ∘ shows_nl ∘ s ∘ shows_nl);
check_allm_index (λ as j. check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)
ass
<+? (λs. i ∘ shows '': error below unknown proof'' ∘ shows_nl
∘ indent s)
}) else error (i ∘ shows '': the proof contains a finiteness assumption or unknown proof'' ∘ shows_nl)
)"
| "check_dp_termination_proof_main i dpp (Rewriting_Proc U_opt st st' st'' lr p prf) = debug (i []) ''Rewriting_Proc'' (do {
dpp' ← rewriting_proc I U_opt st st' st'' lr p dpp
<+? (λs. i ∘ shows '': error when applying the rewriting processor to rewrite the pair ''
∘ shows_nl ∘ shows_rule st ∘ shows_nl ∘
shows '' to the pair '' ∘ shows_nl ∘ shows_rule st'' ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the rewriting processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Narrowing_Proc st p sts prf) = debug (i []) ''Narrowing_Proc'' (do {
dpp' ← narrowing_proc I st p sts dpp
<+? (λs. i ∘ shows '': error when applying the narrowing processor to narrow the pair ''
∘ shows_nl ∘ shows_rule st ∘ shows_nl ∘
shows '' to the pairs '' ∘ shows_nl ∘ shows_trs sts ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the narrowing processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Instantiation_Proc st sts prf) = debug (i []) ''Instantiation_Proc'' (do {
dpp' ← instantiation_proc I st sts dpp
<+? (λs. i ∘ shows '': error when applying the instantiation processor to instantiate the pair ''
∘ shows_nl ∘ shows_rule st ∘ shows_nl ∘
shows '' to the pairs '' ∘ shows_nl ∘ shows_trs sts ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the instantiation processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Forward_Instantiation_Proc st sts u_opt prf) = debug (i []) ''Forward_Instantiation_Proc'' (do {
dpp' ← forward_instantiation_proc I st sts u_opt dpp
<+? (λs. i ∘ shows '': error when applying the forward_instantiation processor to instantiate the pair ''
∘ shows_nl ∘ shows_rule st ∘ shows_nl ∘
shows '' to the pairs '' ∘ shows_nl ∘ shows_trs sts ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the forward instantiation processor'' ∘ shows_nl ∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (Unlab_Proc P R prf) = debug (i []) ''Unlab_Proc'' (error (shows ''unlabeling processor not supported''))"
| "check_dp_termination_proof_main i dpp (General_Redpair_Proc rp ps pb prof prfs) =
debug (i []) ''General_Redpair_ProcProc'' (do {
let n = length prfs;
check (n > 0) (shows ''at least one subproof is required'');
let Merge = (n = 1);
dpps ← conditional_general_reduction_pair_proc I (get_non_inf_order rp) ps pb prof Merge dpp
<+? (λs. i ∘ shows '': error when applying the generic reduction pair processor to the DP problem''
∘ shows_nl ∘ shows_dpp I dpp ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') (dpps ! 0) (prfs ! 0)
<+? (λs. i ∘ shows '': error below the generic reduction pair processor'' ∘ shows_nl ∘ indent s);
if Merge then succeed else (
check_dp_termination_proof_main (i ∘ shows_string ''.2'') (dpps ! 1) (prfs ! 1)
<+? (λs. i ∘ shows '': error below the generic reduction pair processor'' ∘ shows_nl
∘ indent s))
})"
| "check_dp_termination_proof_main i dpp (Complex_Constant_Removal_Proc p prf) =
debug (i []) ''Complex_Constant_Removal_Proc'' (do {
dpp' ← complex_constant_removal_proc I p dpp
<+? (λs. i ∘ shows '': error when applying the complex constant removal processor to the DP problem''
∘ shows_nl ∘ shows_dpp I dpp
∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp' prf
<+? (λs. i ∘ shows '': error below the complex constant removal processor'' ∘ shows_nl
∘ indent s)
})"
| "check_dp_termination_proof_main i dpp (To_Trs_Proc prf) =
debug (i []) ''To_Trs_Proc'' (do {
check_trs_termination_proof_main (i ∘ shows_string ''.1'')
(mk_tp J (dpp_ops.nfs I dpp, dpp_ops.Q I dpp, dpp_ops.P I dpp @ dpp_ops.R I dpp, dpp_ops.Pw I dpp @ dpp_ops.Rw I dpp)) prf
<+? (λs. i ∘ shows '': error below the To-Trs processor'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp R_is_Empty = debug (i []) ''R is empty''
(if tp_ops.R J tp = []
then succeed
else error (i ∘ shows '': R is not empty in the following termination-problem '' ∘
shows_nl ∘ shows_tp J tp))"
| "check_trs_termination_proof_main i tp (Rule_Removal redp rR prf) = debug (i []) ''Rule Removal'' (do {
let R = tp_ops.rules J tp;
let Rr = ceta_list_diff R rR;
tp' ← rule_removal_tt J (get_redtriple redp) Rr tp
<+? (λs. i ∘ shows '': error when applying the rule removal technique on ''
∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘
shows '' to remove the rules '' ∘ shows_nl ∘ shows_rules Rr ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the rule removal technique'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (DP_Trans nfs m P prf) = debug (i []) ''DP trans'' (do {
dpp ← dependency_pairs_tt Sharp J I tp nfs m P
<+? (λs. i ∘ shows '': error when switching from the TRS'' ∘ shows_nl ∘ shows_tp J tp
∘ shows_nl ∘ shows ''to the initial DP problem with pairs '' ∘ shows_nl ∘ shows_rules P ∘ shows_nl ∘ s);
check_dp_termination_proof_main (i ∘ shows_string ''.1'') dpp prf
<+? (λs. i ∘ shows '': error below switch to dependency pairs'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (String_Reversal prf) = debug (i []) ''String Reversal'' (do {
tp' ← string_reversal_tt J tp
<+? (λs. i ∘ shows '': error when applying string reversal on ''
∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the string reversal technique'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Constant_String p prf) = debug (i []) ''Constant to Unary'' (do {
tp' ← const_to_string_sound_tt p J tp
<+? (λs. i ∘ shows '': error when turning constants into unary symbols on ''
∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the constant to unary technique'' ∘ shows_nl∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Semlab sli lQ lAll prf) = debug (i []) ''Semlab'' (do {
tp' ← semlab_fin_tt J sli lQ lAll tp
<+? (λs. i ∘ shows '': error when applying semantic labelling on ''
∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the sem.lab technique'' ∘ shows_nl
∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Bounds info) = debug (i []) ''Bounds'' (do {
bounds_tt J info tp
<+? (λs. i ∘ shows '': error when applying bounds on the termination problem '' ∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘ s)})"
| "check_trs_termination_proof_main i tp (Uncurry u_info rR prf) = debug (i []) ''Uncurry'' (do {
tp' ← uncurry_tt J u_info rR tp
<+? (λs. i ∘ shows '': error when applying currying transformation'' ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the uncurrying technique'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Fcc fcs R' prf) = debug (i []) ''Fcc'' (do {
tp' ← fcc_tt J fcs R' tp
<+? (λs. i ∘ shows '': error when applying flat context closure'' ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below flat context closure'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Split Rrem prf1 prf2) = debug (i []) ''Split'' (do {
let (tp1,tp2) = split_tt J tp Rrem;
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp1 prf1
<+? (λs. i ∘ shows '': error below the splitting'' ∘ shows_nl ∘ indent s);
check_trs_termination_proof_main (i ∘ shows_string ''.2'') tp2 prf2
<+? (λs. i ∘ shows '': error below the splitting'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Switch_Innermost joins prf) = debug (i []) ''Switch Innermost'' (do {
tp' ← switch_innermost_tt J joins tp
<+? (λs. i ∘ shows '': error when switching to innermost on ''
∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the switch to innermost'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Drop_Equality prf) = debug (i []) ''Drop Equality'' (do {
let tp' = tp_ops.mk J (tp_ops.nfs J tp) (tp_ops.Q J tp) (tp_ops.R J tp) (filter (λ (l,r). l ≠ r) (tp_ops.Rw J tp));
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below dropping equality rules'' ∘ shows_nl ∘ indent s)
})"
| "check_trs_termination_proof_main i tp (Remove_Nonapplicable_Rules r prf) = debug (i []) ''Removing non-applicable rules'' (do {
let R = tp_ops.R J tp;
check_non_applicable_rules (tp_ops.is_QNF J tp) r
<+? (λ s. i ∘ shows '': error when removing non-applicable rules'' ∘ shows_nl ∘ indent (shows_rule s ∘ shows '' is applicable''));
let tp' = tp_spec.delete_rules J tp r;
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the non-applicable rules removal'' ∘ shows_nl ∘ indent s)})"
| "check_trs_termination_proof_main i tp (Permuting_AFS pi prf) = debug (i []) ''Permuting some rules'' (do {
tp' ← argument_filter_tt J pi tp
<+? (λs. i ∘ shows '': error when permuting arguments on '' ∘ shows_nl ∘ shows_tp J tp ∘ shows_nl ∘ s);
check_trs_termination_proof_main (i ∘ shows_string ''.1'') tp' prf
<+? (λs. i ∘ shows '': error below the permutation of arguments'' ∘ shows_nl ∘ indent s)})"
| "check_trs_termination_proof_main i tp (Assume_SN tp' ass) =
debug (i []) ''Termination Assumption or Unknown Proof'' (
if assms
then (do {
check_tp_subsumes J tp' tp
<+? (λs. i ∘ shows '': error in termination assumption or unknown proof'' ∘ shows_nl ∘ s ∘ shows_nl);
check_allm_index (λ as j. check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)
ass
}) else error (i ∘ shows '': the proof contains a termination assumption or unknown proof'' ∘ shows_nl)
)"
| "check_fptrs_termination_proof_main i tp (Assume_FP_SN tp' ass) =
debug (i []) ''Outermost Termination Assumption or Unknown Proof'' (
if assms
then (do {
check (tp = tp') (shows ''outermost assumption does not match current goal'');
check_allm_index (λ as j. check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)
ass
}) else error (i ∘ shows '': the proof contains a termination assumption or unknown proof'' ∘ shows_nl)
)"
| "check_unknown_proof_main i tp (Assume_Unknown tp' ass) =
debug (i []) ''Unknown Proof'' (
if assms
then (do {
check (tp = tp') (shows ''unknown problems are not identical: '' ∘ shows_nl ∘ shows tp ∘ shows_nl
∘ shows '' vs '' ∘ shows_nl ∘ shows tp')
<+? (λs. i ∘ shows '': error in termination assumption or unknown proof'' ∘ shows_nl ∘ s ∘ shows_nl);
check_allm_index (λ as j. check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)
ass
}) else error (i ∘ shows '': the proof contains an unknown proof'' ∘ shows_nl)
)"
by pat_completeness auto
termination
proof -
let ?dpp = "λ x. Inl (Inl x)"
let ?trs = "λ x. Inl (Inr x)"
let ?fptrs = "λ x. Inr (Inl x)"
let ?unk = "λ x. Inr (Inr x)"
let ?M = "(λ c. case c of ?dpp (i, dpp, prof) ⇒ size prof
| ?trs (i, tp, prof) ⇒ size prof
| ?fptrs (i, tp, prof) ⇒ size prof
| ?unk (i, tp, prof) ⇒ size prof)"
show ?thesis
proof (rule, unfold update_error_return)
fix i dpp
and edpts :: "(('f, label_type, string) dp_termination_proof option
× ('f, label_type, string ) trsLL) list"
and pdpps pdpp i' prof dpp' j
assume proc: "dep_graph_proc I dpp edpts = Inr pdpps"
and mem: "pdpp ∈ set pdpps" and pdpp: "(prof, dpp') = pdpp"
show "(?dpp (i ∘ shows ''.'' ∘ shows (Suc j), dpp', prof),
?dpp (i, dpp, Dep_Graph_Proc edpts))
∈ measure ?M"
proof -
from proc mem [unfolded pdpp [symmetric]]
have "Some prof ∈ set (map fst edpts)" unfolding dep_graph_proc_def by force
then obtain P where "(Some prof, P) ∈ set edpts" by auto
thus ?thesis
by (induct edpts, auto)
qed
next
fix i dpp Prem Rrem prf1 prf2 a x y xa ya xb yb xc yc yd xd ye
assume ass1: "get_fcc_option prf1 = Some a" and ass2: "(x, y) = a" "(xa, ya) = y"
"(xb, yb) = ya" "(xc, yc) = yb"
"fcc_split_proc I x xa xb xc Prem Rrem dpp = Inr yd" "(xd, ye) = yd"
show "(?dpp (i ∘ shows_string ''.1.1'', xd, yc),
?dpp (i, dpp, Split_Proc Prem Rrem prf1 prf2))
∈ measure ?M"
proof -
from ass1 obtain f fcs Pb' Rb' prf1a
where prf1: "prf1 = Fcc_Proc f fcs Pb' Rb' prf1a" by (cases prf1, force+)
from ass1 ass2
show ?thesis unfolding prf1 by auto
qed
next
fix i dpp rp ps pb c prfs x y xa ya
show "x = length prfs ⟹
check (0 < x) (shows ''at least one subproof is required'') = Inr y ⟹
xa = (x = 1) ⟹
conditional_general_reduction_pair_proc I (get_non_inf_order rp) ps pb c xa dpp = Inr ya ⟹
(?dpp (i ∘ shows_string ''.1'', ya ! 0, prfs ! 0),
(?dpp (i, dpp, General_Redpair_Proc rp ps pb c prfs)))
∈ measure ?M"
by (cases prfs, auto simp: check_def)
next
fix x prfs xa y rp ps pb c assms i dpp ya
show "x = length prfs ⟹
check (0 < x) (shows ''at least one subproof is required'') = Inr y ⟹
xa = (x = 1) ⟹ ¬ xa ⟹
(?dpp (i ∘ shows_string ''.2'', ya ! 1, prfs ! 1),
?dpp (i, dpp, General_Redpair_Proc rp ps pb c prfs))
∈ measure ?M"
by (cases prfs, simp add: check_def, cases "tl prfs", auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹ x = Finite_assm_proof t p ⟹
(?dpp (i ∘ shows ''.'' ∘ shows (Suc ia), mk_dpp I t, p), ?trs (i, tp, Assume_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_assm_proof t p ⟹
(?trs (i ∘ shows ''.'' ∘ shows (Suc ia), mk_tp J t, p), ?trs (i, tp, Assume_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_FP_assm_proof t p ⟹
(?fptrs (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?trs (i, tp, Assume_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = Unknown_assm_proof t p ⟹
(?unk (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?trs (i, tp, Assume_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹ x = Finite_assm_proof t p ⟹
(?dpp (i ∘ shows ''.'' ∘ shows (Suc ia), mk_dpp I t, p), ?dpp (i, tp, Assume_Finite tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_FP_assm_proof t p ⟹
(?fptrs (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?dpp (i, tp, Assume_Finite tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_assm_proof t p ⟹
(?trs (i ∘ shows ''.'' ∘ shows (Suc ia), mk_tp J t, p), ?dpp (i, tp, Assume_Finite tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = Unknown_assm_proof t p ⟹
(?unk (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?dpp (i, tp, Assume_Finite tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹ x = Finite_assm_proof t p ⟹
(?dpp (i ∘ shows ''.'' ∘ shows (Suc ia), mk_dpp I t, p), ?fptrs (i, tp, Assume_FP_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_assm_proof t p ⟹
(?trs (i ∘ shows ''.'' ∘ shows (Suc ia), mk_tp J t, p), ?fptrs (i, tp, Assume_FP_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_FP_assm_proof t p ⟹
(?fptrs (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?fptrs (i, tp, Assume_FP_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = Unknown_assm_proof t p ⟹
(?unk (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?fptrs (i, tp, Assume_FP_SN tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹ x = Finite_assm_proof t p ⟹
(?dpp (i ∘ shows ''.'' ∘ shows (Suc ia), mk_dpp I t, p), ?unk (i, tp, Assume_Unknown tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_assm_proof t p ⟹
(?trs (i ∘ shows ''.'' ∘ shows (Suc ia), mk_tp J t, p), ?unk (i, tp, Assume_Unknown tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = SN_FP_assm_proof t p ⟹
(?fptrs (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?unk (i, tp, Assume_Unknown tp' ass)) ∈ measure ?M"
by (induct ass, auto)
next
fix i tp tp' ass y x ia t p
show "x ∈ set ass ⟹
x = Unknown_assm_proof t p ⟹
(?unk (i ∘ shows ''.'' ∘ shows (Suc ia), t, p), ?unk (i, tp, Assume_Unknown tp' ass)) ∈ measure ?M"
by (induct ass, auto)
qed auto
qed
lemma isOK_check_dp_termination_proof_main_Assume_Finite_False [simp]:
assumes "¬ assms"
shows "isOK (check_dp_termination_proof_main i dpp (Assume_Finite dpp' dps)) = False"
by (simp, insert assms, auto)
lemma check_dp_trs_unknown_termination_proof_main_with_assms:
assumes I: "dpp_spec I" and J: "tp_spec J"
shows "isOK (check_dp_termination_proof_main i dpp prf) ⟹ ∀assm∈set (dp_assms assms prf). holds assm
⟹ finite_dpp (dpp_ops.dpp I dpp)" (is "_ ⟹ ?P prf ⟹ _")
"isOK (check_trs_termination_proof_main i' tp prf') ⟹ ∀assm∈set (sn_assms assms prf'). holds assm
⟹ SN_qrel (tp_ops.qreltrs J tp)" (is "_ ⟹ ?Q prf' ⟹ _")
"isOK (check_fptrs_termination_proof_main i'' fptp prf'') ⟹ ∀assm∈set (sn_fp_assms assms prf''). holds assm
⟹ SN_fpstep (mk_fptp_set fptp)" (is "_ ⟹ ?R prf'' ⟹ _")
"isOK (check_unknown_proof_main i''' unk prf''') ⟹ ∀assm∈set (unknown_assms assms prf'''). holds assm
⟹ unknown_satisfied unk" (is "_ ⟹ ?R prf''' ⟹ _")
proof (induct i dpp "prf" and i' tp prf' and i'' fptp prf'' and i''' unk prf'''
rule: check_dp_termination_proof_main_check_trs_termination_proof_main_check_fptrs_termination_proof_main_check_unknown_proof_main.induct)
case (1 i dpp)
note IH = this
interpret dpp_spec I by fact
from IH(1) show ?case by (auto simp:
finite_dpp_def ichain.simps)
next
case (2 i dpp p rseq rP prof)
note IH = this
interpret dpp_spec I by fact
let ?Pr = "ceta_list_diff (dpp_ops.pairs I dpp) rP"
let ?i = "i ∘ shows_string ''.1''"
from IH(2)
obtain dpp' where proc: "subterm_criterion_proc I p rseq ?Pr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF subterm_criterion_proc[OF I] proc],
rule IH(1)[OF HOL.refl HOL.refl _ rec fin], insert proc, simp)
next
case (3 i dpp p Pr prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2)
obtain dpp' where proc: "generalized_subterm_proc I p Pr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF generalized_subterm_proc proc],
rule IH(1)[OF _ rec fin], insert proc, simp)
next
case (4 i dpp rpc rP prof)
note IH = this
interpret dpp_spec I by fact
let ?Pr = "ceta_list_diff (dpp_ops.pairs I dpp) rP"
let ?i = "i ∘ shows_string ''.1''"
from IH have fin: "?P prof" by simp
show ?case
proof (cases rpc)
case (Inr rp)
with IH(2)
obtain dpp' where proc: "generic_ur_af_redtriple_proc I (get_redtriple rp) None ?Pr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH(1)[OF HOL.refl HOL.refl HOL.refl _ rec fin, unfolded Inr update_error_return sum.simps, OF proc]
have fin: "finite_dpp (dpp_ops.dpp I dpp')" .
show ?thesis
by (rule sound_proc_impl[OF generic_ur_af_redtriple_proc[OF I get_redtriple] _ fin],
rule proc)
next
case (Inl rrp)
with IH(2)
obtain dpp' where proc: "generic_ur_af_root_redtriple_proc I (get_root_redtriple rrp) None ?Pr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH(1)[OF HOL.refl HOL.refl HOL.refl _ rec fin, unfolded Inl update_error_return sum.simps, OF proc]
have fin: "finite_dpp (dpp_ops.dpp I dpp')" .
show ?thesis
by (rule sound_proc_impl[OF generic_ur_af_root_redtriple_proc[OF I get_root_redtriple] _ fin], rule proc)
qed
next
case (5 i dpp ur prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "usable_rules_proc I ur dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF usable_rules_proc[OF I] proc IH(1)[OF _ rec fin]], insert proc, auto)
next
case (6 i dpp q prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2)
obtain dpp' where proc: "q_reduction_proc I q dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF q_reduction_proc[OF I], OF proc IH(1),
unfolded update_error_return, OF proc rec fin])
next
case (7 i dpp rp rP rR prof)
note IH = this
interpret dpp_spec I by fact
let ?Pr = "ceta_list_diff (dpp_ops.pairs I dpp) rP"
let ?Rr = "ceta_list_diff (dpp_ops.rules I dpp) rR"
let ?i = "i ∘ shows_string ''.1''"
from IH(2)
obtain dpp' where proc: "mono_redpair_proc I (get_redtriple rp) ?Pr ?Rr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF mono_redpair_proc[OF get_redtriple],
OF proc IH(1)[OF HOL.refl HOL.refl HOL.refl HOL.refl _ rec fin]],
unfold update_error_return, rule proc)
next
case (8 i dpp rp Pr Rr prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2)
obtain dpp' where proc: "mono_urm_redpair_proc I (get_redtriple rp) Pr Rr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF mono_urm_redpair_proc[OF get_redtriple I] proc IH(1)[OF _ rec fin]],
unfold update_error_return, rule proc)
next
case (9 i dpp edpts)
note IH = this
interpret dpp_spec I by fact
from IH(2) obtain pdpps where proc: "dep_graph_proc I dpp edpts = return pdpps"
and rec: "⋀j. j < length pdpps ⟹
isOK ((λ(prof, dpp') j.
check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) dpp' prof) (pdpps ! j) j)"
by auto
show ?case
proof (rule dep_graph_proc[OF I proc])
fix p dpp'
assume mem: "(p, dpp') ∈ set pdpps"
from this[unfolded set_conv_nth]
obtain j where j: "j < length pdpps" and pair: "pdpps ! j = (p, dpp')" by auto
from rec[OF j] have rec: "isOK (check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) dpp' p)"
unfolding pair by simp
from proc[unfolded dep_graph_proc_def, simplified]
have pdpps: "pdpps =
map (λaP. (the (fst aP), dpp_ops.intersect_pairs I dpp (snd aP)))
[aP←edpts . ∃y. fst aP = Some y]" by simp
from mem IH(3) and proc
have fin: "?P p" by (simp add: dep_graph_proc_def) force
show "finite_dpp (dpp_ops.dpp I dpp')"
by (rule IH(1)[unfolded update_error_return, OF proc mem HOL.refl rec fin])
qed
next
case (10 i dpp rpc rP ur prof)
note IH = this
interpret dpp_spec I by fact
let ?Pr = "ceta_list_diff (dpp_ops.pairs I dpp) rP"
let ?i = "i ∘ shows_string ''.1''"
from IH have fin: "?P prof" by simp
show ?case
proof (cases rpc)
case (Inr rp)
with IH(2) obtain dpp'
where proc: "generic_ur_af_redtriple_proc I (get_redtriple rp) (Some ur) ?Pr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
show ?thesis
by (rule sound_proc_impl[OF generic_ur_af_redtriple_proc[OF I get_redtriple],
OF proc IH(1)[OF HOL.refl HOL.refl HOL.refl _ rec fin]],
unfold Inr update_error_return sum.simps, rule proc)
next
case (Inl rrp)
with IH(2) obtain dpp'
where proc: "generic_ur_af_root_redtriple_proc I (get_root_redtriple rrp) (Some ur) ?Pr dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
show ?thesis
by (rule sound_proc_impl[OF generic_ur_af_root_redtriple_proc[OF I get_root_redtriple],
OF proc IH(1)[OF HOL.refl HOL.refl HOL.refl _ rec fin]],
unfold Inl update_error_return sum.simps, rule proc)
qed
next
case (11 i dpp rp rP rR ur prof)
note IH = this
interpret dpp_spec I by fact
let ?Pr = "ceta_list_diff (dpp_ops.pairs I dpp) rP"
let ?Rr = "ceta_list_diff (dpp_ops.rules I dpp) rR"
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "generic_mono_ur_redpair_proc I (get_redtriple rp) ?Pr ?Rr ur dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF generic_mono_ur_redpair_proc[OF I get_redtriple],
OF proc IH(1)[OF HOL.refl HOL.refl HOL.refl HOL.refl _ rec fin]],
unfold update_error_return, rule proc)
next
case (12 i dpp mode u_info P' R' prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain
dpp' where proc: "uncurry_proc_both I mode u_info P' R' dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF uncurry_proc_both[OF I], OF proc IH(1)],
unfold update_error_return, rule proc, rule rec, rule fin)
next
case (13 i dpp graphs)
note IH = this
from IH(1) have proc: "isOK (sct_subterm_proc I graphs dpp)" by auto
show ?case
by (rule sct_subterm_proc_sound[OF ‹dpp_spec I› proc])
next
case (14 i dpp rp u_opt graphs)
note IH = this
interpret dpp_spec I by fact
from IH(1) have proc: "isOK (sct_ur_af_proc I (get_redtriple rp) graphs u_opt dpp)" by auto
show ?case
by (rule sct_ur_af_proc[OF I get_redtriple, OF proc])
next
case (15 i dpp f fcs Pb' R' prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "fcc_proc I f fcs Pb' R' dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)" by auto
from IH have fin: "?P prof" by simp
from IH(1)[OF _ rec fin, simplified, OF proc] have "finite_dpp (dpp_ops.dpp I dpp')"
by simp
from sound_proc_impl[OF fcc_proc, OF proc this] show ?case .
next
case (16 i dpp P' R' prof1 prof2)
note IH = this
interpret dpp_spec I by fact
let ?i = "λs. i ∘ shows_string s"
let ?i1 = "?i ''.1''"
let ?i11 = "?i ''.1.1''"
let ?i2 = "?i ''.2''"
note res = IH(5)[unfolded check_dp_termination_proof_main.simps debug.simps]
note ass = IH(6)[unfolded dp_assms.simps]
show ?case
proof (cases "get_fcc_option prof1")
case None
obtain dpp1 dpp2 where s: "split_proc I dpp P' R' = (dpp1, dpp2)" by force
note ss = s[symmetric]
note res = res[unfolded None s option.simps Let_def split]
from res have ok1: "isOK (check_dp_termination_proof_main ?i1 dpp1 prof1)"
and ok2: "isOK (check_dp_termination_proof_main ?i2 dpp2 prof2)" by auto
from ass have fin1: "?P prof1" and fin2: "?P prof2" by simp_all
from IH(1)[OF None ss refl ok1 fin1]
have fin1': "finite_dpp (dpp_ops.dpp I dpp1)" .
from IH(2)[OF None ss refl _ ok2 fin2] ok1
have fin2': "finite_dpp (dpp_ops.dpp I dpp2)" by auto
show ?thesis
by (rule split_proc[OF s fin1' fin2'])
next
case (Some fcco)
from Some obtain f fcs Pb' Rb' prf1a where prof1: "prof1 = Fcc_Proc f fcs Pb' Rb' prf1a" by (cases prof1, force+)
hence fcco: "get_fcc_option prof1 = Some (f,fcs,Pb',Rb',prf1a)" by simp
note res = res[unfolded option.simps fcco Let_def split]
let ?call = "fcc_split_proc I f fcs Pb' Rb' P' R' dpp"
from res obtain dpp1 dpp2 where proc: "?call = Inr (dpp1,dpp2)"
by (cases ?call, auto)
note res = res[unfolded proc, simplified]
from res have ok1: "isOK (check_dp_termination_proof_main ?i11 dpp1 prf1a)"
and ok2: "isOK (check_dp_termination_proof_main ?i2 dpp2 prof2)" by auto
from ass have fin1: "?P prf1a" and fin2: "?P prof2"
unfolding prof1 by simp_all
from IH(3)[OF fcco refl refl refl refl proc refl ok1 fin1]
have fin1': "finite_dpp (dpp_ops.dpp I dpp1)" .
from IH(4)[OF fcco refl refl refl refl proc refl _ ok2 fin2] ok1
have fin2': "finite_dpp (dpp_ops.dpp I dpp2)" by auto
show ?thesis
by (rule fcc_split_proc[OF I proc fin1' fin2'])
qed
next
case (17 i dpp sli lP lQ lR prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "semlab_fin_proc I sli lP lQ lR dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF semlab_fin_proc[OF I], OF proc IH(1)],
unfold update_error_return, rule proc, rule rec, rule fin)
next
case (18 i dpp joins prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "switch_innermost_proc I joins dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF switch_innermost_proc[OF I] _ IH(1)], rule proc, unfold update_error_return, rule proc, rule rec, rule fin)
next
case (19 i dpp dpp' ass)
note IH = this
interpret dpp_spec I by fact
interpret J: tp_spec J by fact
show ?case
proof (cases assms)
assume not: "¬ assms"
show ?thesis
using ‹isOK (check_dp_termination_proof_main i dpp (Assume_Finite dpp' ass))›
by (simp, insert not, auto)
next
assume "assms"
have ok: "isOK (check_dp_termination_proof_main i dpp (Assume_Finite dpp' ass))" by fact
then have subsumes: "isOK (check_dpp_subsumes I dpp' dpp)" by simp
have "(try check_dpp_subsumes I dpp' dpp catch (λx. Inl (i ∘
shows '': error in finiteness assumption or unknown proof'' ∘ shows_nl ∘ x ∘
shows_nl))) = Inr ()" using subsumes by auto
note IH' = IH(1-4) [OF ‹assms› this]
from IH(6) ‹assms› have "holds (Finite_assm (map assm_proof_to_problem ass) dpp')" by auto
from this have *: "(⋀ x. x ∈ set ass ⟹ satisfied (assm_proof_to_problem x)) ⟹ finite_dpp (mk_dpp_set dpp')"
by auto
show ?thesis
proof (rule check_dpp_subsumes_sound [OF I subsumes *])
fix as
assume as: "as ∈ set ass"
then obtain j where asj: "as = ass ! j" and j: "j < length ass" unfolding set_conv_nth by auto
note IH' = IH'[OF as]
from IH(5)[simplified] asj j have ok:
"isOK (check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)" by auto
from IH(6) ‹assms› as have ass: "∀x∈set (collect_assms (sn_assms assms) (dp_assms assms) (sn_fp_assms assms) (unknown_assms assms) as). holds x"
by simp
show "satisfied (assm_proof_to_problem as)"
proof (rule check_assm[OF _ _ _ _ ok])
fix d p
show "as = Finite_assm_proof d p ⟹
isOK (check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_dpp I d) p) ⟹
finite_dpp (mk_dpp_set d)"
by (rule IH'(2)[folded mk_dpp_set, of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = SN_assm_proof t p ⟹
isOK (check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_tp J t) p) ⟹
SN_qrel (mk_tp_set t)"
by (rule IH'(1)[folded J.mk_tp_set, of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = SN_FP_assm_proof t p ⟹
isOK (check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
SN_fpstep (mk_fptp_set t)"
by (rule IH'(3)[of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = Unknown_assm_proof t p ⟹
isOK (check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
unknown_satisfied t"
by (rule IH'(4)[of _ p j], insert ass, auto simp: o_def)
qed
qed
qed
next
case (20 i dpp U st st' st'' lr p prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "rewriting_proc I U st st' st'' lr p dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF rewriting_proc[OF I] _ IH(1)], rule proc, unfold update_error_return, rule proc, rule rec, rule fin)
next
case (21 i dpp st p sts prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "narrowing_proc I st p sts dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF narrowing_proc[OF I] _ IH(1)],
rule proc, unfold update_error_return, rule proc, rule rec, rule fin)
next
case (22 i dpp st sts prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "instantiation_proc I st sts dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF instantiation_proc[OF I] _ IH(1)], rule proc,
unfold update_error_return, rule proc, rule rec, rule fin)
next
case (23 i dpp st sts u_opt prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "forward_instantiation_proc I st sts u_opt dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)"
by (auto simp: Let_def)
from IH have fin: "?P prof" by simp
show ?case
by (rule sound_proc_impl[OF forward_instantiation_proc[OF I] _ IH(1)], rule proc, unfold update_error_return,
rule proc, rule rec, rule fin)
next
case (24 i dpp P R prof)
thus ?case by simp
next
case (25 i dpp rp Ps Pb prof prfs)
note IH = this
interpret dpp_spec I by fact
let ?i1 = "i ∘ shows_string ''.1''"
let ?i2 = "i ∘ shows_string ''.2''"
note prems = IH(3)[simplified, unfolded Let_def check_def, simplified]
from prems obtain dpps
where proc: "conditional_general_reduction_pair_proc I (get_non_inf_order rp) Ps Pb prof (length prfs = 1) dpp = return dpps"
and len: "length prfs ≠ 0"
by auto
from len obtain p1 ps where prfs: "prfs = p1 # ps" by (cases prfs, auto)
from conditional_general_reduction_pair_proc_len[OF proc] have len: "length dpps = (if length prfs = 1 then 1 else 2)" .
from len obtain d1 ds where dpps: "dpps = d1 # ds" by (cases dpps, cases "length prfs = 1", auto)
from prems proc prfs dpps have ok1: "isOK(check_dp_termination_proof_main ?i1 (dpps ! 0) (prfs ! 0))" by simp
note IH1 = IH(1)[OF refl _ refl _ ok1, unfolded proc prfs]
from IH(4)[unfolded prfs] have ass1: "?P p1" by auto
show ?case
proof (rule conditional_general_reduction_pair_proc[OF I get_non_inf_order proc])
fix d
assume d: "d ∈ set dpps"
show "finite_dpp (dpp_ops.dpp I d)"
proof (cases "d = d1")
case True
hence d: "d = (dpps ! 0)" unfolding dpps by simp
show ?thesis unfolding d
by (rule IH1, insert proc ass1 prfs, auto simp: check_def)
next
case False
with d dpps have d: "d ∈ set ds" by auto
with len dpps prfs have dpps: "dpps = [d1,d]" by (cases ps, auto, cases ds, auto)
with len obtain p2 pps where prfs: "prfs = p1 # p2 # pps" unfolding prfs dpps by (cases ps, auto)
from dpps have d: "d = dpps ! 1" by simp
from prems proc prfs dpps have ok2: "isOK(check_dp_termination_proof_main ?i2 (dpps ! 1) (prfs ! 1))" by auto
from IH(4)[unfolded prfs] have ass2: "?P p2" by auto
show ?thesis unfolding d
by (rule IH(2)[OF refl _ refl _ _ _ ok2], insert proc prfs ok1 ass2 dpps, auto simp: check_def)
qed
qed
next
case (26 i dpp cprf prof)
note IH = this
interpret dpp_spec I by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain dpp'
where proc: "complex_constant_removal_proc I cprf dpp = return dpp'"
and rec: "isOK (check_dp_termination_proof_main ?i dpp' prof)" by auto
from IH have fin: "?P prof" by simp
from IH(1)[OF _ rec fin, simplified, OF proc] have "finite_dpp (dpp_ops.dpp I dpp')"
by simp
from sound_proc_impl[OF complex_constant_removal_proc[OF I] proc this] show ?case .
next
case (27 i dpp prof)
note IH = this
interpret tp_spec J by fact
interpret I: dpp_spec I by fact
from IH(2) have ok: "isOK (check_trs_termination_proof_main (i ∘ shows_string ''.1'')
(mk_tp J
(dpp_ops.nfs I dpp, dpp_ops.Q I dpp, dpp_ops.P I dpp @ dpp_ops.R I dpp, dpp_ops.Pw I dpp @ dpp_ops.Rw I dpp))
prof)" by auto
from IH(3) have "?Q prof" by simp
from IH(1)[OF ok this, unfolded SN_qrel_def]
have "SN_rel (qrstep (dpp_ops.nfs I dpp) (set (dpp_ops.Q I dpp)) (set (dpp_ops.P I dpp) ∪ set (dpp_ops.R I dpp)))
(qrstep (dpp_ops.nfs I dpp) (set (dpp_ops.Q I dpp)) (set (dpp_ops.Pw I dpp) ∪ set (dpp_ops.Rw I dpp)))"
by simp
from SN_rel_imp_finite_dpp[OF this]
show ?case unfolding I.dpp_sound .
next
case (28 i tp)
note IH = this
interpret tp_spec J by fact
from IH show ?case by (simp add: SN_qrel_def SN_rel_on_def)
next
case (29 i tp rp rR prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
let ?Rr = "ceta_list_diff (tp_ops.rules J tp) rR"
from IH(2) obtain tp' where
tt: "rule_removal_tt J (get_redtriple rp) ?Rr tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)" by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl [OF rule_removal_tt [OF get_redtriple], OF tt])
apply (rule IH(1) [OF refl refl _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (30 i tp nfs m P prof)
note IH = this
let ?i = "i ∘ shows_string ''.1''"
from IH obtain dpp where
tt: "dependency_pairs_tt Sharp J I tp nfs m P = return dpp"
and rec: "isOK (check_dp_termination_proof_main ?i dpp prof)" by auto
from IH have fin: "?P prof" by simp
show ?case
apply (rule dependency_pairs_tt [OF J I tt])
apply (rule IH(1)[OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (31 i tp prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain tp' where tt: "string_reversal_tt J tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)"
by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl [OF string_reversal_tt tt])
apply (rule IH(1) [OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (32 i tp p prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain tp' where tt: "const_to_string_sound_tt p J tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)"
by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl [OF const_to_string_sound_tt tt])
apply (rule IH(1) [OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (33 i tp sli lQ lAll prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH obtain tp' where
tt: "semlab_fin_tt J sli lQ lAll tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)"
by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl)
apply (rule semlab_fin_tt)
apply fact
apply (rule tt)
apply (rule IH(1) [OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (34 i tp info)
hence tt: "isOK (bounds_tt J info tp)"
by (auto simp: Let_def)
show ?case
by (rule bounds_tt [OF J tt infinite_lab])
next
case (35 i tp mode info prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain tp' where
tt: "uncurry_tt J mode info tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)"
by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl)
apply (rule uncurry_tt)
apply (fact)
apply (rule tt)
apply (rule IH(1) [OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (36 i tp fcs R' prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain tp' where tt: "fcc_tt J fcs R' tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)" by auto
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl)
apply (rule fcc_tt)
apply (rule tt)
apply (rule IH(1) [OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (37 i tp R' prof1 prof2)
note IH = this
interpret tp_spec J by fact
let ?i = "λs. i ∘ shows_string s"
let ?i1 = "?i ''.1''"
let ?i2 = "?i ''.2''"
obtain tp1 tp2 where s: "split_tt J tp R' = (tp1, tp2)" by force
from IH(3) s have ok1: "isOK (check_trs_termination_proof_main ?i1 tp1 prof1)"
and ok2: "isOK (check_trs_termination_proof_main ?i2 tp2 prof2)" by auto
from IH(4) have fin1: "?Q prof1" and fin2: "?Q prof2" by simp_all
show ?case
apply (rule split_tt)
apply (rule s)
apply (rule IH(1) [OF _ refl ok1 fin1])
apply (rule s [symmetric])
apply (rule IH(2) [OF _ refl _ ok2 fin2])
apply (rule s [symmetric])
apply (unfold update_error_return)
using ok1
apply auto
done
next
case (38 i tp joins prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain tp' where
tt: "switch_innermost_tt J joins tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)"
by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
apply (rule sound_tt_impl)
apply (rule switch_innermost_tt [OF J])
apply (rule infinite_lab)
apply (rule tt)
apply (rule IH(1) [OF _ rec fin])
apply (unfold update_error_return)
apply (rule tt)
done
next
case (39 i tp prof)
note IH = this
interpret tp_spec J by fact
let ?Rw = "filter (λ (l,r). l ≠ r) (Rw tp)"
let ?Rw' = "filter (λ (l,r). l = r) (Rw tp)"
let ?nfs = "NFS tp"
let ?tp = "mk ?nfs (Q tp) (R tp) ?Rw"
let ?i = "i ∘ shows_string ''.1''"
from IH(3) have fin: "?Q prof" by simp
from IH(2) have ok: "isOK (check_trs_termination_proof_main ?i ?tp prof)" by auto
have SN: "SN_qrel (qreltrs ?tp)"
apply (rule IH(1) [OF _ ok fin])
apply simp_all
done
let ?Q = "qrstep ?nfs (set (Q tp))"
let ?QR = "?Q (set (R tp))"
let ?QRw = "?Q (set (Rw tp))"
let ?QRw' = "?Q (set ?Rw)"
note d = qreltrs_sound SN_qrel_def mk_simps split
from SN [unfolded d] have "SN_rel ?QR ?QRw'" .
hence SN: "SN_rel ?QR (?QRw'^=)" unfolding SN_rel_Id .
have id: "set (Rw tp) = set ?Rw ∪ set ?Rw'" by auto
show "SN_qrel (qreltrs tp)" unfolding d
proof (rule SN_rel_mono [OF subset_refl _ SN], unfold id qrstep_union, rule Un_mono [OF subset_refl])
have "?Q (set ?Rw') ⊆ ?Q Id" by (rule qrstep_mono, auto)
also have "... ⊆ Id" by (rule qrstep_Id)
finally show "?Q (set ?Rw') ⊆ Id" .
qed
next
case (40 i tp Rdelete prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
let ?R = "delete_rules tp Rdelete"
from IH(2) have ok: "isOK (check_non_applicable_rules (λt. t ∈ NF_terms (set (Q tp))) Rdelete)"
and rec: "isOK (check_trs_termination_proof_main ?i ?R prof)" by auto
from IH(3) have fin: "?Q prof" by simp
from check_non_applicable_rules [OF refl ok]
have id: "⋀R. qrstep (NFS tp) (set (Q tp)) (R - set Rdelete) = qrstep (NFS tp) (set (Q tp)) R" .
have "SN_qrel (tp_ops.qreltrs J
(tp_ops.delete_R_Rw J tp Rdelete
Rdelete))"
apply (rule IH(1) [OF _ _ refl rec fin])
using ok by auto
then show ?case
by (simp add: id SN_qrel_def)
next
case (41 i tp pi prof)
note IH = this
interpret tp_spec J by fact
let ?i = "i ∘ shows_string ''.1''"
from IH(2) obtain tp' where
tt: "argument_filter_tt J pi tp = return tp'"
and rec: "isOK (check_trs_termination_proof_main ?i tp' prof)"
by (auto simp: Let_def)
from IH(3) have fin: "?Q prof" by simp
show ?case
by (rule sound_tt_impl[OF argument_filter_tt[OF J] tt IH(1)[OF _ rec fin]], insert tt, auto)
next
case (42 i tp tp' ass)
note IH = this
interpret J: tp_spec J by fact
interpret dpp_spec I by fact
show ?case
proof (cases assms)
assume False: "¬ assms"
show ?thesis using IH(5) by (simp, insert False, auto)
next
assume "assms"
have ok: "isOK (check_trs_termination_proof_main i tp (Assume_SN tp' ass))" by fact
then have subsumes: "isOK (check_tp_subsumes J tp' tp)" by simp
have "(try check_tp_subsumes J tp' tp catch (λx. Inl (i ∘
shows '': error in termination assumption or unknown proof'' ∘ shows_nl ∘ x ∘
shows_nl))) = Inr ()" using subsumes by auto
note IH' = IH(1-4)[OF ‹assms› this]
from IH(6) ‹assms› have "holds (SN_assm (map assm_proof_to_problem ass) tp')" by auto
from this have *: "(⋀ x. x ∈ set ass ⟹ satisfied (assm_proof_to_problem x)) ⟹ SN_qrel (mk_tp_set tp')"
by auto
show ?thesis
proof (rule check_tp_subsumes_sound [OF J subsumes *])
fix as
assume as: "as ∈ set ass"
then obtain j where asj: "as = ass ! j" and j: "j < length ass" unfolding set_conv_nth by auto
note IH' = IH'[OF as]
from IH(5)[simplified] asj j have ok:
"isOK (check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)" by auto
from IH(6) ‹assms› as have ass: "∀x∈set (collect_assms (sn_assms assms) (dp_assms assms) (sn_fp_assms assms) (unknown_assms assms) as). holds x"
by simp
show "satisfied (assm_proof_to_problem as)"
proof (rule check_assm[OF _ _ _ _ ok])
fix d p
show "as = Finite_assm_proof d p ⟹
isOK (check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_dpp I d) p) ⟹
finite_dpp (mk_dpp_set d)"
by (rule IH'(2)[folded mk_dpp_set, of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = SN_assm_proof t p ⟹
isOK (check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_tp J t) p) ⟹
SN_qrel (mk_tp_set t)"
by (rule IH'(1)[folded J.mk_tp_set, of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = SN_FP_assm_proof t p ⟹
isOK (check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
SN_fpstep (mk_fptp_set t)"
by (rule IH'(3)[of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = Unknown_assm_proof t p ⟹
isOK (check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
unknown_satisfied t"
by (rule IH'(4)[of _ p j], insert ass, auto simp: o_def)
qed
qed
qed
next
case (43 i tp tp' ass)
note IH = this
interpret J: tp_spec J by fact
interpret dpp_spec I by fact
show ?case
proof (cases assms)
assume False: "¬ assms"
show ?thesis using IH(5) by (simp, insert False, auto)
next
assume "assms"
have ok: "isOK (check_fptrs_termination_proof_main i tp (Assume_FP_SN tp' ass))" by fact
then have subsumes: "tp = tp'" by simp
have "check (tp = tp') (shows ''outermost assumption does not match current goal'') = Inr ()" using subsumes
by (auto simp: check_def)
note IH' = IH(1-4)[OF ‹assms› this]
from IH(6) ‹assms› have "holds (SN_FP_assm (map assm_proof_to_problem ass) tp')" by auto
from this have *: "(⋀ x. x ∈ set ass ⟹ satisfied (assm_proof_to_problem x)) ⟹ SN_fpstep (mk_fptp_set tp')"
by auto
show ?thesis unfolding subsumes
proof (rule *)
fix as
assume as: "as ∈ set ass"
then obtain j where asj: "as = ass ! j" and j: "j < length ass" unfolding set_conv_nth by auto
note IH' = IH'[OF as]
from IH(5)[simplified] asj j have ok:
"isOK (check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)" by auto
from IH(6) ‹assms› as have ass: "∀x∈set (collect_assms (sn_assms assms) (dp_assms assms) (sn_fp_assms assms) (unknown_assms assms) as). holds x"
by simp
show "satisfied (assm_proof_to_problem as)"
proof (rule check_assm[OF _ _ _ _ ok])
fix d p
show "as = Finite_assm_proof d p ⟹
isOK (check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_dpp I d) p) ⟹
finite_dpp (mk_dpp_set d)"
by (rule IH'(2)[folded mk_dpp_set, of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = SN_assm_proof t p ⟹
isOK (check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_tp J t) p) ⟹
SN_qrel (mk_tp_set t)"
by (rule IH'(1)[folded J.mk_tp_set, of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = SN_FP_assm_proof t p ⟹
isOK (check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
SN_fpstep (mk_fptp_set t)"
by (rule IH'(3)[of _ p j], insert ass, auto simp: o_def)
next
fix t p
show "as = Unknown_assm_proof t p ⟹
isOK (check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
unknown_satisfied t"
by (rule IH'(4)[of _ p j], insert ass, auto simp: o_def)
qed
qed
qed
next
case (44 i tp tp' ass)
note IH = this
interpret J: tp_spec J by fact
interpret dpp_spec I by fact
show ?case
proof (cases assms)
assume "¬ assms"
show ?thesis using IH(5) by (simp, insert ‹¬ assms›, auto)
next
assume assms
have ok: "isOK (check_unknown_proof_main i tp (Assume_Unknown tp' ass))" by fact
hence tp: "tp = tp'" by auto
note IH' = IH(1-4)[OF ‹assms›, unfolded tp]
from IH(6) ‹assms› have "holds (Unknown_assm (map assm_proof_to_problem ass) tp')" by auto
from this have *: "(⋀ x. x ∈ set ass ⟹ satisfied (assm_proof_to_problem x)) ⟹ unknown_satisfied tp'"
by auto
show ?thesis unfolding tp
proof (rule *)
fix as
assume as: "as ∈ set ass"
then obtain j where asj: "as = ass ! j" and j: "j < length ass" unfolding set_conv_nth by auto
note IH' = IH'[OF _ as]
from IH(5)[simplified] asj j have ok:
"isOK (check_assm
(check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
(check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)))
as)" by auto
from IH(6) ‹assms› as have ass: "∀x∈set (collect_assms (sn_assms assms) (dp_assms assms) (sn_fp_assms assms) (unknown_assms assms) as). holds x"
by simp
show "satisfied (assm_proof_to_problem as)"
proof (rule check_assm[OF _ _ _ _ ok])
fix d p
show "as = Finite_assm_proof d p ⟹
isOK (check_dp_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_dpp I d) p) ⟹
finite_dpp (mk_dpp_set d)"
by (rule IH'(2)[folded mk_dpp_set, of _ _ p j], insert ass, auto simp: o_def check_def)
next
fix t p
show "as = SN_assm_proof t p ⟹
isOK (check_trs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) (mk_tp J t) p) ⟹
SN_qrel (mk_tp_set t)"
by (rule IH'(1)[folded J.mk_tp_set, of _ _ p j], insert ass, auto simp: o_def check_def)
next
fix t p
show "as = SN_FP_assm_proof t p ⟹
isOK (check_fptrs_termination_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
SN_fpstep (mk_fptp_set t)"
by (rule IH'(3)[of _ _ p j], insert ass, auto simp: o_def check_def)
next
fix t p
show "as = Unknown_assm_proof t p ⟹
isOK (check_unknown_proof_main (i ∘ shows ''.'' ∘ shows (Suc j)) t p) ⟹
unknown_satisfied t"
by (rule IH'(4)[of _ _ p j], insert ass, auto simp: o_def check_def)
qed
qed
qed
qed
end
fun update where "update p_to_p (p, info) = (p_to_p p, info)"
definition "no_decr ≡ filter (λ(l, r). ¬ (l ≠ r ∧ map_funs_term unlab l = map_funs_term unlab r))"
definition "unlab_of_trs r ≡ unlab_rules (no_decr r)"
fun map_assm_proof :: "('tp ⇒ 'tp) ⇒ ('dpp ⇒ 'dpp) ⇒ ('fptp ⇒ 'fptp) ⇒ ('unk ⇒ 'unk) ⇒
('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof ⇒ ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof" where
"map_assm_proof tp dpp fptp unk (SN_assm_proof R p) = SN_assm_proof R (tp p)"
| "map_assm_proof tp dpp fptp unk (Finite_assm_proof d p) = Finite_assm_proof d (dpp p)"
| "map_assm_proof tp dpp fptp unk (SN_FP_assm_proof R p) = SN_FP_assm_proof R (fptp p)"
| "map_assm_proof tp dpp fptp unk (Unknown_assm_proof u p) = Unknown_assm_proof u (unk p)"
| "map_assm_proof tp dpp fptp unk x = x"
lemma assm_proof_to_problem_unlab: "map assm_proof_to_problem
(map (map_assm_proof unlab_to_split_trs (fst ∘ unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) ps)
= map assm_proof_to_problem ps"
proof (induct ps)
case (Cons p ps)
thus ?case by (cases p, auto)
qed auto
lemma map_assm_proof_cong[fundef_cong]:
assumes
"⋀ t p. i = SN_assm_proof t p ⟹ tp p = tp' p"
"⋀ t p. i = Finite_assm_proof t p ⟹ dpp p = dpp' p"
"⋀ t p. i = SN_FP_assm_proof t p ⟹ fptp p = fptp' p"
"⋀ t p. i = Unknown_assm_proof t p ⟹ unk p = unk' p"
shows "map_assm_proof tp dpp fptp unk i = map_assm_proof tp' dpp' fptp' unk' i"
using assms by (cases i, auto)
fun unlab_to_split_dp :: "('f :: key, 'l :: key, 'v :: key) dp_termination_proof ⇒ ('f, 'l, 'v) dp_termination_proof × (('f,'l,'v)trsLL × ('f,'l,'v)trsLL × ('f,'l,'v) dp_termination_proof) list"
and unlab_to_split_trs :: "('f :: key, 'l :: key, 'v :: key) trs_termination_proof ⇒ ('f, 'l, 'v) trs_termination_proof"
and unlab_to_split_otrs :: "('f :: key, 'l :: key, 'v :: key) fptrs_termination_proof ⇒ ('f, 'l, 'v) fptrs_termination_proof"
and unlab_to_split_unknown :: "('f :: key, 'l :: key, 'v :: key) unknown_proof ⇒ ('f, 'l, 'v) unknown_proof" where
"unlab_to_split_dp P_is_Empty = (P_is_Empty,[])"
| "unlab_to_split_dp (Dep_Graph_Proc ps) = (Dep_Graph_Proc
(map (λ (po,P). (map_option (fst o unlab_to_split_dp) po,P)) ps), [])"
| "unlab_to_split_dp (Subterm_Criterion_Proc a1 a2 a3 p) = update (Subterm_Criterion_Proc a1 a2 a3) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Gen_Subterm_Criterion_Proc a1 a2 p) = update (Gen_Subterm_Criterion_Proc a1 a2) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Redpair_Proc a1 a2 p) = update (Redpair_Proc a1 a2) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Redpair_UR_Proc a1 a2 a3 p) = update (Redpair_UR_Proc a1 a2 a3) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Usable_Rules_Proc a1 p) = update (Usable_Rules_Proc a1) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Q_Reduction_Proc a1 p) = update (Q_Reduction_Proc a1) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Mono_Redpair_Proc a1 a2 a3 p) = update (Mono_Redpair_Proc a1 a2 a3) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Mono_URM_Redpair_Proc a1 a2 a3 p) = update (Mono_URM_Redpair_Proc a1 a2 a3) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Mono_Redpair_UR_Proc a1 a2 a3 a4 p) = update (Mono_Redpair_UR_Proc a1 a2 a3 a4) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Size_Change_Subterm_Proc a1) = (Size_Change_Subterm_Proc a1, [])"
| "unlab_to_split_dp (Size_Change_Redpair_Proc a1 a2 a3) = (Size_Change_Redpair_Proc a1 a2 a3, [])"
| "unlab_to_split_dp (Uncurry_Proc a1 a2 a3 a4 p) = update (Uncurry_Proc a1 a2 a3 a4) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Fcc_Proc a1 a2 a3 a4 p) = update (Fcc_Proc a1 a2 a3 a4) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Switch_Innermost_Proc a1 p) = update (Switch_Innermost_Proc a1) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Rewriting_Proc a1 a2 a3 a4 a5 a6 p) = update (Rewriting_Proc a1 a2 a3 a4 a5 a6) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Narrowing_Proc a1 a2 a3 p) = update (Narrowing_Proc a1 a2 a3) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Instantiation_Proc a1 a2 p) = update (Instantiation_Proc a1 a2) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Forward_Instantiation_Proc a1 a2 a3 p) = update (Forward_Instantiation_Proc a1 a2 a3) (unlab_to_split_dp p)"
| "unlab_to_split_dp (Assume_Finite d p) = (Assume_Finite d (map (map_assm_proof unlab_to_split_trs (fst o unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) p), [])"
| "unlab_to_split_dp (To_Trs_Proc p) = (To_Trs_Proc (unlab_to_split_trs p), [])"
| "unlab_to_split_dp (Unlab_Proc P R p) = (case unlab_to_split_dp p of
(p,list) ⇒ (P_is_Empty,(P,R,p) # list))"
| "unlab_to_split_dp (Split_Proc a1 a2 p q) = (Split_Proc a1 a2 (fst (unlab_to_split_dp p)) (fst (unlab_to_split_dp q)), [])"
| "unlab_to_split_dp (Semlab_Proc a1 lP a2 lR p) = (
case unlab_to_split_dp p of
(p,list) ⇒ (let sl = Semlab_Proc a1 lP a2 lR p
in case list of
Nil ⇒ (sl,list)
| Cons (P,R,prof) list' ⇒
(let ulP = unlab_of_trs lP; ulR = unlab_of_trs lR; PR = ceta_list_diff ulP P; RR = ceta_list_diff ulR R
in (Split_Proc PR RR sl prof,list')))
)"
| "unlab_to_split_dp (General_Redpair_Proc a1 a2 a3 a4 ps) = (General_Redpair_Proc a1 a2 a3 a4 ps, [])"
| "unlab_to_split_dp (Complex_Constant_Removal_Proc a1 p) = update (Complex_Constant_Removal_Proc a1) (unlab_to_split_dp p)"
| "unlab_to_split_trs (DP_Trans a1 a2 a3 p) = (DP_Trans a1 a2 a3 (fst (unlab_to_split_dp p)))"
| "unlab_to_split_trs (Rule_Removal a1 a2 p) = (Rule_Removal a1 a2 (unlab_to_split_trs p))"
| "unlab_to_split_trs (String_Reversal p) = (String_Reversal (unlab_to_split_trs p))"
| "unlab_to_split_trs (Constant_String a1 p) = (Constant_String a1 (unlab_to_split_trs p))"
| "unlab_to_split_trs (Bounds a) = (Bounds a)"
| "unlab_to_split_trs (Uncurry a1 a2 p) = (Uncurry a1 a2 (unlab_to_split_trs p))"
| "unlab_to_split_trs (Semlab a1 a2 a3 p) = (Semlab a1 a2 a3 (unlab_to_split_trs p))"
| "unlab_to_split_trs R_is_Empty = R_is_Empty"
| "unlab_to_split_trs (Fcc a1 a2 p) = (Fcc a1 a2 (unlab_to_split_trs p))"
| "unlab_to_split_trs (Split a1 p q) = (Split a1 (unlab_to_split_trs p) (unlab_to_split_trs q))"
| "unlab_to_split_trs (Switch_Innermost a1 p) = (Switch_Innermost a1 (unlab_to_split_trs p))"
| "unlab_to_split_trs (Drop_Equality p) = (Drop_Equality (unlab_to_split_trs p))"
| "unlab_to_split_trs (Remove_Nonapplicable_Rules a1 p) = (Remove_Nonapplicable_Rules a1 (unlab_to_split_trs p))"
| "unlab_to_split_trs (Permuting_AFS a1 p) = (Permuting_AFS a1 (unlab_to_split_trs p))"
| "unlab_to_split_trs (Assume_SN a p) = (Assume_SN a
(map (map_assm_proof unlab_to_split_trs (fst o unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) p))"
| "unlab_to_split_otrs (Assume_FP_SN a p) = (Assume_FP_SN a
(map (map_assm_proof unlab_to_split_trs (fst o unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) p))"
| "unlab_to_split_unknown (Assume_Unknown a1 p) = (Assume_Unknown a1
(map (map_assm_proof unlab_to_split_trs (fst o unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) p))"
lemma unlab_to_split_dp_assms:
fixes "prf" :: "('f :: key, 'l :: key, 'v :: key) dp_termination_proof"
and prf' :: "('f :: key, 'l :: key, 'v :: key) trs_termination_proof"
and prf'' :: "('f :: key, 'l :: key, 'v :: key) fptrs_termination_proof"
and prf''' :: "('f :: key, 'l :: key, 'v :: key) unknown_proof"
shows "set (dp_assms a (fst (unlab_to_split_dp prf)))
∪ (⋃(set (map (λ (_,_,p). set (dp_assms a p)) (snd (unlab_to_split_dp prf))))) ⊆ set (dp_assms a prf)"
"set (sn_assms a (unlab_to_split_trs prf')) ⊆ set (sn_assms a prf')"
"set (sn_fp_assms a (unlab_to_split_otrs prf'')) ⊆ set (sn_fp_assms a prf'')"
"set (unknown_assms a (unlab_to_split_unknown prf''')) ⊆ set (unknown_assms a prf''')"
proof (induct "prf" and prf' and prf'' and prf''' rule:
unlab_to_split_dp_unlab_to_split_trs_unlab_to_split_otrs_unlab_to_split_unknown.induct)
case (2 ps)
note IH = this
let ?a = "dp_assms a"
let ?ap = "λ p. set (?a p)"
let ?aps = "λ pl. ?ap (fst pl) ∪ ⋃(set (map (λ (_,_,p). ?ap p) (snd pl)))"
let ?m = "(λ(po,y). (map_option (fst o unlab_to_split_dp) po,y))"
let ?ps = "map ?m ps"
let ?f = "(λ(po,y). ⋃ (?ap ` set_option po))"
have "?aps (unlab_to_split_dp (Dep_Graph_Proc ps)) = ?ap (Dep_Graph_Proc ?ps)" by simp
also have "... = ⋃ (set (map ?f ?ps))"
by force
also have "... ⊆ ⋃ (set (map ?f ps))"
proof(rule subsetI)
fix r
assume "r ∈ ⋃ (set (map ?f ?ps))"
then obtain x where r: "r ∈ ?f x" and "x ∈ set ?ps" by force+
then obtain y where x: "x = ?m y" and mem: "y ∈ set ps" by auto
obtain y1 y2 where y: "y = (y1,y2)" by force
note x = x[unfolded y split]
have "?f x ⊆ ?f y" unfolding y x split using IH[OF mem y[symmetric]]
by (cases y1, auto)
with mem have "?f x ⊆ ⋃ (set (map ?f ps))" by auto
with r show "r ∈ ⋃ (set (map ?f ps))" by blast
qed
also have "... = ?ap (Dep_Graph_Proc ps)" by force
finally show ?case by auto
next
case (3 a1 a2 a3 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (4 a1 a2 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (5 a1 a2 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (6 a1 a2 a3 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (7 a1 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (8 a1 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (9 a1 a2 a3 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (10 a1 a2 a3 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (11 a1 a2 a3 a4 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (14 a1 a2 a3 a4 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (15 a1 a2 a3 a4 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (16 a1 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (17 a1 a2 a3 a4 a5 a6 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (18 a1 a2 a3 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (19 a1 a2 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (20 a1 a2 a3 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (21 a1 ps)
note IH = this
have IH: "set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a))
(map (map_assm_proof unlab_to_split_trs (fst ∘ unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) ps)))
⊆ set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) ps))" (is "?P ps")
using IH
proof (induct ps)
case (Cons p ps)
have "p ∈ set (p # ps)" by auto
note IH = Cons(2-5)[OF this]
have ps: "?P ps"
by (rule Cons(1)[OF Cons(2-5)], auto)
have p: "?P [p]"
by (cases p, insert IH(1-4), auto)
from p ps show ?case by auto
qed auto
show ?case
unfolding unlab_to_split_dp.simps fst_conv dp_assms.simps
unfolding assm_proof_to_problem_unlab
using IH by auto
next
case (23 a1 a2 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (24 a1 a2 p q)
thus ?case by (cases "unlab_to_split_dp p", cases "unlab_to_split_dp q", auto)
next
case (25 a1 lP a2 lR p)
note IH = this
obtain p' list where up: "unlab_to_split_dp p = (p',list)" by force
show ?case
proof (cases list)
case Nil
show ?thesis using IH
unfolding unlab_to_split_dp.simps up fst_conv snd_conv split Let_def Nil
by auto
next
case (Cons prP list')
obtain P R p'' where prP: "prP = (P,R,p'')" by (cases prP, auto)
show ?thesis using IH
unfolding unlab_to_split_dp.simps up fst_conv snd_conv split Let_def Cons prP list.simps
unfolding dp_assms.simps
by auto
qed
next
case (27 a1 p)
thus ?case by (cases "unlab_to_split_dp p", auto)
next
case (42 a1 ps)
note IH = this
have IH: "set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a))
(map (map_assm_proof unlab_to_split_trs (fst ∘ unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) ps)))
⊆ set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) ps))" (is "?P ps")
using IH
proof (induct ps)
case (Cons p ps)
have "p ∈ set (p # ps)" by auto
note IH = Cons(2-5)[OF this]
have ps: "?P ps"
by (rule Cons(1)[OF Cons(2-5)], auto)
have p: "?P [p]"
by (cases p, insert IH, auto)
from p ps show ?case by auto
qed auto
show ?case
unfolding unlab_to_split_trs.simps fst_conv sn_assms.simps
unfolding assm_proof_to_problem_unlab
using IH by auto
next
case (43 a1 ps)
note IH = this
have IH: "set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a))
(map (map_assm_proof unlab_to_split_trs (fst ∘ unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) ps)))
⊆ set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) ps))" (is "?P ps")
using IH
proof (induct ps)
case (Cons p ps)
have "p ∈ set (p # ps)" by auto
note IH = Cons(2-5)[OF this]
have ps: "?P ps"
by (rule Cons(1)[OF Cons(2-5)], auto)
have p: "?P [p]"
by (cases p, insert IH, auto)
from p ps show ?case by auto
qed auto
show ?case
unfolding unlab_to_split_otrs.simps fst_conv sn_fp_assms.simps
unfolding assm_proof_to_problem_unlab
using IH by auto
next
case (44 a1 ps)
note IH = this
have IH: "set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a))
(map (map_assm_proof unlab_to_split_trs (fst ∘ unlab_to_split_dp) unlab_to_split_otrs unlab_to_split_unknown) ps)))
⊆ set (concat (map (collect_assms (sn_assms a) (dp_assms a) (sn_fp_assms a) (unknown_assms a)) ps))" (is "?P ps")
using IH
proof (induct ps)
case (Cons p ps)
have "p ∈ set (p # ps)" by auto
note IH = Cons(2-5)[OF this]
have ps: "?P ps"
by (rule Cons(1)[OF Cons(2-5)], auto)
have p: "?P [p]"
by (cases p, insert IH, auto)
from p ps show ?case by auto
qed auto
show ?case
unfolding unlab_to_split_unknown.simps fst_conv unknown_assms.simps
unfolding assm_proof_to_problem_unlab
using IH by auto
qed auto
hide_const Check_Termination.update
definition "check_dp_termination_proof I J a i dpp prf
≡ check_dp_termination_proof_main I J a i dpp (fst (unlab_to_split_dp prf))"
definition "check_trs_termination_proof I J a i tp prf
≡ check_trs_termination_proof_main I J a i tp (unlab_to_split_trs prf)"
definition "check_fptrs_termination_proof I J a i tp prf
≡ check_fptrs_termination_proof_main I J a i tp (unlab_to_split_otrs prf)"
definition "check_unknown_proof I J a i u prf
≡ check_unknown_proof_main I J a i u (unlab_to_split_unknown prf)"
lemma check_dp_termination_proof_with_assms:
assumes I: "tp_spec I" and J: "dpp_spec J"
and ok: "isOK (check_dp_termination_proof I J a i dpp prf)"
and ass: "∀assm∈set (dp_assms a prf). holds assm"
shows "finite_dpp (dpp_ops.dpp J dpp)"
by (rule check_dp_trs_unknown_termination_proof_main_with_assms(1)[OF J I
ok[unfolded check_dp_termination_proof_def]],
insert ass unlab_to_split_dp_assms(1), auto)
lemma check_dp_termination_proof:
assumes "tp_spec I" and "dpp_spec J"
and "isOK (check_dp_termination_proof I J False i dpp prf)"
shows "finite_dpp (dpp_ops.dpp J dpp)"
using check_dp_termination_proof_with_assms[OF assms] by simp
lemma check_trs_termination_proof_with_assms:
assumes I: "tp_spec I" and J: "dpp_spec J"
and ok: "isOK (check_trs_termination_proof I J a i tp prf)"
and ass: "∀assm∈set (sn_assms a prf). holds assm"
shows "SN_qrel (tp_ops.qreltrs I tp)"
by (rule check_dp_trs_unknown_termination_proof_main_with_assms(2)[OF J I
ok[unfolded check_trs_termination_proof_def]],
insert ass unlab_to_split_dp_assms(2), auto)
lemma check_trs_termination_proof:
assumes "tp_spec I" and "dpp_spec J"
and "isOK (check_trs_termination_proof I J False i tp prf)"
shows "SN_qrel (tp_ops.qreltrs I tp)"
using check_trs_termination_proof_with_assms[OF assms] by simp
lemma check_fptrs_termination_proof_with_assms:
assumes I: "tp_spec I" and J: "dpp_spec J"
and ok: "isOK (check_fptrs_termination_proof I J a i tp prf)"
and ass: "∀assm∈set (sn_fp_assms a prf). holds assm"
shows "SN_fpstep (mk_fptp_set tp)"
by (rule check_dp_trs_unknown_termination_proof_main_with_assms(3)[OF J I
ok[unfolded check_fptrs_termination_proof_def]],
insert ass unlab_to_split_dp_assms(3), auto)
lemma check_fptrs_termination_proof:
assumes "tp_spec I" and "dpp_spec J"
and "isOK (check_fptrs_termination_proof I J False i tp prf)"
shows "SN_fpstep (mk_fptp_set tp)"
using check_fptrs_termination_proof_with_assms[OF assms] by simp
lemma check_unknown_proof_with_assms:
assumes I: "tp_spec I" and J: "dpp_spec J"
and ok: "isOK (check_unknown_proof I J a i u prf)"
and ass: "∀assm∈set (unknown_assms a prf). holds assm"
shows "unknown_satisfied u"
by (rule check_dp_trs_unknown_termination_proof_main_with_assms(4)[OF J I
ok[unfolded check_unknown_proof_def]],
insert ass unlab_to_split_dp_assms(4), auto)
lemma check_unknown_proof:
assumes "tp_spec I" and "dpp_spec J"
and "isOK (check_unknown_proof I J False i u prf)"
shows "unknown_satisfied u"
using check_unknown_proof_with_assms[OF assms] by simp
end