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