src/HOL/ex/BT.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8339 bcadeb9c7095
child 11024 23bf8d787b04
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
     1
(*  Title:      HOL/ex/BT.thy
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
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
Binary trees (based on the ZF version)
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
8339
paulson
parents: 5184
diff changeset
     9
BT = Main +
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    10
8339
paulson
parents: 5184
diff changeset
    11
datatype 'a bt = Lf
paulson
parents: 5184
diff changeset
    12
               | Br 'a ('a bt) ('a bt)
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    13
  
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    14
consts
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    15
    n_nodes     :: 'a bt => nat
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    16
    n_leaves    :: 'a bt => nat
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
    17
    reflect     :: 'a bt => 'a bt
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1167
diff changeset
    18
    bt_map      :: ('a=>'b) => ('a bt => 'b bt)
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1167
diff changeset
    19
    preorder    :: 'a bt => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1167
diff changeset
    20
    inorder     :: 'a bt => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 1167
diff changeset
    21
    postorder   :: 'a bt => 'a list
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    22
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    23
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    24
  "n_nodes (Lf) = 0"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    25
  "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    26
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    27
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    28
  "n_leaves (Lf) = Suc 0"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    29
  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    30
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    31
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    32
  "reflect (Lf) = Lf"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    33
  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    34
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    35
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    36
  "bt_map f Lf = Lf"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    37
  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    38
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    39
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    40
  "preorder (Lf) = []"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    41
  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    42
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    43
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    44
  "inorder (Lf) = []"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    45
  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    46
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 1896
diff changeset
    47
primrec
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    48
  "postorder (Lf) = []"
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    49
  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    50
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    51
end
1896
df4e40b9ff6d Simplified primrec - definitions.
berghofe
parents: 1476
diff changeset
    52