|
515
|
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 = Univ +
|
|
|
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 |
|
|
753
|
21 |
defs
|
|
515
|
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
|