src/ZF/ex/BT_Fn.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 0 a5a9c433f639
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/bt-fn.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_Fn = BT +
    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 rules
    17   bt_rec_def
    18     "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
    19 
    20   n_nodes_def	"n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
    21   n_leaves_def	"n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
    22   bt_reflect_def "bt_reflect(t) == bt_rec(t,  Lf,  %x y z r s. Br(x,s,r))"
    23 
    24 end