Theory 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


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)


subsection ‹Unifiers and Most General Unifiers›

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

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)

end