1476
|
1 |
(* Title: Subst/unifier.thy
|
|
2 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
968
|
3 |
Copyright 1993 University of Cambridge
|
|
4 |
|
|
5 |
Definition of most general idempotent unifier
|
|
6 |
*)
|
|
7 |
|
|
8 |
Unifier = Subst +
|
|
9 |
|
|
10 |
consts
|
|
11 |
|
|
12 |
Idem :: "('a*('a uterm))list=> bool"
|
|
13 |
Unifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
|
|
14 |
">>" :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
|
|
15 |
MGUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
|
|
16 |
MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
|
1374
|
17 |
UWFD :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool
|
968
|
18 |
|
|
19 |
rules (*Definitions*)
|
|
20 |
|
|
21 |
Idem_def "Idem(s) == s <> s =s= s"
|
|
22 |
Unifier_def "Unifier s t u == t <| s = u <| s"
|
|
23 |
MoreGeneral_def "r >> s == ? q.s =s= r <> q"
|
1151
|
24 |
MGUnifier_def "MGUnifier s t u == Unifier s t u &
|
1476
|
25 |
(! r.Unifier r t u --> s >> r)"
|
968
|
26 |
MGIUnifier_def "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
|
|
27 |
|
|
28 |
UWFD_def
|
1151
|
29 |
"UWFD x y x' y' ==
|
|
30 |
(vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |
|
|
31 |
(vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
|
968
|
32 |
|
|
33 |
end
|