Theory TRS.Sharp_Syntax
section ‹Overloading for the Sharp Symbol›
theory Sharp_Syntax
imports
First_Order_Rewriting.Trs
begin
consts SHARP :: "'a ⇒ 'b" ("♯")
locale sharp_syntax =
fixes shp :: "'f ⇒ 'f"
begin
adhoc_overloading SHARP ⇌ shp
end
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
fun sharp_term :: "('f, 'v) term ⇒ ('f, 'v) term"
where
"sharp_term (Var x) = Var x" |
"sharp_term (Fun f ss) = Fun (♯ f) ss"
fun sharp_ctxt :: "('f, 'v) ctxt ⇒ ('f, 'v) ctxt"
where
"sharp_ctxt □ = □" |
"sharp_ctxt (More f ss⇩1 C ss⇩2) = More (♯ f) ss⇩1 C ss⇩2"
abbreviation sharp_sig :: "('f × nat) set ⇒ ('f × nat) set"
where
"sharp_sig ≡ image (λ(f, n). (♯ f, n))"
end
context sharp_syntax
begin
adhoc_overloading
SHARP ⇌ "sharp_term shp" "sharp_ctxt shp" "sharp_sig shp"
end
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
lemma sharp_term_ctxt_apply [simp]:
"C ≠ □ ⟹ ♯(C⟨t⟩) = (♯ C)⟨t⟩"
by (cases C) simp_all
lemma supt_sharp_term_subst [simp]:
"♯ s ⋅ σ ⊳ t ⟷ s ⋅ σ ⊳ t"
by (cases s) auto
end
lemma sharp_term_id [simp]:
"sharp_term id t = t"
"sharp_term (λx. x) t = t"
by (induct t) simp_all
text ‹A theory on first-order term rewrite systems (TRSs).›
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
abbreviation sharp_trs :: "('f, 'v) trs ⇒ ('f, 'v) trs"
where
"sharp_trs R ≡ dir_image R ♯"
end
context sharp_syntax
begin
adhoc_overloading
SHARP ⇌ "sharp_trs shp"
end
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
definition DP_on :: "'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs"
where
"DP_on F R = {(s, t). ∃l r h us. s = ♯ l ∧ t = ♯ (Fun h us) ∧
(l, r) ∈ R ∧ r ⊵ Fun h us ∧ (h, length us) ∈ F ∧ ¬ l ⊳ Fun h us}"
abbreviation "DP R ≡ DP_on {f. defined R f} R"
lemma nrrstep_imp_sharp_nrrstep: assumes "(s, t) ∈ nrrstep R"
shows "(♯ s, ♯ t) ∈ nrrstep R"
proof -
from assms obtain C l r σ where "C ≠ □" and "(l, r) ∈ R"
and *: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
by (auto elim: nrrstepE)
then obtain D f ss ts where "C = More f ss D ts"
and "s = Fun f (ss @ D⟨l ⋅ σ⟩ # ts)" by (cases C) (auto elim: sharp_term.elims)
moreover with ‹t = C⟨r ⋅ σ⟩› have "t = Fun f (ss @ D⟨r ⋅ σ⟩ # ts)"
using assms by auto
moreover define C' where "C' = More (♯ f) ss D ts"
ultimately have "♯ s = C'⟨l ⋅ σ⟩" and "♯ t = C'⟨r ⋅ σ⟩" by simp+
moreover have "C' ≠ □" using ‹C ≠ □› by (simp add: C'_def)
ultimately show "(♯ s, ♯ t) ∈ nrrstep R" using ‹(l, r) ∈ R› by (auto simp: nrrstep_def')
qed
lemma nrrstep_imp_sharp_rstep:
assumes "(s, t) ∈ nrrstep R"
shows "(♯ s, ♯ t) ∈ rstep R"
using nrrstep_imp_sharp_nrrstep[OF assms] by (rule nrrstep_imp_rstep)
lemma nrrsteps_imp_sharp_rsteps:
"(s, t) ∈ (nrrstep R)⇧* ⟹ (♯ s, ♯ t) ∈ (rstep R)⇧*"
proof (induct rule: rtrancl_induct)
case (step a b)
from ‹(a,b) ∈ nrrstep R› have "(♯ a, ♯ b) ∈ rstep R"
by (rule nrrstep_imp_sharp_rstep)
with step show ?case by auto
qed simp
lemma finiteR_imp_finiteDP:
assumes "finite R"
shows "finite (DP_on F R)"
proof -
have fS: "finite {(l, r, u).
∃h us. u = Fun h us ∧ (l,r) ∈ R ∧ r ⊵ u ∧ (h, length us) ∈ F ∧ ¬(l ⊳ u)}" (is "finite ?S")
using assms by (rule finite_imp_finite_DP_on')
let ?f = "λ(x :: ('f, 'v) term, y, z :: ('f, 'v) term). (♯ x, ♯ z)"
have eq1: "(⋃y∈?S. {x. x = ?f y}) = ?f ` ?S" by blast
with fS have "finite(?f ` ?S)" by auto
have "DP_on F R = ?f ` ?S" (is "?DP = ?T")
proof
show "?DP ⊆ ?T"
proof
fix x assume "x ∈ ?DP"
then obtain l r h us
where "fst x = ♯ l" and "snd x = ♯ (Fun h us)"
and "(l,r) ∈ R" "r ⊵ Fun h us" and "(h, length us) ∈ F" and " ¬(l ⊳ Fun h us)"
by (auto simp: DP_on_def split_def)
then have "(l,r,Fun h us) ∈ ?S" by auto
then show "x ∈ ?T" unfolding eq1[symmetric]
proof (rule UN_I)
have "x = (fst x, snd x)" by simp
then have "x = (♯ l, ♯ (Fun h us))"
unfolding ‹fst x = ♯ l› ‹snd x = ♯ (Fun h us)› .
then show "x ∈ {x. x = ?f (l,r,Fun h us)}" by auto
qed
qed
next
show "?T ⊆ ?DP"
proof
fix x assume "x ∈ ?T"
then have "x ∈ (⋃y∈?S. {x. x = ?f y})" unfolding eq1 .
then obtain y where "y ∈ ?S" and "x = ?f y" by fast
then obtain l r h us where "y = (l, r, Fun h us)" and dp: "(l, r) ∈ R"
and "r ⊵ Fun h us" and "(h, length us) ∈ F" and "¬ (l ⊳ Fun h us)" by blast
moreover with ‹x = ?f y› have "x = (♯ l, ♯ (Fun h us))" by auto
ultimately show "x ∈ ?DP" using dp unfolding DP_on_def by auto
qed
qed
with fS show ?thesis by auto
qed
lemma vars_sharp_eq_vars [simp]: "vars_term (♯ t) = vars_term t"
by (induct t) auto
lemma wf_trs_imp_wf_DP_on:
assumes "wf_trs R"
shows "wf_trs (DP_on F R)"
unfolding wf_trs_def
proof (intro allI impI)
fix s t
assume "(s,t) ∈ DP_on F R"
then obtain l r h us where "s = ♯ l" and "t = ♯ (Fun h us)" and "(l, r) ∈ R"
and "r ⊵ (Fun h us)" "¬ (l ⊳ Fun h us)"
by (auto simp:DP_on_def)
from ‹wf_trs R› and ‹(l,r) ∈ R›
have "∃f ss. l = Fun f ss" and "vars_term r ⊆ vars_term l" by (auto simp: wf_trs_def)
from ‹∃f ss. l = Fun f ss› obtain f ss where "l = Fun f ss" by auto
then have "s = Fun (♯ f) ss" unfolding ‹s = ♯ l› by simp
then have "∃f ss. s = Fun f ss" by auto
from ‹r ⊵ Fun h us› have "vars_term(Fun h us) ≤ vars_term r" by (induct rule: supteq.induct) auto
then have "vars_term t ⊆ vars_term s" unfolding ‹s = ♯ l›
and ‹t = ♯ (Fun h us)› vars_sharp_eq_vars using ‹vars_term r ≤ vars_term l› by simp
from ‹∃f ss. s = Fun f ss› ‹vars_term t ⊆ vars_term s›
show "(∃f ss. s = Fun f ss) ∧ vars_term t ⊆ vars_term s" by simp
qed
lemma sharp_eq_imp_eq:
fixes s :: "('f, 'v) term"
assumes "inj (♯ :: 'f ⇒ 'f)"
shows "♯ s = ♯ t ⟹ s = t"
proof (cases s)
case (Var x)
assume "♯ s = ♯ t" with Var show ?thesis by (induct t) auto
next
case (Fun f ss)
assume "♯ s = ♯ t"
with Fun have "♯ (Fun f ss) = ♯ t" by simp
then obtain g ts where t: "t = Fun g ts" by (induct t) auto
with ‹♯ s = ♯ t› have "Fun (♯ f) ss = Fun (♯ g) ts" unfolding ‹s = Fun f ss› ‹t = Fun g ts›
by simp
then have "f = g" and "ss = ts" using ‹inj (♯ :: 'f ⇒ 'f)›[unfolded inj_on_def] by auto
then show ?thesis unfolding Fun t by simp
qed
lemma DP_on_step_in_R:
fixes R :: "('f, 'v) trs" and v :: "('f, 'v) term ⇒ 'v"
assumes "(s, t) ∈ DP_on F R" and inj: "inj (♯ :: 'f ⇒ 'f)"
shows "∃C. funas_ctxt C ⊆ funas_trs R ∧
(sharp_term (the_inv ♯) s, C⟨sharp_term (the_inv ♯) t⟩) ∈ R"
proof -
let ?us = "sharp_term (the_inv (♯ :: 'f ⇒ 'f))"
from assms obtain l r f ts
where s: "s = ♯ l" and t: "t = ♯ (Fun f ts)"
and R: "(l,r) ∈ R" and sub: "r ⊵ Fun f ts" unfolding DP_on_def supt_supteq_conv by auto
from sub obtain C where r: "r = C⟨Fun f ts⟩" by auto
from rhs_wf[OF R subset_refl] have "funas_term r ⊆ funas_trs R" .
then have "funas_term (C⟨Fun f ts⟩) ⊆ funas_trs R" unfolding r .
then have "funas_ctxt C ⊆ funas_trs R" and "funas_term (Fun f ts) ⊆ funas_trs R" by auto
from lhs_wf[OF R subset_refl] have "funas_term l ⊆ funas_trs R" .
have us: "?us s = l" unfolding s by (cases l, auto simp: the_inv_f_f[OF inj])
have ut: "?us t = Fun f ts" unfolding t by (simp add: the_inv_f_f[OF inj])
from R have "(?us s,C⟨?us t⟩) ∈ R" unfolding us ut r .
with ‹funas_ctxt C ⊆ funas_trs R› show ?thesis by best
qed
lemma sharp_rrstep_imp_rstep:
assumes rrstep: "(♯ s, ♯ t) ∈ subst.closure (DP_on F R)" and "inj (♯ :: 'f ⇒ 'f)" and "wf_trs R"
shows "∃C. (s, C⟨t⟩) ∈ rstep R"
proof -
from ‹wf_trs R› have "wf_trs (DP_on F R)" by (rule wf_trs_imp_wf_DP_on)
from rrstep obtain l r σ where "(l,r) ∈ DP_on F R" and ss: "♯ s = l⋅σ" and st: "♯ t = r⋅σ"
by (induct, auto)
from ‹(l,r) ∈ DP_on F R› obtain l' r' h' us'
where l: "l = ♯ l'" and r: "r = ♯ (Fun h' us')" (is "r = ♯ ?u'")
and l'r': "(l',r') ∈ R" and "r' ⊵ (Fun h' us')" and "¬ l' ⊳ Fun h' us'"
unfolding DP_on_def by auto
from ‹wf_trs R› and ‹(l',r') ∈ R› obtain f' ss' where l': "l' = Fun f' ss'" using wf_trs_imp_lhs_Fun by best
from ‹r' ⊵ ?u'› obtain C where r': "r' = C⟨?u'⟩" by best
have ss: "♯ s = (Fun (♯ f') ss') ⋅ σ" unfolding ss l l' by simp
then obtain f where s: "s = (Fun f ss') ⋅ σ" by (cases s, auto)
from s ss have "♯ f = ♯ f'" by simp
with ‹inj (♯ :: 'f ⇒ 'f)›[unfolded inj_on_def] have f: "f = f'" by simp
have ts: "♯ t = (Fun (♯ h') us') ⋅ σ" unfolding st r by simp
then obtain h where t: "t = (Fun h us') ⋅ σ" by (cases t, auto)
from t ts have "♯ h = ♯ h'" by simp
with ‹inj (♯ :: 'f ⇒ 'f)›[unfolded inj_on_def] have h: "h = h'" by simp
show ?thesis
by (rule exI[of _ "C ⋅⇩c σ"], unfold s t f h, rule rstepI[OF l'r', of _ □ σ], unfold l' r', simp, simp)
qed
definition DP_simple :: " 'f sig ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs"
where
"DP_simple D R = {(s, t).
∃l r h us. s = ♯ l ∧ t = ♯ (Fun h us) ∧ (l, r) ∈ R ∧ (h, length us) ∈ D ∧ r ⊵ Fun h us}"
lemma DP_on_subset_DP_simple: "DP_on F R ⊆ DP_simple F R"
by (auto simp: DP_on_def DP_simple_def)
lemma funas_DP_simple_subset:
"funas_trs (DP_simple D R) ⊆ funas_trs R ∪ ♯ (funas_trs R)"
(is "?F ⊆ ?H ∪ ?I")
proof (rule subrelI)
fix f n
assume "(f,n) ∈ ?F"
then obtain s t where st: "(s,t) ∈ DP_simple D R" and "(f,n) ∈ funas_rule (s,t)"
unfolding funas_trs_def by auto
then obtain u where fn: "(f,n) ∈ funas_term u" and u: "u = s ∨ u = t" unfolding funas_rule_def
by auto
from st[unfolded DP_simple_def] obtain l r uu where lr: "(l,r) ∈ R" and s: "s = ♯ l" and t: "t = ♯ uu" and uu: "r ⊵ uu"
by force
from fn u[unfolded s t] obtain v where fn: "(f, n) ∈ funas_term (♯ v)" and v: "v = l ∨ v = uu" by auto
from fn have fn: "(f, n) ∈ funas_term v ∪ ♯ (funas_term v)"
by (cases v, auto)
from uu obtain C where r: "r = C⟨uu⟩" ..
have "funas_term uu ⊆ funas_term r" unfolding r by simp
with v have "funas_term v ⊆ funas_rule (l,r)" unfolding funas_rule_def by auto
then have subset: "funas_term v ⊆ funas_trs R" using lr unfolding funas_trs_def by auto
with fn show "(f,n) ∈ ?H ∪ ?I" by auto
qed
lemma funas_DP_on_subset:
"funas_trs (DP_on F R) ⊆ funas_trs R ∪ ♯ (funas_trs R)"
by (rule order.trans [OF _ funas_DP_simple_subset [of F]])
(insert DP_on_subset_DP_simple, auto simp: funas_trs_def)
end
end