author | paulson |
Thu, 25 Jun 1998 13:57:34 +0200 | |
changeset 5078 | 7b5ea59c0275 |
parent 5069 | 3ea049f7979d |
child 5184 | 9b8547a9496a |
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 |
open BT; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
10 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
11 |
(** BT simplification **) |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
12 |
|
5069 | 13 |
Goal "n_leaves(reflect(t)) = n_leaves(t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
14 |
by (bt.induct_tac "t" 1); |
4089 | 15 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute]))); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
16 |
qed "n_leaves_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
17 |
|
5069 | 18 |
Goal "n_nodes(reflect(t)) = n_nodes(t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
19 |
by (bt.induct_tac "t" 1); |
4089 | 20 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute]))); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
21 |
qed "n_nodes_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
22 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
23 |
(*The famous relationship between the numbers of leaves and nodes*) |
5069 | 24 |
Goal "n_leaves(t) = Suc(n_nodes(t))"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
25 |
by (bt.induct_tac "t" 1); |
1266 | 26 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
27 |
qed "n_leaves_nodes"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
28 |
|
5069 | 29 |
Goal "reflect(reflect(t))=t"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
30 |
by (bt.induct_tac "t" 1); |
1266 | 31 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
32 |
qed "reflect_reflect_ident"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
33 |
|
5069 | 34 |
Goal "bt_map f (reflect t) = reflect (bt_map f t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
35 |
by (bt.induct_tac "t" 1); |
1266 | 36 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
37 |
qed "bt_map_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
38 |
|
5069 | 39 |
Goal "inorder (bt_map f t) = map f (inorder t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
40 |
by (bt.induct_tac "t" 1); |
1266 | 41 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
42 |
qed "inorder_bt_map"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
43 |
|
5069 | 44 |
Goal "preorder (reflect t) = rev (postorder t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
45 |
by (bt.induct_tac "t" 1); |
1266 | 46 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
47 |
qed "preorder_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
48 |
|
5069 | 49 |
Goal "inorder (reflect t) = rev (inorder t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
50 |
by (bt.induct_tac "t" 1); |
1266 | 51 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
52 |
qed "inorder_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
53 |
|
5069 | 54 |
Goal "postorder (reflect t) = rev (preorder t)"; |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
55 |
by (bt.induct_tac "t" 1); |
1266 | 56 |
by (ALLGOALS Asm_simp_tac); |
1167
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
57 |
qed "postorder_reflect"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
58 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
59 |