New theory and proofs including preorder, inorder, ..., initially
from ZF/ex/BT. Demonstrates datatypes and primrec.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/BT.ML	Thu Jun 29 16:16:24 1995 +0200
@@ -0,0 +1,69 @@
+(*  Title: 	HOL/ex/BT.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+Datatype definition of binary trees
+*)
+
+open BT;
+
+(** BT simplification **)
+
+val bt_ss = list_ss
+    addsimps [n_nodes_Lf, n_nodes_Br,
+	      n_leaves_Lf, n_leaves_Br,
+	      reflect_Lf, reflect_Br,
+	      bt_map_Lf, bt_map_Br,
+	      preorder_Lf, preorder_Br,
+	      inorder_Lf, inorder_Br,
+	      postorder_Lf, postorder_Br];
+
+
+goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute])));
+qed "n_leaves_reflect";
+
+goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute])));
+qed "n_nodes_reflect";
+
+(*The famous relationship between the numbers of leaves and nodes*)
+goal BT.thy "n_leaves(t) = Suc(n_nodes(t))";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+qed "n_leaves_nodes";
+
+goal BT.thy "reflect(reflect(t))=t";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+qed "reflect_reflect_ident";
+
+goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+qed "bt_map_reflect";
+
+goal BT.thy "inorder (bt_map f t) = map f (inorder t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+qed "inorder_bt_map";
+
+goal BT.thy "preorder (reflect t) = rev (postorder t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append])));
+qed "preorder_reflect";
+
+goal BT.thy "inorder (reflect t) = rev (inorder t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append])));
+qed "inorder_reflect";
+
+goal BT.thy "postorder (reflect t) = rev (preorder t)";
+by (bt.induct_tac "t" 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append])));
+qed "postorder_reflect";
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/BT.thy	Thu Jun 29 16:16:24 1995 +0200
@@ -0,0 +1,50 @@
+(*  Title: 	HOL/ex/BT.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+Binary trees (based on the ZF version)
+*)
+
+BT = List +
+
+datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
+  
+consts
+    n_nodes	:: "'a bt => nat"
+    n_leaves   	:: "'a bt => nat"
+    reflect 	:: "'a bt => 'a bt"
+    bt_map      :: "('a=>'b) => ('a bt => 'b bt)"
+    preorder    :: "'a bt => 'a list"
+    inorder     :: "'a bt => 'a list"
+    postorder   :: "'a bt => 'a list"
+
+primrec n_nodes bt
+  n_nodes_Lf "n_nodes (Lf) = 0"
+  n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
+
+primrec n_leaves bt
+  n_leaves_Lf "n_leaves (Lf) = Suc 0"
+  n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
+
+primrec reflect bt
+  reflect_Lf "reflect (Lf) = Lf"
+  reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
+
+primrec bt_map bt
+  bt_map_Lf  "bt_map f Lf = Lf"
+  bt_map_Br  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+
+primrec preorder bt
+  preorder_Lf "preorder (Lf) = []"
+  preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+
+primrec inorder bt
+  inorder_Lf "inorder (Lf) = []"
+  inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+
+primrec postorder bt
+  postorder_Lf "postorder (Lf) = []"
+  postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+
+end