datatype 'a bst = Leaf | Node "'a bst" 'a "'a bst"

fun heights :: "'a bst ⇒ nat list" where
  "heights Leaf = [0]"
| "heights (Node a _ b) = map (λx. x + 1) (heights a) @ map (λx. x + 1) (heights b)"

definition maximum :: "nat list ⇒ nat" where
  "maximum xs ≡ foldl max 0 xs"

definition complete :: "'a bst ⇒ bool" where
  "complete t ≡ (∃n. set (heights t) = { n, Suc n }) ∨ (∃n. set (heights t) = { n })"

lemma height_log: "complete t ⟹ ceil (log2 (size t)) = maximum (heights t)"
  sorry

fun valid_bst :: "'a::linorder bst ⇒ bool" where
  "valid_bst Leaf = True"
| "valid_bst (Node l a r) ⟷ (∀x∈set_bst l. x < a) ∧ (∀x∈set_bst r. a < x) ∧ valid_bst l ∧ valid_bst r"

fun isin :: "'a::linorder ⇒ 'a bst ⇒ bool" where
  "isin _ Leaf = False"
| "isin x (Node l a r) = (if a = x then True else
    if x < a then isin x l else isin x r
  )"
fun isin_t :: "'a::linorder ⇒ 'a bst ⇒ nat" where
  "isin_t _ Leaf = 1"
| "isin_t x (Node l a r) = (if a = x then 1 else
    if x < a then 1 + isin_t x l else 1 + isin_t x r
  )"

lemma "⟦ complete t ; valid_bst t ⟧ ⟹ isin_t x t ≤ ceil (log2 (size t))"
  sorry