# 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 \<times> 'a trm) list"
 
-text {* Applying a substitution to a variable: *}
-
 fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> '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 \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<lhd>" 55)
 where
   "(Var v) \<lhd> s = assoc v (Var v) s"
@@ -87,9 +87,6 @@
   "[] \<lozenge> bl = bl"
 | "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
 
-
-subsection {* Basic Laws *}
-
 lemma subst_Nil[simp]: "t \<lhd> [] = t"
 by (induct t) auto
 
@@ -122,8 +119,6 @@
   \<Longrightarrow> t \<lhd> [(v,s)] = t"
 by (induct t) auto
 
-text {* Composition of Substitutions *}
-
 lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
 by (induct \<sigma>) 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 \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
 where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
@@ -195,16 +190,8 @@
   by (auto simp: MGU_def Unifier_def)
   
 
-definition Idem :: "'a subst \<Rightarrow> bool"
-where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
-
-
-
 subsection {* The unification algorithm *}
 
-
-text {* The unification algorithm: *}
-
 function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
 where
   "unify (Const c) (M \<cdot> 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 \<sigma> \<Longrightarrow> MGU \<sigma> 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 \<Rightarrow> bool"
+where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
+
 lemma Idem_Nil [iff]: "Idem []"
   by (simp add: Idem_def)