section ‹A Concrete Unification Algorithm›
theory Unification
imports
Abstract_Unification
"../Auxiliaries/Decomp"
begin
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 set_subst_list [simp]:
"set (subst_list σ E) = subst_set σ (set E)"
by (simp add: subst_list_def subst_set_def)
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 mset_map)
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)+
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"
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 ‹@{const unify} can be simulated by @{const 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 (1 bs)
then show ?case by force
next
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
lemma finite_subst_domain_subst:
"finite (subst_domain (subst x y))"
by simp
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_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
text ‹If @{const unify} gives up, then the given set of equations
cannot be reduced to the empty set by @{const 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⇧*"
by (simp add: unifiable_imp_empty)
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
by auto (metis normalizability_I single_not_empty)
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 **: "t ⊳ Var x" by (metis subterm.le_imp_less_or_eq supteq_Var)
have ?case
proof (cases "unifiable (set E)")
case True
then have "(mset E, {#}) ∈ unif⇧*"
by (simp add: unifiable_imp_empty)
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 supt_imp_not_unifiable [OF supt_stable [OF **], of σ]
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
by (simp add: not_unifiable_imp_not_empty_NF)
qed }
ultimately show ?case by blast
next
case (4 f ss x E bs)
def 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 **: "t ⊳ Var x" by (auto simp: t_def)
have ?case
proof (cases "unifiable (set E)")
case True
then have "(mset E, {#}) ∈ unif⇧*"
by (simp add: unifiable_imp_empty)
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 supt_imp_not_unifiable [OF supt_stable [OF **], of σ]
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
text ‹Computing the mgu of two terms.›
fun 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))"
text ‹Computing the mgu of two terms (to be used if it is guaranteed that
the terms are unifiable).›
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 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 split: option.splits)
then have "is_imgu σ (set [(s, t)])" by (metis unify_sound)
then show ?thesis by simp
qed
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)
then have "unifiers (set [(s, t)]) = {}" by (rule unify_complete)
then show ?thesis by simp
qed
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
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
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_pair ≡ mgu_var_disjoint_generic Inl Inr"
lemma mgu_var_disjoint_pair_sound:
"mgu_var_disjoint_pair s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
by (rule mgu_var_disjoint_generic_sound)
lemma mgu_var_disjoint_pair_complete:
fixes σ :: "('f, 'v, 'v + 'w) gsubst" and τ :: "('f, 'w, 'v + 'w) gsubst"
assumes unif_disj: "s ⋅ σ = t ⋅ τ"
shows "∃μ1 μ2 δ. mgu_var_disjoint_pair 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_pair_instance:
fixes σ :: "('f, 'v) subst" and δ :: "('f, 'v) subst"
assumes unif_disj: "s ⋅ σ = t ⋅ δ"
shows "∃μ1 μ2 τ. mgu_var_disjoint_pair s t = Some (μ1, μ2) ∧
σ = μ1 ∘⇩s τ ∧
δ = μ2 ∘⇩s τ ∧
s ⋅ μ1 = t ⋅ μ2"
proof -
let ?m = "map_vars_subst_ran (Inl :: ('v ⇒ 'v + 'v))"
let ?m' = "map_vars_subst_ran (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_pair_complete[OF id[unfolded map_vars_subst_ran]]
obtain μ1 μ2 τ where mgu: "mgu_var_disjoint_pair 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_subst_ran)
} 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
abbreviation (input) x_var :: "string ⇒ string" where "x_var ≡ Cons (CHR ''x'')"
abbreviation (input) y_var :: "string ⇒ string" where "y_var ≡ Cons (CHR ''y'')"
abbreviation (input) z_var :: "string ⇒ string" where "z_var ≡ Cons (CHR ''z'')"
abbreviation "mgu_var_disjoint_string ≡ mgu_var_disjoint_generic x_var y_var"
lemma mgu_var_disjoint_string_sound:
"mgu_var_disjoint_string s t = Some (γ1, γ2) ⟹ s ⋅ γ1 = t ⋅ γ2"
by (rule mgu_var_disjoint_generic_sound)
lemma mgu_var_disjoint_string_complete:
fixes σ :: "('f, string) subst" and τ :: "('f, string) subst"
assumes unif_disj: "s ⋅ σ = t ⋅ τ"
shows "∃μ1 μ2 δ. mgu_var_disjoint_string 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_right:
fixes s t :: "('f, 'v) term" and σ τ :: "('f, 'v) subst" and T
assumes s: "vars_term s ⊆ S"
and inj: "inj T"
and ST: "S ∩ range T = {}"
and id: "s ⋅ σ = t ⋅ τ"
shows "∃ μ δ. mgu s (map_vars_term T t) = Some μ ∧
s ⋅ σ = s ⋅ μ ⋅ δ ∧
(∀t::('f, 'v) term. t ⋅ τ = map_vars_term T t ⋅ μ ⋅ δ) ∧
(∀x∈S. σ x = μ x ⋅ δ)"
proof -
let ?σ = "λ x. if x ∈ S then σ x else τ ((the_inv T) x)"
let ?t = "map_vars_term T t"
have ids: "s ⋅ σ = s ⋅ ?σ"
by (rule term_subst_eq, insert s, auto)
have "t ⋅ τ = map_vars_term (the_inv T) ?t ⋅ τ"
unfolding map_vars_term_compose o_def using the_inv_f_f[OF inj] by (auto simp: term.map_ident)
also have "... = ?t ⋅ (τ ∘ the_inv T)" unfolding apply_subst_map_vars_term ..
also have "... = ?t ⋅ ?σ"
proof (rule term_subst_eq)
fix x
assume "x ∈ vars_term ?t"
then have "x ∈ T ` UNIV" unfolding term.set_map by auto
then have "x ∉ S" using ST by auto
then show "(τ ∘ the_inv T) x = ?σ x" by simp
qed
finally have idt: "t ⋅ τ = ?t ⋅ ?σ" by simp
from id[unfolded ids idt] have id: "s ⋅ ?σ = ?t ⋅ ?σ" .
with mgu_complete[of s ?t] id obtain μ where μ: "mgu s ?t = Some μ"
unfolding unifiers_def by (cases "mgu s ?t", auto)
from the_mgu[OF id] have id: "s ⋅ μ = map_vars_term T t ⋅ μ" and σ: "?σ = μ ∘⇩s ?σ"
unfolding the_mgu_def μ by auto
have "s ⋅ σ = s ⋅ (μ ∘⇩s ?σ)" unfolding ids using σ by simp
also have "... = s ⋅ μ ⋅ ?σ" by simp
finally have ids: "s ⋅ σ = s ⋅ μ ⋅ ?σ" .
{
fix x
have "τ x = ?σ (T x)" using ST unfolding the_inv_f_f[OF inj] by auto
also have "... = (μ ∘⇩s ?σ) (T x)" using σ by simp
also have "... = μ (T x) ⋅ ?σ" unfolding subst_compose_def by simp
finally have "τ x = μ (T x) ⋅ ?σ" .
} note τ = this
{
fix t :: "('f,'v)term"
have "t ⋅ τ = t ⋅ (λ x. μ (T x) ⋅ ?σ)" unfolding τ[symmetric] ..
also have "... = map_vars_term T t ⋅ μ ⋅ ?σ" unfolding apply_subst_map_vars_term
subst_compose_apply_term_distrib[symmetric]
by (rule term_subst_eq, simp add: subst_compose_def)
finally have "t ⋅ τ = map_vars_term T t ⋅ μ ⋅ ?σ" .
} note idt = this
{
fix x
assume "x ∈ S"
then have "σ x = ?σ x" by simp
also have "... = (μ ∘⇩s ?σ) x" using σ by simp
also have "... = μ x ⋅ ?σ" unfolding subst_compose_def ..
finally have "σ x = μ x ⋅ ?σ" .
} note σ = this
show ?thesis
by (rule exI[of _ μ], rule exI[of _ ?σ], insert μ ids idt σ, auto)
qed
lemma mgu_var_disjoint_right_string:
fixes s t :: "('f, string) term" and σ τ :: "('f, string) subst"
assumes s: "vars_term s ⊆ range x_var ∪ range z_var"
and id: "s ⋅ σ = t ⋅ τ"
shows "∃ μ δ. mgu s (map_vars_term y_var t) = Some μ ∧
s ⋅ σ = s ⋅ μ ⋅ δ ∧ (∀t::('f, string) term. t ⋅ τ = map_vars_term y_var t ⋅ μ ⋅ δ) ∧
(∀x ∈ range x_var ∪ range z_var. σ x = μ x ⋅ δ)"
proof -
have inj: "inj y_var" unfolding inj_on_def by simp
show ?thesis
by (rule mgu_var_disjoint_right[OF s inj _ id], auto)
qed
lemma mgu_finite_subst_domain:
"mgu s t = Some σ ⟹ finite (subst_domain σ)"
by (cases "unify [(s, t)] []")
(auto simp: finite_subst_domain_subst_of)
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 [simp]: "subst_of xs = σ"
using assms by (simp split: option.splits)
from unify_Some_UNIF [OF *] obtain ss
where "compose ss = σ" and "UNIF ss {#(s, t)#} {#}" by auto
with UNIF_subst_domain_subset [of ss "{#(s, t)#}" "{#}"]
show ?thesis by simp
qed
end