TFL/examples/Subst/Unifier.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/Unifier.thy	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,24 @@
+(*  Title:      Subst/unifier.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Definition of most general unifier
+*)
+
+Unifier = Subst + 
+
+consts
+
+  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"
+  Idem       :: "('a*('a uterm))list => bool"
+
+rules  (*Definitions*)
+
+  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)"
+  Idem_def         "Idem(s) == s <> s =s= s"
+end