src/HOL/ex/Unification.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 24444 448978b61556
child 30909 bd4f255837e5
permissions -rw-r--r--
added lemmas
     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] 
   238 	eqv_dest[OF eqv2])
   239     thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
   240   qed
   241 qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   242 
   243 
   244 subsection {* Properties used in termination proof *}
   245 
   246 text {* The variables of a term: *}
   247 
   248 fun vars_of:: "'a trm \<Rightarrow> 'a set"
   249 where
   250   "vars_of (Var v) = { v }"
   251 | "vars_of (Const c) = {}"
   252 | "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
   253 
   254 lemma vars_of_finite[intro]: "finite (vars_of t)"
   255   by (induct t) simp_all
   256 
   257 text {* Elimination of variables by a substitution: *}
   258 
   259 definition
   260   "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   261 
   262 lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   263   by (auto simp:elim_def)
   264 
   265 lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   266   by (auto simp:elim_def)
   267 
   268 lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   269   by (auto simp:elim_def eqv_def)
   270 
   271 
   272 text {* Replacing a variable by itself yields an identity subtitution: *}
   273 
   274 lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
   275 proof
   276   fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
   277     by (induct t) simp_all
   278 qed
   279 
   280 lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
   281 proof
   282   assume t_v: "t = Var v"
   283   thus "[(v, t)] =\<^sub>s []"
   284     by auto
   285 next
   286   assume id: "[(v, t)] =\<^sub>s []"
   287   show "t = Var v"
   288   proof -
   289     have "t = Var v \<triangleleft> [(v, t)]" by simp
   290     also from id have "\<dots> = Var v \<triangleleft> []" ..
   291     finally show ?thesis by simp
   292   qed
   293 qed
   294 
   295 text {* A lemma about occ and elim *}
   296 
   297 lemma remove_var:
   298   assumes [simp]: "v \<notin> vars_of s"
   299   shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
   300   by (induct t) simp_all
   301 
   302 lemma occ_elim: "\<not>occ (Var v) t 
   303   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
   304 proof (induct t)
   305   case (Var x)
   306   show ?case
   307   proof cases
   308     assume "v = x"
   309     thus ?thesis
   310       by (simp add:var_same[symmetric])
   311   next
   312     assume neq: "v \<noteq> x"
   313     have "elim [(v, Var x)] v"
   314       by (auto intro!:remove_var simp:neq)
   315     thus ?thesis ..
   316   qed
   317 next
   318   case (Const c)
   319   have "elim [(v, Const c)] v"
   320     by (auto intro!:remove_var)
   321   thus ?case ..
   322 next
   323   case (App M N)
   324   
   325   hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
   326     and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
   327     and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
   328     by auto
   329 
   330   from nonocc have "\<not> [(v,M)] =\<^sub>s []"
   331     by (simp add:var_same[symmetric])
   332   with ih1 have "elim [(v, M)] v" by blast
   333   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
   334   hence not_in_M: "v \<notin> vars_of M" by simp
   335 
   336   from nonocc have "\<not> [(v,N)] =\<^sub>s []"
   337     by (simp add:var_same[symmetric])
   338   with ih2 have "elim [(v, N)] v" by blast
   339   hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
   340   hence not_in_N: "v \<notin> vars_of N" by simp
   341 
   342   have "elim [(v, M \<cdot> N)] v"
   343   proof 
   344     fix t 
   345     show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
   346     proof (induct t)
   347       case (Var x) thus ?case by (simp add: not_in_M not_in_N)
   348     qed auto
   349   qed
   350   thus ?case ..
   351 qed
   352 
   353 text {* The result of a unification never introduces new variables: *}
   354 
   355 lemma unify_vars: 
   356   assumes "unify_dom (M, N)"
   357   assumes "unify M N = Some \<sigma>"
   358   shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   359   (is "?P M N \<sigma> t")
   360 using assms
   361 proof (induct M N arbitrary:\<sigma> t)
   362   case (3 c v) 
   363   hence "\<sigma> = [(v, Const c)]" by simp
   364   thus ?case by (induct t) auto
   365 next
   366   case (4 M N v) 
   367   hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   368   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   369   thus ?case by (induct t) auto
   370 next
   371   case (5 v M)
   372   hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   373   with 5 have "\<sigma> = [(v, M)]" by simp
   374   thus ?case by (induct t) auto
   375 next
   376   case (7 M N M' N' \<sigma>)
   377   then obtain \<theta>1 \<theta>2 
   378     where "unify M M' = Some \<theta>1"
   379     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   380     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   381     and ih1: "\<And>t. ?P M M' \<theta>1 t"
   382     and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
   383     by (auto split:option.split_asm)
   384 
   385   show ?case
   386   proof
   387     fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
   388     
   389     show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   390     proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   391 	    \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   392       case True
   393       with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   394 	    by auto
   395       
   396       from a and ih2[where t="t \<triangleleft> \<theta>1"]
   397       have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1) 
   398         \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
   399 	    by auto
   400       hence "v \<in> vars_of t"
   401       proof
   402 	    assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   403 	    with True show ?thesis by (auto dest:l)
   404       next
   405 	    assume "v \<in> vars_of (t \<triangleleft> \<theta>1)" 
   406 	    thus ?thesis by (rule l)
   407       qed
   408       
   409       thus ?thesis by auto
   410     qed auto
   411   qed
   412 qed (auto split: split_if_asm)
   413 
   414 
   415 text {* The result of a unification is either the identity
   416 substitution or it eliminates a variable from one of the terms: *}
   417 
   418 lemma unify_eliminates: 
   419   assumes "unify_dom (M, N)"
   420   assumes "unify M N = Some \<sigma>"
   421   shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
   422   (is "?P M N \<sigma>")
   423 using assms
   424 proof (induct M N arbitrary:\<sigma>)
   425   case 1 thus ?case by simp
   426 next
   427   case 2 thus ?case by simp
   428 next
   429   case (3 c v)
   430   have no_occ: "\<not> occ (Var v) (Const c)" by simp
   431   with 3 have "\<sigma> = [(v, Const c)]" by simp
   432   with occ_elim[OF no_occ]
   433   show ?case by auto
   434 next
   435   case (4 M N v)
   436   hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   437   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   438   with occ_elim[OF no_occ]
   439   show ?case by auto 
   440 next
   441   case (5 v M) 
   442   hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   443   with 5 have "\<sigma> = [(v, M)]" by simp
   444   with occ_elim[OF no_occ]
   445   show ?case by auto 
   446 next 
   447   case (6 c d) thus ?case
   448     by (cases "c = d") auto
   449 next
   450   case (7 M N M' N' \<sigma>)
   451   then obtain \<theta>1 \<theta>2 
   452     where "unify M M' = Some \<theta>1"
   453     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   454     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   455     and ih1: "?P M M' \<theta>1"
   456     and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
   457     by (auto split:option.split_asm)
   458 
   459   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   460   have "unify_dom (M, M')"
   461     by (rule accp_downward) (rule unify_rel.intros)
   462   hence no_new_vars: 
   463     "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   464     by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
   465 
   466   from ih2 show ?case 
   467   proof 
   468     assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
   469     then obtain v 
   470       where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   471       and el: "elim \<theta>2 v" by auto
   472     with no_new_vars show ?thesis unfolding \<sigma> 
   473       by (auto simp:elim_def)
   474   next
   475     assume empty[simp]: "\<theta>2 =\<^sub>s []"
   476 
   477     have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
   478       by (rule compose_eqv) auto
   479     also have "\<dots> =\<^sub>s \<theta>1" by auto
   480     finally have "\<sigma> =\<^sub>s \<theta>1" .
   481 
   482     from ih1 show ?thesis
   483     proof
   484       assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   485       with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
   486       show ?thesis by auto
   487     next
   488       note `\<sigma> =\<^sub>s \<theta>1`
   489       also assume "\<theta>1 =\<^sub>s []"
   490       finally show ?thesis ..
   491     qed
   492   qed
   493 qed
   494 
   495 
   496 subsection {* Termination proof *}
   497 
   498 termination unify
   499 proof 
   500   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
   501                            \<lambda>(M, N). size M]"
   502   show "wf ?R" by simp
   503 
   504   fix M N M' N' 
   505   show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
   506     by (rule measures_lesseq) (auto intro: card_mono)
   507 
   508   fix \<theta>                                   -- "Outer call"
   509   assume inner: "unify_dom (M, M')"
   510     "unify M M' = Some \<theta>"
   511 
   512   from unify_eliminates[OF inner]
   513   show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   514   proof
   515     -- {* Either a variable is eliminated \ldots *}
   516     assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   517     then obtain v 
   518 	  where "elim \<theta> v" 
   519 	  and "v\<in>vars_of M \<union> vars_of M'" by auto
   520     with unify_vars[OF inner]
   521     have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
   522 	  \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   523 	  by auto
   524     
   525     thus ?thesis
   526       by (auto intro!: measures_less intro: psubset_card_mono)
   527   next
   528     -- {* Or the substitution is empty *}
   529     assume "\<theta> =\<^sub>s []"
   530     hence "N \<triangleleft> \<theta> = N" 
   531 	  and "N' \<triangleleft> \<theta> = N'" by auto
   532     thus ?thesis 
   533        by (auto intro!: measures_less intro: psubset_card_mono)
   534   qed
   535 qed
   536 
   537 end