61224

1 
theory Tree2


2 
imports Main


3 
begin


4 


5 
datatype ('a,'b) tree =


6 
Leaf ("\<langle>\<rangle>") 

68413

7 
Node "('a,'b)tree" 'a 'b "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")

61224

8 


9 
fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where


10 
"inorder Leaf = []" 

68413

11 
"inorder (Node l a _ r) = inorder l @ a # inorder r"

61224

12 


13 
fun height :: "('a,'b) tree \<Rightarrow> nat" where


14 
"height Leaf = 0" 

68413

15 
"height (Node l a _ r) = max (height l) (height r) + 1"

61224

16 

67967

17 
fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where


18 
"set_tree Leaf = {}" 

68413

19 
"set_tree (Node l a _ r) = Set.insert a (set_tree l \<union> set_tree r)"

67967

20 


21 
fun bst :: "('a::linorder,'b) tree \<Rightarrow> bool" where


22 
"bst Leaf = True" 

68413

23 
"bst (Node l a _ r) = (bst l \<and> bst r \<and> (\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x))"

67967

24 

68998

25 
fun size1 :: "('a,'b) tree \<Rightarrow> nat" where


26 
"size1 \<langle>\<rangle> = 1" 


27 
"size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r"

62650

28 

70742

29 
fun complete :: "('a,'b) tree \<Rightarrow> bool" where


30 
"complete Leaf = True" 


31 
"complete (Node l _ _ r) = (complete l \<and> complete r \<and> height l = height r)"


32 

68998

33 
lemma size1_size: "size1 t = size t + 1"


34 
by (induction t) simp_all

62650

35 


36 
lemma size1_ge0[simp]: "0 < size1 t"

68998

37 
by (simp add: size1_size)

62650

38 

68411

39 
lemma finite_set_tree[simp]: "finite(set_tree t)"


40 
by(induction t) auto


41 

70745

42 
lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"

70744

43 
by (cases t) auto


44 

62390

45 
end
