author | wenzelm |
Mon, 16 Nov 1998 10:41:08 +0100 | |
changeset 5869 | b279a84ac11c |
parent 5227 | e5a6ace920a0 |
child 8339 | bcadeb9c7095 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/BT.ML |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
2 |
ID: $Id$ |
1465 | 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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
6 |
Datatype definition of binary trees |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
9 |
(** BT simplification **) |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
10 |
|
5069 | 11 |
Goal "n_leaves(reflect(t)) = n_leaves(t)"; |
5184 | 12 |
by (induct_tac "t" 1); |
4089 | 13 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute]))); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
14 |
qed "n_leaves_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
15 |
|
5069 | 16 |
Goal "n_nodes(reflect(t)) = n_nodes(t)"; |
5184 | 17 |
by (induct_tac "t" 1); |
4089 | 18 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute]))); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
19 |
qed "n_nodes_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
20 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
21 |
(*The famous relationship between the numbers of leaves and nodes*) |
5069 | 22 |
Goal "n_leaves(t) = Suc(n_nodes(t))"; |
5184 | 23 |
by (induct_tac "t" 1); |
1266 | 24 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
25 |
qed "n_leaves_nodes"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
26 |
|
5069 | 27 |
Goal "reflect(reflect(t))=t"; |
5184 | 28 |
by (induct_tac "t" 1); |
1266 | 29 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
30 |
qed "reflect_reflect_ident"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
31 |
|
5069 | 32 |
Goal "bt_map f (reflect t) = reflect (bt_map f t)"; |
5184 | 33 |
by (induct_tac "t" 1); |
1266 | 34 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
35 |
qed "bt_map_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
36 |
|
5069 | 37 |
Goal "inorder (bt_map f t) = map f (inorder t)"; |
5184 | 38 |
by (induct_tac "t" 1); |
1266 | 39 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
40 |
qed "inorder_bt_map"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
41 |
|
5069 | 42 |
Goal "preorder (reflect t) = rev (postorder t)"; |
5184 | 43 |
by (induct_tac "t" 1); |
1266 | 44 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
45 |
qed "preorder_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
46 |
|
5069 | 47 |
Goal "inorder (reflect t) = rev (inorder t)"; |
5184 | 48 |
by (induct_tac "t" 1); |
1266 | 49 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
50 |
qed "inorder_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
51 |
|
5069 | 52 |
Goal "postorder (reflect t) = rev (preorder t)"; |
5184 | 53 |
by (induct_tac "t" 1); |
1266 | 54 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
55 |
qed "postorder_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
56 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
57 |