equal
deleted
inserted
replaced
1 (* Title: HOL/ex/BT.thy |
1 (* Title: HOL/ex/BT.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 |
5 |
6 Binary trees (based on the ZF version) |
6 Binary trees (based on the ZF version) |
7 *) |
7 *) |
8 |
8 |
9 BT = List + |
9 BT = List + |
10 |
10 |
11 datatype 'a bt = Lf | Br 'a ('a bt) ('a bt) |
11 datatype 'a bt = Lf | Br 'a ('a bt) ('a bt) |
12 |
12 |
13 consts |
13 consts |
14 n_nodes :: 'a bt => nat |
14 n_nodes :: 'a bt => nat |
15 n_leaves :: 'a bt => nat |
15 n_leaves :: 'a bt => nat |
16 reflect :: 'a bt => 'a bt |
16 reflect :: 'a bt => 'a bt |
17 bt_map :: ('a=>'b) => ('a bt => 'b bt) |
17 bt_map :: ('a=>'b) => ('a bt => 'b bt) |
18 preorder :: 'a bt => 'a list |
18 preorder :: 'a bt => 'a list |
19 inorder :: 'a bt => 'a list |
19 inorder :: 'a bt => 'a list |
20 postorder :: 'a bt => 'a list |
20 postorder :: 'a bt => 'a list |
21 |
21 |