section ‹The Encompassment Relation›
theory Encompassment
imports Litsim_Trs
begin
lemmas converse_inward = rtrancl_converse[symmetric] converse_Un converse_UNION converse_relcomp
converse_converse converse_Id
lemma qc_SN_relto_iff:
assumes "r O s ⊆ s O (s ∪ r)⇧*"
shows "SN (r⇧* O s O r⇧*) = SN s"
proof -
from converse_mono [THEN iffD2 , OF assms]
have *: "s¯ O r¯ ⊆ (s¯ ∪ r¯)⇧* O s¯" unfolding converse_inward .
have "(r⇧* O s O r⇧*)¯ = (r¯)⇧* O s¯ O (r¯)⇧*"
by (simp only: converse_relcomp O_assoc rtrancl_converse)
with qc_wf_relto_iff [OF *]
show ?thesis by (simp add: SN_iff_wf)
qed
inductive encompeq :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "⊴⋅" 50)
where
[intro]: "t = C⟨s ⋅ σ⟩ ⟹ s ⊴⋅ t"
lemma encompeq_termE [elim]:
assumes "s ⊴⋅ t"
obtains C σ where "t = C⟨s ⋅ σ⟩"
using assms by (cases)
lemma encompeq_refl:
"t ⊴⋅ t"
by (rule encompeq.intros [of t □ t Var]) simp
lemma encompeq_trans:
assumes "s ⊴⋅ t"
and "t ⊴⋅ u"
shows "s ⊴⋅ u"
proof -
obtain C D σ τ
where [simp]: "t = C⟨s ⋅ σ⟩" "u = D⟨t ⋅ τ⟩" using assms by fastforce
show ?thesis
by (rule encompeq.intros [of _ "D ∘⇩c (C ⋅⇩c τ)" _ "σ ∘⇩s τ"]) simp
qed
definition encomp (infix "⊲⋅" 50)
where
"t ⊲⋅ s ⟷ t ⊴⋅ s ∧ ¬ s ⊴⋅ t"
abbreviation (input) revencompeq (infix "⋅⊵" 50) where
"x ⋅⊵ y ≡ y ⊴⋅ x"
abbreviation (input) revencomp (infix "⋅⊳" 50) where
"x ⋅⊳ y ≡ y ⊲⋅ x"
abbreviation encompeq_set ("{⊴⋅}")
where
"{⊴⋅} ≡ {(x, y). x ⊴⋅ y}"
abbreviation encomp_set ("{⊲⋅}")
where
"{⊲⋅} ≡ {(x, y). x ⊲⋅ y}"
abbreviation revencompeq_set ("{⋅⊵}")
where
"{⋅⊵} ≡ {(x, y). y ⊴⋅ x}"
abbreviation revencomp_set ("{⋅⊳}")
where
"{⋅⊳} ≡ {(x, y). y ⊲⋅ x}"
interpretation encomp_order: preorder "op ⊴⋅" "op ⊲⋅"
by standard (auto simp: encomp_def encompeq_refl elim: encompeq_trans)
text ‹Encompassment is the composition of subsumption and the subterm relation.›
lemma encompeq_eq_subteq_instance:
"s ⊴⋅ t ⟷ (op ≤⋅ OO op ⊴) s t"
by (force simp: OO_def subsumeseq_term_iff)
lemma subsumeseq_size:
"s ≤⋅ t ⟹ size s ≤ size t"
by (cases s t rule: subsumeseq_term.cases) (auto simp: size_subst)
lemma subsumeseq_imp_encompeq:
"s ≤⋅ t ⟹ s ⊴⋅ t"
by (cases s t rule: subsumeseq_term.cases) (auto intro: encompeq.intros [of _ □])
lemma encompeq_size:
"s ⊴⋅ t ⟹ size s ≤ size t"
by (force simp: encompeq_eq_subteq_instance dest: subsumeseq_size supteq_size)
lemma encompeq_subsumeseq_cases:
"s ⊴⋅ t ⟷ s ≤⋅ t ∨ (op ≤⋅ OO op ⊲) s t"
by (auto simp: encompeq_eq_subteq_instance)
lemma revencompeq_set_cases:
"{⋅⊵} = {⋅≥} ∪ ({⊳} O {⋅≥})"
unfolding encompeq_subsumeseq_cases by blast
lemma encomp_subsumes_cases:
"s ⊲⋅ t ⟷ s <⋅ t ∨ (op ≤⋅ OO op ⊲) s t"
by (auto simp: encomp_def term_subsumable.subsumes_def encompeq_subsumeseq_cases OO_def)
(auto dest!: supt_size subsumeseq_size)
lemma wf_subsumeseq_O_subt:
"wf ({≤⋅} O {(x, y). x ⊲ y})"
proof -
have "⋀x y. (x, y) ∈ {≤⋅} O {(x, y). x ⊲ y} ⟹ size x < size y"
by (auto simp: OO_def dest!: subsumeseq_size supt_size)
then have "{≤⋅} O {(x, y). x ⊲ y} ⊆ inv_image {(x, y). x < y} size"
by (auto simp: inv_image_def)
moreover have "wf (inv_image {(x, y). x < y} size)" by (rule wf_inv_image [OF wf_less])
ultimately show ?thesis by (metis wf_subset)
qed
lemma litsim_encompeq_iff:
"s ≐ t ⟷ s ⊴⋅ t ∧ t ⊴⋅ s"
proof
assume "s ≐ t"
then show "s ⊴⋅ t ∧ t ⊴⋅ s"
by (auto simp: term_subsumable.litsim_def dest: subsumeseq_imp_encompeq)
next
presume "s ⊴⋅ t" and "t ⊴⋅ s"
then have "s ≤⋅ t" and "t ≤⋅ s"
by (auto simp: encompeq_subsumeseq_cases dest!: supt_size subsumeseq_size)
then show "s ≐ t" by (auto simp: term_subsumable.litsim_def)
qed auto
lemma encompeq_litsim_encomp_iff:
"s ⊴⋅ t ⟷ s ≐ t ∨ s ⊲⋅ t"
by (auto simp: litsim_encompeq_iff encomp_def)
lemmas encompeq_cases [consumes 1] = encompeq_litsim_encomp_iff [THEN iffD1]
lemma encomp_supt:
assumes "s ⋅> t" and "t ⊳ u"
shows "∃t ⊲ s. t ⋅≥ u"
proof -
from assms [unfolded term_subsumable.subsumes_def subsumeseq_term_iff] obtain σ
where "s = t ⋅ σ" and "¬ (∃σ. t = s ⋅ σ)" by blast
moreover with ‹t ⊳ u› have "t ⋅ σ ⊳ u ⋅ σ"
by (metis instance_no_supt_imp_no_supt)
ultimately have "s ⊳ u ⋅ σ" and "u ⋅ σ ⋅≥ u"
by (auto simp: term_subsumable.subsumes_def)
then show ?thesis by blast
qed
lemma wf_encomp:
"wf ({⊲⋅} :: ('f, 'v) term rel)"
proof -
have "{⊳} O {⋅≥} ∪ {⋅>} = ({⋅⊳} :: ('f, 'v) term rel)" by (auto simp: encomp_subsumes_cases)
moreover
have "SN ({⊳} O {⋅≥} ∪ ({⋅>} :: ('f, 'v) term rel))"
proof (rule quasi_commute_imp_SN)
have [simp]: "{(s, u). ∃t. s ≤⋅ t ∧ u ⊳ t} = {(s, u). ∃t ⊲ u. s ≤⋅ t}" by auto
show "SN ({⊳} O {⋅≥})"
using wf_subsumeseq_O_subt
by (auto simp: SN_iff_wf converse_unfold OO_def relcomp_def)
show "SN ({⋅>} :: ('f, 'v) term rel)"
using wf_subsumes by (auto simp: SN_iff_wf converse_unfold)
show "quasi_commute ({⊳} O {⋅≥}) ({⋅>} :: ('f, 'v) term rel)"
proof (unfold quasi_commute_def, intro subrelI)
fix s t :: "('f, 'v) term"
assume "(s, t) ∈ {⋅>} O {⊳} O {⋅≥}"
moreover have "{⋅>} O {⊳} ⊆ {⊳} O {⋅≥}"
by (auto simp: relcomp_def OO_def dest: encomp_supt)
ultimately have "(s, t) ∈ {⊳} O {⋅≥} O {⋅≥}" by auto
then have "(s, t) ∈ {⊳} O {⋅≥}"
by (auto simp: relcomp_def OO_def dest: subsumeseq_term_trans)
then show "(s, t) ∈ ({⊳} O {⋅≥}) O ({⊳} O {⋅≥} ∪ {⋅>})⇧*" by auto
qed
qed
ultimately
show ?thesis by (auto simp: SN_iff_wf converse_unfold)
qed
lemmas encomp_induct = wfP_induct [OF wf_encomp [to_pred]]
lemma SN_encomp:
"SN {⋅⊳}"
using wf_encomp by (auto simp: SN_iff_wf converse_unfold)
lemma qc_SN_relto_encompeq:
"SN r ⟹ {⋅⊵} O r ⊆ r O (r ∪ {⋅⊵})⇧* ⟹ SN (relto r {⋅⊵})"
by (intro qc_SN_relto_iff [THEN iffD2])
context
fixes r :: "('f, 'v) term rel"
assumes r_ctxt: "(s, t) ∈ r ⟹ (C⟨s⟩, C⟨t⟩) ∈ r"
and r_subst: "(s, t) ∈ r ⟹ (s ⋅ σ, t ⋅ σ) ∈ r"
begin
lemma commutes_rewrel_encomp:
"{⋅⊵} O r ⊆ r O {⋅⊵}"
proof -
{ fix s t u
assume "s ⋅⊵ t" and "(t, u) ∈ r"
then obtain C and σ :: "('f, 'v) subst" where "s = C⟨t ⋅ σ⟩"
and "(C⟨t ⋅ σ⟩, C⟨u ⋅ σ⟩) ∈ r" by (auto simp: encomp_def r_ctxt r_subst)
then have "(s, u) ∈ r O {⋅⊵}" by auto }
then show ?thesis by blast
qed
context
assumes SN_rewrel: "SN r"
begin
lemma SN_rewrel_relto_encomp:
"SN (relto r {⋅⊵})"
using SN_rewrel and commutes_rewrel_encomp
by (intro qc_SN_relto_encompeq) auto
lemma SN_encomp_Un_rewrel:
"SN ({⋅⊳} ∪ r)"
proof -
have "{⋅⊳}⇧* O r O {⋅⊳}⇧* ⊆ {⋅⊵}⇧* O r O {⋅⊵}⇧*"
by (intro relcomp_mono rtrancl_mono) (auto simp: encomp_def)
with SN_rewrel_relto_encomp have "SN ({⋅⊳}⇧* O r O {⋅⊳}⇧*)" by (rule SN_subset)
from SN_relto_split [of _ "{}" _ "{}", simplified, OF this SN_encomp]
show ?thesis by (simp add: ac_simps)
qed
end
end
lemma revencompeq_set_eqvt [simp]:
"π ∙ {⋅⊵} = {⋅⊵}"
by (simp add: revencompeq_set_cases trs_pt.union_eqvt trs_pt.relcomp_eqvt)
end