src/HOL/ex/BT.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 1896 df4e40b9ff6d
child 5184 9b8547a9496a
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/BT.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 
     6 Binary trees (based on the ZF version)
     7 *)
     8 
     9 BT = List +
    10 
    11 datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
    12   
    13 consts
    14     n_nodes     :: 'a bt => nat
    15     n_leaves    :: 'a bt => nat
    16     reflect     :: 'a bt => 'a bt
    17     bt_map      :: ('a=>'b) => ('a bt => 'b bt)
    18     preorder    :: 'a bt => 'a list
    19     inorder     :: 'a bt => 'a list
    20     postorder   :: 'a bt => 'a list
    21 
    22 primrec n_nodes bt
    23   "n_nodes (Lf) = 0"
    24   "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
    25 
    26 primrec n_leaves bt
    27   "n_leaves (Lf) = Suc 0"
    28   "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
    29 
    30 primrec reflect bt
    31   "reflect (Lf) = Lf"
    32   "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
    33 
    34 primrec bt_map bt
    35   "bt_map f Lf = Lf"
    36   "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
    37 
    38 primrec preorder bt
    39   "preorder (Lf) = []"
    40   "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
    41 
    42 primrec inorder bt
    43   "inorder (Lf) = []"
    44   "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
    45 
    46 primrec postorder bt
    47   "postorder (Lf) = []"
    48   "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
    49 
    50 end
    51