equal
deleted
inserted
replaced
|
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 |