isabelle: src/HOL/ex/BT.ML@f886dbd91ee5 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	1	(* Title: HOL/ex/BT.ML
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 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	Datatype definition of binary trees
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	open BT;
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	( BT simplification )
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	goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	14	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	15	by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_commute])));
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	16	qed "n_leaves_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	17
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	18	goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	19	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	20	by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_commute])));
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	21	qed "n_nodes_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	22
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	23	(The famous relationship between the numbers of leaves and nodes)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	24	goal BT.thy "n_leaves(t) = Suc(n_nodes(t))";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	25	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	26	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	27	qed "n_leaves_nodes";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	28
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	29	goal BT.thy "reflect(reflect(t))=t";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	30	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	31	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	32	qed "reflect_reflect_ident";
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	goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	35	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	36	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	37	qed "bt_map_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	38
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	39	goal BT.thy "inorder (bt_map f t) = map f (inorder t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	40	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	41	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	42	qed "inorder_bt_map";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	43
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	44	goal BT.thy "preorder (reflect t) = rev (postorder t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	45	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	46	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	47	qed "preorder_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	48
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	49	goal BT.thy "inorder (reflect t) = rev (inorder t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	50	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	51	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	52	qed "inorder_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	53
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	54	goal BT.thy "postorder (reflect t) = rev (preorder t)";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	55	by (bt.induct_tac "t" 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1167 diff changeset	56	by (ALLGOALS Asm_simp_tac);
1167 cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	57	qed "postorder_reflect";
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	58
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially lcp parents: diff changeset	59

author	paulson
	Wed, 23 Jul 1997 11:52:22 +0200
changeset 3564	f886dbd91ee5
parent 1465	5d7a7e439cec
child 4089	96fba19bcbe2
permissions	-rw-r--r--