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 unifiation. |
|
6 Binary trees with leaves that are constants or variables. |
|
7 *) |
|
8 |
|
9 UTerm = Sexp + |
|
10 |
|
11 types uterm 1 |
|
12 |
|
13 arities |
|
14 uterm :: (term)term |
|
15 |
|
16 consts |
|
17 uterm :: "'a item set => 'a item set" |
|
18 Rep_uterm :: "'a uterm => 'a item" |
|
19 Abs_uterm :: "'a item => 'a uterm" |
|
20 VAR :: "'a item => 'a item" |
|
21 CONST :: "'a item => 'a item" |
|
22 COMB :: "['a item, 'a item] => 'a item" |
|
23 Var :: "'a => 'a uterm" |
|
24 Const :: "'a => 'a uterm" |
|
25 Comb :: "['a uterm, 'a uterm] => 'a uterm" |
|
26 UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, |
|
27 ['a item , 'a item, 'b, 'b]=>'b] => 'b" |
|
28 uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, |
|
29 ['a uterm, 'a uterm,'b,'b]=>'b] => 'b" |
|
30 |
|
31 defs |
|
32 (*defining the concrete constructors*) |
|
33 VAR_def "VAR(v) == In0(v)" |
|
34 CONST_def "CONST(v) == In1(In0(v))" |
|
35 COMB_def "COMB(t,u) == In1(In1(t $ u))" |
|
36 |
|
37 inductive "uterm(A)" |
|
38 intrs |
|
39 VAR_I "v:A ==> VAR(v) : uterm(A)" |
|
40 CONST_I "c:A ==> CONST(c) : uterm(A)" |
|
41 COMB_I "[| M:uterm(A); N:uterm(A) |] ==> COMB(M,N) : uterm(A)" |
|
42 |
|
43 rules |
|
44 (*faking a type definition...*) |
|
45 Rep_uterm "Rep_uterm(xs): uterm(range(Leaf))" |
|
46 Rep_uterm_inverse "Abs_uterm(Rep_uterm(xs)) = xs" |
|
47 Abs_uterm_inverse "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M" |
|
48 |
|
49 defs |
|
50 (*defining the abstract constructors*) |
|
51 Var_def "Var(v) == Abs_uterm(VAR(Leaf(v)))" |
|
52 Const_def "Const(c) == Abs_uterm(CONST(Leaf(c)))" |
|
53 Comb_def "Comb(t,u) == Abs_uterm(COMB(Rep_uterm(t),Rep_uterm(u)))" |
|
54 |
|
55 (*uterm recursion*) |
|
56 UTerm_rec_def |
|
57 "UTerm_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, |
|
58 Case(%x g.b(x), Case(%y g. c(y), Split(%x y g. d(x,y,g(x),g(y))))))" |
|
59 |
|
60 uterm_rec_def |
|
61 "uterm_rec(t,b,c,d) == |
|
62 UTerm_rec(Rep_uterm(t), %x.b(Inv(Leaf,x)), %x.c(Inv(Leaf,x)), |
|
63 %x y q r.d(Abs_uterm(x),Abs_uterm(y),q,r))" |
|
64 |
|
65 end |
|