src/HOL/ex/BT.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/BT.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 
     6 Datatype definition of binary trees
     7 *)
     8 
     9 open BT;
    10 
    11 (** BT simplification **)
    12 
    13 goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)";
    14 by (bt.induct_tac "t" 1);
    15 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
    16 qed "n_leaves_reflect";
    17 
    18 goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)";
    19 by (bt.induct_tac "t" 1);
    20 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
    21 qed "n_nodes_reflect";
    22 
    23 (*The famous relationship between the numbers of leaves and nodes*)
    24 goal BT.thy "n_leaves(t) = Suc(n_nodes(t))";
    25 by (bt.induct_tac "t" 1);
    26 by (ALLGOALS Asm_simp_tac);
    27 qed "n_leaves_nodes";
    28 
    29 goal BT.thy "reflect(reflect(t))=t";
    30 by (bt.induct_tac "t" 1);
    31 by (ALLGOALS Asm_simp_tac);
    32 qed "reflect_reflect_ident";
    33 
    34 goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)";
    35 by (bt.induct_tac "t" 1);
    36 by (ALLGOALS Asm_simp_tac);
    37 qed "bt_map_reflect";
    38 
    39 goal BT.thy "inorder (bt_map f t) = map f (inorder t)";
    40 by (bt.induct_tac "t" 1);
    41 by (ALLGOALS Asm_simp_tac);
    42 qed "inorder_bt_map";
    43 
    44 goal BT.thy "preorder (reflect t) = rev (postorder t)";
    45 by (bt.induct_tac "t" 1);
    46 by (ALLGOALS Asm_simp_tac);
    47 qed "preorder_reflect";
    48 
    49 goal BT.thy "inorder (reflect t) = rev (inorder t)";
    50 by (bt.induct_tac "t" 1);
    51 by (ALLGOALS Asm_simp_tac);
    52 qed "inorder_reflect";
    53 
    54 goal BT.thy "postorder (reflect t) = rev (preorder t)";
    55 by (bt.induct_tac "t" 1);
    56 by (ALLGOALS Asm_simp_tac);
    57 qed "postorder_reflect";
    58 
    59