Theory Isin2

(* Author: Tobias Nipkow *)

section ‹Function \textit{isin} for Tree2›

theory Isin2
imports
  Tree2
  Cmp
  Set_by_Ordered
begin

fun isin :: "('a::cmp,'b) tree ⇒ 'a ⇒ bool" where
"isin Leaf x = False" |
"isin (Node _ l a r) x =
  (case cmp x a of
     LT ⇒ isin l x |
     EQ ⇒ True |
     GT ⇒ isin r x)"

lemma "sorted(inorder t) ⟹ isin t x = (x ∈ elems(inorder t))"
by (induction t) (auto simp: elems_simps1)

lemma isin_set: "sorted(inorder t) ⟹ isin t x = (x ∈ elems(inorder t))"
by (induction t) (auto simp: elems_simps2)

end