src/HOL/ex/Unification.thy
changeset 22999 c1ce129e6f9c
child 23024 70435ffe077d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Unification.thy	Thu May 17 22:33:41 2007 +0200
     1.3 @@ -0,0 +1,554 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Alexander Krauss, Technische Universitaet Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Case study: Unification Algorithm *}
     1.9 +
    1.10 +(*<*)theory Unification
    1.11 +imports Main
    1.12 +begin(*>*)
    1.13 +
    1.14 +text {* 
    1.15 +  This is a formalization of a first-order unification
    1.16 +  algorithm. It uses the new "function" package to define recursive
    1.17 +  functions, which allows a better treatment of nested recursion. 
    1.18 +
    1.19 +  This is basically a modernized version of a previous formalization
    1.20 +  by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
    1.21 +  previous work by Paulson and Manna & Waldinger (for details, see
    1.22 +  there).
    1.23 +
    1.24 +  Unlike that formalization, where the proofs of termination and
    1.25 +  some partial correctness properties are intertwined, we can prove
    1.26 +  partial correctness and termination separately.
    1.27 +*}
    1.28 +
    1.29 +subsection {* Basic definitions *}
    1.30 +
    1.31 +datatype 'a trm = 
    1.32 +  Var 'a 
    1.33 +  | Const 'a
    1.34 +  | App "'a trm" "'a trm" (infix "\<cdot>" 60)
    1.35 +
    1.36 +types
    1.37 +  'a subst = "('a \<times> 'a trm) list"
    1.38 +
    1.39 +text {* Applying a substitution to a variable: *}
    1.40 +
    1.41 +fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
    1.42 +where
    1.43 +  "assoc x d [] = d"
    1.44 +| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
    1.45 +
    1.46 +text {* Applying a substitution to a term: *}
    1.47 +
    1.48 +fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
    1.49 +where
    1.50 +  "(Var v) \<triangleleft> s = assoc v (Var v) s"
    1.51 +| "(Const c) \<triangleleft> s = (Const c)"
    1.52 +| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
    1.53 +
    1.54 +text {* Composition of substitutions: *}
    1.55 +
    1.56 +fun
    1.57 +  "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
    1.58 +where
    1.59 +  "[] \<bullet> bl = bl"
    1.60 +| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
    1.61 +
    1.62 +text {* Equivalence of substitutions: *}
    1.63 +
    1.64 +definition eqv (infix "=\<^sub>s" 50)
    1.65 +where
    1.66 +  "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2" 
    1.67 +
    1.68 +subsection {* Basic lemmas *}
    1.69 +
    1.70 +lemma apply_empty[simp]: "t \<triangleleft> [] = t"
    1.71 +by (induct t) auto
    1.72 +
    1.73 +lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
    1.74 +by (induct \<sigma>) auto
    1.75 +
    1.76 +lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
    1.77 +proof (induct t)
    1.78 +  case App thus ?case by simp
    1.79 +next 
    1.80 +  case Const thus ?case by simp
    1.81 +next
    1.82 +  case (Var v) thus ?case
    1.83 +  proof (induct s1)
    1.84 +    case Nil show ?case by simp
    1.85 +  next
    1.86 +    case (Cons p s1s) thus ?case by (cases p, simp)
    1.87 +  qed
    1.88 +qed
    1.89 +
    1.90 +lemma eqv_refl[intro]: "s =\<^sub>s s"
    1.91 +  by (auto simp:eqv_def)
    1.92 +
    1.93 +lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
    1.94 +  by (auto simp:eqv_def)
    1.95 +
    1.96 +lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
    1.97 +  by (auto simp:eqv_def)
    1.98 +
    1.99 +lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
   1.100 +  by (auto simp:eqv_def)
   1.101 +
   1.102 +lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
   1.103 +  by (auto simp:eqv_def)
   1.104 +
   1.105 +lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
   1.106 +  by (auto simp:eqv_def)
   1.107 +
   1.108 +lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
   1.109 +  by auto
   1.110 +
   1.111 +subsection {* Specification: Most general unifiers *}
   1.112 +
   1.113 +definition
   1.114 +  "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
   1.115 +
   1.116 +definition
   1.117 +  "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u 
   1.118 +  \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
   1.119 +
   1.120 +lemma MGUI[intro]:
   1.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>
   1.122 +  \<Longrightarrow> MGU \<sigma> t u"
   1.123 +  by (simp only:Unifier_def MGU_def, auto)
   1.124 +
   1.125 +lemma MGU_sym[sym]:
   1.126 +  "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
   1.127 +  by (auto simp:MGU_def Unifier_def)
   1.128 +
   1.129 +
   1.130 +subsection {* The unification algorithm *}
   1.131 +
   1.132 +text {* Occurs check: Proper subterm relation *}
   1.133 +
   1.134 +fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   1.135 +where
   1.136 +  "occ u (Var v) = False"
   1.137 +| "occ u (Const c) = False"
   1.138 +| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
   1.139 +
   1.140 +text {* The unification algorithm: *}
   1.141 +
   1.142 +function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   1.143 +where
   1.144 +  "unify (Const c) (M \<cdot> N)   = None"
   1.145 +| "unify (M \<cdot> N)   (Const c) = None"
   1.146 +| "unify (Const c) (Var v)   = Some [(v, Const c)]"
   1.147 +| "unify (M \<cdot> N)   (Var v)   = (if (occ (Var v) (M \<cdot> N)) 
   1.148 +                                        then None
   1.149 +                                        else Some [(v, M \<cdot> N)])"
   1.150 +| "unify (Var v)   M         = (if (occ (Var v) M) 
   1.151 +                                        then None
   1.152 +                                        else Some [(v, M)])"
   1.153 +| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   1.154 +| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   1.155 +                                    None \<Rightarrow> None |
   1.156 +                                    Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
   1.157 +                                      of None \<Rightarrow> None |
   1.158 +                                         Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   1.159 +  by pat_completeness auto
   1.160 +
   1.161 +
   1.162 +subsection {* Partial correctness *}
   1.163 +
   1.164 +text {* Some lemmas about occ and MGU: *}
   1.165 +
   1.166 +lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
   1.167 +  \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
   1.168 +by (induct t) auto
   1.169 +
   1.170 +lemma MGU_Var[intro]: 
   1.171 +  assumes no_occ: "\<not>occ (Var v) t"
   1.172 +  shows "MGU [(v,t)] (Var v) t"
   1.173 +proof (intro MGUI exI)
   1.174 +  show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
   1.175 +    by (cases "Var v = t", auto simp:subst_no_occ)
   1.176 +next
   1.177 +  fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>" 
   1.178 +  show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>" 
   1.179 +  proof
   1.180 +    fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th 
   1.181 +      by (induct s, auto)
   1.182 +  qed
   1.183 +qed
   1.184 +
   1.185 +declare MGU_Var[symmetric, intro]
   1.186 +
   1.187 +lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
   1.188 +  unfolding MGU_def Unifier_def
   1.189 +  by auto
   1.190 +  
   1.191 +text {* If unification terminates, then it computes most general unifiers: *}
   1.192 +
   1.193 +lemma unify_partial_correctness:
   1.194 +  assumes "unify_dom (M, N)"
   1.195 +  assumes "unify M N = Some \<sigma>"
   1.196 +  shows "MGU \<sigma> M N"
   1.197 +using prems
   1.198 +proof (induct M N arbitrary: \<sigma>)
   1.199 +  case (7 M N M' N' \<sigma>) -- "The interesting case"
   1.200 +
   1.201 +  then obtain \<theta>1 \<theta>2 
   1.202 +    where "unify M M' = Some \<theta>1"
   1.203 +    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   1.204 +    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   1.205 +    and MGU_inner: "MGU \<theta>1 M M'" 
   1.206 +    and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
   1.207 +    by (auto split:option.split_asm)
   1.208 +
   1.209 +  show ?case
   1.210 +  proof
   1.211 +    from MGU_inner and MGU_outer
   1.212 +    have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1" 
   1.213 +      and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
   1.214 +      unfolding MGU_def Unifier_def
   1.215 +      by auto
   1.216 +    thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
   1.217 +      by simp
   1.218 +  next
   1.219 +    fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
   1.220 +    hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
   1.221 +      and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
   1.222 +
   1.223 +    with MGU_inner obtain \<delta>
   1.224 +      where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
   1.225 +      unfolding MGU_def Unifier_def
   1.226 +      by auto
   1.227 +
   1.228 +    from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
   1.229 +      by (simp add:eqv_dest[OF eqv])
   1.230 +
   1.231 +    with MGU_outer obtain \<rho>
   1.232 +      where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
   1.233 +      unfolding MGU_def Unifier_def
   1.234 +      by auto
   1.235 +    
   1.236 +    have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
   1.237 +      by (rule eqv_intro, auto simp:eqv_dest[OF eqv] 
   1.238 +	eqv_dest[OF eqv2])
   1.239 +    thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
   1.240 +  qed
   1.241 +qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
   1.242 +
   1.243 +
   1.244 +subsection {* Properties used in termination proof *}
   1.245 +
   1.246 +text {* The variables of a term: *}
   1.247 +
   1.248 +fun vars_of:: "'a trm \<Rightarrow> 'a set"
   1.249 +where
   1.250 +  "vars_of (Var v) = { v }"
   1.251 +| "vars_of (Const c) = {}"
   1.252 +| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
   1.253 +
   1.254 +lemma vars_of_finite[intro]: "finite (vars_of t)"
   1.255 +  by (induct t) simp_all
   1.256 +
   1.257 +text {* Elimination of variables by a substitution: *}
   1.258 +
   1.259 +definition
   1.260 +  "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   1.261 +
   1.262 +lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   1.263 +  by (auto simp:elim_def)
   1.264 +
   1.265 +lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
   1.266 +  by (auto simp:elim_def)
   1.267 +
   1.268 +lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   1.269 +  by (auto simp:elim_def eqv_def)
   1.270 +
   1.271 +
   1.272 +text {* Replacing a variable by itself yields an identity subtitution: *}
   1.273 +
   1.274 +lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
   1.275 +proof
   1.276 +  fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
   1.277 +    by (induct t) simp_all
   1.278 +qed
   1.279 +
   1.280 +lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])"
   1.281 +proof
   1.282 +  assume t_v: "t = Var v"
   1.283 +  thus "[(v, t)] =\<^sub>s []"
   1.284 +    by auto
   1.285 +next
   1.286 +  assume id: "[(v, t)] =\<^sub>s []"
   1.287 +  show "t = Var v"
   1.288 +  proof -
   1.289 +    have "t = Var v \<triangleleft> [(v, t)]" by simp
   1.290 +    also from id have "\<dots> = Var v \<triangleleft> []" ..
   1.291 +    finally show ?thesis by simp
   1.292 +  qed
   1.293 +qed
   1.294 +
   1.295 +text {* A lemma about occ and elim *}
   1.296 +
   1.297 +lemma remove_var:
   1.298 +  assumes [simp]: "v \<notin> vars_of s"
   1.299 +  shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
   1.300 +  by (induct t) simp_all
   1.301 +
   1.302 +lemma occ_elim: "\<not>occ (Var v) t 
   1.303 +  \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
   1.304 +proof (induct t)
   1.305 +  case (Var x)
   1.306 +  show ?case
   1.307 +  proof cases
   1.308 +    assume "v = x"
   1.309 +    thus ?thesis
   1.310 +      by (simp add:var_same[symmetric])
   1.311 +  next
   1.312 +    assume neq: "v \<noteq> x"
   1.313 +    have "elim [(v, Var x)] v"
   1.314 +      by (auto intro!:remove_var simp:neq)
   1.315 +    thus ?thesis ..
   1.316 +  qed
   1.317 +next
   1.318 +  case (Const c)
   1.319 +  have "elim [(v, Const c)] v"
   1.320 +    by (auto intro!:remove_var)
   1.321 +  thus ?case ..
   1.322 +next
   1.323 +  case (App M N)
   1.324 +  
   1.325 +  hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
   1.326 +    and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
   1.327 +    and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
   1.328 +    by auto
   1.329 +
   1.330 +  from nonocc have "\<not> [(v,M)] =\<^sub>s []"
   1.331 +    by (simp add:var_same[symmetric])
   1.332 +  with ih1 have "elim [(v, M)] v" by blast
   1.333 +  hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
   1.334 +  hence not_in_M: "v \<notin> vars_of M" by simp
   1.335 +
   1.336 +  from nonocc have "\<not> [(v,N)] =\<^sub>s []"
   1.337 +    by (simp add:var_same[symmetric])
   1.338 +  with ih2 have "elim [(v, N)] v" by blast
   1.339 +  hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
   1.340 +  hence not_in_N: "v \<notin> vars_of N" by simp
   1.341 +
   1.342 +  have "elim [(v, M \<cdot> N)] v"
   1.343 +  proof 
   1.344 +    fix t 
   1.345 +    show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
   1.346 +    proof (induct t)
   1.347 +      case (Var x) thus ?case by (simp add: not_in_M not_in_N)
   1.348 +    qed auto
   1.349 +  qed
   1.350 +  thus ?case ..
   1.351 +qed
   1.352 +
   1.353 +text {* The result of a unification never introduces new variables: *}
   1.354 +
   1.355 +lemma unify_vars: 
   1.356 +  assumes "unify_dom (M, N)"
   1.357 +  assumes "unify M N = Some \<sigma>"
   1.358 +  shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   1.359 +  (is "?P M N \<sigma> t")
   1.360 +using prems
   1.361 +proof (induct M N arbitrary:\<sigma> t)
   1.362 +  case (3 c v) 
   1.363 +  hence "\<sigma> = [(v, Const c)]" by simp
   1.364 +  thus ?case by (induct t, auto)
   1.365 +next
   1.366 +  case (4 M N v) 
   1.367 +  hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   1.368 +  with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
   1.369 +  thus ?case by (induct t, auto)
   1.370 +next
   1.371 +  case (5 v M)
   1.372 +  hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   1.373 +  with prems have "\<sigma> = [(v, M)]" by simp
   1.374 +  thus ?case by (induct t, auto)
   1.375 +next
   1.376 +  case (7 M N M' N' \<sigma>)
   1.377 +  then obtain \<theta>1 \<theta>2 
   1.378 +    where "unify M M' = Some \<theta>1"
   1.379 +    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   1.380 +    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   1.381 +    and ih1: "\<And>t. ?P M M' \<theta>1 t"
   1.382 +    and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
   1.383 +    by (auto split:option.split_asm)
   1.384 +
   1.385 +  show ?case
   1.386 +  proof
   1.387 +    fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
   1.388 +    
   1.389 +    show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   1.390 +    proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   1.391 +	    \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   1.392 +      case True
   1.393 +      with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   1.394 +	    by auto
   1.395 +      
   1.396 +      from a and ih2[where t="t \<triangleleft> \<theta>1"]
   1.397 +      have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1) 
   1.398 +        \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
   1.399 +	    by auto
   1.400 +      hence "v \<in> vars_of t"
   1.401 +      proof
   1.402 +	    assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   1.403 +	    with True show ?thesis by (auto dest:l)
   1.404 +      next
   1.405 +	    assume "v \<in> vars_of (t \<triangleleft> \<theta>1)" 
   1.406 +	    thus ?thesis by (rule l)
   1.407 +      qed
   1.408 +      
   1.409 +      thus ?thesis by auto
   1.410 +    qed auto
   1.411 +  qed
   1.412 +qed (auto split: split_if_asm)
   1.413 +
   1.414 +
   1.415 +text {* The result of a unification is either the identity
   1.416 +substitution or it eliminates a variable from one of the terms: *}
   1.417 +
   1.418 +lemma unify_eliminates: 
   1.419 +  assumes "unify_dom (M, N)"
   1.420 +  assumes "unify M N = Some \<sigma>"
   1.421 +  shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
   1.422 +  (is "?P M N \<sigma>")
   1.423 +using prems
   1.424 +proof (induct M N arbitrary:\<sigma>)
   1.425 +  case 1 thus ?case by simp
   1.426 +next
   1.427 +  case 2 thus ?case by simp
   1.428 +next
   1.429 +  case (3 c v)
   1.430 +  have no_occ: "\<not> occ (Var v) (Const c)" by simp
   1.431 +  with prems have "\<sigma> = [(v, Const c)]" by simp
   1.432 +  with occ_elim[OF no_occ]
   1.433 +  show ?case by auto
   1.434 +next
   1.435 +  case (4 M N v)
   1.436 +  hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
   1.437 +  with prems have "\<sigma> = [(v, M\<cdot>N)]" by simp
   1.438 +  with occ_elim[OF no_occ]
   1.439 +  show ?case by auto 
   1.440 +next
   1.441 +  case (5 v M) 
   1.442 +  hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
   1.443 +  with prems have "\<sigma> = [(v, M)]" by simp
   1.444 +  with occ_elim[OF no_occ]
   1.445 +  show ?case by auto 
   1.446 +next 
   1.447 +  case (6 c d) thus ?case
   1.448 +    by (cases "c = d") auto
   1.449 +next
   1.450 +  case (7 M N M' N' \<sigma>)
   1.451 +  then obtain \<theta>1 \<theta>2 
   1.452 +    where "unify M M' = Some \<theta>1"
   1.453 +    and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
   1.454 +    and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
   1.455 +    and ih1: "?P M M' \<theta>1"
   1.456 +    and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
   1.457 +    by (auto split:option.split_asm)
   1.458 +
   1.459 +  from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   1.460 +  have "unify_dom (M, M')"
   1.461 +    by (rule acc_downward) (rule unify_rel.intros)
   1.462 +  hence no_new_vars: 
   1.463 +    "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   1.464 +    by (rule unify_vars)
   1.465 +
   1.466 +  from ih2 show ?case 
   1.467 +  proof 
   1.468 +    assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
   1.469 +    then obtain v 
   1.470 +      where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
   1.471 +      and el: "elim \<theta>2 v" by auto
   1.472 +    with no_new_vars show ?thesis unfolding \<sigma> 
   1.473 +      by (auto simp:elim_def)
   1.474 +  next
   1.475 +    assume empty[simp]: "\<theta>2 =\<^sub>s []"
   1.476 +
   1.477 +    have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
   1.478 +      by (rule compose_eqv) auto
   1.479 +    also have "\<dots> =\<^sub>s \<theta>1" by auto
   1.480 +    finally have "\<sigma> =\<^sub>s \<theta>1" .
   1.481 +
   1.482 +    from ih1 show ?thesis
   1.483 +    proof
   1.484 +      assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   1.485 +      with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
   1.486 +      show ?thesis by auto
   1.487 +    next
   1.488 +      note `\<sigma> =\<^sub>s \<theta>1`
   1.489 +      also assume "\<theta>1 =\<^sub>s []"
   1.490 +      finally show ?thesis ..
   1.491 +    qed
   1.492 +  qed
   1.493 +qed
   1.494 +
   1.495 +
   1.496 +subsection {* Termination proof *}
   1.497 +
   1.498 +
   1.499 +termination unify
   1.500 +proof 
   1.501 +  let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
   1.502 +                           \<lambda>(M, N). size M]"
   1.503 +  show "wf ?R" by simp
   1.504 +
   1.505 +  fix M N M' N' 
   1.506 +  show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
   1.507 +    by (rule measures_lesseq) (auto intro: card_mono)
   1.508 +
   1.509 +  fix \<theta>                                   -- "Outer call"
   1.510 +  assume inner: "unify_dom (M, M')"
   1.511 +    "unify M M' = Some \<theta>"
   1.512 +
   1.513 +  from unify_eliminates[OF inner]
   1.514 +  show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   1.515 +  proof
   1.516 +    -- {* Either a variable is eliminated \ldots *}
   1.517 +    assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   1.518 +    then obtain v 
   1.519 +	  where "elim \<theta> v" 
   1.520 +	  and "v\<in>vars_of M \<union> vars_of M'" by auto
   1.521 +    with unify_vars[OF inner]
   1.522 +    have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
   1.523 +	  \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   1.524 +	  by auto
   1.525 +    
   1.526 +    thus ?thesis
   1.527 +      by (auto intro!: measures_less intro: psubset_card_mono)
   1.528 +  next
   1.529 +    -- {* Or the substitution is empty *}
   1.530 +    assume "\<theta> =\<^sub>s []"
   1.531 +    hence "N \<triangleleft> \<theta> = N" 
   1.532 +	  and "N' \<triangleleft> \<theta> = N'" by auto
   1.533 +    thus ?thesis 
   1.534 +       by (auto intro!: measures_less intro: psubset_card_mono)
   1.535 +  qed
   1.536 +qed
   1.537 +
   1.538 +
   1.539 +(*<*)end(*>*)
   1.540 +
   1.541 +
   1.542 +
   1.543 +
   1.544 +
   1.545 +
   1.546 +
   1.547 +
   1.548 +
   1.549 +
   1.550 +
   1.551 +
   1.552 +
   1.553 +
   1.554 +
   1.555 +
   1.556 +
   1.557 +