Subst/unifier.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Subst/unifier.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,33 @@
+(*  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