author | nipkow |
Mon, 16 Aug 2004 14:22:27 +0200 | |
changeset 15131 | c69542757a4d |
parent 3268 | 012c43174664 |
child 15635 | 8408a06590a6 |
permissions | -rw-r--r-- |
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
1 |
(* Title: Subst/Unifier.thy |
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
2 |
ID: $Id$ |
1476 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
6 |
Definition of most general unifier |
968 | 7 |
*) |
8 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
9 |
Unifier = Subst + |
968 | 10 |
|
11 |
consts |
|
12 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
13 |
Unifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
14 |
">>" :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr 52) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
15 |
MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
16 |
Idem :: "('a * 'a uterm)list => bool" |
968 | 17 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
18 |
defs |
968 | 19 |
|
20 |
Unifier_def "Unifier s t u == t <| s = u <| s" |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
21 |
MoreGeneral_def "r >> s == ? q. s =$= r <> q" |
1151 | 22 |
MGUnifier_def "MGUnifier s t u == Unifier s t u & |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
23 |
(!r. Unifier r t u --> s >> r)" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1476
diff
changeset
|
24 |
Idem_def "Idem(s) == (s <> s) =$= s" |
968 | 25 |
end |