theory Check_Completion_Proof
imports Check_Termination
begin
subsection ‹Proving completion of TRSs›
type_synonym ('f, 'v) conversion = "('f, 'v) equation × ('f, 'v) eseq"
type_synonym ('f, 'v) subsumption_proof = "('f, 'v) conversion list"
datatype ('f, 'l, 'v) completion_proof =
SN_WCR_Eq
"('f, 'l) lab join_info"
"('f, 'l, 'v) trs_termination_proof"
"(('f, 'l) lab, 'v) subsumption_proof"
"(('f, 'l) lab, 'v) subsumption_proof option"
primrec
check_completion_proof ::
"bool ⇒ shows ⇒
('tp, ('f::{show,key,countable}, label_type) lab, string) tp_ops ⇒
('dpp, ('f, label_type) lab, string) dpp_ops ⇒ (('f, label_type) lab, string) equation list ⇒ (('f, label_type) lab, string) rules ⇒
('f, label_type, string) completion_proof ⇒
shows check"
where
"check_completion_proof a i I J E R (SN_WCR_Eq joins_i prf conv1 conv2) = debug (i []) ''SN_WCR_Eq'' (do {
let tp = tp_ops.mk I False [] R []; (*FIXME: default value*)
check_trs_termination_proof I J a (i ∘ shows_string ''.1'') tp prf
<+? (λs. i ∘ shows '': error below strong normalization + wcr'' ∘ shows_nl ∘ indent s);
check_subsumption_guided R E conv1
<+? (λ s. i ∘ shows '': error when showing that rewrite relation can be simulated by equations'' ∘ shows_nl ∘ indent s);
check_subsumption E R conv2
<+? (λ s. i ∘ shows '': error when showing that equations can be simulated by rewrite system'' ∘ shows_nl ∘ indent s);
check_critical_pairs R (critical_pairs_impl R R) joins_i
<+? (λs. i ∘ shows '': error when proving local confluence of '' ∘ shows_nl ∘ shows_tp I tp ∘ shows_nl ∘ indent s)
})"
primrec completion_assms :: "bool ⇒ ('f, 'l, 'v) completion_proof ⇒ (('f, 'l, 'v) assm) list"
where
"completion_assms a (SN_WCR_Eq _ p _ _) = sn_assms a p"
lemma check_completion_proof_with_assms_sound:
assumes I: "tp_spec I" and J: "dpp_spec J"
and fin: "∀p∈set (completion_assms a prf). holds p"
and ok: "isOK (check_completion_proof a i I J E R prf)"
shows "completed_rewrite_system (set E) (set R)"
proof -
interpret tp_spec I by fact
from ok fin show ?thesis
proof (induct "prf" arbitrary: i)
case (SN_WCR_Eq joins_i prof c1 c2 i)
from SN_WCR_Eq(1)
have cp: "isOK (check_critical_pairs R (critical_pairs_impl R R) joins_i)"
and ok: "isOK (check_trs_termination_proof I J a (i ∘ shows_string ''.1'') (mk False [] R []) prof)"
and ok1: "isOK (check_subsumption_guided R E c1)"
and ok2: "isOK (check_subsumption E R c2)" by (auto simp: Let_def)
from SN_WCR_Eq(2) have a: "∀a∈set (sn_assms a prof). holds a" by auto
from check_critical_pairs[OF cp] have WCR: "WCR (rstep (set R))" .
from check_trs_termination_proof_with_assms[OF I J ok a] have SN: "SN (rstep (set R))" by simp
show ?case
by (rule completion_via_WCR_SN_simulation[OF check_subsumption_guided[OF ok1] check_subsumption[OF ok2] WCR SN])
qed
qed
lemma completion_assms_False[simp]: "completion_assms False prf = []"
by (induct "prf") simp_all
lemma check_completion_proof_sound:
assumes I: "tp_spec I" and J: "dpp_spec J"
and ok: "isOK (check_completion_proof False i I J E R prf)"
shows "completed_rewrite_system (set E) (set R)"
by (rule check_completion_proof_with_assms_sound[OF I J _ ok], simp)
datatype ('f, 'l, 'v) ordered_completion_proof = OKB "(('f, 'l) lab, 'v) oc_irule list"
primrec check_ordered_completion_proof ::
"bool ⇒ shows ⇒
('tp, ('f::{show,key}, label_type) lab, string) tp_ops ⇒
('dpp, ('f, label_type) lab, string) dpp_ops ⇒
(('f, label_type) lab, string) equation list ⇒ (('f, label_type) lab, string) equation list ⇒ (('f, label_type) lab, string) rules ⇒
('f, label_type) lab reduction_order_input ⇒ ('f, label_type, string) ordered_completion_proof ⇒
shows check"
where
"check_ordered_completion_proof a i I J E⇩0 E R ro (OKB steps) = debug (i []) ''OKB'' (do {
(case ro of
KBO_Input precw ⇒
let F = funas_trs_list E⇩0 in
check_FGCR_run (create_KBO_redord precw F) F E⇩0 [] E R steps
<+? (λs. i ∘ shows '': error in ground completeness proof '' ∘ shows_nl ∘ indent s)
| _ ⇒ error (shows_string ''unsupported reduction order ''))
})"
lemma check_ordered_completion_proof_sound:
assumes "isOK (check_ordered_completion_proof a i I J E⇩0 E R ro p)"
shows "ordered_completed_rewrite_system (set E⇩0) (set E) (set R) ro"
proof-
let ?F = "funas_trs_list E⇩0"
obtain steps where "p = OKB steps" by (cases p, auto)
note assms = assms [unfolded check_ordered_completion_proof_def this Let_def]
then obtain precw_w0 where ro: "ro = KBO_Input precw_w0" by (cases ro, auto)
obtain precw w0 where pw0: "precw_w0 = (precw, w0)" by (cases precw_w0, auto)
let ?pwfuns = "prec_weight_repr_to_prec_weight_funs precw_w0"
let ?pw = "prec_weight_repr_to_prec_weight precw_w0"
note assms = assms [unfolded ro]
then have run_ok: "isOK (check_FGCR_run (create_KBO_redord precw_w0 ?F) ?F E⇩0 [] E R steps)" by auto
then have FGCR: "isOK (check_FGCR (create_KBO_redord precw_w0 ?F) ?F E R)" by (auto simp: check_FGCR_run_def)
then have valid: "isOK (redord.valid (create_KBO_redord precw_w0 ?F))" by (auto simp: check_FGCR_def)
then obtain p w lcs scf where pwfuns: "?pwfuns = (p, w, w0, lcs, scf)"
unfolding pw0 prec_weight_repr_to_prec_weight_funs_def Let_def split by (cases ?pwfuns, simp)
obtain ok scf' where pw: "?pw = (ok, p, w, w0, lcs, scf_repr_to_scf scf)"
unfolding prec_weight_repr_to_prec_weight_def Let_def pwfuns unfolding pw0 split by (cases ?pw, simp)
note remember = KBO_redord.valid
let ?scf = "scf_repr_to_scf scf"
let ?less = "λs t. fst (kbo.kbo w w0 ?scf (λf. f ∈ set lcs) (λf g. fst (p f g)) (λf g. snd (p f g)) s t)"
have less: "redord.less (create_KBO_redord precw_w0 ?F) = ?less"
unfolding pw create_KBO_redord_def Let_def split by force
then have o: "ordstep (fun_to_rel (redord.less (create_KBO_redord precw_w0 ?F))) (set (Rules E R)) =
ordstep (fun_to_rel ?less) ((set E)⇧↔ ∪ set R)"
unfolding less Rules_def set_union set_sym_list Un_commute [of "set R"] by blast
from check_FGCR_run [OF run_ok] show ?thesis unfolding ordered_completed_rewrite_system_def ro o
using pw0 pwfuns pw by force
qed
end