6 Trees & forests, a mutually recursive type definition. |
6 Trees & forests, a mutually recursive type definition. |
7 *) |
7 *) |
8 |
8 |
9 TF = List + |
9 TF = List + |
10 consts |
10 consts |
11 TF_rec :: [i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i |
11 map :: [i=>i, i] => i |
12 TF_map :: [i=>i, i] => i |
12 size :: i=>i |
13 TF_size :: i=>i |
13 preorder :: i=>i |
14 TF_preorder :: i=>i |
|
15 list_of_TF :: i=>i |
14 list_of_TF :: i=>i |
16 TF_of_list :: i=>i |
15 of_list :: i=>i |
|
16 reflect :: i=>i |
17 |
17 |
18 tree, forest, tree_forest :: i=>i |
18 tree, forest, tree_forest :: i=>i |
19 |
19 |
20 datatype |
20 datatype |
21 "tree(A)" = Tcons ("a: A", "f: forest(A)") |
21 "tree(A)" = Tcons ("a: A", "f: forest(A)") |
22 and |
22 and |
23 "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") |
23 "forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)") |
24 |
24 |
25 defs |
25 primrec |
26 TF_rec_def |
26 "list_of_TF (Tcons(x,f)) = [Tcons(x,f)]" |
27 "TF_rec(z,b,c,d) == Vrec(z, |
27 "list_of_TF (Fnil) = []" |
28 %z r. tree_forest_case(%x f. b(x, f, r`f), |
28 "list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))" |
29 c, |
|
30 %t f. d(t, f, r`t, r`f), z))" |
|
31 |
29 |
32 list_of_TF_def |
30 primrec |
33 "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], |
31 "of_list([]) = Fnil" |
34 %t f r1 r2. Cons(t, r2))" |
32 "of_list(Cons(t,l)) = Fcons(t, of_list(l))" |
35 |
33 |
36 TF_of_list_def |
34 primrec |
37 "TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))" |
35 "map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))" |
|
36 "map (h, Fnil) = Fnil" |
|
37 "map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))" |
38 |
38 |
39 TF_map_def |
39 primrec |
40 "TF_map(h,z) == TF_rec(z, %x f r. Tcons(h(x),r), Fnil, |
40 "size (Tcons(x,f)) = succ(size(f))" |
41 %t f r1 r2. Fcons(r1,r2))" |
41 "size (Fnil) = 0" |
42 |
42 "size (Fcons(t,tf)) = size(t) #+ size(tf)" |
43 TF_size_def |
43 |
44 "TF_size(z) == TF_rec(z, %x f r. succ(r), 0, %t f r1 r2. r1#+r2)" |
44 primrec |
45 |
45 "preorder (Tcons(x,f)) = Cons(x, preorder(f))" |
46 TF_preorder_def |
46 "preorder (Fnil) = Nil" |
47 "TF_preorder(z) == TF_rec(z, %x f r. Cons(x,r), Nil, %t f r1 r2. r1@r2)" |
47 "preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)" |
|
48 |
|
49 primrec |
|
50 "reflect (Tcons(x,f)) = Tcons(x, reflect(f))" |
|
51 "reflect (Fnil) = Fnil" |
|
52 "reflect (Fcons(t,tf)) = of_list |
|
53 (list_of_TF (reflect(tf)) @ |
|
54 Cons(reflect(t), Nil))" |
48 |
55 |
49 end |
56 end |