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