Theory First_Order_Terms.Term_Pair_Multiset
subsection ‹Multisets of Pairs of Terms›
theory Term_Pair_Multiset
imports
Term
"HOL-Library.Multiset"
begin
text ‹Multisets of pairs of terms are used in abstract inference systems for
matching and unification.›
subsection ‹Size›
text ‹Make sure that every pair has size at least @{term "1::nat"}.›
definition "pair_size p = size (fst p) + size (snd p) + 1"
text ‹Compute the number of symbols in a multiset of term pairs.›
definition "size_mset M = fold_mset ((+) ∘ pair_size) 0 M"
interpretation size_mset_fun:
comp_fun_commute "(+) ∘ pair_size"
by standard auto
lemma fold_pair_size_plus:
"fold_mset ((+) ∘ pair_size) 0 M + n = fold_mset ((+) ∘ pair_size) n M"
by (induct M arbitrary: n) (simp add: size_mset_def)+
lemma size_mset_union [simp]:
"size_mset (M + N) = size_mset N + size_mset M"
by (auto simp: size_mset_def fold_pair_size_plus)
lemma size_mset_add_mset [simp]:
"size_mset (add_mset x M) = pair_size x + (size_mset M)"
by (auto simp: size_mset_def)
lemma nonempty_size_mset [simp]:
assumes "M ≠ {#}"
shows "size_mset M > 0"
using assms by (induct M) (simp add: size_mset_def pair_size_def)+
lemma size_mset_singleton [simp]:
"size_mset {#(l, r)#} = size l + size r + 1"
by (auto simp: size_mset_def pair_size_def)
lemma size_mset_empty [simp]:
"size_mset {#} = 0"
by (auto simp: size_mset_def)
lemma size_mset_set_zip_leq:
"size_mset (mset (zip ss ts)) ≤ size_list size ss + size_list size ts"
proof (induct ss arbitrary: ts)
case (Cons s ss)
then show ?case
by (cases ts) (auto intro: le_SucI simp: pair_size_def)
qed simp
lemma size_mset_Fun_less:
"size_mset {#(Fun f ss, Fun g ts)#} > size_mset (mset (zip ss ts))"
by (auto simp: pair_size_def intro: order_le_less_trans size_mset_set_zip_leq)
lemma decomp_size_mset_less:
assumes "length ss = length ts"
shows "size_mset (M + mset (zip ss ts)) < size_mset (M + {#(Fun f ss, Fun f ts)#})"
using assms and size_mset_Fun_less [of ss ts f f] by simp
subsubsection ‹Substitutions›
text ‹Applying a substitution to a multiset of term pairs.›
definition "subst_mset σ M = image_mset (λp. (fst p ⋅ σ, snd p ⋅ σ)) M"
lemma subst_mset_empty [simp]:
"subst_mset σ {#} = {#}"
by (auto simp: subst_mset_def)
lemma subst_mset_union:
"subst_mset σ (M + N) = subst_mset σ M + subst_mset σ N"
by (auto simp: subst_mset_def)
lemma subst_mset_Var [simp]:
"subst_mset Var M = M"
by (auto simp: subst_mset_def)
lemma subst_mset_subst_compose [simp]:
"subst_mset (σ ∘⇩s τ) M = subst_mset τ (subst_mset σ M)"
by (simp add: subst_mset_def image_mset.compositionality o_def)
subsubsection ‹Variables›
text ‹Compute the set of variables occurring in a multiset of term pairs.›
definition "vars_mset M = ⋃(set_mset (image_mset (λr. vars_term (fst r) ∪ vars_term (snd r)) M))"
lemma vars_mset_singleton [simp]:
"vars_mset {#p#} = vars_term (fst p) ∪ vars_term (snd p)"
by (auto simp: vars_mset_def)
lemma vars_mset_union [simp]:
"vars_mset (A + B) = vars_mset A ∪ vars_mset B"
by (auto simp: vars_mset_def)
lemma vars_mset_add_mset [simp]:
"vars_mset (add_mset x M) = vars_term (fst x) ∪ vars_term (snd x) ∪ vars_mset M"
by (auto simp: vars_mset_def)
lemma vars_mset_set_zip [simp]:
assumes "length xs = length ys"
shows "vars_mset (mset (zip xs ys)) = (⋃x∈set xs ∪ set ys. vars_term x)"
using assms by (induct xs ys rule: list_induct2) (auto simp: vars_mset_def)
lemma not_in_vars_mset_subst_mset [simp]:
assumes "x ∉ vars_term t"
shows "x ∉ vars_mset (subst_mset (subst x t) M)"
using assms by (auto simp: vars_mset_def subst_mset_def vars_term_subst subst_def)
lemma vars_mset_subst_mset_subset:
"vars_mset (subst_mset (subst x t) M) ⊆ vars_mset M ∪ vars_term t ∪ {x}" (is "?L ⊆ ?R")
proof
fix y
assume "y ∈ ?L"
then obtain u v where "(u, v) ∈# M"
and "y ∈ vars_term (u ⋅ subst x t) ∪ vars_term (v ⋅ subst x t)"
by (auto simp: vars_mset_def subst_mset_def)
moreover then have "y ∈ vars_term u ∪ vars_term v ∪ vars_term t"
unfolding vars_term_subst subst_def fun_upd_def
by (auto) (metis empty_iff)+
ultimately show "y ∈ ?R" by (force simp: vars_mset_def)
qed
lemma Var_left_vars_mset_less:
assumes "x ∉ vars_term t"
shows "vars_mset (subst_mset (subst x t) M) ⊂ vars_mset (add_mset (Var x, t) M)" (is "?L ⊂ ?R")
proof
show "?L ⊆ ?R" using vars_mset_subst_mset_subset [of x t M] by (simp add: ac_simps)
next
have "x ∈ ?R" using assms by (force simp: vars_mset_def)
moreover have "x ∉ ?L" using assms by simp
ultimately show "?L ≠ ?R" by blast
qed
lemma Var_right_vars_mset_less:
assumes "x ∉ vars_term t"
shows "vars_mset (subst_mset (subst x t) M) ⊂ vars_mset (add_mset (t, Var x) M)"
using Var_left_vars_mset_less [OF assms] by simp
lemma mem_vars_mset_subst_mset:
assumes "y ∈ vars_mset (subst_mset (subst x t) M)"
and "y ≠ x"
and "y ∉ vars_term t"
shows "y ∈ vars_mset M"
using vars_mset_subst_mset_subset [of x t M] and assms by blast
lemma finite_vars_mset:
"finite (vars_mset A)"
by (auto simp: vars_mset_def)
end