author | paulson |
Sat, 04 Mar 2000 11:52:42 +0100 | |
changeset 8339 | bcadeb9c7095 |
parent 5184 | 9b8547a9496a |
child 11024 | 23bf8d787b04 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/ex/BT.thy |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
2 |
ID: $Id$ |
1476 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
4 |
Copyright 1995 University of Cambridge |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
5 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
6 |
Binary trees (based on the ZF version) |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
7 |
*) |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
8 |
|
8339 | 9 |
BT = Main + |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
10 |
|
8339 | 11 |
datatype 'a bt = Lf |
12 |
| Br 'a ('a bt) ('a bt) |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
13 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
14 |
consts |
1476 | 15 |
n_nodes :: 'a bt => nat |
16 |
n_leaves :: 'a bt => nat |
|
17 |
reflect :: 'a bt => 'a bt |
|
1376 | 18 |
bt_map :: ('a=>'b) => ('a bt => 'b bt) |
19 |
preorder :: 'a bt => 'a list |
|
20 |
inorder :: 'a bt => 'a list |
|
21 |
postorder :: 'a bt => 'a list |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
22 |
|
5184 | 23 |
primrec |
1896 | 24 |
"n_nodes (Lf) = 0" |
25 |
"n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
26 |
|
5184 | 27 |
primrec |
1896 | 28 |
"n_leaves (Lf) = Suc 0" |
29 |
"n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
30 |
|
5184 | 31 |
primrec |
1896 | 32 |
"reflect (Lf) = Lf" |
33 |
"reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
34 |
|
5184 | 35 |
primrec |
1896 | 36 |
"bt_map f Lf = Lf" |
37 |
"bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
38 |
|
5184 | 39 |
primrec |
1896 | 40 |
"preorder (Lf) = []" |
41 |
"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
42 |
|
5184 | 43 |
primrec |
1896 | 44 |
"inorder (Lf) = []" |
45 |
"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
46 |
|
5184 | 47 |
primrec |
1896 | 48 |
"postorder (Lf) = []" |
49 |
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
50 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
51 |
end |
1896 | 52 |