(* ID: $Id$ 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 {* Basic definitions *} datatype 'a trm = Var 'a | Const 'a | App "'a trm" "'a trm" (infix "\" 60) types '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: *} fun apply_subst :: "'a trm \ 'a subst \ 'a trm" (infixl "\" 60) where "(Var v) \ s = assoc v (Var v) s" | "(Const c) \ s = (Const c)" | "(M \ N) \ s = (M \ s) \ (N \ s)" text {* Composition of substitutions: *} fun "compose" :: "'a subst \ 'a subst \ 'a subst" (infixl "\" 80) where "[] \ bl = bl" | "((a,b) # al) \ bl = (a, b \ bl) # (al \ bl)" text {* Equivalence of substitutions: *} definition eqv (infix "=\<^sub>s" 50) where "s1 =\<^sub>s s2 \ \t. t \ s1 = t \ s2" subsection {* Basic lemmas *} lemma apply_empty[simp]: "t \ [] = t" by (induct t) auto lemma compose_empty[simp]: "\ \ [] = \" by (induct \) auto lemma apply_compose[simp]: "t \ (s1 \ s2) = t \ s1 \ s2" proof (induct t) case App thus ?case by simp next case Const thus ?case by simp next case (Var v) thus ?case proof (induct s1) case Nil show ?case by simp next case (Cons p s1s) thus ?case by (cases p, simp) qed qed lemma eqv_refl[intro]: "s =\<^sub>s s" by (auto simp:eqv_def) lemma eqv_trans[trans]: "\s1 =\<^sub>s s2; s2 =\<^sub>s s3\ \ s1 =\<^sub>s s3" by (auto simp:eqv_def) lemma eqv_sym[sym]: "\s1 =\<^sub>s s2\ \ s2 =\<^sub>s s1" by (auto simp:eqv_def) lemma eqv_intro[intro]: "(\t. t \ \ = t \ \) \ \ =\<^sub>s \" by (auto simp:eqv_def) lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \ t \ s1 = t \ s2" by (auto simp:eqv_def) lemma compose_eqv: "\\ =\<^sub>s \'; \ =\<^sub>s \'\ \ (\ \ \) =\<^sub>s (\' \ \')" by (auto simp:eqv_def) lemma compose_assoc: "(a \ b) \ c =\<^sub>s a \ (b \ c)" by auto subsection {* Specification: Most general unifiers *} definition "Unifier \ t u \ (t\\ = u\\)" definition "MGU \ t u \ Unifier \ t u \ (\\. Unifier \ t u \ (\\. \ =\<^sub>s \ \ \))" lemma MGUI[intro]: "\t \ \ = u \ \; \\. t \ \ = u \ \ \ \\. \ =\<^sub>s \ \ \\ \ 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) subsection {* The unification algorithm *} text {* Occurs check: Proper subterm relation *} fun occ :: "'a trm \ 'a trm \ bool" where "occ u (Var v) = False" | "occ u (Const c) = False" | "occ u (M \ N) = (u = M \ u = N \ occ u M \ occ u N)" 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 (occ (Var v) (M \ N)) then None else Some [(v, M \ N)])" | "unify (Var v) M = (if (occ (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 {* Partial correctness *} text {* Some lemmas about occ and MGU: *} lemma subst_no_occ: "\occ (Var v) t \ Var v \ t \ t \ [(v,s)] = t" by (induct t) auto lemma MGU_Var[intro]: assumes no_occ: "\occ (Var v) t" shows "MGU [(v,t)] (Var v) t" proof (intro MGUI exI) show "Var v \ [(v,t)] = t \ [(v,t)]" using no_occ by (cases "Var v = t", auto simp:subst_no_occ) next fix \ assume th: "Var v \ \ = t \ \" show "\ =\<^sub>s [(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: "\' =\<^sub>s \1 \ \" unfolding MGU_def Unifier_def by auto from Ns have "N \ \1 \ \ = N' \ \1 \ \" by (simp add:eqv_dest[OF eqv]) with MGU_outer obtain \ where eqv2: "\ =\<^sub>s \2 \ \" unfolding MGU_def Unifier_def by auto have "\' =\<^sub>s \ \ \" unfolding \ by (rule eqv_intro, auto simp:eqv_dest[OF eqv] eqv_dest[OF eqv2]) thus "\\. \' =\<^sub>s \ \ \" .. qed qed (auto split:split_if_asm) -- "Solve the remaining cases automatically" subsection {* Properties used in termination proof *} text {* The variables of a term: *} fun 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" lemma vars_of_finite[intro]: "finite (vars_of t)" by (induct t) simp_all 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: "\ =\<^sub>s \ \ elim \ x = elim \ x" by (auto simp:elim_def eqv_def) text {* Replacing a variable by itself yields an identity subtitution: *} lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []" proof fix t show "t \ [(v, Var v)] = t \ []" by (induct t) simp_all qed lemma var_same: "(t = Var v) = ([(v, t)] =\<^sub>s [])" proof assume t_v: "t = Var v" thus "[(v, t)] =\<^sub>s []" by auto next assume id: "[(v, t)] =\<^sub>s []" 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 occ and elim *} lemma remove_var: assumes [simp]: "v \ vars_of s" shows "v \ vars_of (t \ [(v, s)])" by (induct t) simp_all lemma occ_elim: "\occ (Var v) t \ elim [(v,t)] v \ [(v,t)] =\<^sub>s []" proof (induct t) case (Var x) show ?case proof cases assume "v = x" thus ?thesis by (simp add:var_same[symmetric]) 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 (App M N) hence ih1: "elim [(v, M)] v \ [(v, M)] =\<^sub>s []" and ih2: "elim [(v, N)] v \ [(v, N)] =\<^sub>s []" and nonocc: "Var v \ M" "Var v \ N" by auto from nonocc have "\ [(v,M)] =\<^sub>s []" by (simp add:var_same[symmetric]) 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 nonocc have "\ [(v,N)] =\<^sub>s []" by (simp add:var_same[symmetric]) 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 "\occ (Var v) (M\N)" by (cases "occ (Var v) (M\N)", auto) with 4 have "\ = [(v, M\N)]" by simp thus ?case by (induct t) auto next case (5 v M) hence "\occ (Var v) M" by (cases "occ (Var v) M", 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) \ \ =\<^sub>s []" (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_occ: "\ occ (Var v) (Const c)" by simp with 3 have "\ = [(v, Const c)]" by simp with occ_elim[OF no_occ] show ?case by auto next case (4 M N v) hence no_occ: "\occ (Var v) (M\N)" by (cases "occ (Var v) (M\N)", auto) with 4 have "\ = [(v, M\N)]" by simp with occ_elim[OF no_occ] show ?case by auto next case (5 v M) hence no_occ: "\occ (Var v) M" by (cases "occ (Var v) M", auto) with 5 have "\ = [(v, M)]" by simp with occ_elim[OF no_occ] 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 =\<^sub>s []" have "\ =\<^sub>s (\1 \ [])" unfolding \ by (rule compose_eqv) auto also have "\ =\<^sub>s \1" by auto finally have "\ =\<^sub>s \1" . from ih1 show ?thesis proof assume "\v\vars_of M \ vars_of M'. elim \1 v" with elim_eqv[OF `\ =\<^sub>s \1`] show ?thesis by auto next note `\ =\<^sub>s \1` also assume "\1 =\<^sub>s []" 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 "\ =\<^sub>s []" hence "N \ \ = N" and "N' \ \ = N'" by auto thus ?thesis by (auto intro!: measures_less intro: psubset_card_mono) qed qed end