isabelle: src/HOL/ex/BT.thy@92f83b9d17e1 (annotated)

1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	1	(* Title: HOL/ex/BT.thy
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	2	ID: $Id$
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
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
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	9	BT = List +
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	10
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	11	datatype 'a bt = Lf \| Br 'a ('a bt) ('a bt)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	12
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	13	consts
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	14	n_nodes :: 'a bt => nat
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	15	n_leaves :: 'a bt => nat
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	16	reflect :: 'a bt => 'a bt
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	17	bt_map :: ('a=>'b) => ('a bt => 'b bt)
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	18	preorder :: 'a bt => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	19	inorder :: 'a bt => 'a list
92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1167 diff changeset	20	postorder :: 'a bt => 'a list
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	21
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	22	primrec n_nodes bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	23	n_nodes_Lf "n_nodes (Lf) = 0"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	24	n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	25
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	26	primrec n_leaves bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	27	n_leaves_Lf "n_leaves (Lf) = Suc 0"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	28	n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	29
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	30	primrec reflect bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	31	reflect_Lf "reflect (Lf) = Lf"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	32	reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	33
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	34	primrec bt_map bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	35	bt_map_Lf "bt_map f Lf = Lf"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	36	bt_map_Br "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	37
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	38	primrec preorder bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	39	preorder_Lf "preorder (Lf) = []"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	40	preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	41
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	42	primrec inorder bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	43	inorder_Lf "inorder (Lf) = []"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	44	inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	45
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	46	primrec postorder bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	47	postorder_Lf "postorder (Lf) = []"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	48	postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	49
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	50	end

author	clasohm
	Fri, 01 Dec 1995 12:03:13 +0100
changeset 1376	92f83b9d17e1
parent 1167	cbd32a0f2f41
child 1476	608483c2122a
permissions	-rw-r--r--