src/HOL/ex/Unification.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 62390 842917225d56
child 67443 3abf6a722518
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Unification.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Author:     Konrad Slind, TUM & Cambridge University Computer Laboratory
     4     Author:     Alexander Krauss, TUM
     5 *)
     6 
     7 section \<open>Substitution and Unification\<close>
     8 
     9 theory Unification
    10 imports Main
    11 begin
    12 
    13 text \<open>
    14   Implements Manna \& Waldinger's formalization, with Paulson's
    15   simplifications, and some new simplifications by Slind and Krauss.
    16 
    17   Z Manna \& R Waldinger, Deductive Synthesis of the Unification
    18   Algorithm.  SCP 1 (1981), 5-48
    19 
    20   L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
    21   (1985), 143-170
    22 
    23   K Slind, Reasoning about Terminating Functional Programs,
    24   Ph.D. thesis, TUM, 1999, Sect. 5.8
    25 
    26   A Krauss, Partial and Nested Recursive Function Definitions in
    27   Higher-Order Logic, JAR 44(4):303-336, 2010. Sect. 6.3
    28 \<close>
    29 
    30 
    31 subsection \<open>Terms\<close>
    32 
    33 text \<open>Binary trees with leaves that are constants or variables.\<close>
    34 
    35 datatype 'a trm = 
    36   Var 'a 
    37   | Const 'a
    38   | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
    39 
    40 primrec vars_of :: "'a trm \<Rightarrow> 'a set"
    41 where
    42   "vars_of (Var v) = {v}"
    43 | "vars_of (Const c) = {}"
    44 | "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
    45 
    46 fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54) 
    47 where
    48   "u \<prec> Var v \<longleftrightarrow> False"
    49 | "u \<prec> Const c \<longleftrightarrow> False"
    50 | "u \<prec> M \<cdot> N \<longleftrightarrow> u = M \<or> u = N \<or> u \<prec> M \<or> u \<prec> N"
    51 
    52 
    53 lemma finite_vars_of[intro]: "finite (vars_of t)"
    54   by (induct t) simp_all
    55 
    56 lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
    57   by (induct t) auto
    58 
    59 lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
    60   by (induct N) auto
    61 
    62 
    63 subsection \<open>Substitutions\<close>
    64 
    65 type_synonym 'a subst = "('a \<times> 'a trm) list"
    66 
    67 fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
    68 where
    69   "assoc x d [] = d"
    70 | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
    71 
    72 primrec subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<lhd>" 55)
    73 where
    74   "(Var v) \<lhd> s = assoc v (Var v) s"
    75 | "(Const c) \<lhd> s = (Const c)"
    76 | "(M \<cdot> N) \<lhd> s = (M \<lhd> s) \<cdot> (N \<lhd> s)"
    77 
    78 definition subst_eq (infixr "\<doteq>" 52)
    79 where
    80   "s1 \<doteq> s2 \<longleftrightarrow> (\<forall>t. t \<lhd> s1 = t \<lhd> s2)" 
    81 
    82 fun comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
    83 where
    84   "[] \<lozenge> bl = bl"
    85 | "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
    86 
    87 lemma subst_Nil[simp]: "t \<lhd> [] = t"
    88 by (induct t) auto
    89 
    90 lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
    91 by (induct u) auto
    92 
    93 lemma agreement: "(t \<lhd> r = t \<lhd> s) \<longleftrightarrow> (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
    94 by (induct t) auto
    95 
    96 lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
    97 by (simp add: agreement)
    98 
    99 lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
   100 by (induct t) simp_all
   101 
   102 lemma subst_refl[iff]: "s \<doteq> s"
   103   by (auto simp:subst_eq_def)
   104 
   105 lemma subst_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
   106   by (auto simp:subst_eq_def)
   107 
   108 lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
   109   by (auto simp:subst_eq_def)
   110 
   111 lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
   112   \<Longrightarrow> t \<lhd> [(v,s)] = t"
   113 by (induct t) auto
   114 
   115 lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
   116 by (induct \<sigma>) auto
   117 
   118 lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
   119 proof (induct t)
   120   case (Var v) thus ?case
   121     by (induct r) auto
   122 qed auto
   123 
   124 lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
   125   by (auto simp:subst_eq_def)
   126 
   127 lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
   128   by (auto simp:subst_eq_def)
   129 
   130 lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
   131   by auto
   132 
   133 lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
   134   by (auto simp: subst_eq_def)
   135 
   136 lemma var_self: "[(v, Var v)] \<doteq> []"
   137 proof
   138   fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
   139     by (induct t) simp_all
   140 qed
   141 
   142 lemma var_same[simp]: "[(v, t)] \<doteq> [] \<longleftrightarrow> t = Var v"
   143 by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
   144 
   145 
   146 subsection \<open>Unifiers and Most General Unifiers\<close>
   147 
   148 definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
   149 where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
   150 
   151 definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
   152   "MGU \<sigma> t u \<longleftrightarrow> 
   153    Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
   154 
   155 lemma MGUI[intro]:
   156   "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
   157   \<Longrightarrow> MGU \<sigma> t u"
   158   by (simp only:Unifier_def MGU_def, auto)
   159 
   160 lemma MGU_sym[sym]:
   161   "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
   162   by (auto simp:MGU_def Unifier_def)
   163 
   164 lemma MGU_is_Unifier: "MGU \<sigma> t u \<Longrightarrow> Unifier \<sigma> t u"
   165 unfolding MGU_def by (rule conjunct1)
   166 
   167 lemma MGU_Var: 
   168   assumes "\<not> Var v \<prec> t"
   169   shows "MGU [(v,t)] (Var v) t"
   170 proof (intro MGUI exI)
   171   show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using assms
   172     by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
   173 next
   174   fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
   175   show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
   176   proof
   177     fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
   178       by (induct s) auto
   179   qed
   180 qed
   181 
   182 lemma MGU_Const: "MGU [] (Const c) (Const d) \<longleftrightarrow> c = d"
   183   by (auto simp: MGU_def Unifier_def)
   184   
   185 
   186 subsection \<open>The unification algorithm\<close>
   187 
   188 function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   189 where
   190   "unify (Const c) (M \<cdot> N)   = None"
   191 | "unify (M \<cdot> N)   (Const c) = None"
   192 | "unify (Const c) (Var v)   = Some [(v, Const c)]"
   193 | "unify (M \<cdot> N)   (Var v)   = (if Var v \<prec> M \<cdot> N 
   194                                         then None
   195                                         else Some [(v, M \<cdot> N)])"
   196 | "unify (Var v)   M         = (if Var v \<prec> M
   197                                         then None
   198                                         else Some [(v, M)])"
   199 | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
   200 | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
   201                                     None \<Rightarrow> None |
   202                                     Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
   203                                       of None \<Rightarrow> None |
   204                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
   205   by pat_completeness auto
   206 
   207 subsection \<open>Properties used in termination proof\<close>
   208 
   209 text \<open>Elimination of variables by a substitution:\<close>
   210 
   211 definition
   212   "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<lhd> \<sigma>)"
   213 
   214 lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<lhd> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
   215   by (auto simp:elim_def)
   216 
   217 lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
   218   by (auto simp:elim_def)
   219 
   220 lemma elim_eq: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
   221   by (auto simp:elim_def subst_eq_def)
   222 
   223 lemma occs_elim: "\<not> Var v \<prec> t 
   224   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
   225 by (metis elim_intro remove_var var_same vars_iff_occseq)
   226 
   227 text \<open>The result of a unification never introduces new variables:\<close>
   228 
   229 declare unify.psimps[simp]
   230 
   231 lemma unify_vars: 
   232   assumes "unify_dom (M, N)"
   233   assumes "unify M N = Some \<sigma>"
   234   shows "vars_of (t \<lhd> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
   235   (is "?P M N \<sigma> t")
   236 using assms
   237 proof (induct M N arbitrary:\<sigma> t)
   238   case (3 c v) 
   239   hence "\<sigma> = [(v, Const c)]" by simp
   240   thus ?case by (induct t) auto
   241 next
   242   case (4 M N v) 
   243   hence "\<not> Var v \<prec> M \<cdot> N" by auto
   244   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   245   thus ?case by (induct t) auto
   246 next
   247   case (5 v M)
   248   hence "\<not> Var v \<prec> M" by auto
   249   with 5 have "\<sigma> = [(v, M)]" by simp
   250   thus ?case by (induct t) auto
   251 next
   252   case (7 M N M' N' \<sigma>)
   253   then obtain \<theta>1 \<theta>2 
   254     where "unify M M' = Some \<theta>1"
   255     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   256     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   257     and ih1: "\<And>t. ?P M M' \<theta>1 t"
   258     and ih2: "\<And>t. ?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2 t"
   259     by (auto split:option.split_asm)
   260 
   261   show ?case
   262   proof
   263     fix v assume a: "v \<in> vars_of (t \<lhd> \<sigma>)"
   264     
   265     show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
   266     proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
   267         \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
   268       case True
   269       with ih1 have l:"\<And>t. v \<in> vars_of (t \<lhd> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
   270         by auto
   271       
   272       from a and ih2[where t="t \<lhd> \<theta>1"]
   273       have "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1) 
   274         \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
   275         by auto
   276       hence "v \<in> vars_of t"
   277       proof
   278         assume "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
   279         with True show ?thesis by (auto dest:l)
   280       next
   281         assume "v \<in> vars_of (t \<lhd> \<theta>1)" 
   282         thus ?thesis by (rule l)
   283       qed
   284       
   285       thus ?thesis by auto
   286     qed auto
   287   qed
   288 qed (auto split: if_split_asm)
   289 
   290 
   291 text \<open>The result of a unification is either the identity
   292 substitution or it eliminates a variable from one of the terms:\<close>
   293 
   294 lemma unify_eliminates: 
   295   assumes "unify_dom (M, N)"
   296   assumes "unify M N = Some \<sigma>"
   297   shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> \<doteq> []"
   298   (is "?P M N \<sigma>")
   299 using assms
   300 proof (induct M N arbitrary:\<sigma>)
   301   case 1 thus ?case by simp
   302 next
   303   case 2 thus ?case by simp
   304 next
   305   case (3 c v)
   306   have no_occs: "\<not> Var v \<prec> Const c" by simp
   307   with 3 have "\<sigma> = [(v, Const c)]" by simp
   308   with occs_elim[OF no_occs]
   309   show ?case by auto
   310 next
   311   case (4 M N v)
   312   hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
   313   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
   314   with occs_elim[OF no_occs]
   315   show ?case by auto 
   316 next
   317   case (5 v M) 
   318   hence no_occs: "\<not> Var v \<prec> M" by auto
   319   with 5 have "\<sigma> = [(v, M)]" by simp
   320   with occs_elim[OF no_occs]
   321   show ?case by auto 
   322 next 
   323   case (6 c d) thus ?case
   324     by (cases "c = d") auto
   325 next
   326   case (7 M N M' N' \<sigma>)
   327   then obtain \<theta>1 \<theta>2 
   328     where "unify M M' = Some \<theta>1"
   329     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   330     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   331     and ih1: "?P M M' \<theta>1"
   332     and ih2: "?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2"
   333     by (auto split:option.split_asm)
   334 
   335   from \<open>unify_dom (M \<cdot> N, M' \<cdot> N')\<close>
   336   have "unify_dom (M, M')"
   337     by (rule accp_downward) (rule unify_rel.intros)
   338   hence no_new_vars: 
   339     "\<And>t. vars_of (t \<lhd> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
   340     by (rule unify_vars) (rule \<open>unify M M' = Some \<theta>1\<close>)
   341 
   342   from ih2 show ?case 
   343   proof 
   344     assume "\<exists>v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1). elim \<theta>2 v"
   345     then obtain v 
   346       where "v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
   347       and el: "elim \<theta>2 v" by auto
   348     with no_new_vars show ?thesis unfolding \<sigma> 
   349       by (auto simp:elim_def)
   350   next
   351     assume empty[simp]: "\<theta>2 \<doteq> []"
   352 
   353     have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
   354       by (rule subst_cong) auto
   355     also have "\<dots> \<doteq> \<theta>1" by auto
   356     finally have "\<sigma> \<doteq> \<theta>1" .
   357 
   358     from ih1 show ?thesis
   359     proof
   360       assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
   361       with elim_eq[OF \<open>\<sigma> \<doteq> \<theta>1\<close>]
   362       show ?thesis by auto
   363     next
   364       note \<open>\<sigma> \<doteq> \<theta>1\<close>
   365       also assume "\<theta>1 \<doteq> []"
   366       finally show ?thesis ..
   367     qed
   368   qed
   369 qed
   370 
   371 declare unify.psimps[simp del]
   372 
   373 subsection \<open>Termination proof\<close>
   374 
   375 termination unify
   376 proof 
   377   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
   378                            \<lambda>(M, N). size M]"
   379   show "wf ?R" by simp
   380 
   381   fix M N M' N' :: "'a trm"
   382   show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" \<comment> "Inner call"
   383     by (rule measures_lesseq) (auto intro: card_mono)
   384 
   385   fix \<theta>                                   \<comment> "Outer call"
   386   assume inner: "unify_dom (M, M')"
   387     "unify M M' = Some \<theta>"
   388 
   389   from unify_eliminates[OF inner]
   390   show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
   391   proof
   392     \<comment> \<open>Either a variable is eliminated \ldots\<close>
   393     assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
   394     then obtain v 
   395       where "elim \<theta> v" 
   396       and "v\<in>vars_of M \<union> vars_of M'" by auto
   397     with unify_vars[OF inner]
   398     have "vars_of (N\<lhd>\<theta>) \<union> vars_of (N'\<lhd>\<theta>)
   399       \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
   400       by auto
   401     
   402     thus ?thesis
   403       by (auto intro!: measures_less intro: psubset_card_mono)
   404   next
   405     \<comment> \<open>Or the substitution is empty\<close>
   406     assume "\<theta> \<doteq> []"
   407     hence "N \<lhd> \<theta> = N" 
   408       and "N' \<lhd> \<theta> = N'" by auto
   409     thus ?thesis 
   410        by (auto intro!: measures_less intro: psubset_card_mono)
   411   qed
   412 qed
   413 
   414 
   415 subsection \<open>Unification returns a Most General Unifier\<close>
   416 
   417 lemma unify_computes_MGU:
   418   "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
   419 proof (induct M N arbitrary: \<sigma> rule: unify.induct)
   420   case (7 M N M' N' \<sigma>) \<comment> "The interesting case"
   421 
   422   then obtain \<theta>1 \<theta>2 
   423     where "unify M M' = Some \<theta>1"
   424     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   425     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   426     and MGU_inner: "MGU \<theta>1 M M'" 
   427     and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   428     by (auto split:option.split_asm)
   429 
   430   show ?case
   431   proof
   432     from MGU_inner and MGU_outer
   433     have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
   434       and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
   435       unfolding MGU_def Unifier_def
   436       by auto
   437     thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
   438       by simp
   439   next
   440     fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
   441     hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
   442       and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
   443 
   444     with MGU_inner obtain \<delta>
   445       where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
   446       unfolding MGU_def Unifier_def
   447       by auto
   448 
   449     from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
   450       by (simp add:subst_eq_dest[OF eqv])
   451 
   452     with MGU_outer obtain \<rho>
   453       where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
   454       unfolding MGU_def Unifier_def
   455       by auto
   456     
   457     have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
   458       by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
   459     thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
   460   qed
   461 qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: if_split_asm)
   462 
   463 
   464 subsection \<open>Unification returns Idempotent Substitution\<close>
   465 
   466 definition Idem :: "'a subst \<Rightarrow> bool"
   467 where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
   468 
   469 lemma Idem_Nil [iff]: "Idem []"
   470   by (simp add: Idem_def)
   471 
   472 lemma Var_Idem: 
   473   assumes "~ (Var v \<prec> t)" shows "Idem [(v,t)]"
   474   unfolding Idem_def
   475 proof
   476   from assms have [simp]: "t \<lhd> [(v, t)] = t"
   477     by (metis assoc.simps(2) subst.simps(1) subst_no_occs)
   478 
   479   fix s show "s \<lhd> [(v, t)] \<lozenge> [(v, t)] = s \<lhd> [(v, t)]"
   480     by (induct s) auto
   481 qed
   482 
   483 lemma Unifier_Idem_subst: 
   484   "Idem(r) \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
   485     Unifier (r \<lozenge> s) (t \<lhd> r) (u \<lhd> r)"
   486 by (simp add: Idem_def Unifier_def subst_eq_def)
   487 
   488 lemma Idem_comp:
   489   "Idem r \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
   490       (!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
   491     Idem (r \<lozenge> s)"
   492   apply (frule Unifier_Idem_subst, blast) 
   493   apply (force simp add: Idem_def subst_eq_def)
   494   done
   495 
   496 theorem unify_gives_Idem:
   497   "unify M N  = Some \<sigma> \<Longrightarrow> Idem \<sigma>"
   498 proof (induct M N arbitrary: \<sigma> rule: unify.induct)
   499   case (7 M M' N N' \<sigma>)
   500 
   501   then obtain \<theta>1 \<theta>2 
   502     where "unify M N = Some \<theta>1"
   503     and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
   504     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
   505     and "Idem \<theta>1" 
   506     and "Idem \<theta>2"
   507     by (auto split: option.split_asm)
   508 
   509   from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   510     by (rule unify_computes_MGU[THEN MGU_is_Unifier])
   511 
   512   with \<open>Idem \<theta>1\<close>
   513   show "Idem \<sigma>" unfolding \<sigma>
   514   proof (rule Idem_comp)
   515     fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
   516     with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
   517       using unify_computes_MGU MGU_def by blast
   518 
   519     have "\<theta>2 \<lozenge> \<sigma> \<doteq> \<theta>2 \<lozenge> (\<theta>2 \<lozenge> \<gamma>)" by (rule subst_cong) (auto simp: \<sigma>)
   520     also have "... \<doteq> (\<theta>2 \<lozenge> \<theta>2) \<lozenge> \<gamma>" by (rule comp_assoc[symmetric])
   521     also have "... \<doteq> \<theta>2 \<lozenge> \<gamma>" by (rule subst_cong) (auto simp: \<open>Idem \<theta>2\<close>[unfolded Idem_def])
   522     also have "... \<doteq> \<sigma>" by (rule \<sigma>[symmetric])
   523     finally show "\<theta>2 \<lozenge> \<sigma> \<doteq> \<sigma>" .
   524   qed
   525 qed (auto intro!: Var_Idem split: option.splits if_splits)
   526 
   527 end