|
0
|
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
|