Quelle  Isin2.thy   Sprache: Isabelle

(* Author: Tobias Nipkow *)

section ‹Function \textit{isin} for Tree2›

theory Isin2
imports
  Tree2
  Cmp
  Set_Specs
begin

fun isin :: "('a::linorder*'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 isin_set_inorder: "sorted(inorder t) \ isin t x = (x \ set(inorder t))"
by (induction t rule: tree2_induct) (auto simp: isin_simps)

lemma isin_set_tree: "bst t \ isin t x \ x \ set_tree t"
by(induction t rule: tree2_induct) auto

end