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