author | haftmann |
Mon, 04 Jun 2007 15:43:32 +0200 | |
changeset 23236 | 91d71bde1112 |
parent 23023 | 7b52c4fde622 |
child 39246 | 9e58f0499f57 |
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 |
|
20711 | 6 |
Binary trees |
1167
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 |
|
11024 | 9 |
header {* Binary trees *} |
10 |
||
16417 | 11 |
theory BT imports Main begin |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
12 |
|
11024 | 13 |
datatype 'a bt = |
14 |
Lf |
|
15 |
| Br 'a "'a bt" "'a bt" |
|
16 |
||
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
17 |
consts |
19478 | 18 |
n_nodes :: "'a bt => nat" |
19 |
n_leaves :: "'a bt => nat" |
|
20 |
depth :: "'a bt => nat" |
|
21 |
reflect :: "'a bt => 'a bt" |
|
22 |
bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
|
23 |
preorder :: "'a bt => 'a list" |
|
24 |
inorder :: "'a bt => 'a list" |
|
11024 | 25 |
postorder :: "'a bt => 'a list" |
23236 | 26 |
append :: "'a bt => 'a bt => 'a bt" |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
27 |
|
5184 | 28 |
primrec |
19478 | 29 |
"n_nodes Lf = 0" |
11024 | 30 |
"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
|
31 |
|
5184 | 32 |
primrec |
19478 | 33 |
"n_leaves Lf = Suc 0" |
1896 | 34 |
"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
|
35 |
|
5184 | 36 |
primrec |
19478 | 37 |
"depth Lf = 0" |
20711 | 38 |
"depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" |
19478 | 39 |
|
40 |
primrec |
|
41 |
"reflect Lf = Lf" |
|
1896 | 42 |
"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
|
43 |
|
5184 | 44 |
primrec |
1896 | 45 |
"bt_map f Lf = Lf" |
46 |
"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
|
47 |
|
5184 | 48 |
primrec |
19478 | 49 |
"preorder Lf = []" |
1896 | 50 |
"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
51 |
|
5184 | 52 |
primrec |
19478 | 53 |
"inorder Lf = []" |
1896 | 54 |
"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
55 |
|
5184 | 56 |
primrec |
19478 | 57 |
"postorder Lf = []" |
1896 | 58 |
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
59 |
|
19478 | 60 |
primrec |
23236 | 61 |
"append Lf t = t" |
62 |
"append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" |
|
19478 | 63 |
|
11024 | 64 |
|
65 |
text {* \medskip BT simplification *} |
|
66 |
||
67 |
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
|
68 |
apply (induct t) |
|
69 |
apply auto |
|
70 |
done |
|
71 |
||
72 |
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
|
73 |
apply (induct t) |
|
74 |
apply auto |
|
75 |
done |
|
76 |
||
19478 | 77 |
lemma depth_reflect: "depth (reflect t) = depth t" |
20711 | 78 |
apply (induct t) |
79 |
apply auto |
|
19478 | 80 |
done |
81 |
||
11024 | 82 |
text {* |
83 |
The famous relationship between the numbers of leaves and nodes. |
|
84 |
*} |
|
85 |
||
86 |
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
|
87 |
apply (induct t) |
|
88 |
apply auto |
|
89 |
done |
|
90 |
||
91 |
lemma reflect_reflect_ident: "reflect (reflect t) = t" |
|
92 |
apply (induct t) |
|
93 |
apply auto |
|
94 |
done |
|
95 |
||
96 |
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
|
97 |
apply (induct t) |
|
98 |
apply simp_all |
|
99 |
done |
|
100 |
||
19526 | 101 |
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
102 |
apply (induct t) |
|
103 |
apply simp_all |
|
104 |
done |
|
105 |
||
11024 | 106 |
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
107 |
apply (induct t) |
|
108 |
apply simp_all |
|
109 |
done |
|
110 |
||
19526 | 111 |
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" |
112 |
apply (induct t) |
|
113 |
apply simp_all |
|
114 |
done |
|
115 |
||
116 |
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" |
|
117 |
apply (induct t) |
|
118 |
apply simp_all |
|
119 |
done |
|
120 |
||
121 |
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" |
|
122 |
apply (induct t) |
|
123 |
apply (simp_all add: left_distrib) |
|
124 |
done |
|
125 |
||
11024 | 126 |
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
127 |
apply (induct t) |
|
128 |
apply simp_all |
|
129 |
done |
|
130 |
||
131 |
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
|
132 |
apply (induct t) |
|
133 |
apply simp_all |
|
134 |
done |
|
135 |
||
136 |
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
|
137 |
apply (induct t) |
|
138 |
apply simp_all |
|
139 |
done |
|
140 |
||
19478 | 141 |
text {* |
142 |
Analogues of the standard properties of the append function for lists. |
|
143 |
*} |
|
144 |
||
145 |
lemma append_assoc [simp]: |
|
23236 | 146 |
"append (append t1 t2) t3 = append t1 (append t2 t3)" |
19478 | 147 |
apply (induct t1) |
148 |
apply simp_all |
|
149 |
done |
|
150 |
||
23236 | 151 |
lemma append_Lf2 [simp]: "append t Lf = t" |
19478 | 152 |
apply (induct t) |
153 |
apply simp_all |
|
154 |
done |
|
155 |
||
23236 | 156 |
lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" |
19478 | 157 |
apply (induct t1) |
158 |
apply (simp_all add: max_add_distrib_left) |
|
159 |
done |
|
160 |
||
161 |
lemma n_leaves_append [simp]: |
|
23236 | 162 |
"n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
19478 | 163 |
apply (induct t1) |
164 |
apply (simp_all add: left_distrib) |
|
165 |
done |
|
166 |
||
19526 | 167 |
lemma bt_map_append: |
23236 | 168 |
"bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" |
19526 | 169 |
apply (induct t1) |
170 |
apply simp_all |
|
171 |
done |
|
172 |
||
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
173 |
end |