|
2113
|
1 |
(* Title: Substitutions/UTerm.thy
|
|
|
2 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
|
|
3 |
Copyright 1993 University of Cambridge
|
|
|
4 |
|
|
|
5 |
Simple term structure for unification.
|
|
|
6 |
Binary trees with leaves that are constants or variables.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
UTerm = Finite +
|
|
|
10 |
|
|
|
11 |
datatype 'a uterm = Var ('a)
|
|
|
12 |
| Const ('a)
|
|
|
13 |
| Comb ('a uterm) ('a uterm)
|
|
|
14 |
|
|
|
15 |
consts
|
|
|
16 |
vars_of :: 'a uterm => 'a set
|
|
|
17 |
"<:" :: 'a uterm => 'a uterm => bool (infixl 54)
|
|
|
18 |
uterm_size :: 'a uterm => nat
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
primrec vars_of uterm
|
|
|
22 |
vars_of_Var "vars_of (Var v) = {v}"
|
|
|
23 |
vars_of_Const "vars_of (Const c) = {}"
|
|
|
24 |
vars_of_Comb "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
|
|
|
25 |
|
|
|
26 |
|
|
|
27 |
primrec "op <:" uterm
|
|
|
28 |
occs_Var "u <: (Var v) = False"
|
|
|
29 |
occs_Const "u <: (Const c) = False"
|
|
|
30 |
occs_Comb "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
|
|
|
31 |
|
|
|
32 |
primrec uterm_size uterm
|
|
|
33 |
uterm_size_Var "uterm_size (Var v) = 0"
|
|
|
34 |
uterm_size_Const "uterm_size (Const c) = 0"
|
|
|
35 |
uterm_size_Comb "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
|
|
|
36 |
|
|
|
37 |
end
|