Theory Unification

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


header {* 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 "\<prec>" 54)
where
"u \<prec> Var v <-> False"
| "u \<prec> Const c <-> False"
| "u \<prec> M · N <-> u = M ∨ u = N ∨ u \<prec> M ∨ u \<prec> 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 \<prec> t ∨ Var x = t"
by (induct t) auto

lemma occs_vars_subset: "M \<prec> 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 "\<lhd>" 55)
where
"(Var v) \<lhd> s = assoc v (Var v) s"
| "(Const c) \<lhd> s = (Const c)"
| "(M · N) \<lhd> s = (M \<lhd> s) · (N \<lhd> s)"

definition subst_eq (infixr "\<doteq>" 52)
where
"s1 \<doteq> s2 <-> (∀t. t \<lhd> s1 = t \<lhd> s2)"

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

lemma subst_Nil[simp]: "t \<lhd> [] = t"
by (induct t) auto

lemma subst_mono: "t \<prec> u ==> t \<lhd> s \<prec> u \<lhd> s"
by (induct u) auto

lemma agreement: "(t \<lhd> r = t \<lhd> s) <-> (∀v ∈ vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
by (induct t) auto

lemma repl_invariance: "v ∉ vars_of t ==> t \<lhd> (v,u) # s = t \<lhd> s"
by (simp add: agreement)

lemma remove_var: "v ∉ vars_of s ==> v ∉ vars_of (t \<lhd> [(v, s)])"
by (induct t) simp_all

lemma subst_refl[iff]: "s \<doteq> s"
by (auto simp:subst_eq_def)

lemma subst_sym[sym]: "[|s1 \<doteq> s2|] ==> s2 \<doteq> s1"
by (auto simp:subst_eq_def)

lemma subst_trans[trans]: "[|s1 \<doteq> s2; s2 \<doteq> s3|] ==> s1 \<doteq> s3"
by (auto simp:subst_eq_def)

lemma subst_no_occs: "¬ Var v \<prec> t ==> Var v ≠ t
==> t \<lhd> [(v,s)] = t"

by (induct t) auto

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

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

lemma subst_eq_intro[intro]: "(!!t. t \<lhd> σ = t \<lhd> ϑ) ==> σ \<doteq> ϑ"
by (auto simp:subst_eq_def)

lemma subst_eq_dest[dest]: "s1 \<doteq> s2 ==> t \<lhd> s1 = t \<lhd> s2"
by (auto simp:subst_eq_def)

lemma comp_assoc: "(a ◊ b) ◊ c \<doteq> a ◊ (b ◊ c)"
by auto

lemma subst_cong: "[|σ \<doteq> σ'; ϑ \<doteq> ϑ'|] ==> (σ ◊ ϑ) \<doteq> (σ' ◊ ϑ')"
by (auto simp: subst_eq_def)

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

lemma var_same[simp]: "[(v, t)] \<doteq> [] <-> 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 \<lhd> σ = u \<lhd> σ)"

definition MGU :: "'a subst => 'a trm => 'a trm => bool" where
"MGU σ t u <->
Unifier σ t u ∧ (∀ϑ. Unifier ϑ t u --> (∃γ. ϑ \<doteq> σ ◊ γ))"


lemma MGUI[intro]:
"[|t \<lhd> σ = u \<lhd> σ; !!ϑ. t \<lhd> ϑ = u \<lhd> ϑ ==> ∃γ. ϑ \<doteq> σ ◊ γ|]
==> 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 \<prec> t"
shows "MGU [(v,t)] (Var v) t"
proof (intro MGUI exI)
show "Var v \<lhd> [(v,t)] = t \<lhd> [(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 \<lhd> ϑ = t \<lhd> ϑ"
show "ϑ \<doteq> [(v,t)] ◊ ϑ"
proof
fix s show "s \<lhd> ϑ = s \<lhd> [(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 \<prec> M · N
then None
else Some [(v, M · N)])"

| "unify (Var v) M = (if Var v \<prec> 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 \<lhd> ϑ) (N' \<lhd> ϑ)
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 \<lhd> σ)"

lemma elim_intro[intro]: "(!!t. v ∉ vars_of (t \<lhd> σ)) ==> elim σ v"
by (auto simp:elim_def)

lemma elim_dest[dest]: "elim σ v ==> v ∉ vars_of (t \<lhd> σ)"
by (auto simp:elim_def)

lemma elim_eq: "σ \<doteq> ϑ ==> elim σ x = elim ϑ x"
by (auto simp:elim_def subst_eq_def)

lemma occs_elim: "¬ Var v \<prec> t
==> elim [(v,t)] v ∨ [(v,t)] \<doteq> []"

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 \<lhd> σ) ⊆ 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 \<prec> 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 \<prec> 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 \<lhd> ϑ1) (N' \<lhd> ϑ1) = Some ϑ2"
and σ: "σ = ϑ1 ◊ ϑ2"
and ih1: "!!t. ?P M M' ϑ1 t"
and ih2: "!!t. ?P (N\<lhd>ϑ1) (N'\<lhd>ϑ1) ϑ2 t"
by (auto split:option.split_asm)

show ?case
proof
fix v assume a: "v ∈ vars_of (t \<lhd> σ)"

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 \<lhd> ϑ1) ==> v ∈ vars_of t"
by auto

