# HG changeset patch # User lcp # Date 804435384 -7200 # Node ID cbd32a0f2f41995b278edd26208b6e3e689b39e5 # Parent def4ee9e116dca4334ba9698173f99d818309e38 New theory and proofs including preorder, inorder, ..., initially from ZF/ex/BT. Demonstrates datatypes and primrec. diff -r def4ee9e116d -r cbd32a0f2f41 src/HOL/ex/BT.ML --- /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"; + + diff -r def4ee9e116d -r cbd32a0f2f41 src/HOL/ex/BT.thy --- /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