src/HOL/ex/Unification.thy
author krauss
Tue Sep 28 09:54:07 2010 +0200 (2010-09-28)
changeset 39754 150f831ce4a3
parent 32960 69916a850301
child 41460 ea56b98aee83
permissions -rw-r--r--
no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.
     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 declare unify.psimps[simp]
   162 
   163 subsection {* Partial correctness *}
   164 
   165 text {* Some lemmas about occ and MGU: *}
   166 
   167 lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
   168   \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
   169 by (induct t) auto
   170 
   171 lemma MGU_Var[intro]: 
   172   assumes no_occ: "\<not>occ (Var v) t"
   173   shows "MGU [(v,t)] (Var v) t"
   174 proof (intro MGUI exI)
   175   show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
   176     by (cases "Var v = t", auto simp:subst_no_occ)
   177 next
   178   fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>" 
   179   show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>" 
   180   proof
   181     fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th 
   182       by (induct s) auto
   183   qed
   184 qed
   185 
   186 declare MGU_Var[symmetric, intro]
   187 
   188 lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
   189   unfolding MGU_def Unifier_def
   190   by auto
   191   
   192 text {* If unification terminates, then it computes most general unifiers: *}
   193 
   194 lemma unify_partial_correctness:
   195   assumes "unify_dom (M, N)"
   196   assumes "unify M N = Some \<sigma>"
   197   shows "MGU \<sigma> M N"
   198 using assms
   199 proof (induct M N arbitrary: \<sigma>)
   200   case (7 M N M' N' \<sigma>) -- "The interesting case"
   201 
   202   then obtain \<theta>1 \<theta>2 
   203     where "unify M M' = Some \<theta>1"
   204     and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   205     and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   206     and MGU_inner: "MGU \<theta>1 M M'" 
   207     and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
   208     by (auto split:option.split_asm)
   209 
   210   show ?case
   211   proof
   212     from MGU_inner and MGU_outer
   213     have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1" 
   214       and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
   215       unfolding MGU_def Unifier_def
   216       by auto
   217     thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
   218       by simp
   219   next
   220     fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
   221     hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
   222       and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
   223 
   224     with MGU_inner obtain \<delta>
   225       where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
   226       unfolding MGU_def Unifier_def
   227       by auto
   228 
   229     from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
   230       by (simp add:eqv_dest[OF eqv])
   231 
   232     with MGU_outer obtain \<rho>
   233       where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
   234       unfolding MGU_def Unifier_def
   235       by auto
   236     
   237     have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
   238       by (rule eqv_intro, auto simp:eqv_dest[OF eqv] 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: "([(v, t)] =\<^sub>s []) = (t = Var v)"
   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)
   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)
   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)
   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 declare unify.psimps[simp del]
   538 
   539 end