Theory HOL-ex.Unification

(*  Title:      HOL/ex/Unification.thy
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Author:     Konrad Slind, TUM & Cambridge University Computer Laboratory
    Author:     Alexander Krauss, TUM
*)

section ‹Substitution and Unification›

theory Unification
imports Main
begin

text ‹
  Implements Manna \& Waldinger's formalization, with Paulson's
  simplifications, and some new simplifications by Slind and Krauss.

  Z Manna \& R Waldinger, Deductive Synthesis of the Unification
  Algorithm.  SCP 1 (1981), 5-48

  L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
  (1985), 143-170

  K Slind, Reasoning about Terminating Functional Programs,
  Ph.D. thesis, TUM, 1999, Sect. 5.8

  A Krauss, Partial and Nested Recursive Function Definitions in
  Higher-Order Logic, JAR 44(4):303-336, 2010. Sect. 6.3
›


subsection ‹Terms›

text ‹Binary trees with leaves that are constants or variables.›

datatype 'a trm = 
  Var 'a 
  | Const 'a
  | Comb "'a trm" "'a trm" (infix "" 60)

primrec vars_of :: "'a trm  'a set"
where
  "vars_of (Var v) = {v}"
| "vars_of (Const c) = {}"
| "vars_of (M  N) = vars_of M  vars_of N"

fun occs :: "'a trm  'a trm  bool" (infixl "" 54) 
where
  "u  Var v  False"
| "u  Const c  False"
| "u  M  N  u = M  u = N  u  M  u  N"


lemma finite_vars_of[intro]: "finite (vars_of t)"
  by (induct t) simp_all

lemma vars_iff_occseq: "x  vars_of t  Var x  t  Var x = t"
  by (induct t) auto

lemma occs_vars_subset: "M  N  vars_of M  vars_of N"
  by (induct N) auto

lemma size_less_size_if_occs: "t  u  size t < size u"
proof (induction u arbitrary: t)
  case (Comb u1 u2)
  thus ?case by fastforce
qed simp_all

corollary neq_if_occs: "t  u  t  u"
  using size_less_size_if_occs by auto

subsection ‹Substitutions›

type_synonym 'a subst = "('a × 'a trm) list"

fun assoc :: "'a  'b  ('a × 'b) list  'b"
where
  "assoc x d [] = d"
| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"

primrec subst :: "'a trm  'a subst  'a trm" (infixl "" 55)
where
  "(Var v)  s = assoc v (Var v) s"
| "(Const c)  s = (Const c)"
| "(M  N)  s = (M  s)  (N  s)"

definition subst_eq (infixr "" 52)
where
  "s1  s2  (t. t  s1 = t  s2)" 

fun comp :: "'a subst  'a subst  'a subst" (infixl "" 56)
where
  "[]  bl = bl"
| "((a,b) # al)  bl = (a, b  bl) # (al  bl)"

lemma subst_Nil[simp]: "t  [] = t"
by (induct t) auto

lemma subst_mono: "t  u  t  s  u  s"
by (induct u) auto

lemma agreement: "(t  r = t  s)  (v  vars_of t. Var v  r = Var v  s)"
by (induct t) auto

lemma repl_invariance: "v  vars_of t  t  (v,u) # s = t  s"
by (simp add: agreement)

lemma remove_var: "v  vars_of s  v  vars_of (t  [(v, s)])"
by (induct t) simp_all

lemma subst_refl[iff]: "s  s"
  by (auto simp:subst_eq_def)

lemma subst_sym[sym]: "s1  s2  s2  s1"
  by (auto simp:subst_eq_def)

lemma subst_trans[trans]: "s1  s2; s2  s3  s1  s3"
  by (auto simp:subst_eq_def)

lemma subst_no_occs: "¬ Var v  t  Var v  t
   t  [(v,s)] = t"
by (induct t) auto

lemma comp_Nil[simp]: "σ  [] = σ"
by (induct σ) auto

lemma subst_comp[simp]: "t  (r  s) = t  r  s"
proof (induct t)
  case (Var v) thus ?case
    by (induct r) auto
