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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1266
diff changeset
     1
(*  Title:      HOL/ex/BT.ML
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1266
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     5
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     6
Datatype definition of binary trees
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     7
*)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     8
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     9
(** BT simplification **)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    10
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    11
Goal "n_leaves(reflect(t)) = n_leaves(t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    12
by (induct_tac "t" 1);
8339
paulson
parents: 5227
diff changeset
    13
by Auto_tac;
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    14
qed "n_leaves_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    15
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    16
Goal "n_nodes(reflect(t)) = n_nodes(t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    17
by (induct_tac "t" 1);
8339
paulson
parents: 5227
diff changeset
    18
by Auto_tac;
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    19
qed "n_nodes_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    20
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    21
(*The famous relationship between the numbers of leaves and nodes*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    22
Goal "n_leaves(t) = Suc(n_nodes(t))";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    23
by (induct_tac "t" 1);
8339
paulson
parents: 5227
diff changeset
    24
by Auto_tac;
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    25
qed "n_leaves_nodes";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    26
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    27
Goal "reflect(reflect(t))=t";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    28
by (induct_tac "t" 1);
8339
paulson
parents: 5227
diff changeset
    29
by Auto_tac;
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    30
qed "reflect_reflect_ident";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    31
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    32
Goal "bt_map f (reflect t) = reflect (bt_map f t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    33
by (induct_tac "t" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1167
diff changeset
    34
by (ALLGOALS Asm_simp_tac);
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    35
qed "bt_map_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    36
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    37
Goal "inorder (bt_map f t) = map f (inorder t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    38
by (induct_tac "t" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1167
diff changeset
    39
by (ALLGOALS Asm_simp_tac);
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    40
qed "inorder_bt_map";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    41
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    42
Goal "preorder (reflect t) = rev (postorder t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    43
by (induct_tac "t" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1167
diff changeset
    44
by (ALLGOALS Asm_simp_tac);
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    45
qed "preorder_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    46
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    47
Goal "inorder (reflect t) = rev (inorder t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    48
by (induct_tac "t" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1167
diff changeset
    49
by (ALLGOALS Asm_simp_tac);
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    50
qed "inorder_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    51
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4089
diff changeset
    52
Goal "postorder (reflect t) = rev (preorder t)";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    53
by (induct_tac "t" 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1167
diff changeset
    54
by (ALLGOALS Asm_simp_tac);
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    55
qed "postorder_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    56
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    57