# HG changeset patch # User nipkow # Date 1402601008 -7200 # Node ID cddaf5b93728622de110a712631fa040fab2dadc # Parent 5c75baf68b774ed8104dc7f3e984ad6c510f137f new theory of binary trees diff -r 5c75baf68b77 -r cddaf5b93728 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Jun 12 18:02:39 2014 +0200 +++ b/src/HOL/Library/Library.thy Thu Jun 12 21:23:28 2014 +0200 @@ -64,6 +64,7 @@ Sublist Sum_of_Squares Transitive_Closure_Table + Tree While_Combinator begin end diff -r 5c75baf68b77 -r cddaf5b93728 src/HOL/Library/Tree.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Tree.thy Thu Jun 12 21:23:28 2014 +0200 @@ -0,0 +1,46 @@ +(* Author: Tobias Nipkow *) + +header {* Binary Tree *} + +theory Tree +imports Main +begin + +datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree" + +fun set_tree :: "'a tree \ 'a set" where +"set_tree Leaf = {}" | +"set_tree (Node l x r) = insert x (set_tree l \ set_tree r)" + +fun subtrees :: "'a tree \ 'a tree set" where +"subtrees Leaf = {Leaf}" | +"subtrees (Node l a r) = insert (Node l a r) (subtrees l \ subtrees r)" + +fun inorder :: "'a tree \ 'a list" where +"inorder Leaf = []" | +"inorder (Node l x r) = inorder l @ [x] @ inorder r" + +text{* Binary Search Tree predicate: *} +fun bst :: "'a::linorder tree \ bool" where +"bst Leaf = True" | +"bst (Node l a r) = + (bst l & bst r & (\x \ set_tree l. x < a) & (\x \ set_tree r. a < x))" + +lemma neq_Leaf_iff: "(t \ Leaf) = (\l a r. t = Node l a r)" +by (cases t) auto + +lemma set_inorder[simp]: "set(inorder t) = set_tree t" +by (induction t) auto + +lemma set_treeE: "a : set_tree t \ \l r. Node l a r \ subtrees t" +by(induction t)(auto) + +lemma Node_notin_subtrees_if[simp]: + "a \ set_tree t \ Node l a r \ subtrees t" +by (induction t) auto + +lemma in_set_tree_if: + "Node l a r \ subtrees t \ a \ set_tree t" +by (metis Node_notin_subtrees_if) + +end