isabelle: src/HOL/ex/BT.thy@6ed42bcba707 (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	1	(* Title: HOL/ex/BT.thy
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	5
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	6	Binary trees (based on the ZF version)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	7	*)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	8
8339 bcadeb9c7095 tidied paulson parents: 5184 diff changeset	9	BT = Main +
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	10
8339 bcadeb9c7095 tidied paulson parents: 5184 diff changeset	11	datatype 'a bt = Lf
bcadeb9c7095 tidied paulson parents: 5184 diff changeset	12	\| Br 'a ('a bt) ('a bt)
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	13
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	14	consts
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	15	n_nodes :: 'a bt => nat
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	16	n_leaves :: 'a bt => nat
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	17	reflect :: 'a bt => 'a bt
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	18	bt_map :: ('a=>'b) => ('a bt => 'b bt)
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	19	preorder :: 'a bt => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	20	inorder :: 'a bt => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	21	postorder :: 'a bt => 'a list
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	22
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	23	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	24	"n_nodes (Lf) = 0"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	25	"n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	26
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	27	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	28	"n_leaves (Lf) = Suc 0"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	29	"n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	30
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	31	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	32	"reflect (Lf) = Lf"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	33	"reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	34
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	35	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	36	"bt_map f Lf = Lf"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	37	"bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	38
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	39	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	40	"preorder (Lf) = []"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	41	"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	42
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	43	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	44	"inorder (Lf) = []"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	45	"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	46
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 1896 diff changeset	47	primrec
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	48	"postorder (Lf) = []"
df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	49	"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	50
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	51	end
1896 df4e40b9ff6d Simplified primrec - definitions. berghofe parents: 1476 diff changeset	52

author	paulson
	Thu, 14 Sep 2000 11:34:13 +0200
changeset 9955	6ed42bcba707
parent 8339	bcadeb9c7095
child 11024	23bf8d787b04
permissions	-rw-r--r--