src/ZF/ex/BT.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 1171 e4d6b42be73a
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
lcp@1171
     1
(*  Title: 	ZF/ex/BT.thy
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1992  University of Cambridge
lcp@515
     5
lcp@515
     6
Binary trees
lcp@515
     7
*)
lcp@515
     8
lcp@935
     9
BT = Datatype +
lcp@515
    10
consts
clasohm@1401
    11
    bt_rec    	:: [i, i, [i,i,i,i,i]=>i] => i
clasohm@1401
    12
    n_nodes	:: i=>i
clasohm@1401
    13
    n_leaves   	:: i=>i
clasohm@1401
    14
    bt_reflect 	:: i=>i
lcp@515
    15
clasohm@1401
    16
    bt 	        :: i=>i
lcp@515
    17
lcp@515
    18
datatype
lcp@515
    19
  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
lcp@515
    20
  
lcp@753
    21
defs
lcp@515
    22
  bt_rec_def
lcp@515
    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))"
lcp@515
    24
lcp@515
    25
  n_nodes_def	"n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
lcp@515
    26
  n_leaves_def	"n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
lcp@515
    27
  bt_reflect_def "bt_reflect(t) == bt_rec(t,  Lf,  %x y z r s. Br(x,s,r))"
lcp@515
    28
lcp@515
    29
end