qed auto

lemma subst_eq_intro[intro]: "(t. t  σ = t  θ)  σ  θ"
  by (auto simp:subst_eq_def)

lemma subst_eq_dest[dest]: "s1  s2  t  s1 = t  s2"
  by (auto simp:subst_eq_def)

lemma comp_assoc: "(a  b)  c  a  (b  c)"
  by auto

lemma subst_cong: "σ  σ'; θ  θ'  (σ  θ)  (σ'  θ')"
  by (auto simp: subst_eq_def)

lemma var_self: "[(v, Var v)]  []"
proof
  fix t show "t  [(v, Var v)] = t  []"
    by (induct t) simp_all
qed

lemma var_same[simp]: "[(v, t)]  []  t = Var v"
by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)

lemma vars_of_subst_conv_Union: "vars_of (t  η) = (vars_of ` (λx. Var x  η) ` vars_of t)"
  by (induction t) simp_all

lemma domain_comp: "fst ` set (σ  θ) = fst ` (set σ  set θ)"
  by (induction σ θ rule: comp.induct) auto

subsection ‹Unifiers and Most General Unifiers›

definition Unifier :: "'a subst  'a trm  'a trm  bool"
  where "Unifier σ t u  (t  σ = u  σ)"

lemma not_occs_if_Unifier:
  assumes "Unifier σ t u"
  shows "¬ (t  u)  ¬ (u  t)"
proof -
  from assms have "t  σ = u  σ"
    unfolding Unifier_def by simp
  thus ?thesis
    using neq_if_occs subst_mono by metis
qed

definition MGU :: "'a subst  'a trm  'a trm  bool" where
  "MGU σ t u  
   Unifier σ t u  (θ. Unifier θ t u  (γ. θ  σ  γ))"

lemma MGUI[intro]:
  "t  σ = u  σ; θ. t  θ = u  θ  γ. θ  σ  γ
   MGU σ t u"
  by (simp only:Unifier_def MGU_def, auto)

lemma MGU_sym[sym]:
  "MGU σ s t  MGU σ t s"
  by (auto simp:MGU_def Unifier_def)

lemma MGU_is_Unifier: "MGU σ t u  Unifier σ t u"
unfolding MGU_def by (rule conjunct1)

lemma MGU_Var: 
  assumes "¬ Var v  t"
  shows "MGU [(v,t)] (Var v) t"
proof (intro MGUI exI)
  show "Var v  [(v,t)] = t  [(v,t)]" using assms
    by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
next
  fix θ assume th: "Var v  θ = t  θ" 
  show "θ  [(v,t)]  θ" 
  proof
    fix s show "s  θ = s  [(v,t)]  θ" using th 
      by (induct s) auto
  qed
qed

lemma MGU_Const: "MGU [] (Const c) (Const d)  c = d"
  by (auto simp: MGU_def Unifier_def)
  

subsection ‹The unification algorithm›

function unify :: "'a trm  'a trm  'a subst option"
where
  "unify (Const c) (M  N)   = None"
| "unify (M  N)   (Const c) = None"
| "unify (Const c) (Var v)   = Some [(v, Const c)]"
| "unify (M  N)   (Var v)   = (if Var v  M  N 
                                        then None
                                        else Some [(v, M  N)])"
| "unify (Var v)   M         = (if Var v  M
                                        then None
                                        else Some [(v, M)])"
| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
| "unify (M  N) (M'  N') = (case unify M M' of
                                    None  None |
                                    Some θ  (case unify (N  θ) (N'  θ)
                                      of None  None |
                                         Some σ  Some (θ  σ)))"
  by pat_completeness auto

subsection ‹Properties used in termination proof›

text ‹Elimination of variables by a substitution:›

definition
  "elim σ v  t. v  vars_of (t  σ)"

lemma elim_intro[intro]: "(t. v  vars_of (t  σ))  elim σ v"
  by (auto simp:elim_def)

lemma elim_dest[dest]: "elim σ v  v  vars_of (t  σ)"
  by (auto simp:elim_def)

