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