Added unification case study (using new function package)
authorkrauss
Thu May 17 22:33:41 2007 +0200 (2007-05-17)
changeset 22999c1ce129e6f9c
parent 22998 97e1f9c2cc46
child 23000 6f158bba99e4
Added unification case study (using new function package)
src/HOL/ex/ROOT.ML
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu May 17 21:51:32 2007 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu May 17 22:33:41 2007 +0200
     1.3 @@ -79,3 +79,5 @@
     1.4  
     1.5  HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
     1.6  HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
     1.7 +
     1.8 +time_use_thy "Unification";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Unification.thy	Thu May 17 22:33:41 2007 +0200
     2.3 @@ -0,0 +1,554 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Alexander Krauss, Technische Universitaet Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* Case study: Unification Algorithm *}
     2.9 +
    2.10 +(*<*)theory Unification
    2.11 +imports Main
    2.12 +begin(*>*)
    2.13 +
    2.14 +text {* 
    2.15 +  This is a formalization of a first-order unification
    2.16 +  algorithm. It uses the new "function" package to define recursive
    2.17 +  functions, which allows a better treatment of nested recursion. 
    2.18 +
    2.19 +  This is basically a modernized version of a previous formalization
    2.20 +  by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
    2.21 +  previous work by Paulson and Manna & Waldinger (for details, see
    2.22 +  there).
    2.23 +
    2.24 +  Unlike that formalization, where the proofs of termination and
    2.25 +  some partial correctness properties are intertwined, we can prove
    2.26 +  partial correctness and termination separately.
    2.27 +*}
    2.28 +
    2.29 +subsection {* Basic definitions *}
    2.30 +
    2.31 +datatype 'a trm = 
    2.32 +  Var 'a 
    2.33 +  | Const 'a
    2.34 +  | App "'a trm" "'a trm" (infix "\<cdot>" 60)
    2.35 +
    2.36 +types
    2.37 +  'a subst = "('a \<times> 'a trm) list"
    2.38 +
    2.39 +text {* Applying a substitution to a variable: *}
    2.40 +
    2.41 +fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
    2.42 +where
    2.43 +  "assoc x d [] = d"
    2.44 +| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
    2.45 +
    2.46 +text {* Applying a substitution to a term: *}
    2.47 +
    2.48 +fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
    2.49 +where
    2.50 +  "(Var v) \<triangleleft> s = assoc v (Var v) s"
    2.51 +| "(Const c) \<triangleleft> s = (Const c)"
    2.52 +| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
    2.53 +
    2.54 +text {* Composition of substitutions: *}
    2.55 +
    2.56 +fun
    2.57 +  "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
    2.58 +where
    2.59 +  "[] \<bullet> bl = bl"
    2.60 +| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
    2.61 +
    2.62 +text {* Equivalence of substitutions: *}
    2.63 +
    2.64 +definition eqv (infix "=\<^sub>s" 50)
    2.65 +where
    2.66 +  "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
    2.67 +
    2.68 +subsection {* Basic lemmas *}
    2.69 +
    2.70 +lemma apply_empty[simp]: "t \<triangleleft> [] = t"
    2.71 +by (induct t) auto
    2.72 +
    2.73 +lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
    2.74 +by (induct \<sigma>) auto
    2.75 +
    2.76 +lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
    2.77 +proof (induct t)
    2.78 +  case App thus ?case by simp
    2.79 +next 
    2.80 +  case Const thus ?case by simp
    2.81 +next
    2.82 +  case (Var v) thus ?case
    2.83 +  proof (induct s1)
    2.84 +    case Nil show ?case by simp
    2.85 +  next
    2.86 +    case (Cons p s1s) thus ?case by (cases p, simp)
    2.87 +  qed
    2.88 +qed
    2.89 +
    2.90 +lemma eqv_refl[intro]: "s =\<^sub>s s"
    2.91 +  by (auto simp:eqv_def)
    2.92 +
    2.93 +lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
    2.94 +  by (auto simp:eqv_def)
    2.95 +
    2.96 +lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
    2.97 +  by (auto simp:eqv_def)
    2.98 +
    2.99 +lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
   2.100 +  by (auto simp:eqv_def)
   2.101 +
   2.102 +lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
   2.103 +  by (auto simp:eqv_def)
   2.104 +
   2.105 +lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
   2.106 +  by (auto simp:eqv_def)
   2.107 +
   2.108 +lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
   2.109 +  by auto
   2.110 +
   2.111 +subsection {* Specification: Most general unifiers *}
   2.112 +
   2.113 +definition
   2.114 +  "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
   2.115 +
   2.116 +definition
   2.117 +  "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
   2.118 +  \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
   2.119 +
   2.120 +lemma MGUI[intro]:
   2.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>
   2.122 +  \<Longrightarrow> MGU \<sigma> t u"
   2.123 +  by (simp only:Unifier_def MGU_def, auto)
   2.124 +
   2.125 +lemma MGU_sym[sym]:
   2.126 +  "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
   2.127 +  by (auto simp:MGU_def Unifier_def)
   2.128 +
   2.129 +
   2.130 +subsection {* The unification algorithm *}
   2.131 +
   2.132 +text {* Occurs check: Proper subterm relation *}
   2.133 +
   2.134 +fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   2.135 +where
   2.136 +  "occ u (Var v) = False"
   2.137 +| "occ u (Const c) = False"
   2.138 +| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
   2.139 +
   2.140 +text {* The unification algorithm: *}
   2.141 +
   2.142 +function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   2.143 +where
   2.144 +  "unify (Const c) (M \<cdot> N)   = None"
   2.145 +| "unify (M \<cdot> N)   (Const c) = None"
   2.146 +| "unify (Const c) (Var v)   = Some [(v, Const c)]"
   2.147 +| "unify (M \<cdot> N)   (Var v)   = (if (occ (Var v) (M \<cdot> N)) 
   2.148 +                                        then None
   2.149 +                                        else Some [(v, M \<cdot> N)])"
   2.150 +| "unify (Var v)   M         = (if (occ (Var v) M) 
   2.151 +                                        then None
   2.152 +                                        else Some [(v, M)])"
   2.153 +| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   2.154 +| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   2.155 +                                    None \<Rightarrow> None |
   2.156 +                                    Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
   2.157 +                                      of None \<Rightarrow> None |
   2.158 +                                         Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   2.159 +  by pat_completeness auto
   2.160 +
   2.161 +
   2.162 +subsection {* Partial correctness *}
   2.163 +
   2.164 +text {* Some lemmas about occ and MGU: *}
   2.165 +
   2.166 +lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
   2.167 +  \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
   2.168 +by (induct t) auto
   2.169 +
   2.170 +lemma MGU_Var[intro]: 
   2.171 +  assumes no_occ: "\<not>occ (Var v) t"
   2.172 +  shows "MGU [(v,t)] (Var v) t"
   2.173 +proof (intro MGUI exI)
   2.174 +  show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
   2.175 +    by (cases "Var v = t", auto simp:subst_no_occ)
   2.176 +next
   2.177 +  fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>" 
   2.178 +  show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>" 
   2.179 +  proof
   2.180 +    fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th 
   2.181 +      by (induct s, auto)
   2.182 +  qed
   2.183 +qed
   2.184 +
   2.185 +declare MGU_Var[symmetric, intro]
   2.186 +
   2.187 +lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
   2.188 +  unfolding MGU_def Unifier_def
   2.189 +  by auto
   2.190 +  
   2.191 +text {* If unification terminates, then it computes most general unifiers: *}
   2.192 +
   2.193 +lemma unify_partial_correctness:
   2.194 +  assumes "unify_dom (M, N)"
   2.195 +  assumes "unify M N = Some \<sigma>"
   2.196 +  shows "MGU \<sigma> M N"
   2.197 +using prems
   2.198 +proof (induct M N arbitrary: \<sigma>)
   2.199 +  case (7 M N M' N' \<sigma>) -- "The interesting case"
   2.200 +
   2.201 +  then obtain \<theta>1 \<theta>2 
   2.202 +    where "unify M M' = Some \<theta>1"
   2.203 +    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   2.204 +    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   2.205 +    and MGU_inner: "MGU \<theta>1 M M'" 
   2.206 +    and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
   2.207 +    by (auto split:option.split_asm)
   2.208 +
   2.209 +  show ?case
   2.210 +  proof
   2.211 +    from MGU_inner and MGU_outer
   2.212 +    have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1" 
   2.213 +      and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
   2.214 +      unfolding MGU_def Unifier_def
   2.215 +      by auto
   2.216 +    thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
   2.217 +      by simp
   2.218 +  next
   2.219 +    fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
   2.220 +    hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
   2.221 +      and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
   2.222 +
   2.223 +    with MGU_inner obtain \<delta>
   2.224 +      where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
   2.225 +      unfolding MGU_def Unifier_def
   2.226 +      by auto
   2.227 +
   2.228 +    from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
   2.229 +      by (simp add:eqv_dest[OF eqv])
   2.230 +
   2.231 +    with MGU_outer obtain \<rho>
   2.232 +      where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
   2.233 +      unfolding MGU_def Unifier_def
   2.234 +      by auto
   2.235 +    
   2.236 +    have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
   2.237 +      by (rule eqv_intro, auto simp:eqv_dest[OF eqv] 
   2.238 +	eqv_dest[OF eqv2])
   2.239 +    thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
   2.240 +  qed
   2.241 +qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   2.242 +
   2.243 +
   2.244 +subsection {* Properties used in termination proof *}
   2.245 +
   2.246 +text {* The variables of a term: *}
   2.247 +
   2.248 +fun vars_of:: "'a trm \<Rightarrow> 'a set"
   2.249 +where
   2.250 +  "vars_of (Var v) = { v }"
   2.251 +| "vars_of (Const c) = {}"
   2.252 +| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
   2.253 +
   2.254 +lemma vars_of_finite[intro]: "finite (vars_of t)"
   2.255 +  by (induct t) simp_all
   2.256 +
   2.257 +text {* Elimination of variables by a substitution: *}
   2.258 +
   2.259 +definition
   2.260 +  "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   2.261 +
   2.262 +lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   2.263 +  by (auto simp:elim_def)
   2.264 +
   2.265 +lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   2.266 +  by (auto simp:elim_def)
   2.267 +
   2.268 +lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   2.269 +  by (auto simp:elim_def eqv_def)
   2.270 +
   2.271 +
   2.272 +text {* Replacing a variable by itself yields an identity subtitution: *}
   2.273 +
   2.274 +lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
   2.275 +proof
   2.276 +  fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
   2.277 +    by (induct t) simp_all
   2.278 +qed
   2.279 +
   2.280 +lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
   2.281 +proof
   2.282 +  assume t_v: "t = Var v"
   2.283 +  thus "[(v, t)] =\<^sub>s []"
   2.284 +    by auto
   2.285 +next
   2.286 +  assume id: "[(v, t)] =\<^sub>s []"
   2.287 +  show "t = Var v"
   2.288 +  proof -
   2.289 +    have "t = Var v \<triangleleft> [(v, t)]" by simp
   2.290 +    also from id have "\<dots> = Var v \<triangleleft> []" ..
   2.291 +    finally show ?thesis by simp
   2.292 +  qed
   2.293 +qed
   2.294 +
   2.295 +text {* A lemma about occ and elim *}
   2.296 +
   2.297 +lemma remove_var:
   2.298 +  assumes [simp]: "v \<notin> vars_of s"
   2.299 +  shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
   2.300 +  by (induct t) simp_all
   2.301 +
   2.302 +lemma occ_elim: "\<not>occ (Var v) t 
   2.303 +  \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
   2.304 +proof (induct t)
   2.305 +  case (Var x)
   2.306 +  show ?case
   2.307 +  proof cases
   2.308 +    assume "v = x"
   2.309 +    thus ?thesis
   2.310 +      by (simp add:var_same[symmetric])
   2.311 +  next
   2.312 +    assume neq: "v \<noteq> x"
   2.313 +    have "elim [(v, Var x)] v"
   2.314 +      by (auto intro!:remove_var simp:neq)
   2.315 +    thus ?thesis ..
   2.316 +  qed
   2.317 +next
   2.318 +  case (Const c)
   2.319 +  have "elim [(v, Const c)] v"
   2.320 +    by (auto intro!:remove_var)
   2.321 +  thus ?case ..
   2.322 +next
   2.323 +  case (App M N)
   2.324 +  
   2.325 +  hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
   2.326 +    and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
   2.327 +    and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
   2.328 +    by auto
   2.329 +
   2.330 +  from nonocc have "\<not> [(v,M)] =\<^sub>s []"
   2.331 +    by (simp add:var_same[symmetric])
   2.332 +  with ih1 have "elim [(v, M)] v" by blast
   2.333 +  hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
   2.334 +  hence not_in_M: "v \<notin> vars_of M" by simp
   2.335 +
   2.336 +  from nonocc have "\<not> [(v,N)] =\<^sub>s []"
   2.337 +    by (simp add:var_same[symmetric])
   2.338 +  with ih2 have "elim [(v, N)] v" by blast
   2.339 +  hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
   2.340 +  hence not_in_N: "v \<notin> vars_of N" by simp
   2.341 +
   2.342 +  have "elim [(v, M \<cdot> N)] v"
   2.343 +  proof 
   2.344 +    fix t 
   2.345 +    show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
   2.346 +    proof (induct t)
   2.347 +      case (Var x) thus ?case by (simp add: not_in_M not_in_N)
   2.348 +    qed auto
   2.349 +  qed
   2.350 +  thus ?case ..
   2.351 +qed
   2.352 +
   2.353 +text {* The result of a unification never introduces new variables: *}
   2.354 +
   2.355 +lemma unify_vars: 
   2.356 +  assumes "unify_dom (M, N)"
   2.357 +  assumes "unify M N = Some \<sigma>"
   2.358 +  shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   2.359 +  (is "?P M N \<sigma> t")
   2.360 +using prems
   2.361 +proof (induct M N arbitrary:\<sigma> t)
   2.362 +  case (3 c v) 
   2.363 +  hence "\<sigma> = [(v, Const c)]" by simp
   2.364 +  thus ?case by (induct t, auto)
   2.365 +next
   2.366 +  case (4 M N v) 
   2.367 +  hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   2.368 +  with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
   2.369 +  thus ?case by (induct t, auto)
   2.370 +next
   2.371 +  case (5 v M)
   2.372 +  hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   2.373 +  with prems have "\<sigma> = [(v, M)]" by simp
   2.374 +  thus ?case by (induct t, auto)
   2.375 +next
   2.376 +  case (7 M N M' N' \<sigma>)
   2.377 +  then obtain \<theta>1 \<theta>2 
   2.378 +    where "unify M M' = Some \<theta>1"
   2.379 +    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   2.380 +    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   2.381 +    and ih1: "\<And>t. ?P M M' \<theta>1 t"
   2.382 +    and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
   2.383 +    by (auto split:option.split_asm)
   2.384 +
   2.385 +  show ?case
   2.386 +  proof
   2.387 +    fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
   2.388 +    
   2.389 +    show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   2.390 +    proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   2.391 +	    \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   2.392 +      case True
   2.393 +      with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   2.394 +	    by auto
   2.395 +      
   2.396 +      from a and ih2[where t="t \<triangleleft> \<theta>1"]
   2.397 +      have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1) 
   2.398 +        \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
   2.399 +	    by auto
   2.400 +      hence "v \<in> vars_of t"
   2.401 +      proof
   2.402 +	    assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   2.403 +	    with True show ?thesis by (auto dest:l)
   2.404 +      next
   2.405 +	    assume "v \<in> vars_of (t \<triangleleft> \<theta>1)" 
   2.406 +	    thus ?thesis by (rule l)
   2.407 +      qed
   2.408 +      
   2.409 +      thus ?thesis by auto
   2.410 +    qed auto
   2.411 +  qed
   2.412 +qed (auto split: split_if_asm)
   2.413 +
   2.414 +
   2.415 +text {* The result of a unification is either the identity
   2.416 +substitution or it eliminates a variable from one of the terms: *}
   2.417 +
   2.418 +lemma unify_eliminates: 
   2.419 +  assumes "unify_dom (M, N)"
   2.420 +  assumes "unify M N = Some \<sigma>"
   2.421 +  shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
   2.422 +  (is "?P M N \<sigma>")
   2.423 +using prems
   2.424 +proof (induct M N arbitrary:\<sigma>)
   2.425 +  case 1 thus ?case by simp
   2.426 +next
   2.427 +  case 2 thus ?case by simp
   2.428 +next
   2.429 +  case (3 c v)
   2.430 +  have no_occ: "\<not> occ (Var v) (Const c)" by simp
   2.431 +  with prems have "\<sigma> = [(v, Const c)]" by simp
   2.432 +  with occ_elim[OF no_occ]
   2.433 +  show ?case by auto
   2.434 +next
   2.435 +  case (4 M N v)
   2.436 +  hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   2.437 +  with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
   2.438 +  with occ_elim[OF no_occ]
   2.439 +  show ?case by auto 
   2.440 +next
   2.441 +  case (5 v M) 
   2.442 +  hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   2.443 +  with prems have "\<sigma> = [(v, M)]" by simp
   2.444 +  with occ_elim[OF no_occ]
   2.445 +  show ?case by auto 
   2.446 +next 
   2.447 +  case (6 c d) thus ?case
   2.448 +    by (cases "c = d") auto
   2.449 +next
   2.450 +  case (7 M N M' N' \<sigma>)
   2.451 +  then obtain \<theta>1 \<theta>2 
   2.452 +    where "unify M M' = Some \<theta>1"
   2.453 +    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   2.454 +    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   2.455 +    and ih1: "?P M M' \<theta>1"
   2.456 +    and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
   2.457 +    by (auto split:option.split_asm)
   2.458 +
   2.459 +  from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   2.460 +  have "unify_dom (M, M')"
   2.461 +    by (rule acc_downward) (rule unify_rel.intros)
   2.462 +  hence no_new_vars: 
   2.463 +    "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   2.464 +    by (rule unify_vars)
   2.465 +
   2.466 +  from ih2 show ?case 
   2.467 +  proof 
   2.468 +    assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
   2.469 +    then obtain v 
   2.470 +      where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   2.471 +      and el: "elim \<theta>2 v" by auto
   2.472 +    with no_new_vars show ?thesis unfolding \<sigma> 
   2.473 +      by (auto simp:elim_def)
   2.474 +  next
   2.475 +    assume empty[simp]: "\<theta>2 =\<^sub>s []"
   2.476 +
   2.477 +    have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
   2.478 +      by (rule compose_eqv) auto
   2.479 +    also have "\<dots> =\<^sub>s \<theta>1" by auto
   2.480 +    finally have "\<sigma> =\<^sub>s \<theta>1" .
   2.481 +
   2.482 +    from ih1 show ?thesis
   2.483 +    proof
   2.484 +      assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   2.485 +      with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
   2.486 +      show ?thesis by auto
   2.487 +    next
   2.488 +      note `\<sigma> =\<^sub>s \<theta>1`
   2.489 +      also assume "\<theta>1 =\<^sub>s []"
   2.490 +      finally show ?thesis ..
   2.491 +    qed
   2.492 +  qed
   2.493 +qed
   2.494 +
   2.495 +
   2.496 +subsection {* Termination proof *}
   2.497 +
   2.498 +
   2.499 +termination unify
   2.500 +proof 
   2.501 +  let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
   2.502 +                           \<lambda>(M, N). size M]"
   2.503 +  show "wf ?R" by simp
   2.504 +
   2.505 +  fix M N M' N' 
   2.506 +  show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
   2.507 +    by (rule measures_lesseq) (auto intro: card_mono)
   2.508 +
   2.509 +  fix \<theta>                                   -- "Outer call"
   2.510 +  assume inner: "unify_dom (M, M')"
   2.511 +    "unify M M' = Some \<theta>"
   2.512 +
   2.513 +  from unify_eliminates[OF inner]
   2.514 +  show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   2.515 +  proof
   2.516 +    -- {* Either a variable is eliminated \ldots *}
   2.517 +    assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   2.518 +    then obtain v 
   2.519 +	  where "elim \<theta> v" 
   2.520 +	  and "v\<in>vars_of M \<union> vars_of M'" by auto
   2.521 +    with unify_vars[OF inner]
   2.522 +    have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
   2.523 +	  \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   2.524 +	  by auto
   2.525 +    
   2.526 +    thus ?thesis
   2.527 +      by (auto intro!: measures_less intro: psubset_card_mono)
   2.528 +  next
   2.529 +    -- {* Or the substitution is empty *}
   2.530 +    assume "\<theta> =\<^sub>s []"
   2.531 +    hence "N \<triangleleft> \<theta> = N" 
   2.532 +	  and "N' \<triangleleft> \<theta> = N'" by auto
   2.533 +    thus ?thesis 
   2.534 +       by (auto intro!: measures_less intro: psubset_card_mono)
   2.535 +  qed
   2.536 +qed
   2.537 +
   2.538 +
   2.539 +(*<*)end(*>*)
   2.540 +
   2.541 +
   2.542 +
   2.543 +
   2.544 +
   2.545 +
   2.546 +
   2.547 +
   2.548 +
   2.549 +
   2.550 +
   2.551 +
   2.552 +
   2.553 +
   2.554 +
   2.555 +
   2.556 +
   2.557 +