lemma elim_eq: "σ  θ  elim σ x = elim θ x"
  by (auto simp:elim_def subst_eq_def)

lemma occs_elim: "¬ Var v  t 
   elim [(v,t)] v  [(v,t)]  []"
by (metis elim_intro remove_var var_same vars_iff_occseq)

text ‹The result of a unification never introduces new variables:›

declare unify.psimps[simp]

lemma unify_vars: 
  assumes "unify_dom (M, N)"
  assumes "unify M N = Some σ"
  shows "vars_of (t  σ)  vars_of M  vars_of N  vars_of t"
  (is "?P M N σ t")
using assms
proof (induct M N arbitrary:σ t)
  case (3 c v) 
  hence "σ = [(v, Const c)]" by simp
  thus ?case by (induct t) auto
next
  case (4 M N v) 
  hence "¬ Var v  M  N" by auto
  with 4 have "σ = [(v, MN)]" by simp
  thus ?case by (induct t) auto
next
  case (5 v M)
  hence "¬ Var v  M" by auto
  with 5 have "σ = [(v, M)]" by simp
  thus ?case by (induct t) auto
next
  case (7 M N M' N' σ)
  then obtain θ1 θ2 
    where "unify M M' = Some θ1"
    and "unify (N  θ1) (N'  θ1) = Some θ2"
    and σ: "σ = θ1  θ2"
    and ih1: "t. ?P M M' θ1 t"
    and ih2: "t. ?P (Nθ1) (N'θ1) θ2 t"
    by (auto split:option.split_asm)

  show ?case
  proof
    fix v assume a: "v  vars_of (t  σ)"
    
    show "v  vars_of (M  N)  vars_of (M'  N')  vars_of t"
    proof (cases "v  vars_of M  v  vars_of M'
         v  vars_of N  v  vars_of N'")
      case True
      with ih1 have l:"t. v  vars_of (t  θ1)  v  vars_of t"
        by auto
      
      from a and ih2[where t="t  θ1"]
      have "v  vars_of (N  θ1)  vars_of (N'  θ1) 
         v  vars_of (t  θ1)" unfolding σ
        by auto
      hence "v  vars_of t"
      proof
        assume "v  vars_of (N  θ1)  vars_of (N'  θ1)"
        with True show ?thesis by (auto dest:l)
      next
        assume "v  vars_of (t  θ1)" 
        thus ?thesis by (rule l)
      qed
      
      thus ?thesis by auto
    qed auto
  qed
qed (auto split: if_split_asm)


text ‹The result of a unification is either the identity
substitution or it eliminates a variable from one of the terms:›

lemma unify_eliminates: 
  assumes "unify_dom (M, N)"
  assumes "unify M N = Some σ"
  shows "(vvars_of M  vars_of N. elim σ v)  σ  []"
  (is "?P M N σ")
using assms
proof (induct M N arbitrary:σ)
  case 1 thus ?case by simp
next
  case 2 thus ?case by simp
next
  case (3 c v)
  have no_occs: "¬ Var v  Const c" by simp
  with 3 have "σ = [(v, Const c)]" by simp
  with occs_elim[OF no_occs]
  show ?case by auto
next
  case (4 M N v)
  hence no_occs: "¬ Var v  M  N" by auto
  with 4 have "σ = [(v, MN)]" by simp
  with occs_elim[OF no_occs]
  show ?case by auto 
next
  case (5 v M) 
  hence no_occs: "¬ Var v  M" by auto
  with 5 have "σ = [(v, M)]" by simp
  with occs_elim[OF no_occs]
  show ?case by auto 
next 
  case (6 c d) thus ?case
    by (cases "c = d") auto
next
  case (7 M N M' N' σ)
  then obtain θ1 θ2 
    where "unify M M' = Some θ1"
    and "unify (N  θ1) (N'  θ1) = Some θ2"
    and σ: "σ = θ1  θ2"
    and ih1: "?P M M' θ1"
    and ih2: "?P (Nθ1) (N'θ1) θ2"
    by (auto split:option.split_asm)

  from unify_dom (M  N, M'  N')
  have "unify_dom (M, M')"
    by (rule accp_downward) (rule unify_rel.intros)
  hence no_new_vars: 
    "t. vars_of (t  θ1)  vars_of M  vars_of M'  vars_of t"
    by (rule unify_vars) (rule unify M M' = Some θ1)

  from ih2 show ?case 
  proof 
    assume "vvars_of (N  θ1)  vars_of (N'  θ1). elim θ2 v"
    then obtain v 
      where "vvars_of (N  θ1)  vars_of (N'  θ1)"
      and el: "elim θ2 v" by auto
    with no_new_vars show ?thesis unfolding σ 
      by (auto simp:elim_def)
  next
    assume empty[simp]: "θ2  []"

    have "σ  (θ1  [])" unfolding σ
      by (rule subst_cong) auto
    also have "  θ1" by auto
    finally have "σ  θ1" .

    from ih1 show ?thesis
    proof
      assume "vvars_of M  vars_of M'. elim θ1 v"
      with elim_eq[OF σ  θ1]
      show ?thesis by auto
    next
      note σ  θ1
      also assume "θ1  []"
      finally show ?thesis ..
    qed
  qed
qed

declare unify.psimps[simp del]

subsection ‹Termination proof›

termination unify
proof 
  let ?R = "measures [λ(M,N). card (vars_of M  vars_of N),
                           λ(M, N). size M]"
  show "wf ?R" by simp

  fix M N M' N' :: "'a trm"
  show "((M, M'), (M  N, M'  N'))  ?R" ― ‹Inner call›
    by (rule measures_lesseq) (auto intro: card_mono)

  fix θ                                   ― ‹Outer call›
  assume inner: "unify_dom (M, M')"
    "unify M M' = Some θ"

  from unify_eliminates[OF inner]
  show "((N  θ, N'  θ), (M  N, M'  N')) ?R"
  proof
    ― ‹Either a variable is eliminated \ldots›
    assume "(vvars_of M  vars_of M'. elim θ v)"
    then obtain v 
      where "elim θ v" 
      and "vvars_of M  vars_of M'" by auto
    with unify_vars[OF inner]
    have "vars_of (Nθ)  vars_of (N'θ)
       vars_of (MN)  vars_of (M'N')"
      by auto
    
    thus ?thesis
      by (auto intro!: measures_less intro: psubset_card_mono)
  next
    ― ‹Or the substitution is empty›
    assume "θ  []"
    hence "N  θ = N" 
      and "N'  θ = N'" by auto
    thus ?thesis 
       by (auto intro!: measures_less intro: psubset_card_mono)
  qed
qed


subsection ‹Unification returns a Most General Unifier›

lemma unify_computes_MGU:
  "unify M N = Some σ  MGU σ M N"
proof (induct M N arbitrary: σ rule: unify.induct)
  case (7 M N M' N' σ) ― ‹The interesting case›

  then obtain θ1 θ2 
    where "unify M M' = Some θ1"
    and "unify (N  θ1) (N'  θ1) = Some θ2"
    and σ: "σ = θ1  θ2"
    and MGU_inner: "MGU θ1 M M'" 
    and MGU_outer: "MGU θ2 (N  θ1) (N'  θ1)"
    by (auto split:option.split_asm)

  show ?case
  proof
    from MGU_inner and MGU_outer
    have "M  θ1 = M'  θ1" 
      and "N  θ1  θ2 = N'  θ1  θ2"
      unfolding MGU_def Unifier_def
      by auto
    thus "M  N  σ = M'  N'  σ" unfolding σ
      by simp
  next
    fix σ' assume "M  N  σ' = M'  N'  σ'"
    hence "M  σ' = M'  σ'"
      and Ns: "N  σ' = N'  σ'" by auto

    with MGU_inner obtain δ
      where eqv: "σ'  θ1  δ"
      unfolding MGU_def Unifier_def
      by auto

    from Ns have "N  θ1  δ = N'  θ1  δ"
      by (simp add:subst_eq_dest[OF eqv])

    with MGU_outer obtain ρ
      where eqv2: "δ  θ2  ρ"
      unfolding MGU_def Unifier_def
      by auto
    
    have "σ'  σ  ρ" unfolding σ
      by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
    thus "γ. σ'  σ  γ" ..
  qed
qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: if_split_asm)


