src/HOL/ex/BT.ML
 author nipkow Fri, 24 Nov 2000 16:49:27 +0100 changeset 10519 ade64af4c57c parent 8339 bcadeb9c7095 permissions -rw-r--r--
hide many names from Datatype_Universe.
```
(*  Title:      HOL/ex/BT.ML
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Datatype definition of binary trees
*)

(** BT simplification **)

Goal "n_leaves(reflect(t)) = n_leaves(t)";
by (induct_tac "t" 1);
by Auto_tac;
qed "n_leaves_reflect";

Goal "n_nodes(reflect(t)) = n_nodes(t)";
by (induct_tac "t" 1);
by Auto_tac;
qed "n_nodes_reflect";

(*The famous relationship between the numbers of leaves and nodes*)
Goal "n_leaves(t) = Suc(n_nodes(t))";
by (induct_tac "t" 1);
by Auto_tac;
qed "n_leaves_nodes";

Goal "reflect(reflect(t))=t";
by (induct_tac "t" 1);
by Auto_tac;
qed "reflect_reflect_ident";

Goal "bt_map f (reflect t) = reflect (bt_map f t)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "bt_map_reflect";

Goal "inorder (bt_map f t) = map f (inorder t)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "inorder_bt_map";

Goal "preorder (reflect t) = rev (postorder t)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "preorder_reflect";

Goal "inorder (reflect t) = rev (inorder t)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "inorder_reflect";

Goal "postorder (reflect t) = rev (preorder t)";
by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "postorder_reflect";

```