Theory First_Order_Terms.Unification

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

theory Unification
  imports
    Abstract_Unification
    Option_Monad
    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)"
  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)

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"
      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: ✐‹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⇧*"
        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

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]
  by (simp add: is_imgu_def unifiers_def)

lemma mgu_same: "mgu t t = Some Var" ✐‹contributor ‹Martin Desharnais››
  by (simp add: mgu_def unify_same)

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 γ"
    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: ✐‹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 γ"
    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: ✐‹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 τ = τ"
    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: ✐‹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 τ = τ"
    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: ✐‹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))"
    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

(* 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: 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 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