subsection ‹Unification returns Idempotent Substitution›

definition Idem :: "'a subst  bool"
where "Idem s  (s  s)  s"

lemma Idem_Nil [iff]: "Idem []"
  by (simp add: Idem_def)

lemma Var_Idem: 
  assumes "~ (Var v  t)" shows "Idem [(v,t)]"
  unfolding Idem_def
proof
  from assms have [simp]: "t  [(v, t)] = t"
    by (metis assoc.simps(2) subst.simps(1) subst_no_occs)

  fix s show "s  [(v, t)]  [(v, t)] = s  [(v, t)]"
    by (induct s) auto
qed

lemma Unifier_Idem_subst: 
  "Idem(r)  Unifier s (t  r) (u  r) 
    Unifier (r  s) (t  r) (u  r)"
by (simp add: Idem_def Unifier_def subst_eq_def)

lemma Idem_comp:
  "Idem r  Unifier s (t  r) (u  r) 
      (!!q. Unifier q (t  r) (u  r)  s  q  q) 
    Idem (r  s)"
  apply (frule Unifier_Idem_subst, blast) 
  apply (force simp add: Idem_def subst_eq_def)
  done

theorem unify_gives_Idem:
  "unify M N  = Some σ  Idem σ"
proof (induct M N arbitrary: σ rule: unify.induct)
  case (7 M M' N N' σ)

  then obtain θ1 θ2 
    where "unify M N = Some θ1"
    and θ2: "unify (M'  θ1) (N'  θ1) = Some θ2"
    and σ: "σ = θ1  θ2"
    and "Idem θ1" 
    and "Idem θ2"
    by (auto split: option.split_asm)

  from θ2 have "Unifier θ2 (M'  θ1) (N'  θ1)"
    by (rule unify_computes_MGU[THEN MGU_is_Unifier])

  with Idem θ1
  show "Idem σ" unfolding σ
  proof (rule Idem_comp)
    fix σ assume "Unifier σ (M'  θ1) (N'  θ1)"
    with θ2 obtain γ where σ: "σ  θ2  γ"
      using unify_computes_MGU MGU_def by blast

    have "θ2  σ  θ2  (θ2  γ)" by (rule subst_cong) (auto simp: σ)
    also have "...  (θ2  θ2)  γ" by (rule comp_assoc[symmetric])
    also have "...  θ2  γ" by (rule subst_cong) (auto simp: Idem θ2[unfolded Idem_def])
    also have "...  σ" by (rule σ[symmetric])
    finally show "θ2  σ  σ" .
  qed
