(* Title: HOL/ex/Unification.thy Author: Martin Coen, Cambridge University Computer Laboratory Author: Konrad Slind, TUM & Cambridge University Computer Laboratory Author: Alexander Krauss, TUM *) section ‹Substitution and Unification› theory Unification imports Main begin text ‹ Implements Manna \& Waldinger's formalization, with Paulson's simplifications, and some new simplifications by Slind and Krauss. Z Manna \& R Waldinger, Deductive Synthesis of the Unification Algorithm. SCP 1 (1981), 5-48 L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170 K Slind, Reasoning about Terminating Functional Programs, Ph.D. thesis, TUM, 1999, Sect. 5.8 A Krauss, Partial and Nested Recursive Function Definitions in Higher-Order Logic, JAR 44(4):303-336, 2010. Sect. 6.3 › subsection ‹Terms› text ‹Binary trees with leaves that are constants or variables.› datatype 'a trm = Var 'a | Const 'a | Comb "'a trm" "'a trm" (infix "⋅" 60) primrec vars_of :: "'a trm ⇒ 'a set" where "vars_of (Var v) = {v}" | "vars_of (Const c) = {}" | "vars_of (M ⋅ N) = vars_of M ∪ vars_of N" fun occs :: "'a trm ⇒ 'a trm ⇒ bool" (infixl "≺" 54) where "u ≺ Var v ⟷ False" | "u ≺ Const c ⟷ False" | "u ≺ M ⋅ N ⟷ u = M ∨ u = N ∨ u ≺ M ∨ u ≺ N" lemma finite_vars_of[intro]: "finite (vars_of t)" by (induct t) simp_all lemma vars_iff_occseq: "x ∈ vars_of t ⟷ Var x ≺ t ∨ Var x = t" by (induct t) auto lemma occs_vars_subset: "M ≺ N ⟹ vars_of M ⊆ vars_of N" by (induct N) auto subsection ‹Substitutions› type_synonym 'a subst = "('a × 'a trm) list" fun assoc :: "'a ⇒ 'b ⇒ ('a × 'b) list ⇒ 'b" where "assoc x d [] = d" | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)" primrec subst :: "'a trm ⇒ 'a subst ⇒ 'a trm" (infixl "⊲" 55) where "(Var v) ⊲ s = assoc v (Var v) s" | "(Const c) ⊲ s = (Const c)" | "(M ⋅ N) ⊲ s = (M ⊲ s) ⋅ (N ⊲ s)" definition subst_eq (infixr "≐" 52) where "s1 ≐ s2 ⟷ (∀t. t ⊲ s1 = t ⊲ s2)" fun comp :: "'a subst ⇒ 'a subst ⇒ 'a subst" (infixl "◊" 56) where "[] ◊ bl = bl" | "((a,b) # al) ◊ bl = (a, b ⊲ bl) # (al ◊ bl)" lemma subst_Nil[simp]: "t ⊲ [] = t" by (induct t) auto lemma subst_mono: "t ≺ u ⟹ t ⊲ s ≺ u ⊲ s" by (induct u) auto lemma agreement: "(t ⊲ r = t ⊲ s) ⟷ (∀v ∈ vars_of t. Var v ⊲ r = Var v ⊲ s)" by (induct t) auto lemma repl_invariance: "v ∉ vars_of t ⟹ t ⊲ (v,u) # s = t ⊲ s" by (simp add: agreement) lemma remove_var: "v ∉ vars_of s ⟹ v ∉ vars_of (t ⊲ [(v, s)])" by (induct t) simp_all lemma subst_refl[iff]: "s ≐ s" by (auto simp:subst_eq_def) lemma subst_sym[sym]: "⟦s1 ≐ s2⟧ ⟹ s2 ≐ s1" by (auto simp:subst_eq_def) lemma subst_trans[trans]: "⟦s1 ≐ s2; s2 ≐ s3⟧ ⟹ s1 ≐ s3" by (auto simp:subst_eq_def) lemma subst_no_occs: "¬ Var v ≺ t ⟹ Var v ≠ t ⟹ t ⊲ [(v,s)] = t" by (induct t) auto lemma comp_Nil[simp]: "σ ◊ [] = σ" by (induct σ) auto lemma subst_comp[simp]: "t ⊲ (r ◊ s) = t ⊲ r ⊲ s" proof (induct t) case (Var v) thus ?case by (induct r) auto qed auto lemma subst_eq_intro[intro]: "(⋀t. t ⊲ σ = t ⊲ θ) ⟹ σ ≐ θ" by (auto simp:subst_eq_def) lemma subst_eq_dest[dest]: "s1 ≐ s2 ⟹ t ⊲ s1 = t ⊲ s2" by (auto simp:subst_eq_def) lemma comp_assoc: "(a ◊ b) ◊ c ≐ a ◊ (b ◊ c)" by auto lemma subst_cong: "⟦σ ≐ σ'; θ ≐ θ'⟧ ⟹ (σ ◊ θ) ≐ (σ' ◊ θ')" by (auto simp: subst_eq_def) lemma var_self: "[(v, Var v)] ≐ []" proof fix t show "t ⊲ [(v, Var v)] = t ⊲ []" by (induct t) simp_all qed lemma var_same[simp]: "[(v, t)] ≐ [] ⟷ t = Var v" by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self) subsection ‹Unifiers and Most General Unifiers› definition Unifier :: "'a subst ⇒ 'a trm ⇒ 'a trm ⇒ bool" where "Unifier σ t u ⟷ (t ⊲ σ = u ⊲ σ)" definition MGU :: "'a subst ⇒ 'a trm ⇒ 'a trm ⇒ bool" where "MGU σ t u ⟷ Unifier σ t u ∧ (∀θ. Unifier θ t u ⟶ (∃γ. θ ≐ σ ◊ γ))" lemma MGUI[intro]: "⟦t ⊲ σ = u ⊲ σ; ⋀θ. t ⊲ θ = u ⊲ θ ⟹ ∃γ. θ ≐ σ ◊ γ⟧ ⟹ MGU σ t u" by (simp only:Unifier_def MGU_def, auto) lemma MGU_sym[sym]: "MGU σ s t ⟹ MGU σ t s" by (auto simp:MGU_def Unifier_def) lemma MGU_is_Unifier: "MGU σ t u ⟹ Unifier σ t u" unfolding MGU_def by (rule conjunct1) lemma MGU_Var: assumes "¬ Var v ≺ t" shows "MGU [(v,t)] (Var v) t" proof (intro MGUI exI) show "Var v ⊲ [(v,t)] = t ⊲ [(v,t)]" using assms by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq) next fix θ assume th: "Var v ⊲ θ = t ⊲ θ" show "θ ≐ [(v,t)] ◊ θ" proof fix s show "s ⊲ θ = s ⊲ [(v,t)] ◊ θ" using th by (induct s) auto qed qed lemma MGU_Const: "MGU [] (Const c) (Const d) ⟷ c = d" by (auto simp: MGU_def Unifier_def) subsection ‹The unification algorithm› function unify :: "'a trm ⇒ 'a trm ⇒ 'a subst option" where "unify (Const c) (M ⋅ N) = None" | "unify (M ⋅ N) (Const c) = None" | "unify (Const c) (Var v) = Some [(v, Const c)]" | "unify (M ⋅ N) (Var v) = (if Var v ≺ M ⋅ N then None else Some [(v, M ⋅ N)])" | "unify (Var v) M = (if Var v ≺ M then None else Some [(v, M)])" | "unify (Const c) (Const d) = (if c=d then Some [] else None)" | "unify (M ⋅ N) (M' ⋅ N') = (case unify M M' of None ⇒ None | Some θ ⇒ (case unify (N ⊲ θ) (N' ⊲ θ) of None ⇒ None | Some σ ⇒ Some (θ ◊ σ)))" by pat_completeness auto subsection ‹Properties used in termination proof› text ‹Elimination of variables by a substitution:› definition "elim σ v ≡ ∀t. v ∉ vars_of (t ⊲ σ)" lemma elim_intro[intro]: "(⋀t. v ∉ vars_of (t ⊲ σ)) ⟹ elim σ v" by (auto simp:elim_def) lemma elim_dest[dest]: "elim σ v ⟹ v ∉ vars_of (t ⊲ σ)" by (auto simp:elim_def) lemma elim_eq: "σ ≐ θ ⟹ elim σ x = elim θ x" by (auto simp:elim_def subst_eq_def) lemma occs_elim: "¬ Var v ≺ t ⟹ elim [(v,t)] v ∨ [(v,t)] ≐ []" by (metis elim_intro remove_var var_same vars_iff_occseq) text ‹The result of a unification never introduces new variables:› declare unify.psimps[simp] lemma unify_vars: assumes "unify_dom (M, N)" assumes "unify M N = Some σ" shows "vars_of (t ⊲ σ) ⊆ vars_of M ∪ vars_of N ∪ vars_of t" (is "?P M N σ t") using assms proof (induct M N arbitrary:σ t) case (3 c v) hence "σ = [(v, Const c)]" by simp thus ?case by (induct t) auto next case (4 M N v) hence "¬ Var v ≺ M ⋅ N" by auto with 4 have "σ = [(v, M⋅N)]" by simp thus ?case by (induct t) auto next case (5 v M) hence "¬ Var v ≺ M" by auto with 5 have "σ = [(v, M)]" by simp thus ?case by (induct t) auto next case (7 M N M' N' σ) then obtain θ1 θ2 where "unify M M' = Some θ1" and "unify (N ⊲ θ1) (N' ⊲ θ1) = Some θ2" and σ: "σ = θ1 ◊ θ2" and ih1: "⋀t. ?P M M' θ1 t" and ih2: "⋀t. ?P (N⊲θ1) (N'⊲θ1) θ2 t" by (auto split:option.split_asm) show ?case proof fix v assume a: "v ∈ vars_of (t ⊲ σ)" show "v ∈ vars_of (M ⋅ N) ∪ vars_of (M' ⋅ N') ∪ vars_of t" proof (cases "v ∉ vars_of M ∧ v ∉ vars_of M' ∧ v ∉ vars_of N ∧ v ∉ vars_of N'") case True with ih1 have l:"⋀t. v ∈ vars_of (t ⊲ θ1) ⟹ v ∈ vars_of t" by auto from a and ih2[where t="t ⊲ θ1"] have "v ∈ vars_of (N ⊲ θ1) ∪ vars_of (N' ⊲ θ1) ∨ v ∈ vars_of (t ⊲ θ1)" unfolding σ by auto hence "v ∈ vars_of t" proof assume "v ∈ vars_of (N ⊲ θ1) ∪ vars_of (N' ⊲ θ1)" with True show ?thesis by (auto dest:l) next assume "v ∈ vars_of (t ⊲ θ1)" thus ?thesis by (rule l) qed thus ?thesis by auto qed auto qed qed (auto split: if_split_asm) text ‹The result of a unification is either the identity substitution or it eliminates a variable from one of the terms:› lemma unify_eliminates: assumes "unify_dom (M, N)" assumes "unify M N = Some σ" shows "(∃v∈vars_of M ∪ vars_of N. elim σ v) ∨ σ ≐ []" (is "?P M N σ") using assms proof (induct M N arbitrary:σ) case 1 thus ?case by simp next case 2 thus ?case by simp next case (3 c v) have no_occs: "¬ Var v ≺ Const c" by simp with 3 have "σ = [(v, Const c)]" by simp with occs_elim[OF no_occs] show ?case by auto next case (4 M N v) hence no_occs: "¬ Var v ≺ M ⋅ N" by auto with 4 have "σ = [(v, M⋅N)]" by simp with occs_elim[OF no_occs] show ?case by auto next case (5 v M) hence no_occs: "¬ Var v ≺ M" by auto with 5 have "σ = [(v, M)]" by simp with occs_elim[OF no_occs] show ?case by auto next case (6 c d) thus ?case by (cases "c = d") auto next case (7 M N M' N' σ) then obtain θ1 θ2 where "unify M M' = Some θ1" and "unify (N ⊲ θ1) (N' ⊲ θ1) = Some θ2" and σ: "σ = θ1 ◊ θ2" and ih1: "?P M M' θ1" and ih2: "?P (N⊲θ1) (N'⊲θ1) θ2" by (auto split:option.split_asm) from ‹unify_dom (M ⋅ N, M' ⋅ N')› have "unify_dom (M, M')" by (rule accp_downward) (rule unify_rel.intros) hence no_new_vars: "⋀t. vars_of (t ⊲ θ1) ⊆ vars_of M ∪ vars_of M' ∪ vars_of t" by (rule unify_vars) (rule ‹unify M M' = Some θ1›) from ih2 show ?case proof assume "∃v∈vars_of (N ⊲ θ1) ∪ vars_of (N' ⊲ θ1). elim θ2 v" then obtain v where "v∈vars_of (N ⊲ θ1) ∪ vars_of (N' ⊲ θ1)" and el: "elim θ2 v" by auto with no_new_vars show ?thesis unfolding σ by (auto simp:elim_def) next assume empty[simp]: "θ2 ≐ []" have "σ ≐ (θ1 ◊ [])" unfolding σ by (rule subst_cong) auto also have "… ≐ θ1" by auto finally have "σ ≐ θ1" . from ih1 show ?thesis proof assume "∃v∈vars_of M ∪ vars_of M'. elim θ1 v" with elim_eq[OF ‹σ ≐ θ1›] show ?thesis by auto next note ‹σ ≐ θ1› also assume "θ1 ≐ []" finally show ?thesis .. qed qed qed declare unify.psimps[simp del] subsection ‹Termination proof› termination unify proof let ?R = "measures [λ(M,N). card (vars_of M ∪ vars_of N), λ(M, N). size M]" show "wf ?R" by simp fix M N M' N' :: "'a trm" show "((M, M'), (M ⋅ N, M' ⋅ N')) ∈ ?R" ― ‹Inner call› by (rule measures_lesseq) (auto intro: card_mono) fix θ ― ‹Outer call› assume inner: "unify_dom (M, M')" "unify M M' = Some θ" from unify_eliminates[OF inner] show "((N ⊲ θ, N' ⊲ θ), (M ⋅ N, M' ⋅ N')) ∈?R" proof ― ‹Either a variable is eliminated \ldots› assume "(∃v∈vars_of M ∪ vars_of M'. elim θ v)" then obtain v where "elim θ v" and "v∈vars_of M ∪ vars_of M'" by auto with unify_vars[OF inner] have "vars_of (N⊲θ) ∪ vars_of (N'⊲θ) ⊂ vars_of (M⋅N) ∪ vars_of (M'⋅N')" by auto thus ?thesis by (auto intro!: measures_less intro: psubset_card_mono) next ― ‹Or the substitution is empty› assume "θ ≐ []" hence "N ⊲ θ = N" and "N' ⊲ θ = N'" by auto thus ?thesis by (auto intro!: measures_less intro: psubset_card_mono) qed qed subsection ‹Unification returns a Most General Unifier› lemma unify_computes_MGU: "unify M N = Some σ ⟹ MGU σ M N" proof (induct M N arbitrary: σ rule: unify.induct) case (7 M N M' N' σ) ― ‹The interesting case› then obtain θ1 θ2 where "unify M M' = Some θ1" and "unify (N ⊲ θ1) (N' ⊲ θ1) = Some θ2" and σ: "σ = θ1 ◊ θ2" and MGU_inner: "MGU θ1 M M'" and MGU_outer: "MGU θ2 (N ⊲ θ1) (N' ⊲ θ1)" by (auto split:option.split_asm) show ?case proof from MGU_inner and MGU_outer have "M ⊲ θ1 = M' ⊲ θ1" and "N ⊲ θ1 ⊲ θ2 = N' ⊲ θ1 ⊲ θ2" unfolding MGU_def Unifier_def by auto thus "M ⋅ N ⊲ σ = M' ⋅ N' ⊲ σ" unfolding σ by simp next fix σ' assume "M ⋅ N ⊲ σ' = M' ⋅ N' ⊲ σ'" hence "M ⊲ σ' = M' ⊲ σ'" and Ns: "N ⊲ σ' = N' ⊲ σ'" by auto with MGU_inner obtain δ where eqv: "σ' ≐ θ1 ◊ δ" unfolding MGU_def Unifier_def by auto from Ns have "N ⊲ θ1 ⊲ δ = N' ⊲ θ1 ⊲ δ" by (simp add:subst_eq_dest[OF eqv]) with MGU_outer obtain ρ where eqv2: "δ ≐ θ2 ◊ ρ" unfolding MGU_def Unifier_def by auto have "σ' ≐ σ ◊ ρ" unfolding σ by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2]) thus "∃γ. σ' ≐ σ ◊ γ" .. qed qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: if_split_asm) subsection ‹Unification returns Idempotent Substitution› definition Idem :: "'a subst ⇒ bool" where "Idem s ⟷ (s ◊ s) ≐ s" lemma Idem_Nil [iff]: "Idem []" by (simp add: Idem_def) lemma Var_Idem: assumes "~ (Var v ≺ t)" shows "Idem [(v,t)]" unfolding Idem_def proof from assms have [simp]: "t ⊲ [(v, t)] = t" by (metis assoc.simps(2) subst.simps(1) subst_no_occs) fix s show "s ⊲ [(v, t)] ◊ [(v, t)] = s ⊲ [(v, t)]" by (induct s) auto qed lemma Unifier_Idem_subst: "Idem(r) ⟹ Unifier s (t ⊲ r) (u ⊲ r) ⟹ Unifier (r ◊ s) (t ⊲ r) (u ⊲ r)" by (simp add: Idem_def Unifier_def subst_eq_def) lemma Idem_comp: "Idem r ⟹ Unifier s (t ⊲ r) (u ⊲ r) ⟹ (!!q. Unifier q (t ⊲ r) (u ⊲ r) ⟹ s ◊ q ≐ q) ⟹ Idem (r ◊ s)" apply (frule Unifier_Idem_subst, blast) apply (force simp add: Idem_def subst_eq_def) done theorem unify_gives_Idem: "unify M N = Some σ ⟹ Idem σ" proof (induct M N arbitrary: σ rule: unify.induct) case (7 M M' N N' σ) then obtain θ1 θ2 where "unify M N = Some θ1" and θ2: "unify (M' ⊲ θ1) (N' ⊲ θ1) = Some θ2" and σ: "σ = θ1 ◊ θ2" and "Idem θ1" and "Idem θ2" by (auto split: option.split_asm) from θ2 have "Unifier θ2 (M' ⊲ θ1) (N' ⊲ θ1)" by (rule unify_computes_MGU[THEN MGU_is_Unifier]) with ‹Idem θ1› show "Idem σ" unfolding σ proof (rule Idem_comp) fix σ assume "Unifier σ (M' ⊲ θ1) (N' ⊲ θ1)" with θ2 obtain γ where σ: "σ ≐ θ2 ◊ γ" using unify_computes_MGU MGU_def by blast have "θ2 ◊ σ ≐ θ2 ◊ (θ2 ◊ γ)" by (rule subst_cong) (auto simp: σ) also have "... ≐ (θ2 ◊ θ2) ◊ γ" by (rule comp_assoc[symmetric]) also have "... ≐ θ2 ◊ γ" by (rule subst_cong) (auto simp: ‹Idem θ2›[unfolded Idem_def]) also have "... ≐ σ" by (rule σ[symmetric]) finally show "θ2 ◊ σ ≐ σ" . qed qed (auto intro!: Var_Idem split: option.splits if_splits) end