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
clasohm@1465
     1
(*  Title:      HOL/ex/BT.ML
lcp@1167
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@1167
     4
    Copyright   1995  University of Cambridge
lcp@1167
     5
lcp@1167
     6
Datatype definition of binary trees
lcp@1167
     7
*)
lcp@1167
     8
lcp@1167
     9
open BT;
lcp@1167
    10
lcp@1167
    11
(** BT simplification **)
lcp@1167
    12
lcp@1167
    13
goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)";
lcp@1167
    14
by (bt.induct_tac "t" 1);
wenzelm@4089
    15
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
lcp@1167
    16
qed "n_leaves_reflect";
lcp@1167
    17
lcp@1167
    18
goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)";
lcp@1167
    19
by (bt.induct_tac "t" 1);
wenzelm@4089
    20
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
lcp@1167
    21
qed "n_nodes_reflect";
lcp@1167
    22
lcp@1167
    23
(*The famous relationship between the numbers of leaves and nodes*)
lcp@1167
    24
goal BT.thy "n_leaves(t) = Suc(n_nodes(t))";
lcp@1167
    25
by (bt.induct_tac "t" 1);
clasohm@1266
    26
by (ALLGOALS Asm_simp_tac);
lcp@1167
    27
qed "n_leaves_nodes";
lcp@1167
    28
lcp@1167
    29
goal BT.thy "reflect(reflect(t))=t";
lcp@1167
    30
by (bt.induct_tac "t" 1);
clasohm@1266
    31
by (ALLGOALS Asm_simp_tac);
lcp@1167
    32
qed "reflect_reflect_ident";
lcp@1167
    33
lcp@1167
    34
goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)";
lcp@1167
    35
by (bt.induct_tac "t" 1);
clasohm@1266
    36
by (ALLGOALS Asm_simp_tac);
lcp@1167
    37
qed "bt_map_reflect";
lcp@1167
    38
lcp@1167
    39
goal BT.thy "inorder (bt_map f t) = map f (inorder t)";
lcp@1167
    40
by (bt.induct_tac "t" 1);
clasohm@1266
    41
by (ALLGOALS Asm_simp_tac);
lcp@1167
    42
qed "inorder_bt_map";
lcp@1167
    43
lcp@1167
    44
goal BT.thy "preorder (reflect t) = rev (postorder t)";
lcp@1167
    45
by (bt.induct_tac "t" 1);
clasohm@1266
    46
by (ALLGOALS Asm_simp_tac);
lcp@1167
    47
qed "preorder_reflect";
lcp@1167
    48
lcp@1167
    49
goal BT.thy "inorder (reflect t) = rev (inorder t)";
lcp@1167
    50
by (bt.induct_tac "t" 1);
clasohm@1266
    51
by (ALLGOALS Asm_simp_tac);
lcp@1167
    52
qed "inorder_reflect";
lcp@1167
    53
lcp@1167
    54
goal BT.thy "postorder (reflect t) = rev (preorder t)";
lcp@1167
    55
by (bt.induct_tac "t" 1);
clasohm@1266
    56
by (ALLGOALS Asm_simp_tac);
lcp@1167
    57
qed "postorder_reflect";
lcp@1167
    58
lcp@1167
    59