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