isabelle: src/ZF/ex/BT.thy@20c42415c07d (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/ex/BT.thy
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	4	Copyright 1992 University of Cambridge
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	5
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	6	Binary trees
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	7	*)
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	8
6112 5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	9	BT = Main +
5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	10	consts
5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	11	bt :: i=>i
5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	12
5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	13	datatype
5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	14	"bt(A)" = Lf \| Br ("a: A", "t1: bt(A)", "t2: bt(A)")
5e4871c5136b datatype package improvements paulson parents: 6046 diff changeset	15
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	16	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	17	n_nodes :: i=>i
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	18	n_leaves :: i=>i
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	19	bt_reflect :: i=>i
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	20
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	21	primrec
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	22	"n_nodes(Lf) = 0"
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	23	"n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	24
6046 2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	25	primrec
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	26	"n_leaves(Lf) = 1"
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	27	"n_leaves(Br(a,l,r)) = n_leaves(l) #+ n_leaves(r)"
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	28
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	29	primrec
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	30	"bt_reflect(Lf) = Lf"
2c8a8be36c94 converted to use new primrec section paulson parents: 3840 diff changeset	31	"bt_reflect(Br(a,l,r)) = Br(a, bt_reflect(r), bt_reflect(l))"
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	32
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	33	end

author	wenzelm
	Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717	20c42415c07d
parent 6112	5e4871c5136b
child 11316	b4e71bd751e4
permissions	-rw-r--r--