author | nipkow |
Mon, 03 Nov 1997 08:08:14 +0100 | |
changeset 4069 | d6d06a03a2e9 |
parent 1465 | 5d7a7e439cec |
child 4089 | 96fba19bcbe2 |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
13 |
goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
14 |
by (bt.induct_tac "t" 1); |
1266 | 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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
18 |
goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)"; |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
19 |
by (bt.induct_tac "t" 1); |
1266 | 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*) |
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
24 |
goal BT.thy "n_leaves(t) = Suc(n_nodes(t))"; |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
29 |
goal BT.thy "reflect(reflect(t))=t"; |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
34 |
goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)"; |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
39 |
goal BT.thy "inorder (bt_map f t) = map f (inorder t)"; |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
44 |
goal BT.thy "preorder (reflect t) = rev (postorder t)"; |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
49 |
goal BT.thy "inorder (reflect t) = rev (inorder t)"; |
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 |
|
cbd32a0f2f41
New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff
changeset
|
54 |
goal BT.thy "postorder (reflect t) = rev (preorder t)"; |
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 |