1theory Tree2 2imports Main 3begin 4 5datatype ('a,'b) tree = 6 Leaf ("\<langle>\<rangle>") | 7 Node "('a,'b)tree" 'a 'b "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)") 8 9fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where 10"inorder Leaf = []" | 11"inorder (Node l a _ r) = inorder l @ a # inorder r" 12 13fun height :: "('a,'b) tree \<Rightarrow> nat" where 14"height Leaf = 0" | 15"height (Node l a _ r) = max (height l) (height r) + 1" 16 17fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where 18"set_tree Leaf = {}" | 19"set_tree (Node l a _ r) = Set.insert a (set_tree l \<union> set_tree r)" 20 21fun bst :: "('a::linorder,'b) tree \<Rightarrow> bool" where 22"bst Leaf = True" | 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))" 24 25definition size1 :: "('a,'b) tree \<Rightarrow> nat" where 26"size1 t = size t + 1" 27 28lemma size1_simps[simp]: 29 "size1 \<langle>\<rangle> = 1" 30 "size1 \<langle>l, x, u, r\<rangle> = size1 l + size1 r" 31by (simp_all add: size1_def) 32 33lemma size1_ge0[simp]: "0 < size1 t" 34by (simp add: size1_def) 35 36lemma finite_set_tree[simp]: "finite(set_tree t)" 37by(induction t) auto 38 39end 40