author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8339  bcadeb9c7095 
permissions  rwrr 
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); 
8339  13 
by Auto_tac; 
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); 
8339  18 
by Auto_tac; 
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); 
8339  24 
by Auto_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); 
8339  29 
by Auto_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 