src/HOL/ex/Unification.thy
author wenzelm
Sat Apr 23 13:00:19 2011 +0200 (2011-04-23)
changeset 42463 f270e3e18be5
parent 41460 ea56b98aee83
child 44367 74c08021ab2e
permissions -rw-r--r--
modernized specifications;
     1 (*
     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 type_synonym 'a subst = "('a \<times> 'a trm) list"
    35 
    36 text {* Applying a substitution to a variable: *}
    37 
    38 fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
    39 where
    40   "assoc x d [] = d"
    41 | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
    42 
    43 text {* Applying a substitution to a term: *}
    44 
    45 fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
    46 where
    47   "(Var v) \<triangleleft> s = assoc v (Var v) s"
    48 | "(Const c) \<triangleleft> s = (Const c)"
    49 | "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
    50 
    51 text {* Composition of substitutions: *}
    52 
    53 fun
    54   "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
    55 where
    56   "[] \<bullet> bl = bl"
    57 | "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
    58 
    59 text {* Equivalence of substitutions: *}
    60 
    61 definition eqv (infix "=\<^sub>s" 50)
    62 where
    63   "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
    64 
    65 
    66 subsection {* Basic lemmas *}
    67 
    68 lemma apply_empty[simp]: "t \<triangleleft> [] = t"
    69 by (induct t) auto
    70 
    71 lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
    72 by (induct \<sigma>) auto
    73 
    74 lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
    75 proof (induct t)
    76   case App thus ?case by simp
    77 next 
    78   case Const thus ?case by simp
    79 next
    80   case (Var v) thus ?case
    81   proof (induct s1)
    82     case Nil show ?case by simp
    83   next
    84     case (Cons p s1s) thus ?case by (cases p, simp)
    85   qed
    86 qed
    87 
    88 lemma eqv_refl[intro]: "s =\<^sub>s s"
    89   by (auto simp:eqv_def)
    90 
    91 lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
    92   by (auto simp:eqv_def)
    93 
    94 lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
    95   by (auto simp:eqv_def)
    96 
    97 lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
    98   by (auto simp:eqv_def)
    99 
   100 lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
   101   by (auto simp:eqv_def)
   102 
   103 lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
   104   by (auto simp:eqv_def)
   105 
   106 lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
   107   by auto
   108 
   109 
   110 subsection {* Specification: Most general unifiers *}
   111 
   112 definition
   113   "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
   114 
   115 definition
   116   "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
   117   \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
   118 
   119 lemma MGUI[intro]:
   120   "\<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>
   121   \<Longrightarrow> MGU \<sigma> t u"
   122   by (simp only:Unifier_def MGU_def, auto)
   123 
   124 lemma MGU_sym[sym]:
   125   "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
   126   by (auto simp:MGU_def Unifier_def)
   127 
   128 
   129 subsection {* The unification algorithm *}
   130 
   131 text {* Occurs check: Proper subterm relation *}
   132 
   133 fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   134 where
   135   "occ u (Var v) = False"
   136 | "occ u (Const c) = False"
   137 | "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
   138 
   139 text {* The unification algorithm: *}
   140 
   141 function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   142 where
   143   "unify (Const c) (M \<cdot> N)   = None"
   144 | "unify (M \<cdot> N)   (Const c) = None"
   145 | "unify (Const c) (Var v)   = Some [(v, Const c)]"
   146 | "unify (M \<cdot> N)   (Var v)   = (if (occ (Var v) (M \<cdot> N)) 
   147                                         then None
   148                                         else Some [(v, M \<cdot> N)])"
   149 | "unify (Var v)   M         = (if (occ (Var v) M) 
   150                                         then None
   151                                         else Some [(v, M)])"
   152 | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   153 | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   154                                     None \<Rightarrow> None |
   155                                     Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
   156                                       of None \<Rightarrow> None |
   157                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   158   by pat_completeness auto
   159 
   160 declare unify.psimps[simp]
   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 declare unify.psimps[simp del]
   537 
   538 end