src/HOL/ex/Unification.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 30909 bd4f255837e5
child 39754 150f831ce4a3
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     1 (*  ID:         $Id$
     2     Author:     Alexander Krauss, Technische Universitaet Muenchen
     3 *)
     4 
     5 header {* Case study: Unification Algorithm *}
     6 
     7 theory Unification
     8 imports Main
     9 begin
    10 
    11 text {* 
    12   This is a formalization of a first-order unification
    13   algorithm. It uses the new "function" package to define recursive
    14   functions, which allows a better treatment of nested recursion. 
    15 
    16   This is basically a modernized version of a previous formalization
    17   by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
    18   previous work by Paulson and Manna \& Waldinger (for details, see
    19   there).
    20 
    21   Unlike that formalization, where the proofs of termination and
    22   some partial correctness properties are intertwined, we can prove
    23   partial correctness and termination separately.
    24 *}
    25 
    26 
    27 subsection {* Basic definitions *}
    28 
    29 datatype 'a trm = 
    30   Var 'a 
    31   | Const 'a
    32   | App "'a trm" "'a trm" (infix "\<cdot>" 60)
    33 
    34 types
    35   'a subst = "('a \<times> 'a trm) list"
    36 
    37 text {* Applying a substitution to a variable: *}
    38 
    39 fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
    40 where
    41   "assoc x d [] = d"
    42 | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
    43 
    44 text {* Applying a substitution to a term: *}
    45 
    46 fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
    47 where
    48   "(Var v) \<triangleleft> s = assoc v (Var v) s"
    49 | "(Const c) \<triangleleft> s = (Const c)"
    50 | "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
    51 
    52 text {* Composition of substitutions: *}
    53 
    54 fun
    55   "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
    56 where
    57   "[] \<bullet> bl = bl"
    58 | "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
    59 
    60 text {* Equivalence of substitutions: *}
    61 
    62 definition eqv (infix "=\<^sub>s" 50)
    63 where
    64   "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
    65 
    66 
    67 subsection {* Basic lemmas *}
    68 
    69 lemma apply_empty[simp]: "t \<triangleleft> [] = t"
    70 by (induct t) auto
    71 
    72 lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
    73 by (induct \<sigma>) auto
    74 
    75 lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
    76 proof (induct t)
    77   case App thus ?case by simp
    78 next 
    79   case Const thus ?case by simp
    80 next
    81   case (Var v) thus ?case
    82   proof (induct s1)
    83     case Nil show ?case by simp
    84   next
    85     case (Cons p s1s) thus ?case by (cases p, simp)
    86   qed
    87 qed
    88 
    89 lemma eqv_refl[intro]: "s =\<^sub>s s"
    90   by (auto simp:eqv_def)
    91 
    92 lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
    93   by (auto simp:eqv_def)
    94 
    95 lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
    96   by (auto simp:eqv_def)
    97 
    98 lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
    99   by (auto simp:eqv_def)
   100 
   101 lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
   102   by (auto simp:eqv_def)
   103 
   104 lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
   105   by (auto simp:eqv_def)
   106 
   107 lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
   108   by auto
   109 
   110 
   111 subsection {* Specification: Most general unifiers *}
   112 
   113 definition
   114   "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
   115 
   116 definition
   117   "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
   118   \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
   119 
   120 lemma MGUI[intro]:
   121   "\<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>
   122   \<Longrightarrow> MGU \<sigma> t u"
   123   by (simp only:Unifier_def MGU_def, auto)
   124 
   125 lemma MGU_sym[sym]:
   126   "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
   127   by (auto simp:MGU_def Unifier_def)
   128 
   129 
   130 subsection {* The unification algorithm *}
   131 
   132 text {* Occurs check: Proper subterm relation *}
   133 
   134 fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   135 where
   136   "occ u (Var v) = False"
   137 | "occ u (Const c) = False"
   138 | "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
   139 
   140 text {* The unification algorithm: *}
   141 
   142 function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   143 where
   144   "unify (Const c) (M \<cdot> N)   = None"
   145 | "unify (M \<cdot> N)   (Const c) = None"
   146 | "unify (Const c) (Var v)   = Some [(v, Const c)]"
   147 | "unify (M \<cdot> N)   (Var v)   = (if (occ (Var v) (M \<cdot> N)) 
   148                                         then None
   149                                         else Some [(v, M \<cdot> N)])"
   150 | "unify (Var v)   M         = (if (occ (Var v) M) 
   151                                         then None
   152                                         else Some [(v, M)])"
   153 | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   154 | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   155                                     None \<Rightarrow> None |
   156                                     Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
   157                                       of None \<Rightarrow> None |
   158                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   159   by pat_completeness auto
   160 
   161 
   162 subsection {* Partial correctness *}
   163 
   164 text {* Some lemmas about occ and MGU: *}
   165 
   166 lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
   167   \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
   168 by (induct t) auto
   169 
   170 lemma MGU_Var[intro]: 
   171   assumes no_occ: "\<not>occ (Var v) t"
   172   shows "MGU [(v,t)] (Var v) t"
   173 proof (intro MGUI exI)
   174   show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
   175     by (cases "Var v = t", auto simp:subst_no_occ)
   176 next
   177   fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>" 
   178   show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>" 
   179   proof
   180     fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th 
   181       by (induct s) auto
   182   qed
   183 qed
   184 
   185 declare MGU_Var[symmetric, intro]
   186 
   187 lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
   188   unfolding MGU_def Unifier_def
   189   by auto
   190   
   191 text {* If unification terminates, then it computes most general unifiers: *}
   192 
   193 lemma unify_partial_correctness:
   194   assumes "unify_dom (M, N)"
   195   assumes "unify M N = Some \<sigma>"
   196   shows "MGU \<sigma> M N"
   197 using assms
   198 proof (induct M N arbitrary: \<sigma>)
   199   case (7 M N M' N' \<sigma>) -- "The interesting case"
   200 
   201   then obtain \<theta>1 \<theta>2 
   202     where "unify M M' = Some \<theta>1"
   203     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   204     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   205     and MGU_inner: "MGU \<theta>1 M M'" 
   206     and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
   207     by (auto split:option.split_asm)
   208 
   209   show ?case
   210   proof
   211     from MGU_inner and MGU_outer
   212     have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1" 
   213       and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
   214       unfolding MGU_def Unifier_def
   215       by auto
   216     thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
   217       by simp
   218   next
   219     fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
   220     hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
   221       and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
   222 
   223     with MGU_inner obtain \<delta>
   224       where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
   225       unfolding MGU_def Unifier_def
   226       by auto
   227 
   228     from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
   229       by (simp add:eqv_dest[OF eqv])
   230 
   231     with MGU_outer obtain \<rho>
   232       where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
   233       unfolding MGU_def Unifier_def
   234       by auto
   235     
   236     have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
   237       by (rule eqv_intro, auto simp:eqv_dest[OF eqv] eqv_dest[OF eqv2])
   238     thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
   239   qed
   240 qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   241 
   242 
   243 subsection {* Properties used in termination proof *}
   244 
   245 text {* The variables of a term: *}
   246 
   247 fun vars_of:: "'a trm \<Rightarrow> 'a set"
   248 where
   249   "vars_of (Var v) = { v }"
   250 | "vars_of (Const c) = {}"
   251 | "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
   252 
   253 lemma vars_of_finite[intro]: "finite (vars_of t)"
   254   by (induct t) simp_all
   255 
   256 text {* Elimination of variables by a substitution: *}
   257 
   258 definition
   259   "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   260 
   261 lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   262   by (auto simp:elim_def)
   263 
   264 lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   265   by (auto simp:elim_def)
   266 
   267 lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   268   by (auto simp:elim_def eqv_def)
   269 
   270 
   271 text {* Replacing a variable by itself yields an identity subtitution: *}
   272 
   273 lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
   274 proof
   275   fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
   276     by (induct t) simp_all
   277 qed
   278 
   279 lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)"
   280 proof
   281   assume t_v: "t = Var v"
   282   thus "[(v, t)] =\<^sub>s []"
   283     by auto
   284 next
   285   assume id: "[(v, t)] =\<^sub>s []"
   286   show "t = Var v"
   287   proof -
   288     have "t = Var v \<triangleleft> [(v, t)]" by simp
   289     also from id have "\<dots> = Var v \<triangleleft> []" ..
   290     finally show ?thesis by simp
   291   qed
   292 qed
   293 
   294 text {* A lemma about occ and elim *}
   295 
   296 lemma remove_var:
   297   assumes [simp]: "v \<notin> vars_of s"
   298   shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
   299   by (induct t) simp_all
   300 
   301 lemma occ_elim: "\<not>occ (Var v) t 
   302   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
   303 proof (induct t)
   304   case (Var x)
   305   show ?case
   306   proof cases
   307     assume "v = x"
   308     thus ?thesis
   309       by (simp add:var_same)
   310   next
   311     assume neq: "v \<noteq> x"
   312     have "elim [(v, Var x)] v"
   313       by (auto intro!:remove_var simp:neq)
   314     thus ?thesis ..
   315   qed
   316 next
   317   case (Const c)
   318   have "elim [(v, Const c)] v"
   319     by (auto intro!:remove_var)
   320   thus ?case ..
   321 next
   322   case (App M N)
   323   
   324   hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
   325     and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
   326     and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
   327     by auto
   328 
   329   from nonocc have "\<not> [(v,M)] =\<^sub>s []"
   330     by (simp add:var_same)
   331   with ih1 have "elim [(v, M)] v" by blast
   332   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
   333   hence not_in_M: "v \<notin> vars_of M" by simp
   334 
   335   from nonocc have "\<not> [(v,N)] =\<^sub>s []"
   336     by (simp add:var_same)
   337   with ih2 have "elim [(v, N)] v" by blast
   338   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
   339   hence not_in_N: "v \<notin> vars_of N" by simp
   340 
   341   have "elim [(v, M \<cdot> N)] v"
   342   proof 
   343     fix t 
   344     show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
   345     proof (induct t)
   346       case (Var x) thus ?case by (simp add: not_in_M not_in_N)
   347     qed auto
   348   qed
   349   thus ?case ..
   350 qed
   351 
   352 text {* The result of a unification never introduces new variables: *}
   353 
   354 lemma unify_vars: 
   355   assumes "unify_dom (M, N)"
   356   assumes "unify M N = Some \<sigma>"
   357   shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   358   (is "?P M N \<sigma> t")
   359 using assms
   360 proof (induct M N arbitrary:\<sigma> t)
   361   case (3 c v) 
   362   hence "\<sigma> = [(v, Const c)]" by simp
   363   thus ?case by (induct t) auto
   364 next
   365   case (4 M N v) 
   366   hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   367   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   368   thus ?case by (induct t) auto
   369 next
   370   case (5 v M)
   371   hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   372   with 5 have "\<sigma> = [(v, M)]" by simp
   373   thus ?case by (induct t) auto
   374 next
   375   case (7 M N M' N' \<sigma>)
   376   then obtain \<theta>1 \<theta>2 
   377     where "unify M M' = Some \<theta>1"
   378     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   379     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   380     and ih1: "\<And>t. ?P M M' \<theta>1 t"
   381     and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
   382     by (auto split:option.split_asm)
   383 
   384   show ?case
   385   proof
   386     fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
   387     
   388     show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   389     proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   390         \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   391       case True
   392       with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   393         by auto
   394       
   395       from a and ih2[where t="t \<triangleleft> \<theta>1"]
   396       have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1) 
   397         \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
   398         by auto
   399       hence "v \<in> vars_of t"
   400       proof
   401         assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   402         with True show ?thesis by (auto dest:l)
   403       next
   404         assume "v \<in> vars_of (t \<triangleleft> \<theta>1)" 
   405         thus ?thesis by (rule l)
   406       qed
   407       
   408       thus ?thesis by auto
   409     qed auto
   410   qed
   411 qed (auto split: split_if_asm)
   412 
   413 
   414 text {* The result of a unification is either the identity
   415 substitution or it eliminates a variable from one of the terms: *}
   416 
   417 lemma unify_eliminates: 
   418   assumes "unify_dom (M, N)"
   419   assumes "unify M N = Some \<sigma>"
   420   shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
   421   (is "?P M N \<sigma>")
   422 using assms
   423 proof (induct M N arbitrary:\<sigma>)
   424   case 1 thus ?case by simp
   425 next
   426   case 2 thus ?case by simp
   427 next
   428   case (3 c v)
   429   have no_occ: "\<not> occ (Var v) (Const c)" by simp
   430   with 3 have "\<sigma> = [(v, Const c)]" by simp
   431   with occ_elim[OF no_occ]
   432   show ?case by auto
   433 next
   434   case (4 M N v)
   435   hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   436   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   437   with occ_elim[OF no_occ]
   438   show ?case by auto 
   439 next
   440   case (5 v M) 
   441   hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   442   with 5 have "\<sigma> = [(v, M)]" by simp
   443   with occ_elim[OF no_occ]
   444   show ?case by auto 
   445 next 
   446   case (6 c d) thus ?case
   447     by (cases "c = d") auto
   448 next
   449   case (7 M N M' N' \<sigma>)
   450   then obtain \<theta>1 \<theta>2 
   451     where "unify M M' = Some \<theta>1"
   452     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   453     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   454     and ih1: "?P M M' \<theta>1"
   455     and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
   456     by (auto split:option.split_asm)
   457 
   458   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   459   have "unify_dom (M, M')"
   460     by (rule accp_downward) (rule unify_rel.intros)
   461   hence no_new_vars: 
   462     "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   463     by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
   464 
   465   from ih2 show ?case 
   466   proof 
   467     assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
   468     then obtain v 
   469       where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   470       and el: "elim \<theta>2 v" by auto
   471     with no_new_vars show ?thesis unfolding \<sigma> 
   472       by (auto simp:elim_def)
   473   next
   474     assume empty[simp]: "\<theta>2 =\<^sub>s []"
   475 
   476     have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
   477       by (rule compose_eqv) auto
   478     also have "\<dots> =\<^sub>s \<theta>1" by auto
   479     finally have "\<sigma> =\<^sub>s \<theta>1" .
   480 
   481     from ih1 show ?thesis
   482     proof
   483       assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   484       with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
   485       show ?thesis by auto
   486     next
   487       note `\<sigma> =\<^sub>s \<theta>1`
   488       also assume "\<theta>1 =\<^sub>s []"
   489       finally show ?thesis ..
   490     qed
   491   qed
   492 qed
   493 
   494 
   495 subsection {* Termination proof *}
   496 
   497 termination unify
   498 proof 
   499   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
   500                            \<lambda>(M, N). size M]"
   501   show "wf ?R" by simp
   502 
   503   fix M N M' N' 
   504   show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
   505     by (rule measures_lesseq) (auto intro: card_mono)
   506 
   507   fix \<theta>                                   -- "Outer call"
   508   assume inner: "unify_dom (M, M')"
   509     "unify M M' = Some \<theta>"
   510 
   511   from unify_eliminates[OF inner]
   512   show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   513   proof
   514     -- {* Either a variable is eliminated \ldots *}
   515     assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   516     then obtain v 
   517       where "elim \<theta> v" 
   518       and "v\<in>vars_of M \<union> vars_of M'" by auto
   519     with unify_vars[OF inner]
   520     have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
   521       \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   522       by auto
   523     
   524     thus ?thesis
   525       by (auto intro!: measures_less intro: psubset_card_mono)
   526   next
   527     -- {* Or the substitution is empty *}
   528     assume "\<theta> =\<^sub>s []"
   529     hence "N \<triangleleft> \<theta> = N" 
   530       and "N' \<triangleleft> \<theta> = N'" by auto
   531     thus ?thesis 
   532        by (auto intro!: measures_less intro: psubset_card_mono)
   533   qed
   534 qed
   535 
   536 end