# Theory Unification

```(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
*)
subsection ‹A Concrete Unification Algorithm›

theory Unification
imports
Abstract_Unification
Renaming2
begin

definition
"decompose s t =
(case (s, t) of
(Fun f ss, Fun g ts) ⇒ if f = g then zip_option ss ts else None
| _ ⇒ None)"

lemma decompose_same_Fun[simp]: ✐‹contributor ‹Martin Desharnais››
"decompose (Fun f ss) (Fun f ss) = Some (zip ss ss)"

lemma decompose_Some [dest]:
"decompose (Fun f ss) (Fun g ts) = Some E ⟹
f = g ∧ length ss = length ts ∧ E = zip ss ts"
by (cases "f = g") (auto simp: decompose_def)

lemma decompose_None [dest]:
"decompose (Fun f ss) (Fun g ts) = None ⟹ f ≠ g ∨ length ss ≠ length ts"
by (cases "f = g") (auto simp: decompose_def)

text ‹Applying a substitution to a list of equations.›
definition
subst_list :: "('f, 'v) subst ⇒ ('f, 'v) equation list ⇒ ('f, 'v) equation list"
where
"subst_list σ ys = map (λp. (fst p ⋅ σ, snd p ⋅ σ)) ys"

lemma mset_subst_list [simp]:
"mset (subst_list (subst x t) ys) = subst_mset (subst x t) (mset ys)"
by (auto simp: subst_mset_def subst_list_def)

lemma subst_list_append:
"subst_list σ (xs @ ys) = subst_list σ xs @ subst_list σ ys"
by (auto simp: subst_list_def)

function (sequential)
unify ::
"('f, 'v) equation list ⇒ ('v × ('f, 'v) term) list ⇒ ('v × ('f, 'v) term) list option"
where
"unify [] bs = Some bs"
| "unify ((Fun f ss, Fun g ts) # E) bs =
(case decompose (Fun f ss) (Fun g ts) of
None ⇒ None
| Some us ⇒ unify (us @ E) bs)"
| "unify ((Var x, t) # E) bs =
(if t = Var x then unify E bs
else if x ∈ vars_term t then None
else unify (subst_list (subst x t) E) ((x, t) # bs))"
| "unify ((t, Var x) # E) bs =
(if x ∈ vars_term t then None
else unify (subst_list (subst x t) E) ((x, t) # bs))"
by pat_completeness auto
termination
by (standard, rule wf_inv_image [of "unif¯" "mset ∘ fst", OF wf_converse_unif])
(force intro: UNIF1.intros simp: unif_def union_commute)+

lemma unify_append_prefix_same: ✐‹contributor ‹Martin Desharnais››
"(∀e ∈ set es1. fst e = snd e) ⟹ unify (es1 @ es2) bs = unify es2 bs"
proof (induction "es1 @ es2" bs arbitrary: es1 es2 bs rule: unify.induct)
case (1 bs)
thus ?case by simp
next
case (2 f ss g ts E bs)
show ?case
proof (cases es1)
case Nil
thus ?thesis by simp
next
case (Cons e es1')
hence e_def: "e = (Fun f ss, Fun g ts)" and E_def: "E = es1' @ es2"
using "2" by simp_all
hence "f = g" and "ss = ts"
using "2.prems" local.Cons by auto
hence "unify (es1 @ es2) bs = unify ((zip ts ts @ es1') @ es2) bs"
also have "… = unify es2 bs"
proof (rule "2.hyps"(1))
show "decompose (Fun f ss) (Fun g ts) = Some (zip ts ts)"
by (simp add: ‹f = g› ‹ss = ts›)
next
show "zip ts ts @ E = (zip ts ts @ es1') @ es2"
next
show "∀e∈set (zip ts ts @ es1'). fst e = snd e"
using "2.prems" by (auto simp: Cons zip_same)
qed
finally show ?thesis .
qed
next
case (3 x t E bs)
show ?case
proof (cases es1)
case Nil
thus ?thesis by simp
next
case (Cons e es1')
hence e_def: "e = (Var x, t)" and E_def: "E = es1' @ es2"
using 3 by simp_all
show ?thesis
proof (cases "t = Var x")
case True
show ?thesis
using 3(1)[OF True E_def]
using "3.hyps"(3) "3.prems" local.Cons by fastforce
next
case False
thus ?thesis
using "3.prems" e_def local.Cons by force
qed
qed
next
case (4 v va x E bs)
then show ?case
proof (cases es1)
case Nil
thus ?thesis by simp
next
case (Cons e es1')
hence e_def: "e = (Fun v va, Var x)" and E_def: "E = es1' @ es2"
using 4 by simp_all
thus ?thesis
using "4.prems" local.Cons by fastforce
qed
qed

corollary unify_Cons_same: ✐‹contributor ‹Martin Desharnais››
"fst e = snd e ⟹ unify (e # es) bs = unify es bs"
by (rule unify_append_prefix_same[of "[_]", simplified])

corollary unify_same: ✐‹contributor ‹Martin Desharnais››
"(∀e ∈ set es. fst e = snd e) ⟹ unify es bs = Some bs"
by (rule unify_append_prefix_same[of _ "[]", simplified])

definition subst_of :: "('v × ('f, 'v) term) list ⇒ ('f, 'v) subst"
where
"subst_of ss = List.foldr (λ(x, t) σ. σ ∘⇩s subst x t) ss Var"

text ‹Computing the mgu of two terms.›
definition mgu :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) subst option" where
"mgu s t =
(case unify [(s, t)] [] of
None ⇒ None
| Some res ⇒ Some (subst_of res))"

lemma subst_of_simps [simp]:
"subst_of [] = Var"
"subst_of ((x, Var x) # ss) = subst_of ss"
"subst_of (b # ss) = subst_of ss ∘⇩s subst (fst b) (snd b)"
by (simp_all add: subst_of_def split: prod.splits)

lemma subst_of_append [simp]:
"subst_of (ss @ ts) = subst_of ts ∘⇩s subst_of ss"
by (induct ss) (auto simp: ac_simps)

text ‹The concrete algorithm ‹unify› can be simulated by the inference
rules of ‹UNIF›.›
lemma unify_Some_UNIF:
assumes "unify E bs = Some cs"
shows "∃ds ss. cs = ds @ bs ∧ subst_of ds = compose ss ∧ UNIF ss (mset E) {#}"
using assms
proof (induction E bs arbitrary: cs rule: unify.induct)
case (2 f ss g ts E bs)
then obtain us where "decompose (Fun f ss) (Fun g ts) = Some us"
and [simp]: "f = g" "length ss = length ts" "us = zip ss ts"
and "unify (us @ E) bs = Some cs" by (auto split: option.splits)
from "2.IH" [OF this(1, 5)] obtain xs ys
where "cs = xs @ bs"
and [simp]: "subst_of xs = compose ys"
and *: "UNIF ys (mset (us @ E)) {#}" by auto
then have "UNIF (Var # ys) (mset ((Fun f ss, Fun g ts) # E)) {#}"
by (force intro: UNIF1.decomp simp: ac_simps)
moreover have "cs = xs @ bs" by fact
moreover have "subst_of xs = compose (Var # ys)" by simp
ultimately show ?case by blast
next
case (3 x t E bs)
show ?case
proof (cases "t = Var x")
assume "t = Var x"
then show ?case
using 3 by auto (metis UNIF.step compose_simps(2) UNIF1.trivial)
next
assume "t ≠ Var x"
with 3 obtain xs ys
where [simp]: "cs = (ys @ [(x, t)]) @ bs"
and [simp]: "subst_of ys = compose xs"
and "x ∉ vars_term t"
and "UNIF xs (mset (subst_list (subst x t) E)) {#}"
by (cases "x ∈ vars_term t") force+
then have "UNIF (subst x t # xs) (mset ((Var x, t) # E)) {#}"
by (force intro: UNIF1.Var_left simp: ac_simps)
moreover have "cs = (ys @ [(x, t)]) @ bs" by simp
moreover have "subst_of (ys @ [(x, t)]) = compose (subst x t # xs)" by simp
ultimately show ?case by blast
qed
next
case (4 f ss x E bs)
with 4 obtain xs ys
where [simp]: "cs = (ys @ [(x, Fun f ss)]) @ bs"
and [simp]: "subst_of ys = compose xs"
and "x ∉ vars_term (Fun f ss)"
and "UNIF xs (mset (subst_list (subst x (Fun f ss)) E)) {#}"
by (cases "x ∈ vars_term (Fun f ss)") force+
then have "UNIF (subst x (Fun f ss) # xs) (mset ((Fun f ss, Var x) # E)) {#}"
by (force intro: UNIF1.Var_right simp: ac_simps)
moreover have "cs = (ys @ [(x, Fun f ss)]) @ bs" by simp
moreover have "subst_of (ys @ [(x, Fun f ss)]) = compose (subst x (Fun f ss) # xs)" by simp
ultimately show ?case by blast
qed force

lemma unify_sound:
assumes "unify E [] = Some cs"
shows "is_imgu (subst_of cs) (set E)"
proof -
from unify_Some_UNIF [OF assms] obtain ss
where "subst_of cs = compose ss"
and "UNIF ss (mset E) {#}" by auto
with UNIF_empty_imp_is_mgu_compose [OF this(2)]
and UNIF_idemp [OF this(2)]
show ?thesis
by (auto simp add: is_imgu_def is_mgu_def)
(metis subst_compose_assoc)
qed

lemma mgu_sound:
assumes "mgu s t = Some σ"
shows "is_imgu σ {(s, t)}"
proof -
obtain ss where "unify [(s, t)] [] = Some ss"
and "σ = subst_of ss"
using assms by (auto simp: mgu_def split: option.splits)
then have "is_imgu σ (set [(s, t)])" by (metis unify_sound)
then show ?thesis by simp
qed

text ‹If ‹unify› gives up, then the given set of equations
cannot be reduced to the empty set by ‹UNIF›.›
lemma unify_None:
assumes "unify E ss = None"
shows "∃E'. E' ≠ {#} ∧ (mset E, E') ∈ unif⇧!"
using assms
proof (induction E ss rule: unify.induct)
case (1 bs)
then show ?case by simp
next
case (2 f ss g ts E bs)
moreover
{ assume *: "decompose (Fun f ss) (Fun g ts) = None"
have ?case
proof (cases "unifiable (set E)")
case True
then have "(mset E, {#}) ∈ unif⇧*"
from unif_rtrancl_mono [OF this, of "{#(Fun f ss, Fun g ts)#}"] obtain σ
where "(mset E + {#(Fun f ss, Fun g ts)#}, {#(Fun f ss ⋅ σ, Fun g ts ⋅ σ)#}) ∈ unif⇧*"
by (auto simp: subst_mset_def)
moreover have "{#(Fun f ss ⋅ σ, Fun g ts ⋅ σ)#} ∈ NF unif"
using decompose_None [OF *]
by (auto simp: single_is_union NF_def unif_def elim!: UNIF1.cases)
(metis length_map)
ultimately show ?thesis
next
case False
moreover have "¬ unifiable {(Fun f ss, Fun g ts)}"
using * by (auto simp: unifiable_def)
ultimately have "¬ unifiable (set ((Fun f ss, Fun g ts) # E))" by (auto simp: unifiable_def unifiers_def)
then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF)
qed }
moreover
{ fix us
assume *: "decompose (Fun f ss) (Fun g ts) = Some us"
and "unify (us @ E) bs = None"
from "2.IH" [OF this] obtain E'
where "E' ≠ {#}" and "(mset (us @ E), E') ∈ unif⇧!" by blast
moreover have "(mset ((Fun f ss, Fun g ts) # E), mset (us @ E)) ∈ unif"
proof -
have "g = f" and "length ss = length ts" and "us = zip ss ts"
using * by auto
then show ?thesis
by (auto intro: UNIF1.decomp simp: unif_def ac_simps)
qed
ultimately have ?case by auto }
ultimately show ?case by (auto split: option.splits)
next
case (3 x t E bs)
{ assume [simp]: "t = Var x"
obtain E' where "E' ≠ {#}" and "(mset E, E') ∈ unif⇧!" using 3 by auto
moreover have "(mset ((Var x, t) # E), mset E) ∈ unif"
by (auto intro: UNIF1.trivial simp: unif_def)
ultimately have ?case by auto }
moreover
{ assume *: "t ≠ Var x" "x ∉ vars_term t"
then obtain E' where "E' ≠ {#}"
and "(mset (subst_list (subst x t) E), E') ∈ unif⇧!" using 3 by auto
moreover have "(mset ((Var x, t) # E), mset (subst_list (subst x t) E)) ∈ unif"
using * by (auto intro: UNIF1.Var_left simp: unif_def)
ultimately have ?case by auto }
moreover
{ assume *: "t ≠ Var x" "x ∈ vars_term t"
then have "x ∈ vars_term t" "is_Fun t" by auto
then have "¬ unifiable {(Var x, t)}" by (rule in_vars_is_Fun_not_unifiable)
then have **: "¬ unifiable {(Var x ⋅ σ, t ⋅ σ)}" for σ :: "('b, 'a) subst"
using subst_set_reflects_unifiable [of σ "{(Var x, t)}"] by (auto simp: subst_set_def)
have ?case
proof (cases "unifiable (set E)")
case True
then have "(mset E, {#}) ∈ unif⇧*"
from unif_rtrancl_mono [OF this, of "{#(Var x, t)#}"] obtain σ
where "(mset E + {#(Var x, t)#}, {#(Var x ⋅ σ, t ⋅ σ)#}) ∈ unif⇧*"
by (auto simp: subst_mset_def)
moreover obtain E' where "E' ≠ {#}"
and "({#(Var x ⋅ σ, t ⋅ σ)#}, E') ∈ unif⇧!"
using not_unifiable_imp_not_empty_NF and **
by (metis set_mset_single)
ultimately show ?thesis by auto
next
case False
moreover have "¬ unifiable {(Var x, t)}"
using * by (force simp: unifiable_def)
ultimately have "¬ unifiable (set ((Var x, t) # E))" by (auto simp: unifiable_def unifiers_def)
then show ?thesis
qed }
ultimately show ?case by blast
next
case (4 f ss x E bs)
define t where "t = Fun f ss"
{ assume *: "x ∉ vars_term t"
then obtain E' where "E' ≠ {#}"
and "(mset (subst_list (subst x t) E), E') ∈ unif⇧!" using 4 by (auto simp: t_def)
moreover have "(mset ((t, Var x) # E), mset (subst_list (subst x t) E)) ∈ unif"
using * by (auto intro: UNIF1.Var_right simp: unif_def)
ultimately have ?case by (auto simp: t_def) }
moreover
{ assume "x ∈ vars_term t"
then have *: "x ∈ vars_term t" "t ≠ Var x" by (auto simp: t_def)
then have "x ∈ vars_term t" "is_Fun t" by auto
then have "¬ unifiable {(Var x, t)}" by (rule in_vars_is_Fun_not_unifiable)
then have **: "¬ unifiable {(Var x ⋅ σ, t ⋅ σ)}" for σ :: "('b, 'a) subst"
using subst_set_reflects_unifiable [of σ "{(Var x, t)}"] by (auto simp: subst_set_def)
have ?case
proof (cases "unifiable (set E)")
case True
then have "(mset E, {#}) ∈ unif⇧*"
from unif_rtrancl_mono [OF this, of "{#(t, Var x)#}"] obtain σ
where "(mset E + {#(t, Var x)#}, {#(t ⋅ σ, Var x ⋅ σ)#}) ∈ unif⇧*"
by (auto simp: subst_mset_def)
moreover obtain E' where "E' ≠ {#}"
and "({#(t ⋅ σ, Var x ⋅ σ)#}, E') ∈ unif⇧!"
using not_unifiable_imp_not_empty_NF and **
by (metis unifiable_insert_swap set_mset_single)
ultimately show ?thesis by (auto simp: t_def)
next
case False
moreover have "¬ unifiable {(t, Var x)}"
using * by (simp add: unifiable_def)
ultimately have "¬ unifiable (set ((t, Var x) # E))" by (auto simp: unifiable_def unifiers_def)
then show ?thesis by (simp add: not_unifiable_imp_not_empty_NF t_def)
qed }
ultimately show ?case by blast
qed

lemma unify_complete:
assumes "unify E bs = None"
shows "unifiers (set E) = {}"
proof -
from unify_None [OF assms] obtain E'
where "E' ≠ {#}" and "(mset E, E') ∈ unif⇧!" by blast
then have "¬ unifiable (set E)"
using irreducible_reachable_imp_not_unifiable by force
then show ?thesis
by (auto simp: unifiable_def)
qed

corollary ex_unify_if_unifiers_not_empty: ✐‹contributor ‹Martin Desharnais››
"unifiers es ≠ {} ⟹ set xs = es ⟹ ∃ys. unify xs [] = Some ys"
using unify_complete by auto

lemma mgu_complete:
"mgu s t = None ⟹ unifiers {(s, t)} = {}"
proof -
assume "mgu s t = None"
then have "unify [(s, t)] [] = None" by (cases "unify [(s, t)] []", auto simp: mgu_def)
then have "unifiers (set [(s, t)]) = {}" by (rule unify_complete)
then show ?thesis by simp
qed

corollary ex_mgu_if_unifiers_not_empty: ✐‹contributor ‹Martin Desharnais››
"unifiers {(t,u)} ≠ {} ⟹ ∃μ. mgu t u = Some μ"
using mgu_complete by auto

corollary ex_mgu_if_subst_apply_term_eq_subst_apply_term: ✐‹contributor ‹Martin Desharnais››
fixes t u :: "('f, 'v) Term.term" and σ :: "('f, 'v) subst"
assumes t_eq_u: "t ⋅ σ = u ⋅ σ"
shows "∃μ :: ('f, 'v) subst. Unification.mgu t u = Some μ"
proof -
from t_eq_u have "unifiers {(t, u)} ≠ {}"
unfolding unifiers_def by auto
thus ?thesis
by (rule ex_mgu_if_unifiers_not_empty)
qed

lemma finite_subst_domain_subst_of:
"finite (subst_domain (subst_of xs))"
proof (induct xs)
case (Cons x xs)
moreover have "finite (subst_domain (subst (fst x) (snd x)))" by (metis finite_subst_domain_subst)
ultimately show ?case
using subst_domain_compose [of "subst_of xs" "subst (fst x) (snd x)"]
by (simp del: subst_subst_domain) (metis finite_subset infinite_Un)
qed simp

lemma unify_subst_domain: ✐‹contributor ‹Martin Desharnais››
assumes unif: "unify E [] = Some xs"
shows "subst_domain (subst_of xs) ⊆ (⋃e ∈ set E. vars_term (fst e) ∪ vars_term (snd e))"
proof -
from unify_Some_UNIF[OF unif] obtain xs' where
"subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}"
by auto
thus ?thesis
using UNIF_subst_domain_subset
by (metis (mono_tags, lifting) multiset.set_map set_mset_mset vars_mset_def)
qed

lemma mgu_subst_domain:
assumes "mgu s t = Some σ"
shows "subst_domain σ ⊆ vars_term s ∪ vars_term t"
proof -
obtain xs where "unify [(s, t)] [] = Some xs" and "σ = subst_of xs"
using assms by (simp add: mgu_def split: option.splits)
thus ?thesis
using unify_subst_domain by fastforce
qed

lemma mgu_finite_subst_domain:
"mgu s t = Some σ ⟹ finite (subst_domain σ)"
by (drule mgu_subst_domain) (simp add: finite_subset)

lemma unify_range_vars: ✐‹contributor ‹Martin Desharnais››
assumes unif: "unify E [] = Some xs"
shows "range_vars (subst_of xs) ⊆ (⋃e ∈ set E. vars_term (fst e) ∪ vars_term (snd e))"
proof -
from unify_Some_UNIF[OF unif] obtain xs' where
"subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}"
by auto
thus ?thesis
using UNIF_range_vars_subset
by (metis (mono_tags, lifting) multiset.set_map set_mset_mset vars_mset_def)
qed

lemma mgu_range_vars: ✐‹contributor ‹Martin Desharnais››
assumes "mgu s t = Some μ"
shows "range_vars μ ⊆ vars_term s ∪ vars_term t"
proof -
obtain xs where "unify [(s, t)] [] = Some xs" and "μ = subst_of xs"
using assms by (simp add: mgu_def split: option.splits)
thus ?thesis
using unify_range_vars by fastforce
qed

lemma unify_subst_domain_range_vars_disjoint: ✐‹contributor ‹Martin Desharnais››
assumes unif: "unify E [] = Some xs"
shows "subst_domain (subst_of xs) ∩ range_vars (subst_of xs) = {}"
proof -
from unify_Some_UNIF[OF unif] obtain xs' where
"subst_of xs = compose xs'" and "UNIF xs' (mset E) {#}"
by auto
thus ?thesis
using UNIF_subst_domain_range_vars_Int by metis
qed

lemma mgu_subst_domain_range_vars_disjoint: ✐‹contributor ‹Martin Desharnais››
assumes "mgu s t = Some μ"
shows "subst_domain μ ∩ range_vars μ = {}"
proof -
obtain xs where "unify [(s, t)] [] = Some xs" and "μ = subst_of xs"
using assms by (simp add: mgu_def split: option.splits)
thus ?thesis
using unify_subst_domain_range_vars_disjoint by metis
qed

corollary subst_apply_term_eq_subst_apply_term_if_mgu: ✐‹contributor ‹Martin Desharnais››
assumes mgu_t_u: "mgu t u = Some μ"
shows "t ⋅ μ = u ⋅ μ"
using mgu_sound[OF mgu_t_u]

lemma mgu_same: "mgu t t = Some Var" ✐‹contributor ‹Martin Desharnais››

lemma mgu_is_Var_if_not_in_equations: ✐‹contributor ‹Martin Desharnais››
fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and x :: 'v
assumes
mgu_μ: "is_mgu μ E" and
x_not_in: "x ∉ (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e))"
shows "is_Var (μ x)"
proof -
from mgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. ∃γ. τ = μ ∘⇩s γ"

define τ :: "('f, 'v) subst" where
"τ = (λx. if x ∈ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)) then μ x else Var x)"

have ‹τ ∈ unifiers E›
unfolding unifiers_def mem_Collect_eq
proof (rule ballI)
fix e assume "e ∈ E"
with unif_μ have "fst e ⋅ μ = snd e ⋅ μ"
by blast
moreover from ‹e ∈ E› have "fst e ⋅ τ = fst e ⋅ μ" and "snd e ⋅ τ = snd e ⋅ μ"
unfolding term_subst_eq_conv
by (auto simp: τ_def)
ultimately show "fst e ⋅ τ = snd e ⋅ τ"
by simp
qed
with minimal_μ obtain γ where "μ ∘⇩s γ = τ"
by auto
with x_not_in have "(μ ∘⇩s γ) x = Var x"
thus "is_Var (μ x)"
by (metis subst_apply_eq_Var subst_compose term.disc(1))
qed

corollary mgu_ball_is_Var: ✐‹contributor ‹Martin Desharnais››
"is_mgu μ E ⟹ ∀x ∈ - (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e)). is_Var (μ x)"
by (rule ballI) (rule mgu_is_Var_if_not_in_equations[folded Compl_iff])

lemma mgu_inj_on: ✐‹contributor ‹Martin Desharnais››
fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations"
assumes mgu_μ: "is_mgu μ E"
shows "inj_on μ (- (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)))"
proof (rule inj_onI)
fix x y
assume
x_in: "x ∈ - (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e))" and
y_in: "y ∈ - (⋃e∈E. vars_term (fst e) ∪ vars_term (snd e))" and
"μ x = μ y"

from mgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. ∃γ. τ = μ ∘⇩s γ"

define τ :: "('f, 'v) subst" where
"τ = (λx. if x ∈ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)) then μ x else Var x)"

have ‹τ ∈ unifiers E›
unfolding unifiers_def mem_Collect_eq
proof (rule ballI)
fix e assume "e ∈ E"
with unif_μ have "fst e ⋅ μ = snd e ⋅ μ"
by blast
moreover from ‹e ∈ E› have "fst e ⋅ τ = fst e ⋅ μ" and "snd e ⋅ τ = snd e ⋅ μ"
unfolding term_subst_eq_conv
by (auto simp: τ_def)
ultimately show "fst e ⋅ τ = snd e ⋅ τ"
by simp
qed
with minimal_μ obtain γ where "μ ∘⇩s γ = τ"
by auto
hence "(μ ∘⇩s γ) x = Var x" and "(μ ∘⇩s γ) y = Var y"
using ComplD[OF x_in] ComplD[OF y_in]
with ‹μ x = μ y› show "x = y"
qed

lemma imgu_subst_domain_subset: ✐‹contributor ‹Martin Desharnais››
fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set"
assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E"
defines "Evars ≡ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))"
shows "subst_domain μ ⊆ Evars"
proof (intro Set.subsetI)
from imgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. μ ∘⇩s τ = τ"

from fin_E obtain es :: "('f, 'v) equation list" where
"set es = E"
using finite_list by auto
then obtain xs :: "('v × ('f, 'v) Term.term) list" where
unify_es: "unify es [] = Some xs"
using unif_μ ex_unify_if_unifiers_not_empty by blast

define τ :: "('f, 'v) subst" where
"τ = subst_of xs"

have dom_τ: "subst_domain τ ⊆ Evars"
using unify_subst_domain[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] .
have range_vars_τ: "range_vars τ ⊆ Evars"
using unify_range_vars[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] .

have "τ ∈ unifiers E"
using ‹set es = E› unify_es τ_def is_imgu_def unify_sound by blast
with minimal_μ have μ_comp_τ: "⋀x. (μ ∘⇩s τ) x = τ x"
by auto

fix x :: 'v assume "x ∈ subst_domain μ"
hence "μ x ≠ Var x"

show "x ∈ Evars"
proof (cases "x ∈ subst_domain τ")
case True
thus ?thesis
using dom_τ by auto
next
case False
hence "τ x = Var x"
hence "μ x ⋅ τ = Var x"
using μ_comp_τ[of x] by (simp add: subst_compose)
thus ?thesis
proof (rule subst_apply_eq_Var)
show "⋀y. μ x = Var y ⟹ τ y = Var x ⟹ ?thesis"
using ‹μ x ≠ Var x› range_vars_τ mem_range_varsI[of τ _ x] by auto
qed
qed
qed

lemma imgu_range_vars_of_equations_vars_subset: ✐‹contributor ‹Martin Desharnais››
fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set"
assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E"
defines "Evars ≡ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))"
shows "(⋃x ∈ Evars. vars_term (μ x)) ⊆ Evars"
proof (rule Set.subsetI)
from imgu_μ have unif_μ: "μ ∈ unifiers E" and minimal_μ: "∀τ ∈ unifiers E. μ ∘⇩s τ = τ"

from fin_E obtain es :: "('f, 'v) equation list" where
"set es = E"
using finite_list by auto
then obtain xs :: "('v × ('f, 'v) Term.term) list" where
unify_es: "unify es [] = Some xs"
using unif_μ ex_unify_if_unifiers_not_empty by blast

define τ :: "('f, 'v) subst" where
"τ = subst_of xs"

have dom_τ: "subst_domain τ ⊆ Evars"
using unify_subst_domain[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] .
have range_vars_τ: "range_vars τ ⊆ Evars"
using unify_range_vars[OF unify_es, unfolded ‹set es = E›, folded Evars_def τ_def] .
hence ball_vars_apply_τ_subset: "∀x ∈ subst_domain τ. vars_term (τ x) ⊆ Evars"
unfolding range_vars_def

have "τ ∈ unifiers E"
using ‹set es = E› unify_es τ_def is_imgu_def unify_sound by blast
with minimal_μ have μ_comp_τ: "⋀x. (μ ∘⇩s τ) x = τ x"
by auto

fix y :: 'v assume "y ∈ (⋃x ∈ Evars. vars_term (μ x))"
then obtain x :: 'v where
x_in: "x ∈ Evars" and y_in: "y ∈ vars_term (μ x)"
by (auto simp: subst_domain_def)
have vars_τ_x: "vars_term (τ x) ⊆ Evars"
using ball_vars_apply_τ_subset subst_domain_def x_in by fastforce

show "y ∈ Evars"
proof (rule ccontr)
assume "y ∉ Evars"
hence "y ∉ vars_term (τ x)"
using vars_τ_x by blast
moreover have "y ∈ vars_term ((μ ∘⇩s τ) x)"
proof -
have "τ y = Var y"
using ‹y ∉ Evars› dom_τ
thus ?thesis
unfolding subst_compose_def vars_term_subst_apply_term UN_iff
using y_in by force
qed
ultimately show False
using μ_comp_τ[of x] by simp
qed
qed

lemma imgu_range_vars_subset: ✐‹contributor ‹Martin Desharnais››
fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations"
assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E"
shows "range_vars μ ⊆ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))"
proof -
have "range_vars μ = (⋃x ∈ subst_domain μ. vars_term (μ x))"
also have "… ⊆ (⋃x ∈ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e)). vars_term (μ x))"
using imgu_subst_domain_subset[OF imgu_μ fin_E] by fast
also have "… ⊆ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))"
using imgu_range_vars_of_equations_vars_subset[OF imgu_μ fin_E] by metis
finally show ?thesis .
qed

definition the_mgu :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f ,'v) subst" where
"the_mgu s t = (case mgu s t of None ⇒ Var | Some δ ⇒ δ)"

lemma the_mgu_is_imgu:
fixes σ :: "('f, 'v) subst"
assumes "s ⋅ σ = t ⋅ σ"
shows "is_imgu (the_mgu s t) {(s, t)}"
proof -
from assms have "unifiers {(s, t)} ≠ {}" by (force simp: unifiers_def)
then obtain τ where "mgu s t = Some τ"
and "the_mgu s t = τ"
using mgu_complete by (auto simp: the_mgu_def)
with mgu_sound show ?thesis by blast
qed

lemma the_mgu:
fixes σ :: "('f, 'v) subst"
assumes "s ⋅ σ = t ⋅ σ"
shows "s ⋅ the_mgu s t = t ⋅ the_mgu s t ∧ σ = the_mgu s t ∘⇩s σ"
proof -
have *: "σ ∈ unifiers {(s, t)}" by (force simp: assms unifiers_def)
show ?thesis
proof (cases "mgu s t")
assume "mgu s t = None"
then have "unifiers {(s, t)} = {}" by (rule mgu_complete)
with * show ?thesis by simp
next
fix τ
assume "mgu s t = Some τ"
moreover then have "is_imgu τ {(s, t)}" by (rule mgu_sound)
ultimately have "is_imgu (the_mgu s t) {(s, t)}" by (unfold the_mgu_def, simp)
with * show ?thesis by (auto simp: is_imgu_def unifiers_def)
qed
qed

subsubsection ‹Unification of two terms where variables should be considered disjoint›

definition
mgu_var_disjoint_generic ::
"('v ⇒ 'u) ⇒ ('w ⇒ 'u) ⇒ ('f, 'v) term ⇒ ('f, 'w) term ⇒
(('f, 'v, 'u) gsubst × ('f, 'w, 'u) gsubst) option"
where
"mgu_var_disjoint_generic vu wu s t =
(case mgu (map_vars_term vu s) (map_vars_term wu t) of
None ⇒ None
| Some γ ⇒ Some (γ ∘ vu, γ ∘ wu))"

lemma mgu_var_disjoint_generic_sound:
assumes unif: "mgu_var_disjoint_generic vu wu s t = Some (γ1, γ2)"
shows "s ⋅ γ1 = t ⋅ γ2"
proof -
from unif[unfolded mgu_var_disjoint_generic_def] obtain γ where
unif2: "mgu (map_vars_term vu s) (map_vars_term wu t) = Some γ"
by (cases "mgu (map_vars_term vu s) (map_vars_term wu t)", auto)
from mgu_sound[OF unif2[unfolded mgu_var_disjoint_generic_def], unfolded is_imgu_def unifiers_def]
have "map_vars_term vu s ⋅ γ = map_vars_term wu t ⋅ γ" by auto
from this[unfolded apply_subst_map_vars_term] unif[unfolded mgu_var_disjoint_generic_def unif2]
show ?thesis by simp
qed

(* if terms s and t can become identical via two substitutions σ and δ
then mgu_var_disjoint yields two more general substitutions μ1 μ2 *)
lemma mgu_var_disjoint_generic_complete:
fixes σ :: "('f, 'v, 'u) gsubst" and τ :: "('f, 'w, 'u) gsubst"
and vu :: "'v ⇒ 'u" and wu:: "'w ⇒ 'u"
assumes inj: "inj vu" "inj wu"
and vwu: "range vu ∩ range wu = {}"
and unif_disj: "s ⋅ σ = t ⋅ τ"
shows "∃μ1 μ2 δ. mgu_var_disjoint_generic vu wu s t = Some (μ1, μ2) ∧
σ = μ1 ∘⇩s δ ∧
τ = μ2 ∘⇩s δ ∧
s ⋅ μ1 = t ⋅ μ2"
proof -
note inv1[simp] = the_inv_f_f[OF inj(1)]
note inv2[simp] = the_inv_f_f[OF inj(2)]
obtain γ :: "('f,'u)subst" where gamma: "γ = (λ x. if x ∈ range vu then σ (the_inv vu x) else τ (the_inv wu x))" by auto
have ids: "s ⋅ σ = map_vars_term vu s ⋅ γ" unfolding gamma
by (induct s, auto)
have idt: "t ⋅ τ = map_vars_term wu t ⋅ γ" unfolding gamma
by (induct t, insert vwu, auto)
from unif_disj ids idt
have unif: "map_vars_term vu s ⋅ γ = map_vars_term wu t ⋅ γ" (is "?s ⋅ γ = ?t ⋅ γ") by auto
from the_mgu[OF unif] have unif2: "?s ⋅ the_mgu ?s ?t = ?t ⋅ the_mgu ?s ?t" and inst: "γ = the_mgu ?s ?t ∘⇩s γ" by auto
have "mgu ?s ?t = Some (the_mgu ?s ?t)" unfolding the_mgu_def
using mgu_complete[unfolded unifiers_def] unif
by (cases "mgu ?s ?t", auto)
with inst obtain μ where mu: "mgu ?s ?t = Some μ" and gamma_mu: "γ = μ ∘⇩s γ" by auto
let ?tau1 = "μ ∘ vu"
let ?tau2 = "μ ∘ wu"
show ?thesis unfolding mgu_var_disjoint_generic_def mu option.simps
proof (intro exI conjI, rule refl)
show "σ = ?tau1 ∘⇩s γ"
proof (rule ext)
fix x
have "(?tau1 ∘⇩s γ) x = γ (vu x)" using fun_cong[OF gamma_mu, of "vu x"] by (simp add: subst_compose_def)
also have "... = σ x" unfolding gamma by simp
finally show "σ x = (?tau1 ∘⇩s γ) x" by simp
qed
next
show "τ = ?tau2 ∘⇩s γ"
proof (rule ext)
fix x
have "(?tau2 ∘⇩s γ) x = γ (wu x)" using fun_cong[OF gamma_mu, of "wu x"] by (simp add: subst_compose_def)
also have "... = τ x" unfolding gamma using vwu by auto
finally show "τ x = (?tau2 ∘⇩s γ) x" by simp
qed
next
have "s ⋅ ?tau1 = map_vars_term vu s ⋅ μ" unfolding apply_subst_map_vars_term ..
also have "... = map_vars_term wu t ⋅ μ"
unfolding unif2[unfolded the_mgu_def mu option.simps] ..
also have "... = t ⋅ ?tau2" unfolding apply_subst_map_vars_term ..
finally show "s ⋅ ?tau1 = t ⋅ ?tau2" .
qed
qed

abbreviation "mgu_var_disjoint_sum ≡ mgu_var_disjoint_generic Inl Inr"

lemma mgu_var_disjoint_sum_sound:
"mgu_var_disjoint_sum s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
by (rule mgu_var_disjoint_generic_sound)

lemma mgu_var_disjoint_sum_complete:
fixes σ :: "('f, 'v, 'v + 'w) gsubst" and τ :: "('f, 'w, 'v + 'w) gsubst"
assumes unif_disj: "s ⋅ σ = t ⋅ τ"
shows "∃μ1 μ2 δ. mgu_var_disjoint_sum s t = Some (μ1, μ2) ∧
σ = μ1 ∘⇩s δ ∧
τ = μ2 ∘⇩s δ ∧
s ⋅ μ1 = t ⋅ μ2"
by (rule mgu_var_disjoint_generic_complete[OF _ _ _ unif_disj], auto simp: inj_on_def)

lemma mgu_var_disjoint_sum_instance:
fixes σ :: "('f, 'v) subst" and δ :: "('f, 'v) subst"
assumes unif_disj: "s ⋅ σ = t ⋅ δ"
shows "∃μ1 μ2 τ. mgu_var_disjoint_sum s t = Some (μ1, μ2) ∧
σ = μ1 ∘⇩s τ ∧
δ = μ2 ∘⇩s τ ∧
s ⋅ μ1 = t ⋅ μ2"
proof -
let ?map = "λ m σ v. map_vars_term m (σ v)"
let ?m = "?map (Inl :: ('v ⇒ 'v + 'v))"
let ?m' = "?map (case_sum (λ x. x) (λ x. x))"
from unif_disj have id: "map_vars_term Inl (s ⋅ σ) = map_vars_term Inl (t ⋅ δ)" by simp
from mgu_var_disjoint_sum_complete[OF id[unfolded map_vars_term_subst]]
obtain μ1 μ2 τ where mgu: "mgu_var_disjoint_sum s t = Some (μ1,μ2)"
and σ: "?m σ = μ1 ∘⇩s τ"
and δ: "?m δ = μ2 ∘⇩s τ"
and unif: "s ⋅ μ1 = t ⋅ μ2" by blast
{
fix σ :: "('f, 'v) subst"
have "?m' (?m σ) = σ" by (simp add: map_vars_term_compose o_def term.map_ident)
} note id = this
{
fix μ :: "('f,'v,'v+'v)gsubst" and τ :: "('f,'v + 'v)subst"
have "?m' (μ ∘⇩s τ) = μ ∘⇩s ?m' τ"
by (rule ext, unfold subst_compose_def, simp add: map_vars_term_subst)
} note id' = this
from arg_cong[OF σ, of ?m', unfolded id id'] have σ: "σ = μ1 ∘⇩s ?m' τ" .
from arg_cong[OF δ, of ?m', unfolded id id'] have δ: "δ = μ2 ∘⇩s ?m' τ" .
show ?thesis
by (intro exI conjI, rule mgu, rule σ, rule δ, rule unif)
qed

subsubsection ‹A variable disjoint unification algorithm without changing the type›

text ‹We pass the renaming function as additional argument›

definition mgu_vd :: "'v :: infinite renaming2 ⇒ _ ⇒ _" where
"mgu_vd r = mgu_var_disjoint_generic (rename_1 r) (rename_2 r)"

lemma mgu_vd_sound: "mgu_vd r s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
unfolding mgu_vd_def by (rule mgu_var_disjoint_generic_sound)

lemma mgu_vd_complete:
fixes σ :: "('f, 'v :: infinite) subst" and τ :: "('f, 'v) subst"
assumes unif_disj: "s ⋅ σ = t ⋅ τ"
shows "∃μ1 μ2 δ. mgu_vd r s t = Some (μ1, μ2) ∧
σ = μ1 ∘⇩s δ ∧
τ = μ2 ∘⇩s δ ∧
s ⋅ μ1 = t ⋅ μ2"
unfolding mgu_vd_def
by (rule mgu_var_disjoint_generic_complete[OF rename_12 unif_disj])

end
```