--- a/src/HOL/Subst/Unify.thy Wed May 21 10:53:02 1997 +0200
+++ b/src/HOL/Subst/Unify.thy Wed May 21 10:53:38 1997 +0200
@@ -1,4 +1,5 @@
(* Title: Subst/Unify
+ ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
@@ -11,18 +12,17 @@
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)"