1 (* Title: HOL/ex/BT.thy |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1995 University of Cambridge |
|
4 |
|
5 Binary trees |
|
6 *) |
|
7 |
|
8 section {* Binary trees *} |
|
9 |
|
10 theory BT imports Main begin |
|
11 |
|
12 datatype 'a bt = |
|
13 Lf |
|
14 | Br 'a "'a bt" "'a bt" |
|
15 |
|
16 primrec n_nodes :: "'a bt => nat" where |
|
17 "n_nodes Lf = 0" |
|
18 | "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" |
|
19 |
|
20 primrec n_leaves :: "'a bt => nat" where |
|
21 "n_leaves Lf = Suc 0" |
|
22 | "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" |
|
23 |
|
24 primrec depth :: "'a bt => nat" where |
|
25 "depth Lf = 0" |
|
26 | "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" |
|
27 |
|
28 primrec reflect :: "'a bt => 'a bt" where |
|
29 "reflect Lf = Lf" |
|
30 | "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" |
|
31 |
|
32 primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where |
|
33 "bt_map f Lf = Lf" |
|
34 | "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" |
|
35 |
|
36 primrec preorder :: "'a bt => 'a list" where |
|
37 "preorder Lf = []" |
|
38 | "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
|
39 |
|
40 primrec inorder :: "'a bt => 'a list" where |
|
41 "inorder Lf = []" |
|
42 | "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
|
43 |
|
44 primrec postorder :: "'a bt => 'a list" where |
|
45 "postorder Lf = []" |
|
46 | "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
|
47 |
|
48 primrec append :: "'a bt => 'a bt => 'a bt" where |
|
49 "append Lf t = t" |
|
50 | "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" |
|
51 |
|
52 text {* \medskip BT simplification *} |
|
53 |
|
54 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
|
55 apply (induct t) |
|
56 apply auto |
|
57 done |
|
58 |
|
59 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
|
60 apply (induct t) |
|
61 apply auto |
|
62 done |
|
63 |
|
64 lemma depth_reflect: "depth (reflect t) = depth t" |
|
65 apply (induct t) |
|
66 apply auto |
|
67 done |
|
68 |
|
69 text {* |
|
70 The famous relationship between the numbers of leaves and nodes. |
|
71 *} |
|
72 |
|
73 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
|
74 apply (induct t) |
|
75 apply auto |
|
76 done |
|
77 |
|
78 lemma reflect_reflect_ident: "reflect (reflect t) = t" |
|
79 apply (induct t) |
|
80 apply auto |
|
81 done |
|
82 |
|
83 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
|
84 apply (induct t) |
|
85 apply simp_all |
|
86 done |
|
87 |
|
88 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
|
89 apply (induct t) |
|
90 apply simp_all |
|
91 done |
|
92 |
|
93 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
|
94 apply (induct t) |
|
95 apply simp_all |
|
96 done |
|
97 |
|
98 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" |
|
99 apply (induct t) |
|
100 apply simp_all |
|
101 done |
|
102 |
|
103 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" |
|
104 apply (induct t) |
|
105 apply simp_all |
|
106 done |
|
107 |
|
108 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" |
|
109 apply (induct t) |
|
110 apply (simp_all add: distrib_right) |
|
111 done |
|
112 |
|
113 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
|
114 apply (induct t) |
|
115 apply simp_all |
|
116 done |
|
117 |
|
118 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
|
119 apply (induct t) |
|
120 apply simp_all |
|
121 done |
|
122 |
|
123 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
|
124 apply (induct t) |
|
125 apply simp_all |
|
126 done |
|
127 |
|
128 text {* |
|
129 Analogues of the standard properties of the append function for lists. |
|
130 *} |
|
131 |
|
132 lemma append_assoc [simp]: |
|
133 "append (append t1 t2) t3 = append t1 (append t2 t3)" |
|
134 apply (induct t1) |
|
135 apply simp_all |
|
136 done |
|
137 |
|
138 lemma append_Lf2 [simp]: "append t Lf = t" |
|
139 apply (induct t) |
|
140 apply simp_all |
|
141 done |
|
142 |
|
143 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" |
|
144 apply (induct t1) |
|
145 apply (simp_all add: max_add_distrib_left) |
|
146 done |
|
147 |
|
148 lemma n_leaves_append [simp]: |
|
149 "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
|
150 apply (induct t1) |
|
151 apply (simp_all add: distrib_right) |
|
152 done |
|
153 |
|
154 lemma bt_map_append: |
|
155 "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" |
|
156 apply (induct t1) |
|
157 apply simp_all |
|
158 done |
|
159 |
|
160 end |
|