# HG changeset patch # User krauss # Date 1313957584 -7200 # Node ID f9825056dbabfc4c477896eadc03a5373b806e16 # Parent 3a10392fb8c309f199a8fd5e3c4d0ba51b9d7f1e more precise authors and comments; tuned order and headers diff -r 3a10392fb8c3 -r f9825056dbab src/HOL/ex/Unification.thy --- a/src/HOL/ex/Unification.thy Sun Aug 21 22:13:04 2011 +0200 +++ b/src/HOL/ex/Unification.thy Sun Aug 21 22:13:04 2011 +0200 @@ -1,26 +1,30 @@ -(* - Author: Alexander Krauss, Technische Universitaet Muenchen +(* Title: HOL/ex/Unification.thy + Author: Martin Coen, Cambridge University Computer Laboratory + Author: Konrad Slind, TUM & Cambridge University Computer Laboratory + Author: Alexander Krauss, TUM *) -header {* Case study: Unification Algorithm *} +header {* Substitution and Unification *} 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. + 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 - 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). + L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 + (1985), 143-170 - Unlike that formalization, where the proofs of termination and - some partial correctness properties are intertwined, we can prove - partial correctness and termination separately. + 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 *} @@ -63,15 +67,11 @@ 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" @@ -87,9 +87,6 @@ "[] \ bl = bl" | "((a,b) # al) \ bl = (a, b \ bl) # (al \ bl)" - -subsection {* Basic Laws *} - lemma subst_Nil[simp]: "t \ [] = t" by (induct t) auto @@ -122,8 +119,6 @@ \ t \ [(v,s)] = t" by (induct t) auto -text {* Composition of Substitutions *} - lemma comp_Nil[simp]: "\ \ [] = \" by (induct \) auto @@ -155,7 +150,7 @@ by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self) -subsection {* Specification: Most general unifiers *} +subsection {* Unifiers and Most General Unifiers *} definition Unifier :: "'a subst \ 'a trm \ 'a trm \ bool" where "Unifier \ t u \ (t \ \ = u \ \)" @@ -195,16 +190,8 @@ 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" @@ -226,7 +213,6 @@ subsection {* Properties used in termination proof *} - text {* Elimination of variables by a substitution: *} definition @@ -433,7 +419,7 @@ qed -subsection {* Other Properties *} +subsection {* Unification returns a Most General Unifier *} lemma unify_computes_MGU: "unify M N = Some \ \ MGU \ M N" @@ -481,6 +467,12 @@ qed qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_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)