src/HOL/ex/Unification.thy
author krauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 44370 03d91bfad83b
parent 44369 02e13192a053
child 44371 3a10392fb8c3
permissions -rw-r--r--
tuned proofs, sledgehammering overly verbose parts
     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 remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
   110 by (induct t) simp_all
   111 
   112 lemma subst_refl[iff]: "s \<doteq> s"
   113   by (auto simp:subst_eq_def)
   114 
   115 lemma subst_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
   116   by (auto simp:subst_eq_def)
   117 
   118 lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
   119   by (auto simp:subst_eq_def)
   120 
   121 
   122 text {* Composition of Substitutions *}
   123 
   124 lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
   125 by (induct \<sigma>) auto
   126 
   127 lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
   128 proof (induct t)
   129   case (Var v) thus ?case
   130     by (induct r) auto
   131 qed auto
   132 
   133 lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
   134   by (auto simp:subst_eq_def)
   135 
   136 lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
   137   by (auto simp:subst_eq_def)
   138 
   139 lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
   140   by auto
   141 
   142 lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
   143   by (auto simp: subst_eq_def)
   144 
   145 lemma var_self: "[(v, Var v)] \<doteq> []"
   146 proof
   147   fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
   148     by (induct t) simp_all
   149 qed
   150 
   151 lemma var_same[simp]: "[(v, t)] \<doteq> [] \<longleftrightarrow> t = Var v"
   152 by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
   153 
   154 
   155 subsection {* Specification: Most general unifiers *}
   156 
   157 definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   158 where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
   159 
   160 definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
   161   "MGU \<sigma> t u \<longleftrightarrow> 
   162    Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
   163 
   164 lemma MGUI[intro]:
   165   "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
   166   \<Longrightarrow> MGU \<sigma> t u"
   167   by (simp only:Unifier_def MGU_def, auto)
   168 
   169 lemma MGU_sym[sym]:
   170   "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
   171   by (auto simp:MGU_def Unifier_def)
   172 
   173 lemma MGU_Var: 
   174   assumes "\<not> Var v \<prec> t"
   175   shows "MGU [(v,t)] (Var v) t"
   176 proof (intro MGUI exI)
   177   show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using assms
   178     by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
   179 next
   180   fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
   181   show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
   182   proof
   183     fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
   184       by (induct s) auto
   185   qed
   186 qed
   187 
   188 lemma MGU_Const: "MGU [] (Const c) (Const d) \<longleftrightarrow> c = d"
   189   by (auto simp: MGU_def Unifier_def)
   190   
   191 
   192 definition Idem :: "'a subst \<Rightarrow> bool"
   193 where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
   194 
   195 
   196 
   197 subsection {* The unification algorithm *}
   198 
   199 
   200 text {* The unification algorithm: *}
   201 
   202 function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   203 where
   204   "unify (Const c) (M \<cdot> N)   = None"
   205 | "unify (M \<cdot> N)   (Const c) = None"
   206 | "unify (Const c) (Var v)   = Some [(v, Const c)]"
   207 | "unify (M \<cdot> N)   (Var v)   = (if Var v \<prec> M \<cdot> N 
   208                                         then None
   209                                         else Some [(v, M \<cdot> N)])"
   210 | "unify (Var v)   M         = (if Var v \<prec> M
   211                                         then None
   212                                         else Some [(v, M)])"
   213 | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   214 | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   215                                     None \<Rightarrow> None |
   216                                     Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
   217                                       of None \<Rightarrow> None |
   218                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
   219   by pat_completeness auto
   220 
   221 subsection {* Properties used in termination proof *}
   222 
   223 
   224 text {* Elimination of variables by a substitution: *}
   225 
   226 definition
   227   "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<lhd> \<sigma>)"
   228 
   229 lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<lhd> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   230   by (auto simp:elim_def)
   231 
   232 lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
   233   by (auto simp:elim_def)
   234 
   235 lemma elim_eq: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   236   by (auto simp:elim_def subst_eq_def)
   237 
   238 lemma occs_elim: "\<not> Var v \<prec> t 
   239   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
   240 by (metis elim_intro remove_var var_same vars_iff_occseq)
   241 
   242 text {* The result of a unification never introduces new variables: *}
   243 
   244 declare unify.psimps[simp]
   245 
   246 lemma unify_vars: 
   247   assumes "unify_dom (M, N)"
   248   assumes "unify M N = Some \<sigma>"
   249   shows "vars_of (t \<lhd> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   250   (is "?P M N \<sigma> t")
   251 using assms
   252 proof (induct M N arbitrary:\<sigma> t)
   253   case (3 c v) 
   254   hence "\<sigma> = [(v, Const c)]" by simp
   255   thus ?case by (induct t) auto
   256 next
   257   case (4 M N v) 
   258   hence "\<not> Var v \<prec> M \<cdot> N" by auto
   259   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   260   thus ?case by (induct t) auto
   261 next
   262   case (5 v M)
   263   hence "\<not> Var v \<prec> M" by auto
   264   with 5 have "\<sigma> = [(v, M)]" by simp
   265   thus ?case by (induct t) auto
   266 next
   267   case (7 M N M' N' \<sigma>)
   268   then obtain \<theta>1 \<theta>2 
   269     where "unify M M' = Some \<theta>1"
   270     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   271     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   272     and ih1: "\<And>t. ?P M M' \<theta>1 t"
   273     and ih2: "\<And>t. ?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2 t"
   274     by (auto split:option.split_asm)
   275 
   276   show ?case
   277   proof
   278     fix v assume a: "v \<in> vars_of (t \<lhd> \<sigma>)"
   279     
   280     show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   281     proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   282         \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   283       case True
   284       with ih1 have l:"\<And>t. v \<in> vars_of (t \<lhd> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   285         by auto
   286       
   287       from a and ih2[where t="t \<lhd> \<theta>1"]
   288       have "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1) 
   289         \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
   290         by auto
   291       hence "v \<in> vars_of t"
   292       proof
   293         assume "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
   294         with True show ?thesis by (auto dest:l)
   295       next
   296         assume "v \<in> vars_of (t \<lhd> \<theta>1)" 
   297         thus ?thesis by (rule l)
   298       qed
   299       
   300       thus ?thesis by auto
   301     qed auto
   302   qed
   303 qed (auto split: split_if_asm)
   304 
   305 
   306 text {* The result of a unification is either the identity
   307 substitution or it eliminates a variable from one of the terms: *}
   308 
   309 lemma unify_eliminates: 
   310   assumes "unify_dom (M, N)"
   311   assumes "unify M N = Some \<sigma>"
   312   shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> \<doteq> []"
   313   (is "?P M N \<sigma>")
   314 using assms
   315 proof (induct M N arbitrary:\<sigma>)
   316   case 1 thus ?case by simp
   317 next
   318   case 2 thus ?case by simp
   319 next
   320   case (3 c v)
   321   have no_occs: "\<not> Var v \<prec> Const c" by simp
   322   with 3 have "\<sigma> = [(v, Const c)]" by simp
   323   with occs_elim[OF no_occs]
   324   show ?case by auto
   325 next
   326   case (4 M N v)
   327   hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
   328   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   329   with occs_elim[OF no_occs]
   330   show ?case by auto 
   331 next
   332   case (5 v M) 
   333   hence no_occs: "\<not> Var v \<prec> M" by auto
   334   with 5 have "\<sigma> = [(v, M)]" by simp
   335   with occs_elim[OF no_occs]
   336   show ?case by auto 
   337 next 
   338   case (6 c d) thus ?case
   339     by (cases "c = d") auto
   340 next
   341   case (7 M N M' N' \<sigma>)
   342   then obtain \<theta>1 \<theta>2 
   343     where "unify M M' = Some \<theta>1"
   344     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   345     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   346     and ih1: "?P M M' \<theta>1"
   347     and ih2: "?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2"
   348     by (auto split:option.split_asm)
   349 
   350   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
   351   have "unify_dom (M, M')"
   352     by (rule accp_downward) (rule unify_rel.intros)
   353   hence no_new_vars: 
   354     "\<And>t. vars_of (t \<lhd> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   355     by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
   356 
   357   from ih2 show ?case 
   358   proof 
   359     assume "\<exists>v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1). elim \<theta>2 v"
   360     then obtain v 
   361       where "v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
   362       and el: "elim \<theta>2 v" by auto
   363     with no_new_vars show ?thesis unfolding \<sigma> 
   364       by (auto simp:elim_def)
   365   next
   366     assume empty[simp]: "\<theta>2 \<doteq> []"
   367 
   368     have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
   369       by (rule subst_cong) auto
   370     also have "\<dots> \<doteq> \<theta>1" by auto
   371     finally have "\<sigma> \<doteq> \<theta>1" .
   372 
   373     from ih1 show ?thesis
   374     proof
   375       assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   376       with elim_eq[OF `\<sigma> \<doteq> \<theta>1`]
   377       show ?thesis by auto
   378     next
   379       note `\<sigma> \<doteq> \<theta>1`
   380       also assume "\<theta>1 \<doteq> []"
   381       finally show ?thesis ..
   382     qed
   383   qed
   384 qed
   385 
   386 declare unify.psimps[simp del]
   387 
   388 subsection {* Termination proof *}
   389 
   390 termination unify
   391 proof 
   392   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
   393                            \<lambda>(M, N). size M]"
   394   show "wf ?R" by simp
   395 
   396   fix M N M' N' :: "'a trm"
   397   show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
   398     by (rule measures_lesseq) (auto intro: card_mono)
   399 
   400   fix \<theta>                                   -- "Outer call"
   401   assume inner: "unify_dom (M, M')"
   402     "unify M M' = Some \<theta>"
   403 
   404   from unify_eliminates[OF inner]
   405   show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   406   proof
   407     -- {* Either a variable is eliminated \ldots *}
   408     assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   409     then obtain v 
   410       where "elim \<theta> v" 
   411       and "v\<in>vars_of M \<union> vars_of M'" by auto
   412     with unify_vars[OF inner]
   413     have "vars_of (N\<lhd>\<theta>) \<union> vars_of (N'\<lhd>\<theta>)
   414       \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   415       by auto
   416     
   417     thus ?thesis
   418       by (auto intro!: measures_less intro: psubset_card_mono)
   419   next
   420     -- {* Or the substitution is empty *}
   421     assume "\<theta> \<doteq> []"
   422     hence "N \<lhd> \<theta> = N" 
   423       and "N' \<lhd> \<theta> = N'" by auto
   424     thus ?thesis 
   425        by (auto intro!: measures_less intro: psubset_card_mono)
   426   qed
   427 qed
   428 
   429 
   430 subsection {* Other Properties *}
   431 
   432 lemma unify_computes_MGU:
   433   "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
   434 using assms
   435 proof (induct M N arbitrary: \<sigma> rule: unify.induct)
   436   case (7 M N M' N' \<sigma>) -- "The interesting case"
   437 
   438   then obtain \<theta>1 \<theta>2 
   439     where "unify M M' = Some \<theta>1"
   440     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   441     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   442     and MGU_inner: "MGU \<theta>1 M M'" 
   443     and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   444     by (auto split:option.split_asm)
   445 
   446   show ?case
   447   proof
   448     from MGU_inner and MGU_outer
   449     have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
   450       and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
   451       unfolding MGU_def Unifier_def
   452       by auto
   453     thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
   454       by simp
   455   next
   456     fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
   457     hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
   458       and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
   459 
   460     with MGU_inner obtain \<delta>
   461       where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
   462       unfolding MGU_def Unifier_def
   463       by auto
   464 
   465     from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
   466       by (simp add:subst_eq_dest[OF eqv])
   467 
   468     with MGU_outer obtain \<rho>
   469       where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
   470       unfolding MGU_def Unifier_def
   471       by auto
   472     
   473     have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
   474       by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
   475     thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   476   qed
   477 qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
   478 
   479 
   480 
   481 end