author | oheimb |
Thu, 01 Feb 2001 20:51:48 +0100 | |
changeset 11025 | a70b796d9af8 |
parent 11024 | 23bf8d787b04 |
child 16417 | 9bc16273c2d4 |
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 |
|
11024 | 6 |
Binary trees (based on the ZF version). |
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 |
||
11 |
theory BT = Main: |
|
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 |
11024 | 18 |
n_nodes :: "'a bt => nat" |
19 |
n_leaves :: "'a bt => nat" |
|
20 |
reflect :: "'a bt => 'a bt" |
|
21 |
bt_map :: "('a => 'b) => ('a bt => 'b bt)" |
|
22 |
preorder :: "'a bt => 'a list" |
|
23 |
inorder :: "'a bt => 'a list" |
|
24 |
postorder :: "'a bt => 'a list" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
25 |
|
5184 | 26 |
primrec |
1896 | 27 |
"n_nodes (Lf) = 0" |
11024 | 28 |
"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
|
29 |
|
5184 | 30 |
primrec |
1896 | 31 |
"n_leaves (Lf) = Suc 0" |
32 |
"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
|
33 |
|
5184 | 34 |
primrec |
1896 | 35 |
"reflect (Lf) = Lf" |
36 |
"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
|
37 |
|
5184 | 38 |
primrec |
1896 | 39 |
"bt_map f Lf = Lf" |
40 |
"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
|
41 |
|
5184 | 42 |
primrec |
1896 | 43 |
"preorder (Lf) = []" |
44 |
"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
45 |
|
5184 | 46 |
primrec |
1896 | 47 |
"inorder (Lf) = []" |
48 |
"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
49 |
|
5184 | 50 |
primrec |
1896 | 51 |
"postorder (Lf) = []" |
52 |
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" |
|
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
53 |
|
11024 | 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 |
||
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
106 |
end |