qed (auto intro!: Var_Idem split: option.splits if_splits)


subsection ‹Unification Returns Substitution With Minimal Domain And Range›

definition range_vars where
  "range_vars σ =  {vars_of (Var x  σ) |x. Var x  σ  Var x}"

lemma vars_of_subst_subset: "vars_of (N  σ)  vars_of N  range_vars σ"
proof (rule subsetI)
  fix x assume "x  vars_of (N  σ)"
  thus "x  vars_of N  range_vars σ"
  proof (induction N)
    case (Var y)
    thus ?case
      unfolding range_vars_def vars_of.simps by force
  next
    case (Const y)
    thus ?case
      by simp
  next
    case (Comb N1 N2)
    thus ?case
      by auto
  qed
qed

lemma range_vars_comp_subset: "range_vars (σ1  σ2)  range_vars σ1  range_vars σ2"
proof (rule subsetI)
  fix x assume "x  range_vars (σ1  σ2)"
  then obtain x' where
    x'_σ12: "Var x'  σ1  σ2  Var x'" and x_in: "x  vars_of (Var x'  σ1  σ2)"
    unfolding range_vars_def by auto
  
  show "x  range_vars σ1  range_vars σ2"
  proof (cases "Var x'  σ1 = Var x'")
    case True
    with x'_σ12 x_in show ?thesis
      unfolding range_vars_def by auto
  next
    case x'_σ1_neq: False
    show ?thesis
    proof (cases "Var x'  σ1  σ2 = Var x'  σ1")
      case True
      with x'_σ12 x_in x'_σ1_neq show ?thesis
        unfolding range_vars_def by auto
    next
      case False
      with x_in obtain y where "y  vars_of (Var x'  σ1)" and "x  vars_of (Var y  σ2)"
        by (metis (no_types, lifting) UN_E UN_simps(10) vars_of_subst_conv_Union)
      with x'_σ1_neq show ?thesis
        unfolding range_vars_def by force
    qed
  qed
