Quelle  Unification.thy   Sprache: Isabelle

(*  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, M\N)]" 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 "(\v\vars_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, M\N)]" 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 "\v\vars_of (N \ \1) \ vars_of (N' \ \1). elim \2 v"
    then obtain v 
      where "v\vars_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 "\v\vars_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 "(\v\vars_of M \ vars_of M'. elim \ v)"
    then obtain v 
      where "elim \ v" 
      and "v\vars_of M \ vars_of M'" by auto
    with unify_vars[OF inner]
    have "vars_of (N\\) \ vars_of (N'\\)
      ⊂ vars_of (M⋅N) ∪ 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 (\\<^sub>1 \ \\<^sub>2) \ range_vars \\<^sub>1 \ range_vars \\<^sub>2"
proof (rule subsetI)
  fix x assume "x \ range_vars (\\<^sub>1 \ \\<^sub>2)"
  then obtain x' where
    x'_\\<^sub>1_\\<^sub>2: "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 \\<^sub>1 \ range_vars \\<^sub>2"
  proof (cases "Var x' \ \\<^sub>1 = Var x'")
    case True
    with x'_\\<^sub>1_\\<^sub>2 x_in show ?thesis
      unfolding range_vars_def by auto
  next
    case x'_\\<^sub>1_neq: False
    show ?thesis
    proof (cases "Var x' \ \\<^sub>1 \ \\<^sub>2 = Var x' \ \\<^sub>1")
      case True
      with x'_\\<^sub>1_\\<^sub>2 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' \ \\<^sub>1)" and "x \ vars_of (Var y \ \\<^sub>2)"
        by (metis (no_types, lifting) UN_E UN_simps(10) vars_of_subst_conv_Union)
      with x'_\\<^sub>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 \\<^sub>1" and "unify (N \ \\<^sub>1) (N' \ \\<^sub>1) = Some \\<^sub>2" and "\ = \\<^sub>1 \ \\<^sub>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 \\<^sub>1 \ vars_of M \ vars_of M'"
    using ‹unify M M' = Some \\<^sub>1\ by simp

  from "7.hyps"(2) have "range_vars \\<^sub>2 \ vars_of (N \ \\<^sub>1) \ vars_of (N' \ \\<^sub>1)"
    using ‹unify M M' = Some \\<^sub>1\ \unify (N \ \\<^sub>1) (N' ⊲ θ🚫1) = Some θ🚫2› by simp
  hence range_θ🚫2: "range_vars \\<^sub>2 \ vars_of N \ vars_of N' \ range_vars \\<^sub>1"
    using vars_of_subst_subset[of _ θ🚫1] by auto

  have "range_vars \ = range_vars (\\<^sub>1 \ \\<^sub>2)"
    unfolding ‹σ = θ🚫1 ◊ θ🚫2› by simp
  also have "... \ range_vars \\<^sub>1 \ range_vars \\<^sub>2"
    by (rule range_vars_comp_subset)
  also have "... \ range_vars \\<^sub>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 \\<^sub>1" and "unify (N \ \\<^sub>1) (N' \ \\<^sub>1) = Some \\<^sub>2" and "\ = \\<^sub>1 \ \\<^sub>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 \\<^sub>1 \ vars_of M \ vars_of M'"
    using ‹unify M M' = Some \\<^sub>1\ by simp

  from "7.hyps"(2) have "fst ` set \\<^sub>2 \ vars_of (N \ \\<^sub>1) \ vars_of (N' \ \\<^sub>1)"
    using ‹unify M M' = Some \\<^sub>1\ \unify (N \ \\<^sub>1) (N' ⊲ θ🚫1) = Some θ🚫2› by simp
  hence dom_θ🚫2: "fst ` set \\<^sub>2 \ vars_of N \ vars_of N' \ range_vars \\<^sub>1"
    using vars_of_subst_subset[of _ θ🚫1] by auto

  have "fst ` set \ = fst ` set (\\<^sub>1 \ \\<^sub>2)"
    unfolding ‹σ = θ🚫1 ◊ θ🚫2› by simp
  also have "... = fst ` set \\<^sub>1 \ fst ` set \\<^sub>2"
    by (auto simp: domain_comp)
  also have "... \ vars_of M \ vars_of M' \ fst ` set \\<^sub>2"
    using dom_θ🚫1 by auto
  also have "... \ vars_of M \ vars_of M' \ vars_of N \ vars_of N' \ range_vars \\<^sub>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 \\<^sub>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