src/HOL/ex/Unification.thy
changeset 44372 f9825056dbab
parent 44371 3a10392fb8c3
child 44373 7321d628b57d
     1.1 --- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.3 @@ -1,26 +1,30 @@
     1.4 -(*
     1.5 -    Author:     Alexander Krauss, Technische Universitaet Muenchen
     1.6 +(*  Title:      HOL/ex/Unification.thy
     1.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     1.8 +    Author:     Konrad Slind, TUM & Cambridge University Computer Laboratory
     1.9 +    Author:     Alexander Krauss, TUM
    1.10  *)
    1.11  
    1.12 -header {* Case study: Unification Algorithm *}
    1.13 +header {* Substitution and Unification *}
    1.14  
    1.15  theory Unification
    1.16  imports Main
    1.17  begin
    1.18  
    1.19  text {* 
    1.20 -  This is a formalization of a first-order unification
    1.21 -  algorithm. It uses the new "function" package to define recursive
    1.22 -  functions, which allows a better treatment of nested recursion. 
    1.23 +  Implements Manna & Waldinger's formalization, with Paulson's
    1.24 +  simplifications, and some new simplifications by Slind and Krauss.
    1.25 +
    1.26 +  Z Manna & R Waldinger, Deductive Synthesis of the Unification
    1.27 +  Algorithm.  SCP 1 (1981), 5-48
    1.28  
    1.29 -  This is basically a modernized version of a previous formalization
    1.30 -  by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
    1.31 -  previous work by Paulson and Manna \& Waldinger (for details, see
    1.32 -  there).
    1.33 +  L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
    1.34 +  (1985), 143-170
    1.35  
    1.36 -  Unlike that formalization, where the proofs of termination and
    1.37 -  some partial correctness properties are intertwined, we can prove
    1.38 -  partial correctness and termination separately.
    1.39 +  K Slind, Reasoning about Terminating Functional Programs,
    1.40 +  Ph.D. thesis, TUM, 1999, Sect. 5.8
    1.41 +
    1.42 +  A Krauss, Partial and Nested Recursive Function Definitions in
    1.43 +  Higher-Order Logic, JAR 44(4):303–336, 2010. Sect. 6.3
    1.44  *}
    1.45  
    1.46  
    1.47 @@ -63,15 +67,11 @@
    1.48  
    1.49  type_synonym 'a subst = "('a \<times> 'a trm) list"
    1.50  
    1.51 -text {* Applying a substitution to a variable: *}
    1.52 -
    1.53  fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
    1.54  where
    1.55    "assoc x d [] = d"
    1.56  | "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
    1.57  
    1.58 -text {* Applying a substitution to a term: *}
    1.59 -
    1.60  primrec subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<lhd>" 55)
    1.61  where
    1.62    "(Var v) \<lhd> s = assoc v (Var v) s"
    1.63 @@ -87,9 +87,6 @@
    1.64    "[] \<lozenge> bl = bl"
    1.65  | "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
    1.66  
    1.67 -
    1.68 -subsection {* Basic Laws *}
    1.69 -
    1.70  lemma subst_Nil[simp]: "t \<lhd> [] = t"
    1.71  by (induct t) auto
    1.72  
    1.73 @@ -122,8 +119,6 @@
    1.74    \<Longrightarrow> t \<lhd> [(v,s)] = t"
    1.75  by (induct t) auto
    1.76  
    1.77 -text {* Composition of Substitutions *}
    1.78 -
    1.79  lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
    1.80  by (induct \<sigma>) auto
    1.81  
    1.82 @@ -155,7 +150,7 @@
    1.83  by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
    1.84  
    1.85  
    1.86 -subsection {* Specification: Most general unifiers *}
    1.87 +subsection {* Unifiers and Most General Unifiers *}
    1.88  
    1.89  definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
    1.90  where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
    1.91 @@ -195,16 +190,8 @@
    1.92    by (auto simp: MGU_def Unifier_def)
    1.93    
    1.94  
    1.95 -definition Idem :: "'a subst \<Rightarrow> bool"
    1.96 -where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
    1.97 -
    1.98 -
    1.99 -
   1.100  subsection {* The unification algorithm *}
   1.101  
   1.102 -
   1.103 -text {* The unification algorithm: *}
   1.104 -
   1.105  function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
   1.106  where
   1.107    "unify (Const c) (M \<cdot> N)   = None"
   1.108 @@ -226,7 +213,6 @@
   1.109  
   1.110  subsection {* Properties used in termination proof *}
   1.111  
   1.112 -
   1.113  text {* Elimination of variables by a substitution: *}
   1.114  
   1.115  definition
   1.116 @@ -433,7 +419,7 @@
   1.117  qed
   1.118  
   1.119  
   1.120 -subsection {* Other Properties *}
   1.121 +subsection {* Unification returns a Most General Unifier *}
   1.122  
   1.123  lemma unify_computes_MGU:
   1.124    "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
   1.125 @@ -481,6 +467,12 @@
   1.126    qed
   1.127  qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
   1.128  
   1.129 +
   1.130 +subsection {* Unification returns Idempotent Substitution *}
   1.131 +
   1.132 +definition Idem :: "'a subst \<Rightarrow> bool"
   1.133 +where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
   1.134 +
   1.135  lemma Idem_Nil [iff]: "Idem []"
   1.136    by (simp add: Idem_def)
   1.137