theory Q_Relative_Rewriting
imports
Q_Restricted_Rewriting
begin
type_synonym ('f, 'v) qreltrs = "bool × ('f, 'v) terms × ('f, 'v) trs × ('f, 'v) trs"
abbreviation rel_qrstep :: "('f, 'v) qreltrs ⇒ ('f, 'v) term rel" where
"rel_qrstep ≡ λ(nfs,Q, R, S). relto (qrstep nfs Q R) (qrstep nfs Q S)"
abbreviation rel_rstep where "rel_rstep ≡ λ(R, S). rel_qrstep (False, {}, R, S)"
lemma ctxt_closed_rel_qrstep[intro] : "ctxt.closed (rel_qrstep QRS)"
by (cases QRS) auto
lemma subst_closed_rel_rstep : "subst.closed (rel_rstep RS)"
proof (cases RS)
case (Pair R S)
from subst.closed_rtrancl[OF subst_closed_rstep[of S]] have S: "subst.closed ((rstep S)^*)" .
from Pair subst.closed_comp[OF S subst.closed_comp[OF subst_closed_rstep[of R] S] ]
show ?thesis by simp
qed
lemma rel_qrstep_mono: "R ⊆ R' ⟹ S ⊆ S' ⟹ NF_terms Q ⊆ NF_terms Q' ⟹ rel_qrstep (nfs,Q,R,S) ⊆ rel_qrstep (nfs,Q',R',S')"
unfolding split by (rule relto_mono[OF qrstep_mono qrstep_mono]) auto
lemma rel_qrstep_Id: "rel_qrstep (nfs,Q, R, S ∪ Id) = rel_qrstep (nfs,Q, R, S)" (is "?L = ?R")
proof -
have "qrstep nfs Q (S^=) ⊆ (qrstep nfs Q S)^=" unfolding qrstep_union
using qrstep_Id[of nfs Q] by auto
from rtrancl_mono[OF this]
have "?L ⊆ relto (qrstep nfs Q R) ((qrstep nfs Q S)^=)" by auto
also have "... = ?R" unfolding relto_Id by simp
finally have "?L ⊆ ?R" .
moreover
have "?R ⊆ ?L" by (rule rel_qrstep_mono, auto)
ultimately show ?thesis by auto
qed
definition qrs_ideriv where
"qrs_ideriv nfs Q R S = (λ as. ideriv (qrstep nfs Q R) (qrstep nfs Q S) as)"
lemmas qrs_ideriv_defs = qrs_ideriv_def ideriv_def
lemma qrs_ideriv_mono:
assumes R: "R ⊆ R'"
and S: "S ⊆ S'"
and Q: "NF_terms Q ⊆ NF_terms Q'"
and ideriv: "qrs_ideriv nfs Q R S ts"
shows "qrs_ideriv nfs Q' R' S' ts"
unfolding qrs_ideriv_def
by (rule ideriv_mono[OF qrstep_mono[OF R Q] qrstep_mono[OF S Q] ideriv[unfolded qrs_ideriv_def]])
lemma qrs_ideriv_split:
assumes ideriv: "qrs_ideriv nfs Q R S as"
and nideriv: "¬ qrs_ideriv nfs Q (D ∩ (R ∪ S)) (R ∪ S - D) as" (is "¬ ?q")
shows "∃ i. qrs_ideriv nfs Q (R - D) (S - D) (shift as i)"
proof -
let ?D = "D ∩ (R ∪ S)"
let ?Q = "qrstep nfs Q"
let ?QD = "?Q ?D"
let ?QR = "?Q R"
let ?QS = "?Q S"
let ?QRS = "?Q (R ∪ S)"
have nideriv: "¬ ideriv (?QD ∩ ?QRS) (?QRS - ?QD) as" (is "¬ ?i")
proof
assume ?i
have ?q unfolding qrs_ideriv_def
proof (rule ideriv_mono[OF _ _ ‹?i›])
show "?Q (D ∩ (R ∪ S)) ∩ ?QRS ⊆ ?Q (D ∩ (R ∪ S))" by auto
next
{
fix s t
assume "(s,t) ∈ ?QRS" and "(s,t) ∉ ?QD"
then have "(s,t) ∈ ?Q (R ∪ S - D)" unfolding
qrstep_rule_conv[where R = "R ∪ S"]
qrstep_rule_conv[where R = ?D]
qrstep_rule_conv[where R = "R ∪ S - D"]
by auto
}
then show "?QRS - ?QD ⊆ ?Q (R ∪ S - D)" by auto
qed
with nideriv show False ..
qed
have "∃ i. ideriv (?QR - ?QD) (?QS - ?QD) (shift as i)"
by (rule ideriv_split[OF ideriv[unfolded qrs_ideriv_def] nideriv[unfolded qrstep_union]])
then obtain i where ideriv: "ideriv (?QR - ?QD) (?QS - ?QD) (shift as i)" ..
show ?thesis
by (rule exI[of _ i], unfold qrs_ideriv_def,
rule ideriv_mono[OF qrstep_diff qrstep_diff ideriv], auto)
qed
lemma rel_qrstep_SN: "SN_rel (qrstep nfs Q R) (qrstep nfs Q S) = (¬ (∃ ts. qrs_ideriv nfs Q R S ts))"
unfolding qrs_ideriv_def
by (rule SN_rel_ideriv)
definition rel_tt :: "(('f, 'v) qreltrs ⇒ ('f, 'v) qreltrs ⇒ bool) ⇒ bool" where
"rel_tt tt ⟷ (∀nfs Q R S rnfs rQ rR rS ts.
(tt (nfs,Q, R, S) (rnfs,rQ, rR, rS) ⟶ qrs_ideriv nfs Q R S ts ⟶
(∃ts'. qrs_ideriv rnfs rQ rR rS ts')))"
definition SN_qrel :: "('f, 'v) qreltrs ⇒ bool" where
"SN_qrel = (λ(nfs, Q, R, S). SN_rel (qrstep nfs Q R) (qrstep nfs Q S))"
lemma SN_qrel_split:
assumes sn1: "SN_qrel (nfs,Q, D ∩ (R ∪ S), R ∪ S - D)"
and sn2: "SN_qrel (nfs,Q,R - D, S - D)"
shows "SN_qrel (nfs,Q,R,S)"
unfolding SN_qrel_def rel_qrstep_SN split
proof (clarify)
fix ts
assume "qrs_ideriv nfs Q R S ts"
from qrs_ideriv_split[OF this, of D] sn1 sn2
show False unfolding SN_qrel_def rel_qrstep_SN by auto
qed
lemma SN_qrel_map:
fixes R Rw R' Rw' :: "('f, 'v) trs" and Q Q' :: "('f, 'v) terms" and nfs
defines QR: "QR ≡ qrstep nfs Q R"
defines QRw: "QRw ≡ qrstep nfs Q Rw"
defines QR': "QR' ≡ qrstep nfs Q' R'"
defines QRw': "QRw' ≡ qrstep nfs Q' Rw'"
defines A: "A ≡ QR' ∪ QRw'"
assumes SN: "SN_qrel (nfs,Q',R',Rw')"
and R: "⋀ s t. (s,t) ∈ QR ⟹ (f s, f t) ∈ A^* O QR' O A^*"
and Rw: "⋀ s t. (s,t) ∈ QRw ⟹ (f s, f t) ∈ A^*"
shows "SN_qrel (nfs,Q,R,Rw)"
by (unfold SN_qrel_def split,
rule SN_rel_map[OF
SN[unfolded SN_qrel_def split]
R[unfolded QR A QR' QRw']
Rw[unfolded QRw A QR' QRw']])
lemma SN_qrel_empty_S[simp]: "SN_qrel (nfs,Q,R,{}) = SN (qrstep nfs Q R)"
unfolding SN_qrel_def
by auto
lemma SN_qrel_empty_Q[simp]: "SN_qrel (nfs,{},R,S) = SN_rel (rstep R) (rstep S)"
unfolding SN_qrel_def by auto
lemma SN_qrel_mono_plain: assumes subset1: "qrstep nfs Q R ⊆ qrstep nfs Q' R'" and subset2: "qrstep nfs Q S ⊆ qrstep nfs Q' (R' ∪ S')" shows "SN_qrel (nfs,Q',R',S') ⟹ SN_qrel (nfs,Q,R,S)"
using SN_rel_mono'[OF subset1 subset2[unfolded qrstep_union]]
unfolding SN_qrel_def by auto
lemma SN_qrel_mono:
assumes subset1: "NF_terms Q ⊆ NF_terms Q'"
and subset2: "R ⊆ R'"
and subset3: "S ⊆ R' ∪ S'"
shows "SN_qrel (nfs,Q',R',S') ⟹ SN_qrel (nfs,Q,R,S)"
by (rule SN_qrel_mono_plain[OF qrstep_mono[OF subset2 subset1] qrstep_mono[OF subset3 subset1]])
lemma rel_tt:
assumes sound: "rel_tt tt"
and tt: "tt QRS QRS'"
and SN: "SN_qrel QRS'"
shows "SN_qrel QRS"
proof (cases QRS)
case (fields nfs Q R S) note QRS = this
show ?thesis
proof (cases QRS')
case (fields rnfs rQ rR rS) note QRS' = this
show ?thesis unfolding QRS SN_qrel_def
SN_rel_ideriv
proof(clarify)
fix ts
assume "ideriv (qrstep nfs Q R) (qrstep nfs Q S) ts"
then have "qrs_ideriv nfs Q R S ts" unfolding qrs_ideriv_def .
with sound[unfolded rel_tt_def] tt
have "∃ ts. qrs_ideriv rnfs rQ rR rS ts" unfolding QRS QRS' qrs_ideriv_def by blast
with SN[unfolded QRS'] show False unfolding SN_rel_ideriv SN_qrel_def qrs_ideriv_def by auto
qed
qed
qed
lemma SN_qrel_imp_SN_qrstep:
assumes "SN_qrel (nfs,Q, R, S)"
shows "SN (qrstep nfs Q R)"
using assms unfolding SN_qrel_def split_def fst_conv snd_conv
using SN_rel_imp_SN[of "qrstep nfs Q R"] by blast
end