1 (* Title: Subst/unifier.thy |
|
2 Author: Martin Coen, Cambridge University Computer Laboratory |
|
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" |
|
17 UWFD :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool" |
|
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" |
|
24 MGUnifier_def "MGUnifier(s,t,u) == Unifier(s,t,u) & |
|
25 (! r.Unifier(r,t,u) --> s >> r)" |
|
26 MGIUnifier_def "MGIUnifier(s,t,u) == MGUnifier(s,t,u) & Idem(s)" |
|
27 |
|
28 UWFD_def |
|
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')" |
|
32 |
|
33 end |
|