(* 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 \<open>Substitution and Unification\<close>
theory Unification
imports Main
begin
text \<open>
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
\<close>
subsection \<open>Terms\<close>
text \<open>Binary trees with leaves that are constants or variables.\<close>
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 \<open>Substitutions\<close>
type_synonym 'a subst = "('a \<times> '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
\<Longrightarrow> t \<lhd> [(v,s)] = t"
by (induct t) auto
lemma comp_Nil[simp]: "\ \ [] = \"
by (induct \<sigma>) 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 \<open>Unifiers and Most General Unifiers\<close>
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 \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
lemma MGUI[intro]:
"\t \ \ = u \ \; \\. t \ \ = u \ \ \ \\. \ \ \ \ \\
\<Longrightarrow> MGU \<sigma> 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 \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>"
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 \<open>The unification algorithm\<close>
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 \<cdot> 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 \<Rightarrow> None |
Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
of None \<Rightarrow> None |
Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
by pat_completeness auto
subsection \<open>Properties used in termination proof\<close>
text \<open>Elimination of variables by a substitution:\<close>
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
\<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
by (metis elim_intro remove_var var_same vars_iff_occseq)
text \<open>The result of a unification never introduces new variables:\<close>
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:\<sigma> 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' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \1"
and "unify (N \ \1) (N' \ \1) = Some \2"
and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>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'
\<and> v \<notin> vars_of N \<and> v \<notin> 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)
\<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
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 \<open>The result of a unification is either the identity
substitution or it eliminates a variable from one of the terms:\<close>
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:\<sigma>)
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' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \1"
and "unify (N \ \1) (N' \ \1) = Some \2"
and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
and ih1: "?P M M' \1"
and ih2: "?P (N\\1) (N'\\1) \2"
by (auto split:option.split_asm)
from \<open>unify_dom (M \<cdot> N, M' \<cdot> N')\<close>
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 \<open>unify M M' = Some \<theta>1\<close>)
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 \<sigma>
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 \<open>\<sigma> \<doteq> \<theta>1\<close>]
show ?thesis by auto
next
note \<open>\<sigma> \<doteq> \<theta>1\<close>
also assume "\1 \ []"
finally show ?thesis ..
qed
qed
qed
declare unify.psimps[simp del]
subsection \<open>Termination proof\<close>
termination unify
proof
let ?R = "measures [\(M,N). card (vars_of M \ vars_of N),
\<lambda>(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 \<theta> \<comment> \<open>Outer call\<close>
assume inner: "unify_dom (M, M')"
"unify M M' = Some \"
from unify_eliminates[OF inner]
show "((N \ \, N' \ \), (M \ N, M' \ N')) \?R"
proof
\<comment> \<open>Either a variable is eliminated \ldots\<close>
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'\\)
\<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
\<comment> \<open>Or the substitution is empty\<close>
assume "\ \ []"
hence "N \ \ = N"
and "N' \ \ = N'" by auto
thus ?thesis
by (auto intro!: measures_less intro: psubset_card_mono)
qed
qed
subsection \<open>Unification returns a Most General Unifier\<close>
lemma unify_computes_MGU:
"unify M N = Some \ \ MGU \ M N"
proof (induct M N arbitrary: \<sigma> rule: unify.induct)
case (7 M N M' N' \<sigma>) \<comment> \<open>The interesting case\<close>
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \1"
and "unify (N \ \1) (N' \ \1) = Some \2"
and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>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 \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
hence "M \ \' = M' \ \'"
and Ns: "N \ \' = N' \ \'" by auto
with MGU_inner obtain \<delta>
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 \<rho>
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 \<open>Unification returns Idempotent Substitution\<close>
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 \<lozenge> 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 \ r) (u \ r) \
(!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
Idem (r \<lozenge> 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: \<sigma> rule: unify.induct)
case (7 M M' N N' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M N = Some \1"
and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
and "Idem \1"
and "Idem \2"
by (auto split: option.split_asm)
from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
by (rule unify_computes_MGU[THEN MGU_is_Unifier])
with \<open>Idem \<theta>1\<close>
show "Idem \" unfolding \
proof (rule Idem_comp)
fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
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
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
