--- a/Subst/Unifier.thy Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Subst/unifier.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Definition of most general idempotent unifier
-*)
-
-Unifier = Subst +
-
-consts
-
- Idem :: "('a*('a uterm))list=> bool"
- Unifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
- ">>" :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
- MGUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
- MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
- UWFD :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool"
-
-rules (*Definitions*)
-
- Idem_def "Idem(s) == s <> s =s= s"
- Unifier_def "Unifier(s,t,u) == t <| s = u <| s"
- MoreGeneral_def "r >> s == ? q.s =s= r <> q"
- MGUnifier_def "MGUnifier(s,t,u) == Unifier(s,t,u) &
- (! r.Unifier(r,t,u) --> s >> r)"
- MGIUnifier_def "MGIUnifier(s,t,u) == MGUnifier(s,t,u) & Idem(s)"
-
- UWFD_def
- "UWFD(x,y,x',y') ==
- (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |
- (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
-
-end