Renamed accessible part for predicates to accp.
(* ID: $Id$
Author: Alexander Krauss, Technische Universitaet Muenchen
*)
header {* Case study: Unification Algorithm *}
theory Unification
imports Main
begin
text {*
This is a formalization of a first-order unification
algorithm. It uses the new "function" package to define recursive
functions, which allows a better treatment of nested recursion.
This is basically a modernized version of a previous formalization
by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
previous work by Paulson and Manna \& Waldinger (for details, see
there).
Unlike that formalization, where the proofs of termination and
some partial correctness properties are intertwined, we can prove
partial correctness and termination separately.
*}
subsection {* Basic definitions *}
datatype 'a trm =
Var 'a
| Const 'a
| App "'a trm" "'a trm" (infix "\<cdot>" 60)
types
'a subst = "('a \<times> 'a trm) list"
text {* Applying a substitution to a variable: *}
fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
where
"assoc x d [] = d"
| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
text {* Applying a substitution to a term: *}
fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
where
"(Var v) \<triangleleft> s = assoc v (Var v) s"
| "(Const c) \<triangleleft> s = (Const c)"
| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
text {* Composition of substitutions: *}
fun
"compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
where
"[] \<bullet> bl = bl"
| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
text {* Equivalence of substitutions: *}
definition eqv (infix "=\<^sub>s" 50)
where
"s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
subsection {* Basic lemmas *}
lemma apply_empty[simp]: "t \<triangleleft> [] = t"
by (induct t) auto
lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
by (induct \<sigma>) auto
lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
proof (induct t)
case App thus ?case by simp
next
case Const thus ?case by simp
next
case (Var v) thus ?case
proof (induct s1)
case Nil show ?case by simp
next
case (Cons p s1s) thus ?case by (cases p, simp)
qed
qed
lemma eqv_refl[intro]: "s =\<^sub>s s"
by (auto simp:eqv_def)
lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
by (auto simp:eqv_def)
lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
by (auto simp:eqv_def)
lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
by (auto simp:eqv_def)
lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
by (auto simp:eqv_def)
lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
by (auto simp:eqv_def)
lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
by auto
subsection {* Specification: Most general unifiers *}
definition
"Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
definition
"MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u
\<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
lemma MGUI[intro]:
"\<lbrakk>t \<triangleleft> \<sigma> = u \<triangleleft> \<sigma>; \<And>\<theta>. t \<triangleleft> \<theta> = u \<triangleleft> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>\<rbrakk>
\<Longrightarrow> MGU \<sigma> t u"
by (simp only:Unifier_def MGU_def, auto)
lemma MGU_sym[sym]:
"MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
by (auto simp:MGU_def Unifier_def)
subsection {* The unification algorithm *}
text {* Occurs check: Proper subterm relation *}
fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
where
"occ u (Var v) = False"
| "occ u (Const c) = False"
| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
text {* The unification algorithm: *}
function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
where
"unify (Const c) (M \<cdot> N) = None"
| "unify (M \<cdot> N) (Const c) = None"
| "unify (Const c) (Var v) = Some [(v, Const c)]"
| "unify (M \<cdot> N) (Var v) = (if (occ (Var v) (M \<cdot> N))
then None
else Some [(v, M \<cdot> N)])"
| "unify (Var v) M = (if (occ (Var v) M)
then None
else Some [(v, M)])"
| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
None \<Rightarrow> None |
Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
of None \<Rightarrow> None |
Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
by pat_completeness auto
subsection {* Partial correctness *}
text {* Some lemmas about occ and MGU: *}
lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
\<Longrightarrow> t \<triangleleft> [(v,s)] = t"
by (induct t) auto
lemma MGU_Var[intro]:
assumes no_occ: "\<not>occ (Var v) t"
shows "MGU [(v,t)] (Var v) t"
proof (intro MGUI exI)
show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
by (cases "Var v = t", auto simp:subst_no_occ)
next
fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
proof
fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
by (induct s, auto)
qed
qed
declare MGU_Var[symmetric, intro]
lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
unfolding MGU_def Unifier_def
by auto
text {* If unification terminates, then it computes most general unifiers: *}
lemma unify_partial_correctness:
assumes "unify_dom (M, N)"
assumes "unify M N = Some \<sigma>"
shows "MGU \<sigma> M N"
using prems
proof (induct M N arbitrary: \<sigma>)
case (7 M N M' N' \<sigma>) -- "The interesting case"
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \<theta>1"
and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
and MGU_inner: "MGU \<theta>1 M M'"
and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
by (auto split:option.split_asm)
show ?case
proof
from MGU_inner and MGU_outer
have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1"
and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
unfolding MGU_def Unifier_def
by auto
thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
by simp
next
fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
with MGU_inner obtain \<delta>
where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
unfolding MGU_def Unifier_def
by auto
from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
by (simp add:eqv_dest[OF eqv])
with MGU_outer obtain \<rho>
where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
unfolding MGU_def Unifier_def
by auto
have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
by (rule eqv_intro, auto simp:eqv_dest[OF eqv]
eqv_dest[OF eqv2])
thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
qed
qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
subsection {* Properties used in termination proof *}
text {* The variables of a term: *}
fun vars_of:: "'a trm \<Rightarrow> 'a set"
where
"vars_of (Var v) = { v }"
| "vars_of (Const c) = {}"
| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
lemma vars_of_finite[intro]: "finite (vars_of t)"
by (induct t) simp_all
text {* Elimination of variables by a substitution: *}
definition
"elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
by (auto simp:elim_def)
lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
by (auto simp:elim_def)
lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
by (auto simp:elim_def eqv_def)
text {* Replacing a variable by itself yields an identity subtitution: *}
lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
proof
fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
by (induct t) simp_all
qed
lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
proof
assume t_v: "t = Var v"
thus "[(v, t)] =\<^sub>s []"
by auto
next
assume id: "[(v, t)] =\<^sub>s []"
show "t = Var v"
proof -
have "t = Var v \<triangleleft> [(v, t)]" by simp
also from id have "\<dots> = Var v \<triangleleft> []" ..
finally show ?thesis by simp
qed
qed
text {* A lemma about occ and elim *}
lemma remove_var:
assumes [simp]: "v \<notin> vars_of s"
shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
by (induct t) simp_all
lemma occ_elim: "\<not>occ (Var v) t
\<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
proof (induct t)
case (Var x)
show ?case
proof cases
assume "v = x"
thus ?thesis
by (simp add:var_same[symmetric])
next
assume neq: "v \<noteq> x"
have "elim [(v, Var x)] v"
by (auto intro!:remove_var simp:neq)
thus ?thesis ..
qed
next
case (Const c)
have "elim [(v, Const c)] v"
by (auto intro!:remove_var)
thus ?case ..
next
case (App M N)
hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
by auto
from nonocc have "\<not> [(v,M)] =\<^sub>s []"
by (simp add:var_same[symmetric])
with ih1 have "elim [(v, M)] v" by blast
hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
hence not_in_M: "v \<notin> vars_of M" by simp
from nonocc have "\<not> [(v,N)] =\<^sub>s []"
by (simp add:var_same[symmetric])
with ih2 have "elim [(v, N)] v" by blast
hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
hence not_in_N: "v \<notin> vars_of N" by simp
have "elim [(v, M \<cdot> N)] v"
proof
fix t
show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
proof (induct t)
case (Var x) thus ?case by (simp add: not_in_M not_in_N)
qed auto
qed
thus ?case ..
qed
text {* The result of a unification never introduces new variables: *}
lemma unify_vars:
assumes "unify_dom (M, N)"
assumes "unify M N = Some \<sigma>"
shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
(is "?P M N \<sigma> t")
using prems
proof (induct M N arbitrary:\<sigma> t)
case (3 c v)
hence "\<sigma> = [(v, Const c)]" by simp
thus ?case by (induct t, auto)
next
case (4 M N v)
hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
thus ?case by (induct t, auto)
next
case (5 v M)
hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
with prems have "\<sigma> = [(v, M)]" by simp
thus ?case by (induct t, auto)
next
case (7 M N M' N' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \<theta>1"
and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
and ih1: "\<And>t. ?P M M' \<theta>1 t"
and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
by (auto split:option.split_asm)
show ?case
proof
fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
\<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
case True
with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
by auto
from a and ih2[where t="t \<triangleleft> \<theta>1"]
have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)
\<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
by auto
hence "v \<in> vars_of t"
proof
assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
with True show ?thesis by (auto dest:l)
next
assume "v \<in> vars_of (t \<triangleleft> \<theta>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 \<sigma>"
shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
(is "?P M N \<sigma>")
using prems
proof (induct M N arbitrary:\<sigma>)
case 1 thus ?case by simp
next
case 2 thus ?case by simp
next
case (3 c v)
have no_occ: "\<not> occ (Var v) (Const c)" by simp
with prems have "\<sigma> = [(v, Const c)]" by simp
with occ_elim[OF no_occ]
show ?case by auto
next
case (4 M N v)
hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
with occ_elim[OF no_occ]
show ?case by auto
next
case (5 v M)
hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
with prems have "\<sigma> = [(v, M)]" by simp
with occ_elim[OF no_occ]
show ?case by auto
next
case (6 c d) thus ?case
by (cases "c = d") auto
next
case (7 M N M' N' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \<theta>1"
and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
and ih1: "?P M M' \<theta>1"
and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
by (auto split:option.split_asm)
from `unify_dom (M \<cdot> N, M' \<cdot> N')`
have "unify_dom (M, M')"
by (rule accp_downward) (rule unify_rel.intros)
hence no_new_vars:
"\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
from ih2 show ?case
proof
assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
then obtain v
where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
and el: "elim \<theta>2 v" by auto
with no_new_vars show ?thesis unfolding \<sigma>
by (auto simp:elim_def)
next
assume empty[simp]: "\<theta>2 =\<^sub>s []"
have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
by (rule compose_eqv) auto
also have "\<dots> =\<^sub>s \<theta>1" by auto
finally have "\<sigma> =\<^sub>s \<theta>1" .
from ih1 show ?thesis
proof
assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
show ?thesis by auto
next
note `\<sigma> =\<^sub>s \<theta>1`
also assume "\<theta>1 =\<^sub>s []"
finally show ?thesis ..
qed
qed
qed
subsection {* Termination proof *}
termination unify
proof
let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
\<lambda>(M, N). size M]"
show "wf ?R" by simp
fix M N M' N'
show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
by (rule measures_lesseq) (auto intro: card_mono)
fix \<theta> -- "Outer call"
assume inner: "unify_dom (M, M')"
"unify M M' = Some \<theta>"
from unify_eliminates[OF inner]
show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
proof
-- {* Either a variable is eliminated \ldots *}
assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
then obtain v
where "elim \<theta> v"
and "v\<in>vars_of M \<union> vars_of M'" by auto
with unify_vars[OF inner]
have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
\<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
by auto
thus ?thesis
by (auto intro!: measures_less intro: psubset_card_mono)
next
-- {* Or the substitution is empty *}
assume "\<theta> =\<^sub>s []"
hence "N \<triangleleft> \<theta> = N"
and "N' \<triangleleft> \<theta> = N'" by auto
thus ?thesis
by (auto intro!: measures_less intro: psubset_card_mono)
qed
qed
end