theory Complex_Constant_Removal_Impl
imports
Complex_Constant_Removal
QTRS.QDP_Framework_Impl
"Check-NT.Critical_Pairs_Impl"
begin
definition extract_fresh_var :: "(('f,'v)rule × ('f,'v)rule)list ⇒ 'v result" where
"extract_fresh_var sts ≡ case (case sts of [] ⇒ None
| (_,(s,_)) # _ ⇒ (case s of Var _ ⇒ None
| Fun _ ss ⇒ if ss = [] then None else (case (last ss) of
Var x ⇒ Some x | _ ⇒ None))) of
None ⇒ error (shows ''could not extract fresh variable (as last argument from some lhs of new pairs)'')
| Some x ⇒ return x"
definition extract_ren :: "(('f,'v)rule × ('f,'v)rule)list ⇒
('f × nat ⇒ 'f) result" where
"extract_ren ps_ps' ≡ do {
check (∀ st_st' ∈ set ps_ps'. (λ ((s,t),(s',t')). is_Fun s ∧ is_Fun t ∧ is_Fun s' ∧ is_Fun t') st_st')
(shows ''all lhss and rhss of pairs must be non-variables'');
let rt = (λ t. the (root t));
let pair = (λ s s'. (rt s, fst (rt s')));
let pairs = (λ (st,st'). [pair (fst st) (fst st'), pair (snd st) (snd st')]);
let ren' = map_of (remdups (concat (map pairs ps_ps')));
let ren = (λ fn. case ren' fn of None ⇒ fst fn | Some f ⇒ f);
return ren
}"
definition check_drop :: "'v ⇒ ('f :: show,'v :: show)term ⇒ ('f × nat ⇒ 'f) ⇒ ('f,'v)rule × ('f,'v)rule ⇒ shows check" where
"check_drop x c ren st_st' ≡ case st_st' of ((s,t),(s',t')) ⇒ case s of Fun f ss ⇒ case t of Fun g ts ⇒ do {
check (s' = Fun (ren (f,length ss)) (ss @ [Var x]))
(shows ''could not relate '' +@+ shows s +@+ shows '' with '' +@+ shows s');
let ts'' = args t';
let ts' = take (length ts'' - 1) ts'';
check (t' = Fun (ren (g,length ts)) (ts' @ [Var x]) ∧ ts = map (λt. t ⋅ subst x c) ts')
(shows ''could not relate '' +@+ shows t +@+ shows '' with '' +@+ shows t')
}"
lemma check_drop: assumes "isOK (check_drop x c ren ((Fun f ss, Fun g ts), (s', t')))"
shows "∃ts'. s' = Fun (ren (f, length ss)) (ss @ [Var x]) ∧ t' = Fun (ren (g, length ts)) (ts' @ [Var x]) ∧
ts = map (λt. t ⋅ subst x c) ts'"
using assms unfolding check_drop_def by (auto simp: Let_def)
datatype ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof
"('f,'v)term"
"(('f,'v)rule × ('f,'v)rule) list"
primrec
complex_constant_removal_proc ::
"('dpp, 'f :: {key,show}, string) dpp_ops
⇒ ('f,string)complex_constant_removal_prf
⇒ 'dpp ⇒ 'dpp result"
where
"complex_constant_removal_proc I (Complex_Constant_Removal_Proof c ps) dpp =
do {
let p = dpp_ops.P I dpp;
let pw = dpp_ops.Pw I dpp;
let r = dpp_ops.Rw I dpp;
let q = dpp_ops.Q I dpp;
let pairs = dpp_ops.pairs I dpp;
x ← extract_fresh_var ps;
ren ← extract_ren ps;
let is_def = dpp_spec.is_defined I dpp;
let rQs = remdups (map root q);
check_allm (λ(s, t). do { (* require that pairs have standard structure *)
check_no_var s;
check_no_var t;
check_no_defined_root is_def t;
check (x ∉ set (vars_rule_list (s,t))) (shows x +@+ shows '' is not fresh for pair '' +@+ shows_rule (s,t));
let f = the (root s);
let f' = (ren f, Suc (snd f));
check (Some f' ∉ set rQs) (shows ''renaming delivers defined symbol of Q'');
check (¬ is_def f') (shows ''renaming delivers defined symbol of R'')
}) pairs;
let pps = filter (λ st_st'. fst st_st' ∈ set p) ps;
let pwps = filter (λ st_st'. fst st_st' ∈ set pw) ps;
check_allm (λ st. check (st ∈ set (map fst pps)) (shows ''could not find entry for pair '' +@+ shows_rule st)) p;
check_allm (λ st. check (st ∈ set (map fst pwps)) (shows ''could not find entry for pair '' +@+ shows_rule st)) pw;
check (ground c) (shows ''the term '' +@+ shows c +@+ shows '' is not ground'');
check (dpp_ops.NFQ_subset_NF_rules I dpp) (shows ''innermost required'');
check (dpp_ops.R I dpp = []) (shows ''strict rules not allowed'');
check (dpp_ops.rules_no_left_var I dpp) (shows ''rules may not have variables as lhss'');
(if is_NF_trs r c then succeed else check_critical_pairs_innermost r
<+? (λ s. shows ''could not ensure confluence'' +@+ shows_nl +@+ s));
check_allm (λ st_st'. check_drop x c ren st_st' <+? (λ s. shows ''problem in finding correspondence between rule ''
+@+ shows_rule (fst st_st') +@+ shows '' and rule '' +@+ shows_rule (snd st_st') +@+ shows_nl +@+ s)) ps;
return (dpp_ops.mk I (dpp_ops.nfs I dpp) (dpp_ops.minimal I dpp) (map snd pps) (map snd pwps) q [] r)
} <+? (λ s. shows ''problem in complex constant removal proc: '' +@+ shows_nl +@+ s)"
lemma complex_constant_removal_proc: assumes "dpp_spec I"
shows "dpp_spec.sound_proc_impl I (complex_constant_removal_proc I prf)"
proof -
interpret dpp_spec I by fact
note Let_def[simp]
show ?thesis
proof
fix d d'
assume res: "complex_constant_removal_proc I prf d = return d'" and fin: "finite_dpp (dpp d')"
obtain c ps where "prf = Complex_Constant_Removal_Proof c ps" by (cases "prf", auto)
note res = res[unfolded this, simplified]
let ?P = "set (P d)"
let ?Pw = "set (Pw d)"
let ?nfs = "NFS d"
let ?m = "M d"
let ?Q = "set (Q d)"
let ?R = "set (Rw d)"
from res obtain x where x: "extract_fresh_var ps = return x"
by (cases "extract_fresh_var ps", auto)
note res = res[unfolded x, simplified]
from res obtain ren where ren: "extract_ren ps = return ren"
by (cases "extract_ren ps", auto)
note res = res[unfolded ren, simplified]
from res have [simp]: "R d = []" by auto
note res = res[unfolded this, simplified]
from res have d: "dpp d = (?nfs,?m,?P,?Pw,?Q,{},?R)" unfolding dpp_sound by auto
let ?pss = "{ st_st'. st_st' ∈ set ps ∧ fst st_st' ∈ ?P}"
let ?psw = "{ st_st'. st_st' ∈ set ps ∧ fst st_st' ∈ ?Pw}"
from res have "d' = mk ?nfs ?m (map snd [st_st'←ps . fst st_st' ∈ set (P d)])
(map snd [st_st'←ps . fst st_st' ∈ set (Pw d)]) (Q d) [] (Rw d)" by simp
hence d': "dpp d' = (?nfs,?m,snd ` ?pss, snd ` ?psw, ?Q, {}, ?R)" by simp
from res have c: "ground c" by auto
from res have inn: "NF_terms ?Q ⊆ NF_trs ?R" by auto
from res have is_FunR: "⋀ l r. (l,r) ∈ ?R ⟹ is_Fun l" by auto
hence is_FunR': "∀(l,r) ∈ ?R. is_Fun l" by auto
from res have "c ∈ NF_trs ?R ∨ isOK(check_critical_pairs_innermost (Rw d))" by auto
with check_critical_pairs_innermost[OF _ inn is_FunR, of _ ?nfs]
have CR: "c ∈ NF_trs ?R ∨ CR (qrstep ?nfs ?Q ?R)" by force
from res have drop: "⋀ st_st'. st_st' ∈ set ps ⟹ isOK(check_drop x c ren st_st')" by auto
def rel ≡ "λ P P'. ∀ st ∈ P. ∃ st' ∈ P'. (st,st') ∈ set ps"
show "finite_dpp (dpp d)" unfolding d
proof (rule complex_constant_removal[OF fin[unfolded d'] CR inn c _ _ _ _ _ is_FunR'])
fix s t
assume st: "(s,t) ∈ ?P ∪ ?Pw"
show "x ∉ vars_rule (s,t)" using st res by auto
show "is_Fun s ∧ is_Fun t ∧ ¬ defined ?R (the (root t))" using st res by auto
next
fix f ss t
assume mem: "(Fun f ss, t) ∈ ?P ∪ ?Pw"
let ?s = "Fun f ss"
from mem res have ndef: "Some (ren (the (root ?s)), Suc (snd (the (root ?s)))) ∉ root ` ?Q ∧
¬ defined ?R (ren (the (root ?s)), Suc (snd (the (root ?s))))" by blast
show "Some (ren (f, length ss), Suc (length ss)) ∉ root ` ?Q" using ndef by simp
show "¬ defined ?R (ren (f, length ss), Suc (length ss))" using ndef by simp
next
from res have "(∀x∈ ?P. x ∈ fst ` {x ∈ set ps. fst x ∈ ?P})" by auto
thus "rel ?P (snd ` ?pss)" unfolding rel_def by force
from res have "(∀x∈ ?Pw. x ∈ fst ` {x ∈ set ps. fst x ∈ ?Pw})" by auto
thus "rel ?Pw (snd ` ?psw)" unfolding rel_def by force
next
fix P P' f ss g ts
assume rel: "rel P P'" and mem: "(Fun f ss, Fun g ts) ∈ P"
from rel[unfolded rel_def, rule_format, OF mem] obtain st' where
st': "st' ∈ P'" and mem: "((Fun f ss, Fun g ts), st') ∈ set ps" ..
obtain s' t' where id: "st' = (s',t')" by force
note st' = st'[unfolded id]
from drop[OF mem[unfolded id]] have cdrop: "isOK (check_drop x c ren ((Fun f ss, Fun g ts), s', t'))" .
from check_drop[OF cdrop] st'
show "∃ts'. (Fun (ren (f, length ss)) (ss @ [Var x]), Fun (ren (g, length ts)) (ts' @ [Var x])) ∈ P'
∧ ts = map (λt. t ⋅ subst x c) ts'" by auto
qed
qed
qed
end