|
1 (* Title: HOL/ex/BT.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 |
|
6 Datatype definition of binary trees |
|
7 *) |
|
8 |
|
9 open BT; |
|
10 |
|
11 (** BT simplification **) |
|
12 |
|
13 val bt_ss = list_ss |
|
14 addsimps [n_nodes_Lf, n_nodes_Br, |
|
15 n_leaves_Lf, n_leaves_Br, |
|
16 reflect_Lf, reflect_Br, |
|
17 bt_map_Lf, bt_map_Br, |
|
18 preorder_Lf, preorder_Br, |
|
19 inorder_Lf, inorder_Br, |
|
20 postorder_Lf, postorder_Br]; |
|
21 |
|
22 |
|
23 goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)"; |
|
24 by (bt.induct_tac "t" 1); |
|
25 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute]))); |
|
26 qed "n_leaves_reflect"; |
|
27 |
|
28 goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)"; |
|
29 by (bt.induct_tac "t" 1); |
|
30 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute]))); |
|
31 qed "n_nodes_reflect"; |
|
32 |
|
33 (*The famous relationship between the numbers of leaves and nodes*) |
|
34 goal BT.thy "n_leaves(t) = Suc(n_nodes(t))"; |
|
35 by (bt.induct_tac "t" 1); |
|
36 by (ALLGOALS (asm_simp_tac bt_ss)); |
|
37 qed "n_leaves_nodes"; |
|
38 |
|
39 goal BT.thy "reflect(reflect(t))=t"; |
|
40 by (bt.induct_tac "t" 1); |
|
41 by (ALLGOALS (asm_simp_tac bt_ss)); |
|
42 qed "reflect_reflect_ident"; |
|
43 |
|
44 goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)"; |
|
45 by (bt.induct_tac "t" 1); |
|
46 by (ALLGOALS (asm_simp_tac bt_ss)); |
|
47 qed "bt_map_reflect"; |
|
48 |
|
49 goal BT.thy "inorder (bt_map f t) = map f (inorder t)"; |
|
50 by (bt.induct_tac "t" 1); |
|
51 by (ALLGOALS (asm_simp_tac bt_ss)); |
|
52 qed "inorder_bt_map"; |
|
53 |
|
54 goal BT.thy "preorder (reflect t) = rev (postorder t)"; |
|
55 by (bt.induct_tac "t" 1); |
|
56 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); |
|
57 qed "preorder_reflect"; |
|
58 |
|
59 goal BT.thy "inorder (reflect t) = rev (inorder t)"; |
|
60 by (bt.induct_tac "t" 1); |
|
61 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); |
|
62 qed "inorder_reflect"; |
|
63 |
|
64 goal BT.thy "postorder (reflect t) = rev (preorder t)"; |
|
65 by (bt.induct_tac "t" 1); |
|
66 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); |
|
67 qed "postorder_reflect"; |
|
68 |
|
69 |