# Theory Subsumption

```(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
*)
section ‹Subsumption›

text ‹We define the subsumption relation on terms and prove its well-foundedness.›

theory Subsumption
imports
Term
"Abstract-Rewriting.Seq"
Fun_More
Seq_More
begin

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 INSTANCEEQ_SET ("{⋅≥}")
where
"{⋅≥} ≡ {(x, y). y ≤⋅ x}"

abbreviation INSTANCE_SET ("{⋅>}")
where
"{⋅>} ≡ {(x, y). y <⋅ x}"

abbreviation SUBSUMESEQ_SET ("{≤⋅}")
where
"{≤⋅} ≡ {(x, y). x ≤⋅ y}"

abbreviation SUBSUMES_SET ("{<⋅}")
where
"{<⋅} ≡ {(x, y). x <⋅ y}"

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

SUBSUMESEQ subsumeseq

definition "subsumes t s ⟷ t ≤⋅ s ∧ ¬ s ≤⋅ t"

definition "litsim s t ⟷ s ≤⋅ t ∧ t ≤⋅ s"

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 "(≤⋅)" "(<⋅)"
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"

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)+

SUBSUMES term_subsumable.subsumes and
LITSIM term_subsumable.litsim

lemma subsumeseq_term_iff:
"s ⋅≥ t ⟷ (∃σ. s = t ⋅ σ)"
by auto

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_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 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)

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 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 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]
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_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_unique_vars_Fun_Cons:
"num_unique_vars (Fun f (t # ts)) ≤ num_unique_vars t + num_unique_vars (Fun f ts)"
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

lemma num_unique_vars_Var_1 [simp]:
"num_unique_vars (Var x) = 1"

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_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 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 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 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

subsection ‹Well-foundedness›

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
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
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
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

end
```