Theory First_Order_Terms.Unification
subsection ‹A Concrete Unification Algorithm›
theory Unification
imports
Abstract_Unification
Option_Monad
Renaming2
Subterm_and_Context
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]:
"decompose (Fun f ss) (Fun f ss) = Some (zip ss ss)"
by (simp add: decompose_def)
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)
lemma set_subst_list [simp]:
"set (subst_list σ E) = subst_set σ (set E)"
by (simp add: subst_list_def subst_set_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)+
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)
lemma not_elem_subst_of:
assumes "x ∉ set (map fst xs)"
shows "(subst_of xs) x = Var x"
using assms proof (induct xs)
case (Cons y xs)
then show ?case unfolding subst_of_simps
by (metis Term.term.simps(17) insert_iff list.simps(15) list.simps(9) singletonD subst_compose subst_ident)
qed simp
lemma subst_of_id:
assumes "⋀s. s ∈ (set ss) ⟶ (∃x t. s = (x, t) ∧ t = Var x)"
shows "subst_of ss = Var"
using assms proof(induct ss)
case (Cons s ss)
then obtain y t where s:"s = (y, t)" and t:"t = Var y"
by (metis list.set_intros(1))
from Cons have "subst_of ss = Var"
by simp
then show ?case
unfolding subst_of_def foldr.simps o_apply s t by simp
qed simp
lemma subst_of_apply:
assumes "(x, t) ∈ set ss"
and "∀(y,s) ∈ set ss. (y = x ⟶ s = t)"
and "set (map fst ss) ∩ vars_term t = {}"
shows "subst_of ss x = t"
using assms proof(induct ss)
case (Cons a ss)
show ?case proof(cases "(x,t) ∈ set ss")
case True
from Cons(1)[OF True] Cons(3,4) have sub:"subst_of ss x = t"
by (simp add: disjoint_iff)
from Cons(2,4) have "fst a ∉ vars_term t"
by fastforce
then show ?thesis
unfolding subst_of_simps subst_compose sub by simp
next
case False
then have "x ∉ set (map fst ss)"
using Cons(3) by auto
then have sub:"subst_of ss x = Var x"
by (meson not_elem_subst_of)
from Cons(2) False have "a = (x, t)"
by simp
then show ?thesis
unfolding subst_of_simps subst_compose sub by simp
qed
qed simp
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⇧*"
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 add_mset_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 "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⇧*"
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 **
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)
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⇧*"
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 **
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
lemma unify_append_prefix_same:
"(∀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"
by (simp add: Cons e_def)
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"
by (simp add: E_def)
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:
"fst e = snd e ⟹ unify (e # es) bs = unify es bs"
by (rule unify_append_prefix_same[of "[_]", simplified])
corollary unify_same:
"(∀e ∈ set es. fst e = snd e) ⟹ unify es bs = Some bs"
by (rule unify_append_prefix_same[of _ "[]", simplified])
lemma unify_equation_same:
assumes "fst e = snd e"
shows "unify (E1@e#E2) ys = unify (E1@E2) ys"
using assms
proof (induction "E1@e#E2" ys arbitrary: E1 E2 e ys rule: unify.induct)
case (2 f ss g ts E bs)
show ?case proof(cases E1)
case Nil
with 2(3) show ?thesis
by (simp add: unify_Cons_same)
next
case (Cons e1 es1)
then have e1:"e1 = (Fun f ss, Fun g ts)"
using 2(2) by simp
show ?thesis proof(cases "decompose (Fun f ss) (Fun g ts)")
case None
then show ?thesis unfolding Cons e1 by simp
next
case (Some us)
have us:"us @ E = (us @ es1) @ e # E2"
using 2(2) Cons e1 by simp
from 2(1)[OF Some us 2(3)] show ?thesis unfolding Cons e1 append_Cons unify.simps Some by simp
qed
qed
next
case (3 x t E bs)
show ?case
proof(cases E1)
case Nil
with 3(4) show ?thesis
by (simp add: unify_Cons_same)
next
case (Cons e1 es1)
with 3(3) have e1:"e1 = (Var x, t)"
by simp
with 3(3) Cons have E:"E = es1 @ e # E2"
by simp
show ?thesis proof(cases "t = Var x")
case True
from 3(1)[OF True E 3(4)] show ?thesis
unfolding Cons e1 True by simp
next
case False
then show ?thesis proof(cases "x ∉ vars_term t")
case True
let ?σ="(subst x t)"
have substs:"subst_list ?σ E = (subst_list ?σ es1) @ (fst e ⋅ ?σ, snd e ⋅ ?σ) # (subst_list ?σ E2)"
unfolding E by (simp add: subst_list_def)
from 3(2)[OF False True substs] 3(4) show ?thesis
unfolding Cons e1 append_Cons unify.simps using False True
by (smt (verit, ccfv_SIG) E fst_eqD snd_eqD subst_list_append substs)
next
case False
then show ?thesis
unfolding Cons e1 append_Cons unify.simps using 3 Cons by auto
qed
qed
qed
next
case (4 f ts x E bs)
show ?case
proof(cases E1)
case Nil
with 4(3) show ?thesis
by (simp add: unify_Cons_same)
next
case (Cons e1 es1)
with 4(2) have e1:"e1 = (Fun f ts, Var x)"
by simp
with 4(2) Cons have E:"E = es1 @ e # E2"
by simp
show ?thesis proof(cases "x ∉ vars_term (Fun f ts)")
case True
let ?σ="(subst x (Fun f ts))"
have substs:"subst_list ?σ E = (subst_list ?σ es1) @ (fst e ⋅ ?σ, snd e ⋅ ?σ) # (subst_list ?σ E2)"
unfolding E by (simp add: subst_list_def)
from 4(1)[OF True substs] 4(3) show ?thesis
unfolding Cons e1 append_Cons unify.simps using True
by (metis E fst_conv snd_conv subst_list_append substs)
next
case False
then show ?thesis
unfolding Cons e1 append_Cons unify.simps using 4 Cons by auto
qed
qed
qed simp
lemma unify_filter_same:
shows "unify (filter (λe. fst e ≠ snd e) E) ys = unify E ys"
proof(induction "length E" arbitrary:E rule:full_nat_induct)
case 1
show ?case
proof(cases E)
case (Cons e es)
then show ?thesis
proof(cases "filter (λe. fst e ≠ snd e) E = E")
case False
then obtain E1 e E2 where E:"E = E1 @ e # E2" and eq:"fst e = snd e"
by (meson filter_True split_list)
with unify_equation_same have "unify E ys = unify (E1 @ E2) ys"
by blast
moreover from 1 E have "unify (filter (λe. fst e ≠ snd e) (E1 @ E2)) ys = unify (E1 @ E2) ys"
by (metis (no_types, lifting) add_Suc_right length_Cons length_append order_refl)
moreover have "filter (λe. fst e ≠ snd e) E = filter (λe. fst e ≠ snd e) (E1 @ E2)"
unfolding E using eq by auto
ultimately show ?thesis
by presburger
qed simp
qed simp
qed
lemma unify_ctxt_same:
shows "unify ((C⟨s⟩, C⟨t⟩)#xs) ys = unify ((s, t)#xs) ys"
proof(induct C)
case (More f ss1 C ss2)
let ?us="zip (ss1 @ C⟨s⟩ # ss2) (ss1 @ C⟨t⟩ # ss2)"
have decomp:"decompose (Fun f (ss1 @ C⟨s⟩ # ss2)) (Fun f (ss1 @ C⟨t⟩ # ss2)) = Some ?us"
unfolding decompose_def by (simp add: zip_option_zip_conv)
have unif:"unify (((More f ss1 C ss2)⟨s⟩, (More f ss1 C ss2)⟨t⟩) # xs) ys = unify (?us @ xs) ys"
unfolding intp_actxt.simps unify.simps decomp by simp
have *:"?us = (zip ss1 ss1) @ (C⟨s⟩, C⟨t⟩) # (zip ss2 ss2)"
by simp
have filter_us:"filter (λe. fst e ≠ snd e) ?us = filter (λe. fst e ≠ snd e) [(C⟨s⟩, C⟨t⟩)]"
unfolding * filter_append filter.simps by (smt (verit, ccfv_SIG) filter_False in_set_zip self_append_conv2)
have "filter (λe. fst e ≠ snd e) (?us@xs) = filter (λe. fst e ≠ snd e) ((C⟨s⟩, C⟨t⟩)#xs)"
unfolding filter_append filter_us filter.simps by simp
with More have "unify (?us @ xs) ys = unify ((s, t)#xs) ys"
using unify_filter_same by (smt (verit, ccfv_threshold))
with unif show ?case by simp
qed simp
corollary ex_unify_if_unifiers_not_empty:
"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:
"unifiers {(t,u)} ≠ {} ⟹ ∃μ. mgu t u = Some μ"
using mgu_complete by auto
corollary ex_mgu_if_subst_apply_term_eq_subst_apply_term:
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:
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:
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:
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:
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:
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:
assumes mgu_t_u: "mgu t u = Some μ"
shows "t ⋅ μ = u ⋅ μ"
using mgu_sound[OF mgu_t_u]
by (simp add: is_imgu_def unifiers_def)
lemma mgu_same: "mgu t t = Some Var"
by (simp add: mgu_def unify_same)
lemma mgu_is_Var_if_not_in_equations:
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 γ"
by (simp_all add: is_mgu_def)
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"
by (simp add: τ_def)
thus "is_Var (μ x)"
by (metis subst_apply_eq_Var subst_compose term.disc(1))
qed
corollary mgu_ball_is_Var:
"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:
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 γ"
by (simp_all add: is_mgu_def)
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]
by (simp_all add: τ_def)
with ‹μ x = μ y› show "x = y"
by (simp add: eval_subst_def)
qed
lemma imgu_subst_domain_subset:
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 τ = τ"
by (simp_all add: is_imgu_def)
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"
by (simp add: subst_domain_def)
show "x ∈ Evars"
proof (cases "x ∈ subst_domain τ")
case True
thus ?thesis
using dom_τ by auto
next
case False
hence "τ x = Var x"
by (simp add: subst_domain_def)
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:
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 τ = τ"
by (simp_all add: is_imgu_def)
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
by (simp add: SUP_le_iff)
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_τ
by (auto simp add: subst_domain_def)
thus ?thesis
unfolding eval_subst_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:
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))"
by (simp add: range_vars_def)
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
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: eval_subst_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: eval_subst_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 eval_subst_def, simp)
} 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])
text ‹A lemma for variable disjoint unification where a renaming function is
applied on the right term ‹t› when trying to unify ‹s› and ‹t›.›
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_subst 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
end