src/HOL/ex/BT.thy
author clasohm
Mon Feb 05 21:29:06 1996 +0100 (1996-02-05)
changeset 1476 608483c2122a
parent 1376 92f83b9d17e1
child 1896 df4e40b9ff6d
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
clasohm@1476
     1
(*  Title:      HOL/ex/BT.thy
lcp@1167
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@1167
     4
    Copyright   1995  University of Cambridge
lcp@1167
     5
lcp@1167
     6
Binary trees (based on the ZF version)
lcp@1167
     7
*)
lcp@1167
     8
lcp@1167
     9
BT = List +
lcp@1167
    10
lcp@1167
    11
datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
lcp@1167
    12
  
lcp@1167
    13
consts
clasohm@1476
    14
    n_nodes     :: 'a bt => nat
clasohm@1476
    15
    n_leaves    :: 'a bt => nat
clasohm@1476
    16
    reflect     :: 'a bt => 'a bt
clasohm@1376
    17
    bt_map      :: ('a=>'b) => ('a bt => 'b bt)
clasohm@1376
    18
    preorder    :: 'a bt => 'a list
clasohm@1376
    19
    inorder     :: 'a bt => 'a list
clasohm@1376
    20
    postorder   :: 'a bt => 'a list
lcp@1167
    21
lcp@1167
    22
primrec n_nodes bt
lcp@1167
    23
  n_nodes_Lf "n_nodes (Lf) = 0"
lcp@1167
    24
  n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
lcp@1167
    25
lcp@1167
    26
primrec n_leaves bt
lcp@1167
    27
  n_leaves_Lf "n_leaves (Lf) = Suc 0"
lcp@1167
    28
  n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
lcp@1167
    29
lcp@1167
    30
primrec reflect bt
lcp@1167
    31
  reflect_Lf "reflect (Lf) = Lf"
lcp@1167
    32
  reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
lcp@1167
    33
lcp@1167
    34
primrec bt_map bt
lcp@1167
    35
  bt_map_Lf  "bt_map f Lf = Lf"
lcp@1167
    36
  bt_map_Br  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
lcp@1167
    37
lcp@1167
    38
primrec preorder bt
lcp@1167
    39
  preorder_Lf "preorder (Lf) = []"
lcp@1167
    40
  preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
lcp@1167
    41
lcp@1167
    42
primrec inorder bt
lcp@1167
    43
  inorder_Lf "inorder (Lf) = []"
lcp@1167
    44
  inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
lcp@1167
    45
lcp@1167
    46
primrec postorder bt
lcp@1167
    47
  postorder_Lf "postorder (Lf) = []"
lcp@1167
    48
  postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
lcp@1167
    49
lcp@1167
    50
end