8 |
8 |
9 open BT; |
9 open BT; |
10 |
10 |
11 (** BT simplification **) |
11 (** BT simplification **) |
12 |
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)"; |
13 goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)"; |
24 by (bt.induct_tac "t" 1); |
14 by (bt.induct_tac "t" 1); |
25 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute]))); |
15 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_commute]))); |
26 qed "n_leaves_reflect"; |
16 qed "n_leaves_reflect"; |
27 |
17 |
28 goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)"; |
18 goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)"; |
29 by (bt.induct_tac "t" 1); |
19 by (bt.induct_tac "t" 1); |
30 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute]))); |
20 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_commute]))); |
31 qed "n_nodes_reflect"; |
21 qed "n_nodes_reflect"; |
32 |
22 |
33 (*The famous relationship between the numbers of leaves and nodes*) |
23 (*The famous relationship between the numbers of leaves and nodes*) |
34 goal BT.thy "n_leaves(t) = Suc(n_nodes(t))"; |
24 goal BT.thy "n_leaves(t) = Suc(n_nodes(t))"; |
35 by (bt.induct_tac "t" 1); |
25 by (bt.induct_tac "t" 1); |
36 by (ALLGOALS (asm_simp_tac bt_ss)); |
26 by (ALLGOALS Asm_simp_tac); |
37 qed "n_leaves_nodes"; |
27 qed "n_leaves_nodes"; |
38 |
28 |
39 goal BT.thy "reflect(reflect(t))=t"; |
29 goal BT.thy "reflect(reflect(t))=t"; |
40 by (bt.induct_tac "t" 1); |
30 by (bt.induct_tac "t" 1); |
41 by (ALLGOALS (asm_simp_tac bt_ss)); |
31 by (ALLGOALS Asm_simp_tac); |
42 qed "reflect_reflect_ident"; |
32 qed "reflect_reflect_ident"; |
43 |
33 |
44 goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)"; |
34 goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)"; |
45 by (bt.induct_tac "t" 1); |
35 by (bt.induct_tac "t" 1); |
46 by (ALLGOALS (asm_simp_tac bt_ss)); |
36 by (ALLGOALS Asm_simp_tac); |
47 qed "bt_map_reflect"; |
37 qed "bt_map_reflect"; |
48 |
38 |
49 goal BT.thy "inorder (bt_map f t) = map f (inorder t)"; |
39 goal BT.thy "inorder (bt_map f t) = map f (inorder t)"; |
50 by (bt.induct_tac "t" 1); |
40 by (bt.induct_tac "t" 1); |
51 by (ALLGOALS (asm_simp_tac bt_ss)); |
41 by (ALLGOALS Asm_simp_tac); |
52 qed "inorder_bt_map"; |
42 qed "inorder_bt_map"; |
53 |
43 |
54 goal BT.thy "preorder (reflect t) = rev (postorder t)"; |
44 goal BT.thy "preorder (reflect t) = rev (postorder t)"; |
55 by (bt.induct_tac "t" 1); |
45 by (bt.induct_tac "t" 1); |
56 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); |
46 by (ALLGOALS Asm_simp_tac); |
57 qed "preorder_reflect"; |
47 qed "preorder_reflect"; |
58 |
48 |
59 goal BT.thy "inorder (reflect t) = rev (inorder t)"; |
49 goal BT.thy "inorder (reflect t) = rev (inorder t)"; |
60 by (bt.induct_tac "t" 1); |
50 by (bt.induct_tac "t" 1); |
61 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); |
51 by (ALLGOALS Asm_simp_tac); |
62 qed "inorder_reflect"; |
52 qed "inorder_reflect"; |
63 |
53 |
64 goal BT.thy "postorder (reflect t) = rev (preorder t)"; |
54 goal BT.thy "postorder (reflect t) = rev (preorder t)"; |
65 by (bt.induct_tac "t" 1); |
55 by (bt.induct_tac "t" 1); |
66 by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); |
56 by (ALLGOALS Asm_simp_tac); |
67 qed "postorder_reflect"; |
57 qed "postorder_reflect"; |
68 |
58 |
69 |
59 |