qed

theorem unify_gives_minimal_range:
  "unify M N  = Some σ  range_vars σ  vars_of M  vars_of N"
proof (induct M N arbitrary: σ rule: unify.induct)
  case (1 c M N)
  thus ?case by simp
next
  case (2 M N c)
  thus ?case by simp
next
  case (3 c v)
  hence "σ = [(v, Const c)]"
    by simp
  thus ?case
    by (simp add: range_vars_def)
next
  case (4 M N v)
  hence "σ = [(v, M  N)]"
    by (metis option.discI option.sel unify.simps(4))
  thus ?case
    by (auto simp: range_vars_def)
next
  case (5 v M)
  hence "σ = [(v, M)]"
    by (metis option.discI option.inject unify.simps(5))
  thus ?case
    by (auto simp: range_vars_def)
next
  case (6 c d)
  hence "σ = []"
    by (metis option.distinct(1) option.sel unify.simps(6))
  thus ?case
    by (simp add: range_vars_def)
next
  case (7 M N M' N')
  from "7.prems" obtain θ1 θ2 where
    "unify M M' = Some θ1" and "unify (N  θ1) (N'  θ1) = Some θ2" and "σ = θ1  θ2"
    apply simp
    by (metis (no_types, lifting) option.case_eq_if option.collapse option.discI option.sel)

  from "7.hyps"(1) have range_θ1: "range_vars θ1  vars_of M  vars_of M'"
    using unify M M' = Some θ1 by simp

  from "7.hyps"(2) have "range_vars θ2  vars_of (N  θ1)  vars_of (N'  θ1)"
    using unify M M' = Some θ1 unify (N  θ1) (N'  θ1) = Some θ2 by simp
  hence range_θ2: "range_vars θ2  vars_of N  vars_of N'  range_vars θ1"
    using vars_of_subst_subset[of _ θ1] by auto

  have "range_vars σ = range_vars (θ1  θ2)"
    unfolding σ = θ1  θ2 by simp
  also have "...  range_vars θ1  range_vars θ2"
    by (rule range_vars_comp_subset)
  also have "...  range_vars θ1  vars_of N  vars_of N'"
    using range_θ2 by auto
  also have "...  vars_of M  vars_of M'  vars_of N  vars_of N'"
    using range_θ1 by auto
  finally show ?case
    by auto
qed

theorem unify_gives_minimal_domain:
  "unify M N  = Some σ  fst ` set σ  vars_of M  vars_of N"
proof (induct M N arbitrary: σ rule: unify.induct)
  case (1 c M N)
  thus ?case
    by simp
next
  case (2 M N c)
  thus ?case
    by simp
next
  case (3 c v)
  hence "σ = [(v, Const c)]"
    by simp
  thus ?case
    by (simp add: dom_def)
next
  case (4 M N v)
  hence "σ = [(v, M  N)]"
    by (metis option.distinct(1) option.inject unify.simps(4))
  thus ?case
    by (simp add: dom_def)
next
  case (5 v M)
  hence "σ = [(v, M)]"
    by (metis option.distinct(1) option.inject unify.simps(5))
  thus ?case
    by (simp add: dom_def)
next
  case (6 c d)
  hence "σ = []"
    by (metis option.distinct(1) option.sel unify.simps(6))
  thus ?case
    by simp
