src/HOL/Subst/Unify.thy

 (*  Title:      Subst/Unify
+    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
 Unification algorithm
 *)

 
 datatype 'a subst = Fail | Subst ('a list)
 
 consts
 
-   uterm_less :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
-   unifyRel   :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
-   unify      :: "'a uterm * 'a uterm => ('a * 'a uterm) subst"
+   unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set"
+   unify    :: "'a uterm * 'a uterm => ('a * 'a uterm) subst"
 
 defs
 
-  uterm_less_def "uterm_less == rprod (measure uterm_size) 
-                                      (measure uterm_size)"
-  
-  (* Termination relation for the Unify function *)
-  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** uterm_less)
-                               (%(x,y). (vars_of x Un vars_of y, (x,y)))"
+  (*Termination relation for the Unify function:
+    --either the set of variables decreases
+    --or the first argument does (in fact, both do)
+  *)
+  unifyRel_def  "unifyRel == inv_image  (finite_psubset ** measure uterm_size)
+                               (%(M,N). (vars_of M Un vars_of N, M))"
 
 recdef unify "unifyRel"
   "unify(Const m, Const n)  = (if (m=n) then Subst[] else Fail)"
   "unify(Const m, Comb M N) = Fail"
   "unify(Const m, Var v)    = Subst[(v,Const m)]"