57250

1 
(* Author: Tobias Nipkow *)


2 


3 
header {* Binary Tree *}


4 


5 
theory Tree


6 
imports Main


7 
begin


8 


9 
datatype 'a tree = Leaf  Node "'a tree" 'a "'a tree"


10 


11 
fun set_tree :: "'a tree \<Rightarrow> 'a set" where


12 
"set_tree Leaf = {}" 


13 
"set_tree (Node l x r) = insert x (set_tree l \<union> set_tree r)"


14 


15 
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where


16 
"subtrees Leaf = {Leaf}" 


17 
"subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)"


18 


19 
fun inorder :: "'a tree \<Rightarrow> 'a list" where


20 
"inorder Leaf = []" 


21 
"inorder (Node l x r) = inorder l @ [x] @ inorder r"


22 


23 
text{* Binary Search Tree predicate: *}


24 
fun bst :: "'a::linorder tree \<Rightarrow> bool" where


25 
"bst Leaf = True" 


26 
"bst (Node l a r) =


27 
(bst l & bst r & (\<forall>x \<in> set_tree l. x < a) & (\<forall>x \<in> set_tree r. a < x))"


28 


29 
lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)"


30 
by (cases t) auto


31 


32 
lemma set_inorder[simp]: "set(inorder t) = set_tree t"


33 
by (induction t) auto


34 


35 
lemma set_treeE: "a : set_tree t \<Longrightarrow> \<exists>l r. Node l a r \<in> subtrees t"


36 
by(induction t)(auto)


37 


38 
lemma Node_notin_subtrees_if[simp]:


39 
"a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t"


40 
by (induction t) auto


41 


42 
lemma in_set_tree_if:


43 
"Node l a r \<in> subtrees t \<Longrightarrow> a \<in> set_tree t"


44 
by (metis Node_notin_subtrees_if)


45 


46 
end
