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 = Main + |
9 header {* Binary trees *} |
10 |
10 |
11 datatype 'a bt = Lf |
11 theory BT = Main: |
12 | Br 'a ('a bt) ('a bt) |
12 |
13 |
13 datatype 'a bt = |
|
14 Lf |
|
15 | Br 'a "'a bt" "'a bt" |
|
16 |
14 consts |
17 consts |
15 n_nodes :: 'a bt => nat |
18 n_nodes :: "'a bt => nat" |
16 n_leaves :: 'a bt => nat |
19 n_leaves :: "'a bt => nat" |
17 reflect :: 'a bt => 'a bt |
20 reflect :: "'a bt => 'a bt" |
18 bt_map :: ('a=>'b) => ('a bt => 'b bt) |
21 bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
19 preorder :: 'a bt => 'a list |
22 preorder :: "'a bt => 'a list" |
20 inorder :: 'a bt => 'a list |
23 inorder :: "'a bt => 'a list" |
21 postorder :: 'a bt => 'a list |
24 postorder :: "'a bt => 'a list" |
22 |
25 |
23 primrec |
26 primrec |
24 "n_nodes (Lf) = 0" |
27 "n_nodes (Lf) = 0" |
25 "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)" |
28 "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
26 |
29 |
27 primrec |
30 primrec |
28 "n_leaves (Lf) = Suc 0" |
31 "n_leaves (Lf) = Suc 0" |
29 "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
32 "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
30 |
33 |
46 |
49 |
47 primrec |
50 primrec |
48 "postorder (Lf) = []" |
51 "postorder (Lf) = []" |
49 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
52 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
50 |
53 |
|
54 |
|
55 text {* \medskip BT simplification *} |
|
56 |
|
57 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
|
58 apply (induct t) |
|
59 apply auto |
|
60 done |
|
61 |
|
62 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
|
63 apply (induct t) |
|
64 apply auto |
|
65 done |
|
66 |
|
67 text {* |
|
68 The famous relationship between the numbers of leaves and nodes. |
|
69 *} |
|
70 |
|
71 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
|
72 apply (induct t) |
|
73 apply auto |
|
74 done |
|
75 |
|
76 lemma reflect_reflect_ident: "reflect (reflect t) = t" |
|
77 apply (induct t) |
|
78 apply auto |
|
79 done |
|
80 |
|
81 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
|
82 apply (induct t) |
|
83 apply simp_all |
|
84 done |
|
85 |
|
86 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
|
87 apply (induct t) |
|
88 apply simp_all |
|
89 done |
|
90 |
|
91 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
|
92 apply (induct t) |
|
93 apply simp_all |
|
94 done |
|
95 |
|
96 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
|
97 apply (induct t) |
|
98 apply simp_all |
|
99 done |
|
100 |
|
101 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
|
102 apply (induct t) |
|
103 apply simp_all |
|
104 done |
|
105 |
51 end |
106 end |
52 |
|