src/ZF/ex/BT.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/ex/BT.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Binary trees
     7 *)
     8 
     9 BT = Datatype +
    10 consts
    11     bt_rec      :: [i, i, [i,i,i,i,i]=>i] => i
    12     n_nodes     :: i=>i
    13     n_leaves    :: i=>i
    14     bt_reflect  :: i=>i
    15 
    16     bt          :: i=>i
    17 
    18 datatype
    19   "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
    20   
    21 defs
    22   bt_rec_def
    23     "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
    24 
    25   n_nodes_def   "n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
    26   n_leaves_def  "n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
    27   bt_reflect_def "bt_reflect(t) == bt_rec(t,  Lf,  %x y z r s. Br(x,s,r))"
    28 
    29 end