section ‹Sets of Unifiers›
theory Unifiers
imports
Term
begin
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 ‹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 γ))"
lemma is_mguI:
fixes σ :: "('f, 'v) subst"
assumes "∀(s, t) ∈ E. s ⋅ σ = t ⋅ σ"
and "⋀τ :: ('f, 'v) subst. ∀(s, t) ∈ E. s ⋅ τ = t ⋅ τ ⟹ ∃γ :: ('f, 'v) subst. τ = σ ∘⇩s γ"
shows "is_mgu σ E"
using assms by (fastforce simp: is_mgu_def unifiers_def)
text ‹Check whether a set of equations is unifiable.›
definition "unifiable E ⟷ (∃σ. σ ∈ unifiers E)"
text ‹The following property characterizes idempotent mgus, i.e., mgus
@{term σ} for which @{term "σ ∘⇩s σ = σ"}.›
definition is_imgu :: "('f, 'v) subst ⇒ ('f, 'v) equations ⇒ bool" where
"is_imgu σ E ⟷ σ ∈ unifiers E ∧ (∀τ ∈ unifiers E. τ = σ ∘⇩s τ)"
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)
lemma member_unifiersE [elim]:
"⟦σ ∈ unifiers E; (⋀e. e ∈ E ⟹ fst e ⋅ σ = snd e ⋅ σ) ⟹ P⟧ ⟹ P"
by (force simp: unifiers_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_Un [simp]:
"unifiers (s ∪ t) = unifiers s ∩ unifiers t"
by (auto simp: unifiers_def)
lemma unifiers_insert: -- "simp not added for readability (and termination)"
"unifiers (insert p t) = {σ. fst p ⋅ σ = snd p ⋅ σ} ∩ unifiers t"
by (auto simp: unifiers_def)
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_empty [simp]:
"unifiers {} = UNIV"
by (auto simp: unifiers_def)
lemma unifiers_insert_ident [simp]:
"unifiers (insert (t, t) E) = unifiers E"
by (auto simp: unifiers_insert)
lemma subst_set_insert [simp]:
"subst_set σ (insert e E) = insert (fst e ⋅ σ, snd e ⋅ σ) (subst_set σ E)"
by (auto simp: subst_set_def)
lemma unifiers_subst_set [simp]:
"τ ∈ unifiers (subst_set σ E) ⟷ σ ∘⇩s τ ∈ unifiers E"
by (auto simp: unifiers_def subst_set_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_insert_VarD:
shows "σ ∈ unifiers (insert (Var x, t) E) ⟹ subst x t ∘⇩s σ = σ"
and "σ ∈ unifiers (insert (t, Var x) E) ⟹ subst x t ∘⇩s σ = σ"
using assms by (auto simp: unifiers_def)
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_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: subst_compose unifiers_insert)
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_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 unifiable_UnD [dest]:
"unifiable (M ∪ N) ⟹ unifiable M ∧ unifiable N"
by (auto simp: unifiable_def)
lemma supt_imp_not_unifiable:
assumes "s ⊳ t"
shows "¬ unifiable {(t, s)}"
proof
assume "unifiable {(t, s)}"
then obtain σ where "σ ∈ unifiers {(t, s)}"
by (auto simp: unifiable_def)
then have "t ⋅ σ = s ⋅ σ" by (auto)
moreover have "s ⋅ σ ⊳ t ⋅ σ"
using assms by (metis instance_no_supt_imp_no_supt)
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 unifiable_insert_Var_swap [simp]:
"unifiable (insert (t, Var x) E) ⟷ unifiable (insert (Var x, t) E)"
by (rule unifiable_insert_swap)
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)
have "t ⊳ Var x" using assms by auto
from supt_stable [OF this]
have "∀σ::('f, 'v) subst. t ⋅ σ ≠ Var x ⋅ σ" by (auto simp: supt_supteq_conv)
moreover assume "¬ ?thesis"
ultimately show False by (simp add: unifiers_def) metis
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
lemma unifiers_Int1 [simp]:
"(s, t) ∈ E ⟹ unifiers {(s, t)} ∩ unifiers E = unifiers E"
by (auto simp: unifiers_def)
lemma imgu_linear_var_disjoint:
assumes "is_imgu σ {(l2 |_ p, l1)}"
and "p ∈ poss l2"
and "linear_term l2"
and "vars_term l1 ∩ vars_term l2 = {}"
and "q ∈ poss l2"
and "parallel_pos p q"
shows "l2 |_ q = l2 |_ q ⋅ σ"
using assms
proof (induct p arbitrary: q l2)
case (PCons i p)
from this(3) obtain f ls where
l2[simp]: "l2 = Fun f ls" and
i: "i < length ls" and
p: "p ∈ poss (ls ! i)"
by (cases l2) (auto)
then have l2i: "l2 |_ i <# p = ls ! i |_ p" by auto
have "linear_term (ls ! i)" using PCons(4) l2 i by simp
moreover have "vars_term l1 ∩ vars_term (ls ! i) = {}" using PCons(5) l2 i by force
ultimately have IH: "⋀q. q ∈ poss (ls ! i) ⟹ p ⊥ q ⟹ ls ! i |_ q = ls ! i |_ q ⋅ σ"
using PCons(1)[OF PCons(2)[unfolded l2i] p] by blast
from PCons(7) obtain j q' where q: "q = j <# q'" by (cases q) auto
show ?case
proof (cases "j = i")
case True with PCons(6,7) IH q show ?thesis by simp
next
case False
from PCons(6) q have j: "j < length ls" by simp
{ fix y
assume y: "y ∈ vars_term (l2 |_ q)"
let ?τ = "λx. if x = y then Var y else σ x"
from y PCons(6) q j have yj:"y ∈ vars_term (ls ! j)"
by simp (meson subt_at_imp_supteq subteq_Var_imp_in_vars_term supteq_Var supteq_trans)
{ fix i j
assume j:"j < length ls" and i:"i < length ls" and neq: "i ≠ j"
from j PCons(4) have "∀i < j. vars_term (ls ! i) ∩ vars_term (ls ! j) = {}"
by (auto simp : is_partition_def)
moreover from i PCons(4) have "∀j < i. vars_term (ls ! i) ∩ vars_term (ls ! j) = {}"
by (auto simp : is_partition_def)
ultimately have "vars_term (ls ! i) ∩ vars_term (ls ! j) = {}"
using neq by (cases "i < j") auto
}
from this[OF i j False] have "y ∉ vars_term (ls ! i)" using yj by auto
then have "y ∉ vars_term (l2 |_ i <# p)"
by (metis l2i p subt_at_imp_supteq subteq_Var_imp_in_vars_term supteq_Var supteq_trans)
hence "∀x ∈ vars_term (l2 |_ i <# p). ?τ x = σ x" by auto
hence l2τσ: "l2 |_ i <# p ⋅ ?τ = l2 |_ i <# p ⋅ σ" using term_subst_eq[of _ σ ?τ] by simp
from PCons(5) have "y ∉ vars_term l1" using y PCons(6) vars_term_subt_at by fastforce
then have "∀x ∈ vars_term l1. ?τ x = σ x" by auto
then have l1τσ:"l1 ⋅ ?τ = l1 ⋅ σ" using term_subst_eq[of _ σ ?τ] by simp
have "l1 ⋅ σ = l2 |_ i <# p ⋅ σ" using PCons(2) unfolding is_imgu_def by auto
then have "l1 ⋅ ?τ = l2 |_ i <# p ⋅ ?τ" using l1τσ l2τσ by simp
then have "?τ ∈ unifiers {(l2 |_ i <# p, l1)}" unfolding unifiers_def by simp
with PCons(2) have τσ:"?τ = σ ∘⇩s ?τ" unfolding is_imgu_def by blast
have "Var y = Var y ⋅ σ"
proof (rule ccontr)
let ?x = "Var y ⋅ σ"
assume *:"Var y ≠ ?x"
have "Var y = Var y ⋅ ?τ" by auto
also have "... = (Var y ⋅ σ) ⋅ ?τ" using τσ subst_compose_apply_term_distrib by metis
finally have xy:"?x ⋅ σ = Var y" using * by (cases "σ y") auto
have "σ ∘⇩s σ = σ" using PCons(2) unfolding is_imgu_def by auto
then have "?x ⋅ (σ ∘⇩s σ) = Var y" using xy by auto
moreover have "?x ⋅ σ ⋅ σ = ?x" using xy by auto
ultimately show False using * by auto
qed
}
then show ?thesis by (simp add: term_subst_eq)
qed
qed auto
end