from a and ih2[where t="t \<lhd> ϑ1"]
have "v ∈ vars_of (N \<lhd> ϑ1) ∪ vars_of (N' \<lhd> ϑ1)
∨ v ∈ vars_of (t \<lhd> ϑ1)"
unfolding σ
by auto
hence "v ∈ vars_of t"
proof
assume "v ∈ vars_of (N \<lhd> ϑ1) ∪ vars_of (N' \<lhd> ϑ1)"
with True show ?thesis by (auto dest:l)
next
assume "v ∈ vars_of (t \<lhd> ϑ1)"
thus ?thesis by (rule l)
qed

thus ?thesis by auto
qed auto
qed
qed (auto split: split_if_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) ∨ σ \<doteq> []"
(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 \<prec> 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 \<prec> 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 \<prec> 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 \<lhd> ϑ1) (N' \<lhd> ϑ1) = Some ϑ2"
and σ: "σ = ϑ1 ◊ ϑ2"
and ih1: "?P M M' ϑ1"
and ih2: "?P (N\<lhd>ϑ1) (N'\<lhd>ϑ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 \<lhd> ϑ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 \<lhd> ϑ1) ∪ vars_of (N' \<lhd> ϑ1). elim ϑ2 v"
then obtain v
where "v∈vars_of (N \<lhd> ϑ1) ∪ vars_of (N' \<lhd> ϑ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 \<doteq> []"

have "σ \<doteq> (ϑ1 ◊ [])" unfolding σ
by (rule subst_cong) auto
also have "… \<doteq> ϑ1" by auto
finally have "σ \<doteq> ϑ1" .

from ih1 show ?thesis
proof
assume "∃v∈vars_of M ∪ vars_of M'. elim ϑ1 v"
with elim_eq[OF `σ \<doteq> ϑ1`]
show ?thesis by auto
next
note `σ \<doteq> ϑ1`
also assume "ϑ1 \<doteq> []"
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 \<lhd> ϑ, N' \<lhd> ϑ), (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\<lhd>ϑ) ∪ vars_of (N'\<lhd>ϑ)
⊂ 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 "ϑ \<doteq> []"
hence "N \<lhd> ϑ = N"
and "N' \<lhd> ϑ = 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 \<lhd> ϑ1) (N' \<lhd> ϑ1) = Some ϑ2"
and σ: "σ = ϑ1 ◊ ϑ2"
and MGU_inner: "MGU ϑ1 M M'"
and MGU_outer: "MGU ϑ2 (N \<lhd> ϑ1) (N' \<lhd> ϑ1)"
by (auto split:option.split_asm)

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

with MGU_inner obtain δ
where eqv: "σ' \<doteq> ϑ1 ◊ δ"
unfolding MGU_def Unifier_def
by auto

from Ns have "N \<lhd> ϑ1 \<lhd> δ = N' \<lhd> ϑ1 \<lhd> δ"
by (simp add:subst_eq_dest[OF eqv])

with MGU_outer obtain ρ
where eqv2: "δ \<doteq> ϑ2 ◊ ρ"
unfolding MGU_def Unifier_def
by auto

have "σ' \<doteq> σ ◊ ρ" unfolding σ
by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
thus "∃γ. σ' \<doteq> σ ◊ γ" ..
qed
qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)


subsection {* Unification returns Idempotent Substitution *}

definition Idem :: "'a subst => bool"
where "Idem s <-> (s ◊ s) \<doteq> s"

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

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

fix s show "s \<lhd> [(v, t)] ◊ [(v, t)] = s \<lhd> [(v, t)]"
by (induct s) auto
qed

lemma Unifier_Idem_subst:
"Idem(r) ==> Unifier s (t \<lhd> r) (u \<lhd> r) ==>
Unifier (r ◊ s) (t \<lhd> r) (u \<lhd> r)"

by (simp add: Idem_def Unifier_def subst_eq_def)

lemma Idem_comp:
"Idem r ==> Unifier s (t \<lhd> r) (u \<lhd> r) ==>
(!!q. Unifier q (t \<lhd> r) (u \<lhd> r) ==> s ◊ q \<doteq> 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' \<lhd> ϑ1) (N' \<lhd> ϑ1) = Some ϑ2"
and σ: "σ = ϑ1 ◊ ϑ2"
and "Idem ϑ1"
and "Idem ϑ2"
by (auto split: option.split_asm)

from ϑ2 have "Unifier ϑ2 (M' \<lhd> ϑ1) (N' \<lhd> ϑ1)"
by (rule unify_computes_MGU[THEN MGU_is_Unifier])

with `Idem ϑ1`
show "Idem σ" unfolding σ
proof (rule Idem_comp)
fix σ assume "Unifier σ (M' \<lhd> ϑ1) (N' \<lhd> ϑ1)"
with ϑ2 obtain γ where σ: "σ \<doteq> ϑ2 ◊ γ"
using unify_computes_MGU MGU_def by blast

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

end