(* Author: Alexander Krauss, Technische Universitaet Muenchen *) header {* Case study: Unification Algorithm *} theory Unification imports Main begin text {* This is a formalization of a first-order unification algorithm. It uses the new "function" package to define recursive functions, which allows a better treatment of nested recursion. This is basically a modernized version of a previous formalization by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on previous work by Paulson and Manna \& Waldinger (for details, see there). Unlike that formalization, where the proofs of termination and some partial correctness properties are intertwined, we can prove partial correctness and termination separately. *} 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_var_iff: "v \ vars_of (Var w) \ w = v" by auto 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" text {* Applying a substitution to a variable: *} 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)" text {* Applying a substitution to a term: *} 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)" subsection {* Basic Laws *} 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 Var_in_subst: "v \ vars_of t \ w \ vars_of (t \ (v, Var(w)) # s)" by (induct t) auto 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) text {* Composition of Substitutions *} 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) subsection {* Specification: 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) definition Idem :: "'a subst \ bool" where "Idem s \ (s \ s) \ s" subsection {* The unification algorithm *} text {* 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 declare unify.psimps[simp] subsection {* Partial correctness *} text {* Some lemmas about occs and MGU: *} lemma subst_no_occs: "\ Var v \ t \ Var v \ t \ t \ [(v,s)] = t" by (induct t) auto lemma MGU_Var[intro]: assumes no_occs: "\ Var v \ t" shows "MGU [(v,t)] (Var v) t" proof (intro MGUI exI) show "Var v \ [(v,t)] = t \ [(v,t)]" using no_occs by (cases "Var v = t", auto simp:subst_no_occs) 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 declare MGU_Var[symmetric, intro] lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)" unfolding MGU_def Unifier_def by auto text {* If unification terminates, then it computes most general unifiers: *} lemma unify_partial_correctness: assumes "unify_dom (M, N)" assumes "unify M N = Some \" shows "MGU \ M N" using assms proof (induct M N arbitrary: \) 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 split:split_if_asm) -- "Solve the remaining cases automatically" 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_eqv: "\ \ \ \ elim \ x = elim \ x" by (auto simp:elim_def subst_eq_def) text {* Replacing a variable by itself yields an identity subtitution: *} lemma var_self[intro]: "[(v, Var v)] \ []" proof fix t show "t \ [(v, Var v)] = t \ []" by (induct t) simp_all qed lemma var_same: "([(v, t)] \ []) = (t = Var v)" proof assume t_v: "t = Var v" thus "[(v, t)] \ []" by auto next assume id: "[(v, t)] \ []" show "t = Var v" proof - have "t = Var v \ [(v, t)]" by simp also from id have "\ = Var v \ []" .. finally show ?thesis by simp qed qed text {* A lemma about occs and elim *} lemma remove_var: assumes [simp]: "v \ vars_of s" shows "v \ vars_of (t \ [(v, s)])" by (induct t) simp_all lemma occs_elim: "\ Var v \ t \ elim [(v,t)] v \ [(v,t)] \ []" proof (induct t) case (Var x) show ?case proof cases assume "v = x" thus ?thesis by (simp add:var_same) next assume neq: "v \ x" have "elim [(v, Var x)] v" by (auto intro!:remove_var simp:neq) thus ?thesis .. qed next case (Const c) have "elim [(v, Const c)] v" by (auto intro!:remove_var) thus ?case .. next case (Comb M N) hence ih1: "elim [(v, M)] v \ [(v, M)] \ []" and ih2: "elim [(v, N)] v \ [(v, N)] \ []" and nonoccs: "Var v \ M" "Var v \ N" by auto from nonoccs have "\ [(v,M)] \ []" by (simp add:var_same) with ih1 have "elim [(v, M)] v" by blast hence "v \ vars_of (Var v \ [(v,M)])" .. hence not_in_M: "v \ vars_of M" by simp from nonoccs have "\ [(v,N)] \ []" by (simp add:var_same) with ih2 have "elim [(v, N)] v" by blast hence "v \ vars_of (Var v \ [(v,N)])" .. hence not_in_N: "v \ vars_of N" by simp have "elim [(v, M \ N)] v" proof fix t show "v \ vars_of (t \ [(v, M \ N)])" proof (induct t) case (Var x) thus ?case by (simp add: not_in_M not_in_N) qed auto qed thus ?case .. qed text {* The result of a unification never introduces new variables: *} 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: split_if_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_eqv[OF `\ \ \1`] show ?thesis by auto next note `\ \ \1` also assume "\1 \ []" finally show ?thesis .. qed qed qed 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' 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 declare unify.psimps[simp del] end