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