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.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.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.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 +
```