|
968
|
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"
|
|
1151
|
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"
|
|
968
|
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
|
|
1151
|
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)))))"
|
|
968
|
59 |
|
|
|
60 |
uterm_rec_def
|
|
1151
|
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)"
|
|
968
|
64 |
|
|
|
65 |
end
|