Theory Tree2

theory Tree2
imports Main
begin

datatype ('a,'b) tree =
  Leaf ("⟨⟩") |
  Node "('a,'b)tree" 'a 'b "('a,'b) tree" ("(1⟨_,/ _,/ _,/ _⟩)")

fun inorder :: "('a,'b)tree ⇒ 'a list" where
"inorder Leaf = []" |
"inorder (Node l a _ r) = inorder l @ a # inorder r"

fun height :: "('a,'b) tree ⇒ nat" where
"height Leaf = 0" |
"height (Node l a _ r) = max (height l) (height r) + 1"

fun set_tree :: "('a,'b) tree ⇒ 'a set" where
"set_tree Leaf = {}" |
"set_tree (Node l a _ r) = Set.insert a (set_tree l ∪ set_tree r)"

fun bst :: "('a::linorder,'b) 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))"

fun size1 :: "('a,'b) tree ⇒ nat" where
"size1 ⟨⟩ = 1" |
"size1 ⟨l, _, _, r⟩ = size1 l + size1 r"

lemma size1_size: "size1 t = size t + 1"
by (induction t) simp_all

lemma size1_ge0[simp]: "0 < size1 t"
by (simp add: size1_size)

lemma finite_set_tree[simp]: "finite(set_tree t)"
by(induction t) auto

end