Theory Unifiers
section ‹Unification›
subsection ‹Unifiers›
text ‹Definition and properties of (most general) unifiers›
theory Unifiers
imports Term
begin
lemma map_eq_set_zipD [dest]:
assumes "map f xs = map f ys"
and "(x, y) ∈ set (zip xs ys)"
shows "f x = f y"
using assms
proof (induct xs arbitrary: ys)
case (Cons x xs)
then show ?case by (cases ys) auto
qed simp
type_synonym ('f, 'v) equation = "('f, 'v) term × ('f, 'v) term"
type_synonym ('f, 'v) equations = "('f, 'v) equation set"
text ‹The set of unifiers for a given set of equations.›
definition unifiers :: "('f, 'v) equations ⇒ ('f, 'v) subst set"
where
"unifiers E = {σ. ∀p∈E. fst p ⋅ σ = snd p ⋅ σ}"
text ‹Check whether a set of equations is unifiable.›
definition "unifiable E ⟷ (∃σ. σ ∈ unifiers E)"
lemma in_unifiersE [elim]:
"⟦σ ∈ unifiers E; (⋀e. e ∈ E ⟹ fst e ⋅ σ = snd e ⋅ σ) ⟹ P⟧ ⟹ P"
by (force simp: unifiers_def)
text ‹Applying a substitution to a set of equations.›
definition subst_set :: "('f, 'v) subst ⇒ ('f, 'v) equations ⇒ ('f, 'v) equations"
where
"subst_set σ E = (λe. (fst e ⋅ σ, snd e ⋅ σ)) ` E"
text ‹Check whether a substitution is a most-general unifier (mgu) of a set of equations.›
definition is_mgu :: "('f, 'v) subst ⇒ ('f, 'v) equations ⇒ bool"
where
"is_mgu σ E ⟷ σ ∈ unifiers E ∧ (∀τ ∈ unifiers E. (∃γ. τ = σ ∘⇩s γ))"
text ‹The following property characterizes idempotent mgus, that is,
mgus \<^term>‹σ› for which \<^prop>‹σ ∘⇩s σ = σ› holds.›
definition is_imgu :: "('f, 'v) subst ⇒ ('f, 'v) equations ⇒ bool"
where
"is_imgu σ E ⟷ σ ∈ unifiers E ∧ (∀τ ∈ unifiers E. τ = σ ∘⇩s τ)"
subsubsection ‹Properties of sets of unifiers›
lemma unifiers_Un [simp]:
"unifiers (s ∪ t) = unifiers s ∩ unifiers t"
by (auto simp: unifiers_def)
lemma unifiers_empty [simp]:
"unifiers {} = UNIV"
by (auto simp: unifiers_def)
lemma unifiers_insert:
"unifiers (insert p t) = {σ. fst p ⋅ σ = snd p ⋅ σ} ∩ unifiers t"
by (auto simp: unifiers_def)
lemma unifiers_insert_ident [simp]:
"unifiers (insert (t, t) E) = unifiers E"
by (auto simp: unifiers_insert)
lemma unifiers_insert_swap:
"unifiers (insert (s, t) E) = unifiers (insert (t, s) E)"
by (auto simp: unifiers_insert)
lemma unifiers_insert_Var_swap [simp]:
"unifiers (insert (t, Var x) E) = unifiers (insert (Var x, t) E)"
by (rule unifiers_insert_swap)
lemma unifiers_subst_set [simp]:
"τ ∈ unifiers (subst_set σ E) ⟷ σ ∘⇩s τ ∈ unifiers E"
by (auto simp: unifiers_def subst_set_def)
lemma unifiers_insert_VarD:
shows "σ ∈ unifiers (insert (Var x, t) E) ⟹ subst x t ∘⇩s σ = σ"
and "σ ∈ unifiers (insert (t, Var x) E) ⟹ subst x t ∘⇩s σ = σ"
by (auto simp: unifiers_def)
lemma unifiers_insert_Var_left:
"σ ∈ unifiers (insert (Var x, t) E) ⟹ σ ∈ unifiers (subst_set (subst x t) E)"
by (auto simp: unifiers_def subst_set_def)
lemma unifiers_set_zip [simp]:
assumes "length ss = length ts"
shows "unifiers (set (zip ss ts)) = {σ. map (λt. t ⋅ σ) ss = map (λt. t ⋅ σ) ts}"
using assms by (induct ss ts rule: list_induct2) (auto simp: unifiers_def)
lemma unifiers_Fun [simp]:
"σ ∈ unifiers {(Fun f ss, Fun g ts)} ⟷
length ss = length ts ∧ f = g ∧ σ ∈ unifiers (set (zip ss ts))"
by (auto simp: unifiers_def dest: map_eq_imp_length_eq)
(induct ss ts rule: list_induct2, simp_all)
lemma unifiers_occur_left_is_Fun:
fixes t :: "('f, 'v) term"
assumes "x ∈ vars_term t" and "is_Fun t"
shows "unifiers (insert (Var x, t) E) = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain σ :: "('f, 'v) subst" where "σ x = t ⋅ σ" by (auto simp: unifiers_def)
with is_Fun_num_funs_less [OF assms, of σ] show False by auto
qed
lemma unifiers_occur_left_not_Var:
"x ∈ vars_term t ⟹ t ≠ Var x ⟹ unifiers (insert (Var x, t) E) = {}"
using unifiers_occur_left_is_Fun [of x t] by (cases t) simp_all
lemma unifiers_occur_left_Fun:
"x ∈ (⋃t∈set ts. vars_term t) ⟹ unifiers (insert (Var x, Fun f ts) E) = {}"
using unifiers_occur_left_is_Fun [of x "Fun f ts"] by simp
lemmas unifiers_occur_left_simps [simp] =
unifiers_occur_left_is_Fun
unifiers_occur_left_not_Var
unifiers_occur_left_Fun
subsubsection ‹Properties of unifiability›
lemma in_vars_is_Fun_not_unifiable:
assumes "x ∈ vars_term t" and "is_Fun t"
shows "¬ unifiable {(Var x, t)}"
proof
assume "unifiable {(Var x, t)}"
then obtain σ where "σ ∈ unifiers {(Var x, t)}"
by (auto simp: unifiable_def)
then have "σ x = t ⋅ σ" by (auto)
moreover have "num_funs (σ x) < num_funs (t ⋅ σ)"
using is_Fun_num_funs_less [OF assms] by auto
ultimately show False by auto
qed
lemma unifiable_insert_swap:
"unifiable (insert (s, t) E) = unifiable (insert (t, s) E)"
by (auto simp: unifiable_def unifiers_insert_swap)
lemma subst_set_reflects_unifiable:
fixes σ :: "('f, 'v) subst"
assumes "unifiable (subst_set σ E)"
shows "unifiable E"
proof -
{ fix τ :: "('f, 'v) subst" assume "∀p∈E. fst p ⋅ σ ⋅ τ = snd p ⋅ σ ⋅ τ"
then have "∃σ :: ('f, 'v) subst. ∀p∈E. fst p ⋅ σ = snd p ⋅ σ"
by (intro exI [of _ "σ ∘⇩s τ"]) auto }
then show ?thesis using assms by (auto simp: unifiable_def unifiers_def subst_set_def)
qed
subsubsection ‹Properties of \<^term>‹is_mgu››
lemma is_mgu_empty [simp]:
"is_mgu Var {}"
by (auto simp: is_mgu_def)
lemma is_mgu_insert_trivial [simp]:
"is_mgu σ (insert (t, t) E) = is_mgu σ E"
by (auto simp: is_mgu_def)
lemma is_mgu_insert_decomp [simp]:
assumes "length ss = length ts"
shows "is_mgu σ (insert (Fun f ss, Fun f ts) E) ⟷
is_mgu σ (E ∪ set (zip ss ts))"
using assms by (auto simp: is_mgu_def unifiers_insert)
lemma is_mgu_insert_swap:
"is_mgu σ (insert (s, t) E) = is_mgu σ (insert (t, s) E)"
by (auto simp: is_mgu_def unifiers_def)
lemma is_mgu_insert_Var_swap [simp]:
"is_mgu σ (insert (t, Var x) E) = is_mgu σ (insert (Var x, t) E)"
by (rule is_mgu_insert_swap)
lemma is_mgu_subst_set_subst:
assumes "x ∉ vars_term t"
and "is_mgu σ (subst_set (subst x t) E)" (is "is_mgu σ ?E")
shows "is_mgu (subst x t ∘⇩s σ) (insert (Var x, t) E)" (is "is_mgu ?σ ?E'")
proof -
from ‹is_mgu σ ?E›
have "?σ ∈ unifiers E"
and *: "∀τ. (subst x t ∘⇩s τ) ∈ unifiers E ⟶ (∃μ. τ = σ ∘⇩s μ)"
by (auto simp: is_mgu_def)
then have "?σ ∈ unifiers ?E'" using assms by (simp add: unifiers_insert subst_compose)
moreover have "∀τ. τ ∈ unifiers ?E' ⟶ (∃μ. τ = ?σ ∘⇩s μ)"
proof (intro allI impI)
fix τ
assume **: "τ ∈ unifiers ?E'"
then have [simp]: "subst x t ∘⇩s τ = τ" by (blast dest: unifiers_insert_VarD)
from unifiers_insert_Var_left [OF **]
have "subst x t ∘⇩s τ ∈ unifiers E" by (simp)
with * obtain μ where "τ = σ ∘⇩s μ" by blast
then have "subst x t ∘⇩s τ = subst x t ∘⇩s σ ∘⇩s μ" by (auto simp: ac_simps)
then show "∃μ. τ = subst x t ∘⇩s σ ∘⇩s μ" by auto
qed
ultimately show "is_mgu ?σ ?E'" by (simp add: is_mgu_def)
qed
lemma is_imgu_imp_is_mgu:
assumes "is_imgu σ E"
shows "is_mgu σ E"
using assms by (auto simp: is_imgu_def is_mgu_def)
subsubsection ‹Properties of \<^term>‹is_imgu››
lemma rename_subst_domain_range_preserves_is_imgu:
fixes E :: "('f, 'v) equations" and μ ρ :: "('f, 'v) subst"
assumes imgu_μ: "is_imgu μ E" and is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ"
shows "is_imgu (rename_subst_domain_range ρ μ) (subst_set ρ E)"
proof (unfold is_imgu_def, intro conjI ballI)
from imgu_μ have unif_μ: "μ ∈ unifiers E"
by (simp add: is_imgu_def)
show "rename_subst_domain_range ρ μ ∈ unifiers (subst_set ρ E)"
unfolding unifiers_subst_set unifiers_def mem_Collect_eq
proof (rule ballI)
fix e⇩ρ assume "e⇩ρ ∈ subst_set ρ E"
then obtain e where "e ∈ E" and "e⇩ρ = (fst e ⋅ ρ, snd e ⋅ ρ)"
by (auto simp: subst_set_def)
then show "fst e⇩ρ ⋅ rename_subst_domain_range ρ μ = snd e⇩ρ ⋅ rename_subst_domain_range ρ μ"
using unif_μ subst_apply_term_renaming_rename_subst_domain_range[OF is_var_ρ ‹inj ρ›, of _ μ]
by (simp add: unifiers_def)
qed
next
fix υ :: "('f, 'v) subst"
assume "υ ∈ unifiers (subst_set ρ E)"
hence "(ρ ∘⇩s υ) ∈ unifiers E"
by (simp add: subst_set_def unifiers_def)
with imgu_μ have μ_ρ_υ: "μ ∘⇩s ρ ∘⇩s υ = ρ ∘⇩s υ"
by (simp add: is_imgu_def subst_compose_assoc)
show "υ = rename_subst_domain_range ρ μ ∘⇩s υ"
proof (rule ext)
fix x
show "υ x = (rename_subst_domain_range ρ μ ∘⇩s υ) x"
proof (cases "Var x ∈ ρ ` subst_domain μ")
case True
hence "(rename_subst_domain_range ρ μ ∘⇩s υ) x = (μ ∘⇩s ρ ∘⇩s υ) (the_inv ρ (Var x))"
by (simp add: rename_subst_domain_range_def subst_compose_def)
also have "… = (ρ ∘⇩s υ) (the_inv ρ (Var x))"
by (simp add: μ_ρ_υ)
also have "… = (ρ (the_inv ρ (Var x))) ⋅ υ"
by (simp add: subst_compose)
also have "… = Var x ⋅ υ"
using True f_the_inv_into_f[OF ‹inj ρ›, of "Var x"] by force
finally show ?thesis
by simp
next
case False
thus ?thesis
by (simp add: rename_subst_domain_range_def subst_compose)
qed
qed
qed
corollary rename_subst_domain_range_preserves_is_imgu_singleton:
fixes t u :: "('f, 'v) term" and μ ρ :: "('f, 'v) subst"
assumes imgu_μ: "is_imgu μ {(t, u)}" and is_var_ρ: "∀x. is_Var (ρ x)" and "inj ρ"
shows "is_imgu (rename_subst_domain_range ρ μ) {(t ⋅ ρ, u ⋅ ρ)}"
by (rule rename_subst_domain_range_preserves_is_imgu[OF imgu_μ is_var_ρ ‹inj ρ›,
unfolded subst_set_def, simplified])
end