section ‹Subsumption and Encompassment›
theory Encompassment
imports
"../Rewriting/Renaming_Interpretations"
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
no_notation
subset_mset (infix "<#" 50)
subsection ‹Subsumption (the ``instance of'' relation)›
text ‹Syntax for subsumption and literal similarity (also as sets).›
consts
SUBSUMESEQ :: "'a ⇒ 'a ⇒ bool" (infix "≤⋅" 50)
SUBSUMES :: "'a ⇒ 'a ⇒ bool" (infix "<⋅" 50)
LITSIM :: "'a ⇒ 'a ⇒ bool" (infix "≐" 50)
abbreviation (input) INSTANCEQ (infix "⋅≥" 50)
where
"x ⋅≥ y ≡ y ≤⋅ x"
abbreviation (input) INSTANCE (infix "⋅>" 50)
where
"x ⋅> y ≡ y <⋅ x"
abbreviation SUBSUMESEQ_SET ("{≤⋅}")
where
"{≤⋅} ≡ {(x, y). x ≤⋅ y}"
abbreviation SUBSUMES_SET ("{<⋅}")
where
"{<⋅} ≡ {(x, y). x <⋅ y}"
abbreviation INSTANCEEQ_SET ("{⋅≥}")
where
"{⋅≥} ≡ {(x, y). y ≤⋅ x}"
abbreviation INSTANCE_SET ("{⋅>}")
where
"{⋅>} ≡ {(x, y). y <⋅ x}"
abbreviation LITSIM_SET ("{≐}")
where
"{≐} ≡ {(x, y). x ≐ y}"
locale subsumable =
fixes subsumeseq :: "'a ⇒ 'a ⇒ bool"
assumes refl: "subsumeseq x x"
and trans: "subsumeseq x y ⟹ subsumeseq y z ⟹ subsumeseq x z"
begin
adhoc_overloading
SUBSUMESEQ subsumeseq
definition "subsumes t s ⟷ t ≤⋅ s ∧ ¬ s ≤⋅ t"
definition "litsim s t ⟷ s ≤⋅ t ∧ t ≤⋅ s"
adhoc_overloading
SUBSUMES subsumes and
LITSIM litsim
lemma litsim_refl [simp]:
"s ≐ s"
by (auto simp: litsim_def refl)
lemma litsim_sym:
"s ≐ t ⟹ t ≐ s"
by (auto simp: litsim_def)
lemma litsim_trans:
"s ≐ t ⟹ t ≐ u ⟹ s ≐ u"
by (auto simp: litsim_def dest: trans)
end
sublocale subsumable ⊆ subsumption: preorder "op ≤⋅" "op <⋅"
by (unfold_locales) (auto simp: subsumes_def refl elim: trans)
inductive subsumeseq_term :: "('a, 'b) term ⇒ ('a, 'b) term ⇒ bool"
where
[intro]: "t = s ⋅ σ ⟹ subsumeseq_term s t"
adhoc_overloading
SUBSUMESEQ subsumeseq_term
lemma subsumeseq_termE [elim]:
assumes "s ≤⋅ t"
obtains σ where "t = s ⋅ σ"
using assms by (cases)
lemma subsumeseq_term_refl:
fixes t :: "('a, 'b) term"
shows "t ≤⋅ t"
by (rule subsumeseq_term.intros [of t t Var]) simp
lemma subsumeseq_term_trans:
fixes s t u :: "('a, 'b) term"
assumes "s ≤⋅ t" and "t ≤⋅ u"
shows "s ≤⋅ u"
proof -
obtain σ τ
where [simp]: "t = s ⋅ σ" "u = t ⋅ τ" using assms by fastforce
show ?thesis
by (rule subsumeseq_term.intros [of _ _ "σ ∘⇩s τ"]) simp
qed
interpretation term_subsumable: subsumable subsumeseq_term
by standard (force simp: subsumeseq_term_refl dest: subsumeseq_term_trans)+
adhoc_overloading
SUBSUMES term_subsumable.subsumes and
LITSIM term_subsumable.litsim
lemma subsumeseq_term_iff:
"s ⋅≥ t ⟷ (∃σ. s = t ⋅ σ)"
by auto
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
fun num_syms :: "('f, 'v) term ⇒ nat"
where
"num_syms (Var x) = 1" |
"num_syms (Fun f ts) = Suc (sum_list (map num_syms ts))"
fun num_funs :: "('f, 'v) term ⇒ nat"
where
"num_funs (Var x) = 0" |
"num_funs (Fun f ts) = Suc (sum_list (map num_funs ts))"
lemma num_funs_subst:
"num_funs (t ⋅ σ) ≥ num_funs t"
by (induct t) (simp_all, metis comp_apply sum_list_mono)
lemma num_syms_1: "num_syms t ≥ 1"
by (induct t) auto
lemma num_syms_subst:
"num_syms (t ⋅ σ) ≥ num_syms t"
using num_syms_1
by (induct t) (auto, metis comp_apply sum_list_mono)
lemma card_PCons_Collect:
"card {i <# (p :: pos) | p. p ∈ A} = card A"
proof -
have "{i <# p | p. p ∈ A} = (op <# i ` A)" by auto
then show ?thesis by (auto intro: card_image simp: inj_on_def)
qed
lemma Collect_UNION:
"{f i p | i p. i < n ∧ p ∈ A i} = (⋃i < n. {f i p | p. p ∈ A i})"
by auto
lemma card_insert_poss:
"card (insert ε (⋃i < length ts. {i <# p | p. p ∈ poss (ts ! i)})) =
Suc (card (⋃i < length ts. {i <# p | p. p ∈ poss (ts ! i)}))"
(is "_ = Suc (card ?P)")
proof -
have *: "finite ?P"
proof -
fix f
have "poss (Fun f ts) ⊆ poss (Fun f ts)" by auto
then show ?thesis using finite_poss [of "Fun f ts"] by (simp add: Collect_UNION)
qed
have "card ({ε} ∪ ?P) = card {ε} + card ?P"
by (rule card_Un_disjoint) (insert *, auto)
then show ?thesis by simp
qed
lemma card_poss_Fun:
"card (poss (Fun f ts)) = Suc (∑i < length ts. card (poss (ts ! i)))"
proof -
have "card (poss (Fun f ts)) = Suc (∑i < length ts. card {i <# p | p. p ∈ poss (ts ! i)})"
by (auto simp: Collect_UNION card_insert_poss intro: card_UN_disjoint)
then show ?thesis by (simp add: card_PCons_Collect)
qed
lemma card_poss_eq_num_syms:
"card (poss t) = num_syms t"
by (induct t) (simp, unfold card_poss_Fun,
simp add: card_poss_Fun Collect_UNION sum_list_sum_nth atLeast0LessThan)
fun num_vars :: "('f, 'v) term ⇒ nat"
where
"num_vars (Var x) = 1" |
"num_vars (Fun f ts) = sum_list (map num_vars ts)"
definition num_unique_vars :: "('f, 'v) term ⇒ nat"
where
"num_unique_vars t = card (vars_term t)"
lemma finite_Union_vars_term:
"finite (⋃t ∈ set ts. vars_term t)"
by auto
lemma [simp]:
"num_unique_vars (Var x) = 1"
by (simp_all add: num_unique_vars_def)
lemma num_unique_vars_Fun_Cons:
"num_unique_vars (Fun f (t # ts)) ≤ num_unique_vars t + num_unique_vars (Fun f ts)"
apply (simp_all add: num_unique_vars_def)
unfolding card_Un_Int [OF finite_vars_term finite_Union_vars_term]
apply simp
done
lemma sum_list_map_unique_vars:
"sum_list (map num_unique_vars ts) ≥ num_unique_vars (Fun f ts)"
proof (induct ts)
case (Cons t ts)
with num_unique_vars_Fun_Cons [of f t ts]
show ?case by simp
qed (simp add: num_unique_vars_def)
lemma sum_list_mono:
fixes f g :: "'a ⇒ nat"
assumes "∀x ∈ set xs. f x ≥ g x"
shows "sum_list (map f xs) ≥ sum_list (map g xs)"
using assms by (induct xs) simp_all
lemma sum_list_cong:
fixes f g :: "'a ⇒ nat"
assumes "∀x ∈ set xs. f x = g x"
shows "sum_list (map f xs) = sum_list (map g xs)"
using assms by (induct xs) simp_all
lemma num_vars_geq_num_unique_vars:
"num_vars t ≥ num_unique_vars t"
proof -
note * =
sum_list_mono [of _ num_unique_vars num_vars, THEN sum_list_map_unique_vars [THEN le_trans]]
show ?thesis by (induct t) (auto intro: *)
qed
lemma num_syms_geq_num_vars:
"num_syms t ≥ num_vars t"
proof (induct t)
case (Fun f ts)
with sum_list_mono [of ts num_vars num_syms]
have "sum_list (map num_vars ts) ≤ sum_list (map num_syms ts)" by simp
then show ?case by simp
qed simp
lemma num_syms_eq:
"num_syms t = num_funs t + num_vars t"
proof (induct t)
case (Fun f ts)
then have "∀t ∈ set ts. num_syms t = num_funs t + num_vars t" by auto
note * = sum_list_cong [OF this]
show ?case unfolding num_syms.simps *
by (simp add: sum_list_addf)
qed simp
lemma num_funs_0_imp_is_Var [simp]:
"num_funs t = 0 ⟹ is_Var t"
by (induct t) auto
subsection ‹Equality of terms modulo variables›
inductive emv where
Var [simp, intro!]: "emv (Var x) (Var y)" |
Fun [intro]: "⟦f = g; length ss = length ts; ∀i < length ts. emv (ss ! i) (ts ! i)⟧ ⟹
emv (Fun f ss) (Fun g ts)"
lemma emv_refl:
"emv t t"
by (induct t) auto
lemma emv_sym:
assumes "emv s t"
shows "emv t s"
using assms by (induct) auto
lemma emv_Var:
assumes "emv (Var x) t"
obtains y where "t = Var y"
using assms by (cases) simp
lemma emv_Fun_Var [simp]:
"emv (Fun f ts) (Var x) = False"
by (auto elim: emv.cases)
lemma emv_Fun_Fun [iff]:
"emv (Fun f ss) (Fun g ts) ⟷
f = g ∧ length ss = length ts ∧ (∀i < length ts. emv (ss ! i) (ts ! i))"
by (auto elim: emv.cases)
lemma emv_trans:
assumes "emv s t" and "emv t u"
shows "emv s u"
using assms
proof (induct arbitrary: u)
case (Var x y)
then show ?case by (auto elim: emv_Var)
next
case (Fun f g ss ts)
then show ?case by (cases u) simp_all
qed
lemma num_funs_0:
assumes "num_funs t = 0"
obtains x where "t = Var x"
using assms by (induct t) auto
lemma sum_list_map_num_syms_subst:
assumes "sum_list (map (num_syms ∘ (λt. t ⋅ σ)) ts) = sum_list (map num_syms ts)"
shows "∀i < length ts. num_syms (ts ! i ⋅ σ) = num_syms (ts ! i)"
using assms
proof (induct ts)
case (Cons t ts)
then have "num_syms (t ⋅ σ) + sum_list (map (num_syms ∘ (λt. t ⋅ σ)) ts)
= num_syms t + sum_list (map num_syms ts)" by (simp add: o_def)
moreover have "num_syms (t ⋅ σ) ≥ num_syms t" by (metis num_syms_subst)
moreover have "sum_list (map (num_syms ∘ (λt. t ⋅ σ)) ts) ≥ sum_list (map num_syms ts)"
using num_syms_subst [of _ σ] by (induct ts) (auto intro: add_mono)
ultimately show ?case using Cons by (auto) (case_tac i, auto)
qed simp
lemma sum_list_map_num_funs_subst:
assumes "sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts) = sum_list (map num_funs ts)"
shows "∀i < length ts. num_funs (ts ! i ⋅ σ) = num_funs (ts ! i)"
using assms
proof (induct ts)
case (Cons t ts)
then have "num_funs (t ⋅ σ) + sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts)
= num_funs t + sum_list (map num_funs ts)" by (simp add: o_def)
moreover have "num_funs (t ⋅ σ) ≥ num_funs t" by (metis num_funs_subst)
moreover have "sum_list (map (num_funs ∘ (λt. t ⋅ σ)) ts) ≥ sum_list (map num_funs ts)"
using num_funs_subst [of _ σ] by (induct ts) (auto intro: add_mono)
ultimately show ?case using Cons by (auto) (case_tac i, auto)
qed simp
lemma subst_size_emv:
assumes "s = t ⋅ τ" and "num_syms s = num_syms t" and "num_funs s = num_funs t"
shows "emv s t"
using assms
proof (induct t arbitrary: s)
case (Var x)
then show ?case by (force elim: num_funs_0)
next
case (Fun g ts)
note IH = this
show ?case
proof (cases s)
case (Var x)
then show ?thesis using Fun by simp
next
case (Fun f ss)
from IH(2-) [unfolded Fun]
and sum_list_map_num_syms_subst [of τ ts]
and sum_list_map_num_funs_subst [of τ ts]
have "∀i < length ts. num_syms (ts ! i ⋅ τ) = num_syms (ts ! i)"
and "∀i < length ts. num_funs (ts ! i ⋅ τ) = num_funs (ts ! i)"
by auto
with Fun and IH show ?thesis by auto
qed
qed
lemma subsumeseq_term_size_emv:
assumes "s ⋅≥ t" and "num_syms s = num_syms t" and "num_funs s = num_funs t"
shows "emv s t"
using assms(1) and subst_size_emv [OF _ assms(2-)] by (cases) simp
lemma emv_subst_vars_term:
assumes "emv s t"
and "s = t ⋅ σ"
shows "vars_term s = (the_Var ∘ σ) ` vars_term t"
using assms [unfolded subsumeseq_term_iff]
apply (induct)
apply (auto simp: in_set_conv_nth iff: image_iff)
apply (metis nth_mem)
by (metis comp_apply imageI nth_mem)
lemma emv_subst_imp_num_unique_vars_le:
assumes "emv s t"
and "s = t ⋅ σ"
shows "num_unique_vars s ≤ num_unique_vars t"
using emv_subst_vars_term [OF assms]
apply (simp add: num_unique_vars_def)
by (metis card_image_le finite_vars_term)
lemma emv_subsumeseq_term_imp_num_unique_vars_le:
assumes "emv s t"
and "s ⋅≥ t"
shows "num_unique_vars s ≤ num_unique_vars t"
using assms(2) and emv_subst_imp_num_unique_vars_le [OF assms(1)] by (cases) simp
lemma num_syms_ge_num_unique_vars:
"num_syms t ≥ num_unique_vars t"
by (metis le_trans num_syms_geq_num_vars num_vars_geq_num_unique_vars)
lemma inc_seq_greater:
fixes f :: "nat seq"
assumes "∀i. f i < f (Suc i)"
shows "∃i. f i > N"
using assms
apply (induct N)
apply (auto)
apply (metis neq0_conv)
by (metis Suc_lessI)
lemma num_syms_num_unique_vars_clash:
assumes "∀i. num_syms (f i) = num_syms (f (Suc i))"
and "∀i. num_unique_vars (f i) < num_unique_vars (f (Suc i))"
shows False
proof -
have *: "∀i j. i ≤ j ⟶ num_syms (f i) = num_syms (f j)"
proof (intro allI impI)
fix i j :: nat
assume "i ≤ j"
then show "num_syms (f i) = num_syms (f j)"
using assms(1)
apply (induct "j - i" arbitrary: i)
apply auto
by (metis Suc_diff_diff diff_zero less_eq_Suc_le order.not_eq_order_implies_strict)
qed
have "∃i. num_unique_vars (f i) ≥ num_syms (f 0)"
using inc_seq_greater [OF assms(2), of "num_syms (f 0)"] by (metis nat_less_le)
then obtain i where "num_unique_vars (f i) ≥ num_syms (f 0)" by auto
with * and assms(2) have "num_unique_vars (f (Suc i)) > num_syms (f (Suc i))"
by (metis le0 le_antisym num_syms_ge_num_unique_vars)
then show False
by (metis less_Suc_eq_le not_less_eq num_syms_ge_num_unique_vars)
qed
lemma bij_Var_subst_compose_Var:
assumes "bij g"
shows "(Var ∘ g) ∘⇩s (Var ∘ inv g) = Var"
proof
fix x
show "((Var ∘ g) ∘⇩s (Var ∘ inv g)) x = Var x"
using assms
apply (auto simp: subst_compose_def)
by (metis UNIV_I bij_is_inj inv_into_f_f)
qed
lemma emv_subst_imp_is_Var:
assumes "emv s t"
and "s = t ⋅ σ"
shows "∀x ∈ vars_term t. is_Var (σ x)"
using assms
apply (induct)
apply auto
by (metis in_set_conv_nth)
lemma wf_subsumes:
"wf ({<⋅} :: ('f, 'v) term rel)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain f :: "('f, 'v) term seq"
where strict: "∀i. f i ⋅> f (Suc i)"
by (metis mem_Collect_eq case_prodD wf_iff_no_infinite_down_chain)
then have *: "∀i. f i ⋅≥ f (Suc i)" by (metis term_subsumable.subsumption.less_imp_le)
then have "∀i. num_syms (f i) ≥ num_syms (f (Suc i))"
by (auto simp: subsumeseq_term_iff) (metis num_syms_subst)
from down_chain_imp_eq [OF this] obtain N
where N_syms: "∀i > N. num_syms (f i) = num_syms (f (Suc i))" ..
define g where "g i = f (i + N)" for i
from * have "∀i. num_funs (g i) ≥ num_funs (g (Suc i))"
by (auto simp: subsumeseq_term_iff g_def) (metis num_funs_subst)
from down_chain_imp_eq [OF this] obtain K
where K_funs: "∀i > K. num_funs (g i) = num_funs (g (Suc i))" ..
define M where "M = max K N"
have strict_g: "∀i > M. g i ⋅> g (Suc i)" using strict by (simp add: g_def M_def)
have g: "∀i > M. g i ⋅≥ g (Suc i)" using * by (simp add: g_def M_def)
moreover have "∀i > M. num_funs (g i) = num_funs (g (Suc i))"
using K_funs unfolding M_def by (metis max_less_iff_conj)
moreover have syms: "∀i > M. num_syms (g i) = num_syms (g (Suc i))"
using N_syms unfolding M_def g_def
by (metis add_Suc_right add_lessD1 add_strict_left_mono add.commute)
ultimately have emv: "∀i > M. emv (g i) (g (Suc i))" by (metis subsumeseq_term_size_emv)
then have "∀i > M. num_unique_vars (g (Suc i)) ≥ num_unique_vars (g i)"
using emv_subsumeseq_term_imp_num_unique_vars_le and g by fast
then obtain i where "i > M"
and nuv: "num_unique_vars (g (Suc i)) = num_unique_vars (g i)"
using num_syms_num_unique_vars_clash [of "λi. g (i + Suc M)"] and syms
by (metis add_Suc_right add_Suc_shift le_eq_less_or_eq less_add_Suc2)
define s and t where "s = g i" and "t = g (Suc i)"
from nuv have card: "card (vars_term s) = card (vars_term t)"
by (simp add: num_unique_vars_def s_def t_def)
from g [THEN spec, THEN mp, OF ‹i > M›] obtain σ
where "s = t ⋅ σ" by (cases) (auto simp: s_def t_def)
then have "emv s t" and "vars_term s = (the_Var ∘ σ) ` vars_term t"
using emv_subst_vars_term [of s t σ] and emv and ‹i > M› by (auto simp: s_def t_def)
with card have "card ((the_Var ∘ σ) ` vars_term t) = card (vars_term t)" by simp
from finite_card_eq_imp_bij_betw [OF finite_vars_term this]
have "bij_betw (the_Var ∘ σ) (vars_term t) ((the_Var ∘ σ) ` vars_term t)" .
from bij_betw_extend [OF this, of UNIV]
obtain h where *: "∀x∈vars_term t. h x = (the_Var ∘ σ) x"
and "finite {x. h x ≠ x}"
and "bij h" by auto
then have perm: "h ∈ perms" by (auto simp: perms_def)
have "∀x∈vars_term t. (Var ∘ h) x = σ x"
proof
fix x
assume "x ∈ vars_term t"
with * have "h x = (the_Var ∘ σ) x" by simp
with emv_subst_imp_is_Var [OF ‹emv s t› ‹s = t ⋅ σ›] ‹x ∈ vars_term t›
show "(Var ∘ h) x = σ x" by simp
qed
then have "t ⋅ (Var ∘ h) = s"
using ‹s = t ⋅ σ› by (auto simp: term_subst_eq_conv)
then have "t ⋅ (Var ∘ h) ∘⇩s (Var ∘ inv h) = s ⋅ (Var ∘ inv h)" by auto
then have "t = s ⋅ (Var ∘ inv h)"
unfolding bij_Var_subst_compose_Var [OF ‹bij h›] by simp
then have "t ⋅≥ s" by auto
with strict_g and ‹i > M› show False by (auto simp: s_def t_def term_subsumable.subsumes_def)
qed
subsection ‹The Encompassment Relation›
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