next
  case (7 M N M' N')
  from "7.prems" obtain θ1 θ2 where
    "unify M M' = Some θ1" and "unify (N  θ1) (N'  θ1) = Some θ2" and "σ = θ1  θ2"
    apply simp
    by (metis (no_types, lifting) option.case_eq_if option.collapse option.discI option.sel)

  from "7.hyps"(1) have dom_θ1: "fst ` set θ1  vars_of M  vars_of M'"
    using unify M M' = Some θ1 by simp

  from "7.hyps"(2) have "fst ` set θ2  vars_of (N  θ1)  vars_of (N'  θ1)"
    using unify M M' = Some θ1 unify (N  θ1) (N'  θ1) = Some θ2 by simp
  hence dom_θ2: "fst ` set θ2  vars_of N  vars_of N'  range_vars θ1"
    using vars_of_subst_subset[of _ θ1] by auto

  have "fst ` set σ = fst ` set (θ1  θ2)"
    unfolding σ = θ1  θ2 by simp
  also have "... = fst ` set θ1  fst ` set θ2"
    by (auto simp: domain_comp)
  also have "...  vars_of M  vars_of M'  fst ` set θ2"
    using dom_θ1 by auto
  also have "...  vars_of M  vars_of M'  vars_of N  vars_of N'  range_vars θ1"
    using dom_θ2 by auto
  also have "...  vars_of M  vars_of M'  vars_of N  vars_of N'"
    using unify_gives_minimal_range[OF unify M M' = Some θ1] by auto
  finally show ?case
    by auto
qed


subsection ‹Idempotent Most General Unifier›

definition IMGU :: "'a subst  'a trm  'a trm  bool" where
  "IMGU μ t u  Unifier μ t u  (θ. Unifier θ t u  θ  μ  θ)"

lemma IMGU_iff_Idem_and_MGU: "IMGU μ t u  Idem μ  MGU μ t u"
  unfolding IMGU_def Idem_def MGU_def
  by (meson Unification.comp_assoc subst_cong subst_refl subst_sym subst_trans)

lemma unify_computes_IMGU:
  "unify M N = Some σ  IMGU σ M N"
  by (simp add: IMGU_iff_Idem_and_MGU unify_computes_MGU unify_gives_Idem)


subsection ‹Unification is complete›

lemma unify_eq_Some_if_Unifier:
  assumes "Unifier σ t u"
  shows "τ. unify t u = Some τ"
  using assms
proof (induction t u rule: unify.induct)
  case (1 c M N)
  thus ?case
    by (simp add: Unifier_def)
next
  case (2 M N c)
  thus ?case
    by (simp add: Unifier_def)
next
  case (3 c v)
  thus ?case
    by simp
next
  case (4 M N v)
  hence "¬ (Var v  M  N)"
    by (auto dest: not_occs_if_Unifier)
  thus ?case
    by simp
next
  case (5 v M)
  thus ?case
    by (auto dest: not_occs_if_Unifier)
next
  case (6 c d)
  thus ?case
    by (simp add: Unifier_def)
next
  case (7 M N M' N')
  from "7.prems" have "Unifier σ M M'"
    by (simp add: Unifier_def)
  with "7.IH"(1) obtain τ where τ: "unify M M' = Some τ"
    by auto
  then have "Unifier σ (N  τ) (N'  τ)"
    unfolding Unifier_def
    by (metis "7.prems" IMGU_def Unifier_def subst.simps(3) subst_comp subst_eq_def trm.distinct(3) trm.distinct(5) trm.exhaust trm.inject(3) unify_computes_IMGU)
  with τ show ?case
    using "7.IH"(2) by auto
qed

definition subst_domain where
  "subst_domain σ = {x. Var x  σ  Var x}"

lemma subst_domain_subset_list_domain: "subst_domain σ  fst ` set σ"
proof (rule Set.subsetI)
  fix x assume "x  subst_domain σ"
  hence "Var x  σ  Var x"
    by (simp add: subst_domain_def)
  then show "x  fst ` set σ"
  proof (induction σ)
    case Nil
    thus ?case
      by simp
  next
    case (Cons p σ)
    show ?case
    proof (cases "x = fst p")
      case True
      thus ?thesis
        by simp
    next
      case False
      with Cons.IH Cons.prems show ?thesis
        by (cases p) simp
    qed
  qed
qed

lemma subst_apply_eq_Var:
  assumes "s  σ = Var x"
  obtains y where "s = Var y" and "Var y  σ = Var x"
  using assms by (induct s) auto

lemma mem_range_varsI:
  assumes "Var x  σ = Var y" and "x  y"
  shows "y  range_vars σ"
  using assms unfolding range_vars_def
  by (metis (mono_tags, lifting) UnionI mem_Collect_eq trm.inject(1) vars_iff_occseq)

lemma IMGU_subst_domain_subset:
  assumes "IMGU μ t u"
  shows "subst_domain μ  vars_of t  vars_of u"
proof (rule Set.subsetI)
  from assms have "Unifier μ t u"
    by (simp add: IMGU_def)
  then obtain υ where "unify t u = Some υ"
    using unify_eq_Some_if_Unifier by metis
  hence "Unifier υ t u"
    using MGU_def unify_computes_MGU by blast
  with assms have "υ  μ  υ"
    by (simp add: IMGU_def)

  fix x assume "x  subst_domain μ"
  hence "Var x  μ  Var x"
    by (simp add: subst_domain_def)

  show "x  vars_of t  vars_of u"
  proof (cases "x  subst_domain υ")
    case True
    hence "x  fst ` set υ"
      using subst_domain_subset_list_domain by fast
    thus ?thesis
      using unify_gives_minimal_domain[OF unify t u = Some υ] by auto
  next
    case False
    hence "Var x  υ = Var x"
      by (simp add: subst_domain_def)
    hence "Var x  μ  υ = Var x"
      using υ  μ  υ
      by (metis subst_comp subst_eq_dest)
    then show ?thesis
      apply (rule subst_apply_eq_Var)
      using Var x  μ  Var x
      using unify_gives_minimal_range[OF unify t u = Some υ]
      using mem_range_varsI
      by force
  qed
qed

lemma IMGU_range_vars_subset:
  assumes "IMGU μ t u"
  shows "range_vars μ  vars_of t  vars_of u"
proof (rule Set.subsetI)
  from assms have "Unifier μ t u"
    by (simp add: IMGU_def)
  then obtain υ where "unify t u = Some υ"
    using unify_eq_Some_if_Unifier by metis
  hence "Unifier υ t u"
    using MGU_def unify_computes_MGU by blast
  with assms have "υ  μ  υ"
    by (simp add: IMGU_def)

  have ball_subst_dom: "x  subst_domain υ. vars_of (Var x  υ)  vars_of t  vars_of u"
    using unify_gives_minimal_range[OF unify t u = Some υ]
    using range_vars_def subst_domain_def by fastforce

  fix x assume "x  range_vars μ"
  then obtain y where "x  vars_of (Var y  μ)" and "Var y  μ  Var y"
    by (auto simp: range_vars_def)

  have vars_of_y_υ: "vars_of (Var y  υ)  vars_of t  vars_of u"
    using ball_subst_dom
    by (metis (mono_tags, lifting) IMGU_subst_domain_subset Var y  μ  Var y assms empty_iff
        insert_iff mem_Collect_eq subset_eq subst_domain_def vars_of.simps(1))

  show "x  vars_of t  vars_of u"
  proof (rule ccontr)
    assume "x  vars_of t  vars_of u"
    hence "x  vars_of (Var y  υ)"
      using vars_of_y_υ by blast
    moreover have "x  vars_of (Var y  μ  υ)"
    proof -
      have "Var x  υ = Var x"
        using x  vars_of t  vars_of u
        using IMGU_subst_domain_subset unify t u = Some υ subst_domain_def unify_computes_IMGU
        by fastforce
      thus ?thesis
        by (metis x  vars_of (Var y  μ) subst_mono vars_iff_occseq)
    qed
    ultimately show False
      using υ  μ  υ
      by (metis subst_comp subst_eq_dest)
  qed
qed

end