section ‹Literal Similarity of TRSs›
theory Litsim_Trs
imports
"../Rewriting/Renaming_Interpretations"
First_Order_Terms.Subsumption
begin
lemma listsim_equiv_on_terms:
"equiv T {(x, y). x ≐ y ∧ x ∈ T ∧ y ∈ T}"
by (rule equivI)
(auto simp: refl_on_def sym_def trans_def
dest: term_subsumable.litsim_sym term_subsumable.litsim_trans)
lemma equivp_litsim:
"equivp (op ≐ :: ('f, 'v) term ⇒ ('f, 'v) term ⇒ bool)"
by (rule equivpI) (auto simp: reflp_def symp_def transp_def
dest: term_subsumable.litsim_sym term_subsumable.litsim_trans)
lemma litsim_term_iff:
fixes s t :: "('f, 'v :: infinite) term"
shows "s ≐ t ⟷ (∃p. p ∙ s = t)"
proof
assume "∃p. p ∙ s = t"
then obtain p where "p ∙ s = t" ..
then have "t = s ⋅ sop p" and "s = t ⋅ sop (-p)" by auto
from subsumeseq_term.intros [OF this(1)] and subsumeseq_term.intros [OF this(2)]
show "s ≐ t" by (auto simp: term_subsumable.litsim_def)
next
assume "s ≐ t"
then obtain σ τ
where "s ⋅ σ = t" and "t ⋅ τ = s" by (fastforce simp: term_subsumable.litsim_def)
from variants_imp_renaming [OF this] obtain f
where "bij f" and "finite {x. f x ≠ x}" and [simp]: "t = s ⋅ (Var ∘ f)" by blast
then have "f ∈ perms" by (auto simp: perms_def)
then have "Abs_perm f ∙ s = t" by (auto simp: term_apply_subst_Var_Abs_perm)
then show "∃p. p ∙ s = t" ..
qed
lemma instanceeq_set_eqvt [simp]:
"π ∙ {⋅≥} = {⋅≥}"
proof (intro equalityI subrelI)
fix s t :: "('a, 'b) term" assume "(s, t) ∈ π ∙ {⋅≥}"
then have "-π ∙ s ⋅≥ -π ∙ t"
by (auto simp: inv_rule_mem_trs_simps [where p = "π", symmetric])
then obtain σ where "(-π ∙ t) ⋅ σ = -π ∙ s" by auto
then have "t ⋅ conjugate_subst π σ = s"
using term_apply_subst_eqvt [of π "-π ∙ t" σ] by simp
then show "(s, t) ∈ {⋅≥}" by blast
next
fix s t :: "('a, 'b) term" assume "(s, t) ∈ {⋅≥}"
then obtain σ where "s = t ⋅ σ" by auto
then have "-π ∙ s = (-π ∙ t) ⋅ conjugate_subst (-π) σ" by (auto simp: eqvt)
then have "-π ∙ s ⋅≥ -π ∙ t" by blast
then have "-π ∙ (s, t) ∈ {⋅≥}" by (auto simp: eqvt)
then show "(s, t) ∈ π ∙ {⋅≥}" unfolding trs_pt.inv_mem_simps(1) [of π] .
qed
lemma subsumeseq_set_eqvt [simp]:
"π ∙ {≤⋅} = {≤⋅}"
proof (intro equalityI subrelI)
fix s t :: "('a, 'b) term" assume "(s, t) ∈ π ∙ {≤⋅}"
then have "-π ∙ s ≤⋅ -π ∙ t"
by (auto simp: inv_rule_mem_trs_simps [where p = "π", symmetric])
then have "-π ∙ (t, s) ∈ {⋅≥}" by (auto simp: eqvt)
then have "(t, s) ∈ π ∙ {⋅≥}" unfolding trs_pt.inv_mem_simps(1) [of π] .
then show "(s, t) ∈ {≤⋅}" by simp
next
fix s t :: "('a, 'b) term" presume "(t, s) ∈ {⋅≥}"
then have "(t, s) ∈ π ∙ {⋅≥}" by simp
then have "(-π ∙ t, -π ∙ s) ∈ {⋅≥}" unfolding trs_pt.inv_mem_simps(1) [of π, symmetric] by (auto simp: eqvt)
then have "(-π ∙ s, -π ∙ t) ∈ {≤⋅}" by auto
then have "-π ∙ (s, t) ∈ {≤⋅}" by (auto simp: eqvt)
then show "(s, t) ∈ π ∙ {≤⋅}" unfolding trs_pt.inv_mem_simps(1) [of π] .
qed blast
lemma instance_term_set_conv:
"{⋅>} = {⋅≥} - {≤⋅}"
by (auto simp: term_subsumable.subsumes_def)
lemma subsumes_term_set_conv:
"{<⋅} = {≤⋅} - {⋅≥}"
by (auto simp: term_subsumable.subsumes_def)
lemma instance_term_set_eqvt [simp]:
"π ∙ {⋅>} = {⋅>}"
by (simp add: instance_term_set_conv trs_pt.Diff_eqvt)
lemma subsumes_term_set_eqvt [simp]:
"π ∙ {<⋅} = {<⋅}"
by (simp add: subsumes_term_set_conv trs_pt.Diff_eqvt)
definition subsumeseq_trs :: "('f, 'v :: infinite) trs ⇒ ('f, 'v) trs ⇒ bool"
where
"subsumeseq_trs R S ⟷ (∀r ∈ R. ∃p. p ∙ r ∈ S)"
adhoc_overloading
SUBSUMESEQ subsumeseq_trs
lemma subsumeseq_trsI [intro]:
assumes "⋀r. r ∈ R ⟹ ∃p. p ∙ r ∈ S"
shows "R ≤⋅ S"
unfolding subsumeseq_trs_def by (rule ballI) (insert assms, auto)
lemma subsumeseq_trsE [elim]:
assumes "R ≤⋅ S" and "r ∈ R"
obtains p where "p ∙ r ∈ S"
using assms by (auto simp: subsumeseq_trs_def)
lemma subsumeseq_trs_refl:
fixes R :: "('f, 'v :: infinite) trs"
shows "R ≤⋅ R"
using trs_pt.subset_imp_ex_perm [of R, OF subset_refl]
by (auto simp: subsumeseq_trs_def)
lemma subsumeseq_trs_trans:
fixes R S T :: "('f, 'v :: infinite) trs"
assumes "R ≤⋅ S" and "S ≤⋅ T"
shows "R ≤⋅ T"
proof
fix r
assume "r ∈ R"
with ‹R ≤⋅ S› obtain p where "p ∙ r ∈ S" by auto
then obtain q where "q ∙ p ∙ r ∈ T" using ‹S ≤⋅ T› by blast
then have "(q + p) ∙ r ∈ T" by simp
then show "∃p. p ∙ r ∈ T" by blast
qed
interpretation subsumable_trs: subsumable subsumeseq_trs
by standard (force simp: subsumeseq_trs_refl dest: subsumeseq_trs_trans)+
adhoc_overloading
SUBSUMES subsumable_trs.subsumes and
LITSIM subsumable_trs.litsim
end