bulwahn@41460: (*
krauss@22999:     Author:     Alexander Krauss, Technische Universitaet Muenchen
krauss@22999: *)
krauss@22999: 
krauss@22999: header {* Case study: Unification Algorithm *}
krauss@22999: 
wenzelm@23219: theory Unification
krauss@22999: imports Main
wenzelm@23219: begin
krauss@22999: 
krauss@22999: text {* 
krauss@22999:   This is a formalization of a first-order unification
krauss@22999:   algorithm. It uses the new "function" package to define recursive
krauss@22999:   functions, which allows a better treatment of nested recursion. 
krauss@22999: 
krauss@22999:   This is basically a modernized version of a previous formalization
krauss@22999:   by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
wenzelm@23219:   previous work by Paulson and Manna \& Waldinger (for details, see
krauss@22999:   there).
krauss@22999: 
krauss@22999:   Unlike that formalization, where the proofs of termination and
krauss@22999:   some partial correctness properties are intertwined, we can prove
krauss@22999:   partial correctness and termination separately.
krauss@22999: *}
krauss@22999: 
wenzelm@23219: 
krauss@44368: subsection {* Terms *}
krauss@44368: 
krauss@44368: text {* Binary trees with leaves that are constants or variables. *}
krauss@22999: 
krauss@22999: datatype 'a trm = 
krauss@22999:   Var 'a 
krauss@22999:   | Const 'a
krauss@44367:   | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
krauss@22999: 
krauss@44368: primrec vars_of :: "'a trm \<Rightarrow> 'a set"
krauss@44368: where
krauss@44368:   "vars_of (Var v) = {v}"
krauss@44368: | "vars_of (Const c) = {}"
krauss@44368: | "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
krauss@44368: 
krauss@44368: fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54) 
krauss@44368: where
krauss@44369:   "u \<prec> Var v \<longleftrightarrow> False"
krauss@44369: | "u \<prec> Const c \<longleftrightarrow> False"
krauss@44369: | "u \<prec> M \<cdot> N \<longleftrightarrow> u = M \<or> u = N \<or> u \<prec> M \<or> u \<prec> N"
krauss@44368: 
krauss@44368: 
krauss@44368: lemma finite_vars_of[intro]: "finite (vars_of t)"
krauss@44368:   by (induct t) simp_all
krauss@44368: 
krauss@44368: lemma vars_var_iff: "v \<in> vars_of (Var w) \<longleftrightarrow> w = v"
krauss@44368:   by auto
krauss@44368: 
krauss@44368: lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
krauss@44368:   by (induct t) auto
krauss@44368: 
krauss@44368: lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
krauss@44368:   by (induct N) auto
krauss@44368: 
krauss@44368: 
krauss@44368: subsection {* Substitutions *}
krauss@44368: 
wenzelm@42463: type_synonym 'a subst = "('a \<times> 'a trm) list"
krauss@22999: 
krauss@22999: text {* Applying a substitution to a variable: *}
krauss@22999: 
krauss@22999: fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
krauss@22999: where
krauss@22999:   "assoc x d [] = d"
krauss@22999: | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
krauss@22999: 
krauss@22999: text {* Applying a substitution to a term: *}
krauss@22999: 
krauss@44367: primrec subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<lhd>" 55)
krauss@22999: where
krauss@44367:   "(Var v) \<lhd> s = assoc v (Var v) s"
krauss@44367: | "(Const c) \<lhd> s = (Const c)"
krauss@44367: | "(M \<cdot> N) \<lhd> s = (M \<lhd> s) \<cdot> (N \<lhd> s)"
krauss@22999: 
krauss@44368: definition subst_eq (infixr "\<doteq>" 52)
krauss@44368: where
krauss@44368:   "s1 \<doteq> s2 \<longleftrightarrow> (\<forall>t. t \<lhd> s1 = t \<lhd> s2)" 
krauss@22999: 
krauss@44368: fun comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
krauss@22999: where
krauss@44367:   "[] \<lozenge> bl = bl"
krauss@44367: | "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
krauss@22999: 
krauss@44368: 
krauss@44368: subsection {* Basic Laws *}
krauss@44368: 
krauss@44368: lemma subst_Nil[simp]: "t \<lhd> [] = t"
krauss@44368: by (induct t) auto
krauss@44368: 
krauss@44368: lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
krauss@44368: by (induct u) auto
krauss@44368: 
krauss@44368: lemma agreement: "(t \<lhd> r = t \<lhd> s) \<longleftrightarrow> (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
krauss@44368: by (induct t) auto
krauss@44368: 
krauss@44368: lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
krauss@44368: by (simp add: agreement)
krauss@22999: 
krauss@44368: lemma Var_in_subst:
krauss@44368:   "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
krauss@44368: by (induct t) auto
krauss@44368: 
krauss@44370: lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
krauss@44370: by (induct t) simp_all
krauss@44370: 
krauss@44368: lemma subst_refl[iff]: "s \<doteq> s"
krauss@44368:   by (auto simp:subst_eq_def)
krauss@44368: 
krauss@44368: lemma subst_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
krauss@44368:   by (auto simp:subst_eq_def)
krauss@44368: 
krauss@44368: lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
krauss@44368:   by (auto simp:subst_eq_def)
krauss@44368: 
krauss@44371: lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
krauss@44371:   \<Longrightarrow> t \<lhd> [(v,s)] = t"
krauss@44371: by (induct t) auto
krauss@44370: 
krauss@44368: text {* Composition of Substitutions *}
krauss@22999: 
krauss@44368: lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
krauss@22999: by (induct \<sigma>) auto
krauss@22999: 
krauss@44368: lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
krauss@22999: proof (induct t)
krauss@22999:   case (Var v) thus ?case
krauss@44368:     by (induct r) auto
krauss@44368: qed auto
krauss@22999: 
krauss@44368: lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
krauss@44367:   by (auto simp:subst_eq_def)
krauss@22999: 
krauss@44368: lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
krauss@44367:   by (auto simp:subst_eq_def)
krauss@22999: 
krauss@44368: lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
krauss@44368:   by auto
krauss@22999: 
krauss@44368: lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
krauss@44368:   by (auto simp: subst_eq_def)
krauss@22999: 
krauss@44370: lemma var_self: "[(v, Var v)] \<doteq> []"
krauss@44370: proof
krauss@44370:   fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
krauss@44370:     by (induct t) simp_all
krauss@44370: qed
krauss@44370: 
krauss@44370: lemma var_same[simp]: "[(v, t)] \<doteq> [] \<longleftrightarrow> t = Var v"
krauss@44370: by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
krauss@22999: 
wenzelm@23219: 
krauss@22999: subsection {* Specification: Most general unifiers *}
krauss@22999: 
krauss@44368: definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
krauss@44368: where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
krauss@22999: 
krauss@44368: definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
krauss@44368:   "MGU \<sigma> t u \<longleftrightarrow> 
krauss@44368:    Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
krauss@22999: 
krauss@22999: lemma MGUI[intro]:
krauss@44367:   "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
krauss@22999:   \<Longrightarrow> MGU \<sigma> t u"
krauss@22999:   by (simp only:Unifier_def MGU_def, auto)
krauss@22999: 
krauss@22999: lemma MGU_sym[sym]:
krauss@22999:   "MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
krauss@22999:   by (auto simp:MGU_def Unifier_def)
krauss@22999: 
krauss@44371: lemma MGU_is_Unifier: "MGU \<sigma> t u \<Longrightarrow> Unifier \<sigma> t u"
krauss@44371: unfolding MGU_def by (rule conjunct1)
krauss@44371: 
krauss@44370: lemma MGU_Var: 
krauss@44370:   assumes "\<not> Var v \<prec> t"
krauss@44370:   shows "MGU [(v,t)] (Var v) t"
krauss@44370: proof (intro MGUI exI)
krauss@44370:   show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using assms
krauss@44370:     by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
krauss@44370: next
krauss@44370:   fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>" 
krauss@44370:   show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>" 
krauss@44370:   proof
krauss@44370:     fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th 
krauss@44370:       by (induct s) auto
krauss@44370:   qed
krauss@44370: qed
krauss@44370: 
krauss@44370: lemma MGU_Const: "MGU [] (Const c) (Const d) \<longleftrightarrow> c = d"
krauss@44370:   by (auto simp: MGU_def Unifier_def)
krauss@44370:   
krauss@22999: 
krauss@44368: definition Idem :: "'a subst \<Rightarrow> bool"
krauss@44368: where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
krauss@44368: 
krauss@44368: 
krauss@44368: 
krauss@22999: subsection {* The unification algorithm *}
krauss@22999: 
krauss@22999: 
krauss@22999: text {* The unification algorithm: *}
krauss@22999: 
krauss@22999: function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
krauss@22999: where
krauss@22999:   "unify (Const c) (M \<cdot> N)   = None"
krauss@22999: | "unify (M \<cdot> N)   (Const c) = None"
krauss@22999: | "unify (Const c) (Var v)   = Some [(v, Const c)]"
krauss@44369: | "unify (M \<cdot> N)   (Var v)   = (if Var v \<prec> M \<cdot> N 
krauss@22999:                                         then None
krauss@22999:                                         else Some [(v, M \<cdot> N)])"
krauss@44369: | "unify (Var v)   M         = (if Var v \<prec> M
krauss@22999:                                         then None
krauss@22999:                                         else Some [(v, M)])"
krauss@22999: | "unify (Const c) (Const d) = (if c=d then Some [] else None)"
krauss@22999: | "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
krauss@22999:                                     None \<Rightarrow> None |
krauss@44367:                                     Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
krauss@22999:                                       of None \<Rightarrow> None |
krauss@44367:                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
krauss@22999:   by pat_completeness auto
krauss@22999: 
krauss@22999: subsection {* Properties used in termination proof *}
krauss@22999: 
krauss@22999: 
krauss@22999: text {* Elimination of variables by a substitution: *}
krauss@22999: 
krauss@22999: definition
krauss@44367:   "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<lhd> \<sigma>)"
krauss@22999: 
krauss@44367: lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<lhd> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
krauss@22999:   by (auto simp:elim_def)
krauss@22999: 
krauss@44367: lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
krauss@22999:   by (auto simp:elim_def)
krauss@22999: 
krauss@44370: lemma elim_eq: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
krauss@44367:   by (auto simp:elim_def subst_eq_def)
krauss@22999: 
krauss@44369: lemma occs_elim: "\<not> Var v \<prec> t 
krauss@44367:   \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
krauss@44370: by (metis elim_intro remove_var var_same vars_iff_occseq)
krauss@22999: 
krauss@22999: text {* The result of a unification never introduces new variables: *}
krauss@22999: 
krauss@44370: declare unify.psimps[simp]
krauss@44370: 
krauss@22999: lemma unify_vars: 
krauss@22999:   assumes "unify_dom (M, N)"
krauss@22999:   assumes "unify M N = Some \<sigma>"
krauss@44367:   shows "vars_of (t \<lhd> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
krauss@22999:   (is "?P M N \<sigma> t")
wenzelm@24444: using assms
krauss@22999: proof (induct M N arbitrary:\<sigma> t)
krauss@22999:   case (3 c v) 
krauss@22999:   hence "\<sigma> = [(v, Const c)]" by simp
wenzelm@24444:   thus ?case by (induct t) auto
krauss@22999: next
krauss@22999:   case (4 M N v) 
krauss@44369:   hence "\<not> Var v \<prec> M \<cdot> N" by auto
wenzelm@24444:   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
wenzelm@24444:   thus ?case by (induct t) auto
krauss@22999: next
krauss@22999:   case (5 v M)
krauss@44369:   hence "\<not> Var v \<prec> M" by auto
wenzelm@24444:   with 5 have "\<sigma> = [(v, M)]" by simp
wenzelm@24444:   thus ?case by (induct t) auto
krauss@22999: next
krauss@22999:   case (7 M N M' N' \<sigma>)
krauss@22999:   then obtain \<theta>1 \<theta>2 
krauss@22999:     where "unify M M' = Some \<theta>1"
krauss@44367:     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44367:     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@22999:     and ih1: "\<And>t. ?P M M' \<theta>1 t"
krauss@44367:     and ih2: "\<And>t. ?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2 t"
krauss@22999:     by (auto split:option.split_asm)
krauss@22999: 
krauss@22999:   show ?case
krauss@22999:   proof
krauss@44367:     fix v assume a: "v \<in> vars_of (t \<lhd> \<sigma>)"
krauss@22999:     
krauss@22999:     show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
krauss@22999:     proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
wenzelm@32960:         \<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
krauss@22999:       case True
krauss@44367:       with ih1 have l:"\<And>t. v \<in> vars_of (t \<lhd> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
wenzelm@32960:         by auto
krauss@22999:       
krauss@44367:       from a and ih2[where t="t \<lhd> \<theta>1"]
krauss@44367:       have "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1) 
krauss@44367:         \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
wenzelm@32960:         by auto
krauss@22999:       hence "v \<in> vars_of t"
krauss@22999:       proof
krauss@44367:         assume "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
wenzelm@32960:         with True show ?thesis by (auto dest:l)
krauss@22999:       next
krauss@44367:         assume "v \<in> vars_of (t \<lhd> \<theta>1)" 
wenzelm@32960:         thus ?thesis by (rule l)
krauss@22999:       qed
krauss@22999:       
krauss@22999:       thus ?thesis by auto
krauss@22999:     qed auto
krauss@22999:   qed
krauss@22999: qed (auto split: split_if_asm)
krauss@22999: 
krauss@22999: 
krauss@22999: text {* The result of a unification is either the identity
krauss@22999: substitution or it eliminates a variable from one of the terms: *}
krauss@22999: 
krauss@22999: lemma unify_eliminates: 
krauss@22999:   assumes "unify_dom (M, N)"
krauss@22999:   assumes "unify M N = Some \<sigma>"
krauss@44367:   shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> \<doteq> []"
krauss@22999:   (is "?P M N \<sigma>")
wenzelm@24444: using assms
krauss@22999: proof (induct M N arbitrary:\<sigma>)
krauss@22999:   case 1 thus ?case by simp
krauss@22999: next
krauss@22999:   case 2 thus ?case by simp
krauss@22999: next
krauss@22999:   case (3 c v)
krauss@44369:   have no_occs: "\<not> Var v \<prec> Const c" by simp
wenzelm@24444:   with 3 have "\<sigma> = [(v, Const c)]" by simp
krauss@44367:   with occs_elim[OF no_occs]
krauss@22999:   show ?case by auto
krauss@22999: next
krauss@22999:   case (4 M N v)
krauss@44369:   hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
wenzelm@24444:   with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
krauss@44367:   with occs_elim[OF no_occs]
krauss@22999:   show ?case by auto 
krauss@22999: next
krauss@22999:   case (5 v M) 
krauss@44369:   hence no_occs: "\<not> Var v \<prec> M" by auto
wenzelm@24444:   with 5 have "\<sigma> = [(v, M)]" by simp
krauss@44367:   with occs_elim[OF no_occs]
krauss@22999:   show ?case by auto 
krauss@22999: next 
krauss@22999:   case (6 c d) thus ?case
krauss@22999:     by (cases "c = d") auto
krauss@22999: next
krauss@22999:   case (7 M N M' N' \<sigma>)
krauss@22999:   then obtain \<theta>1 \<theta>2 
krauss@22999:     where "unify M M' = Some \<theta>1"
krauss@44367:     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44367:     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@22999:     and ih1: "?P M M' \<theta>1"
krauss@44367:     and ih2: "?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2"
krauss@22999:     by (auto split:option.split_asm)
krauss@22999: 
krauss@22999:   from `unify_dom (M \<cdot> N, M' \<cdot> N')`
krauss@22999:   have "unify_dom (M, M')"
berghofe@23777:     by (rule accp_downward) (rule unify_rel.intros)
krauss@22999:   hence no_new_vars: 
krauss@44367:     "\<And>t. vars_of (t \<lhd> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
wenzelm@23373:     by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
krauss@22999: 
krauss@22999:   from ih2 show ?case 
krauss@22999:   proof 
krauss@44367:     assume "\<exists>v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1). elim \<theta>2 v"
krauss@22999:     then obtain v 
krauss@44367:       where "v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
krauss@22999:       and el: "elim \<theta>2 v" by auto
krauss@22999:     with no_new_vars show ?thesis unfolding \<sigma> 
krauss@22999:       by (auto simp:elim_def)
krauss@22999:   next
krauss@44367:     assume empty[simp]: "\<theta>2 \<doteq> []"
krauss@22999: 
krauss@44367:     have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
krauss@44368:       by (rule subst_cong) auto
krauss@44367:     also have "\<dots> \<doteq> \<theta>1" by auto
krauss@44367:     finally have "\<sigma> \<doteq> \<theta>1" .
krauss@22999: 
krauss@22999:     from ih1 show ?thesis
krauss@22999:     proof
krauss@22999:       assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
krauss@44370:       with elim_eq[OF `\<sigma> \<doteq> \<theta>1`]
krauss@22999:       show ?thesis by auto
krauss@22999:     next
krauss@44367:       note `\<sigma> \<doteq> \<theta>1`
krauss@44367:       also assume "\<theta>1 \<doteq> []"
krauss@22999:       finally show ?thesis ..
krauss@22999:     qed
krauss@22999:   qed
krauss@22999: qed
krauss@22999: 
krauss@44370: declare unify.psimps[simp del]
krauss@22999: 
krauss@22999: subsection {* Termination proof *}
krauss@22999: 
krauss@22999: termination unify
krauss@22999: proof 
krauss@22999:   let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
krauss@22999:                            \<lambda>(M, N). size M]"
krauss@22999:   show "wf ?R" by simp
krauss@22999: 
krauss@44370:   fix M N M' N' :: "'a trm"
krauss@22999:   show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
krauss@22999:     by (rule measures_lesseq) (auto intro: card_mono)
krauss@22999: 
krauss@22999:   fix \<theta>                                   -- "Outer call"
krauss@22999:   assume inner: "unify_dom (M, M')"
krauss@22999:     "unify M M' = Some \<theta>"
krauss@22999: 
krauss@22999:   from unify_eliminates[OF inner]
krauss@44367:   show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
krauss@22999:   proof
krauss@22999:     -- {* Either a variable is eliminated \ldots *}
krauss@22999:     assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
krauss@22999:     then obtain v 
wenzelm@32960:       where "elim \<theta> v" 
wenzelm@32960:       and "v\<in>vars_of M \<union> vars_of M'" by auto
krauss@22999:     with unify_vars[OF inner]
krauss@44367:     have "vars_of (N\<lhd>\<theta>) \<union> vars_of (N'\<lhd>\<theta>)
wenzelm@32960:       \<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
wenzelm@32960:       by auto
krauss@22999:     
krauss@22999:     thus ?thesis
krauss@22999:       by (auto intro!: measures_less intro: psubset_card_mono)
krauss@22999:   next
krauss@22999:     -- {* Or the substitution is empty *}
krauss@44367:     assume "\<theta> \<doteq> []"
krauss@44367:     hence "N \<lhd> \<theta> = N" 
krauss@44367:       and "N' \<lhd> \<theta> = N'" by auto
krauss@22999:     thus ?thesis 
krauss@22999:        by (auto intro!: measures_less intro: psubset_card_mono)
krauss@22999:   qed
krauss@22999: qed
krauss@22999: 
krauss@44370: 
krauss@44370: subsection {* Other Properties *}
krauss@44370: 
krauss@44370: lemma unify_computes_MGU:
krauss@44370:   "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
krauss@44370: proof (induct M N arbitrary: \<sigma> rule: unify.induct)
krauss@44370:   case (7 M N M' N' \<sigma>) -- "The interesting case"
krauss@44370: 
krauss@44370:   then obtain \<theta>1 \<theta>2 
krauss@44370:     where "unify M M' = Some \<theta>1"
krauss@44370:     and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44370:     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@44370:     and MGU_inner: "MGU \<theta>1 M M'" 
krauss@44370:     and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
krauss@44370:     by (auto split:option.split_asm)
krauss@44370: 
krauss@44370:   show ?case
krauss@44370:   proof
krauss@44370:     from MGU_inner and MGU_outer
krauss@44370:     have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1" 
krauss@44370:       and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
krauss@44370:       unfolding MGU_def Unifier_def
krauss@44370:       by auto
krauss@44370:     thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
krauss@44370:       by simp
krauss@44370:   next
krauss@44370:     fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
krauss@44370:     hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
krauss@44370:       and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
krauss@44370: 
krauss@44370:     with MGU_inner obtain \<delta>
krauss@44370:       where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
krauss@44370:       unfolding MGU_def Unifier_def
krauss@44370:       by auto
krauss@44370: 
krauss@44370:     from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
krauss@44370:       by (simp add:subst_eq_dest[OF eqv])
krauss@44370: 
krauss@44370:     with MGU_outer obtain \<rho>
krauss@44370:       where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
krauss@44370:       unfolding MGU_def Unifier_def
krauss@44370:       by auto
krauss@44370:     
krauss@44370:     have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
krauss@44370:       by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
krauss@44370:     thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
krauss@44370:   qed
krauss@44370: qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
krauss@44370: 
krauss@44371: lemma Idem_Nil [iff]: "Idem []"
krauss@44371:   by (simp add: Idem_def)
krauss@44370: 
krauss@44371: lemma Var_Idem: 
krauss@44371:   assumes "~ (Var v \<prec> t)" shows "Idem [(v,t)]"
krauss@44371:   unfolding Idem_def
krauss@44371: proof
krauss@44371:   from assms have [simp]: "t \<lhd> [(v, t)] = t"
krauss@44371:     by (metis assoc.simps(2) subst.simps(1) subst_no_occs)
krauss@44371: 
krauss@44371:   fix s show "s \<lhd> [(v, t)] \<lozenge> [(v, t)] = s \<lhd> [(v, t)]"
krauss@44371:     by (induct s) auto
krauss@44371: qed
krauss@44371: 
krauss@44371: lemma Unifier_Idem_subst: 
krauss@44371:   "Idem(r) \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
krauss@44371:     Unifier (r \<lozenge> s) (t \<lhd> r) (u \<lhd> r)"
krauss@44371: by (simp add: Idem_def Unifier_def subst_eq_def)
krauss@44371: 
krauss@44371: lemma Idem_comp:
krauss@44371:   "Idem r \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
krauss@44371:       (!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
krauss@44371:     Idem (r \<lozenge> s)"
krauss@44371:   apply (frule Unifier_Idem_subst, blast) 
krauss@44371:   apply (force simp add: Idem_def subst_eq_def)
krauss@44371:   done
krauss@44371: 
krauss@44371: theorem unify_gives_Idem:
krauss@44371:   "unify M N  = Some \<sigma> \<Longrightarrow> Idem \<sigma>"
krauss@44371: proof (induct M N arbitrary: \<sigma> rule: unify.induct)
krauss@44371:   case (7 M M' N N' \<sigma>)
krauss@44371: 
krauss@44371:   then obtain \<theta>1 \<theta>2 
krauss@44371:     where "unify M N = Some \<theta>1"
krauss@44371:     and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
krauss@44371:     and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
krauss@44371:     and "Idem \<theta>1" 
krauss@44371:     and "Idem \<theta>2"
krauss@44371:     by (auto split: option.split_asm)
krauss@44371: 
krauss@44371:   from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
krauss@44371:     by (rule unify_computes_MGU[THEN MGU_is_Unifier])
krauss@44371: 
krauss@44371:   with `Idem \<theta>1`
krauss@44371:   show "Idem \<sigma>" unfolding \<sigma>
krauss@44371:   proof (rule Idem_comp)
krauss@44371:     fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
krauss@44371:     with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
krauss@44371:       using unify_computes_MGU MGU_def by blast
krauss@44371: 
krauss@44371:     have "\<theta>2 \<lozenge> \<sigma> \<doteq> \<theta>2 \<lozenge> (\<theta>2 \<lozenge> \<gamma>)" by (rule subst_cong) (auto simp: \<sigma>)
krauss@44371:     also have "... \<doteq> (\<theta>2 \<lozenge> \<theta>2) \<lozenge> \<gamma>" by (rule comp_assoc[symmetric])
krauss@44371:     also have "... \<doteq> \<theta>2 \<lozenge> \<gamma>" by (rule subst_cong) (auto simp: `Idem \<theta>2`[unfolded Idem_def])
krauss@44371:     also have "... \<doteq> \<sigma>" by (rule \<sigma>[symmetric])
krauss@44371:     finally show "\<theta>2 \<lozenge> \<sigma> \<doteq> \<sigma>" .
krauss@44371:   qed
krauss@44371: qed (auto intro!: Var_Idem split: option.splits if_splits)
krauss@39754: 
wenzelm@23219: end