author | wenzelm |
Mon, 20 Oct 1997 11:06:01 +0200 | |
changeset 3942 | 1f1c1f524d19 |
parent 3268 | 012c43174664 |
child 5184 | 9b8547a9496a |
permissions | -rw-r--r-- |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
1 |
(* Title: Subst/UTerm.thy |
3268
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 |
||
1476 | 6 |
Simple term structure for unification. |
968 | 7 |
Binary trees with leaves that are constants or variables. |
8 |
*) |
|
9 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
10 |
UTerm = Finite + |
968 | 11 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
12 |
datatype 'a uterm = Var ('a) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
13 |
| Const ('a) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
14 |
| Comb ('a uterm) ('a uterm) |
968 | 15 |
|
16 |
consts |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
17 |
vars_of :: 'a uterm => 'a set |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
18 |
"<:" :: 'a uterm => 'a uterm => bool (infixl 54) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
19 |
uterm_size :: 'a uterm => nat |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
20 |
|
968 | 21 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
22 |
primrec vars_of uterm |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
23 |
vars_of_Var "vars_of (Var v) = {v}" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
24 |
vars_of_Const "vars_of (Const c) = {}" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
25 |
vars_of_Comb "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))" |
968 | 26 |
|
27 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
28 |
primrec "op <:" uterm |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
29 |
occs_Var "u <: (Var v) = False" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
30 |
occs_Const "u <: (Const c) = False" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
31 |
occs_Comb "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)" |
968 | 32 |
|
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
33 |
primrec uterm_size uterm |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
34 |
uterm_size_Var "uterm_size (Var v) = 0" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
35 |
uterm_size_Const "uterm_size (Const c) = 0" |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
36 |
uterm_size_Comb "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)" |
968 | 37 |
|
38 |
end |