src/HOL/Data_Structures/Isin2.thy
author nipkow
Thu Jul 07 18:08:02 2016 +0200 (2016-07-07)
changeset 63411 e051eea34990
parent 62390 842917225d56
child 67929 30486b96274d
permissions -rw-r--r--
got rid of class cmp; added height-size proofs by Daniel Stuewe
     1 (* Author: Tobias Nipkow *)
     2 
     3 section \<open>Function \textit{isin} for Tree2\<close>
     4 
     5 theory Isin2
     6 imports
     7   Tree2
     8   Cmp
     9   Set_by_Ordered
    10 begin
    11 
    12 fun isin :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> bool" where
    13 "isin Leaf x = False" |
    14 "isin (Node _ l a r) x =
    15   (case cmp x a of
    16      LT \<Rightarrow> isin l x |
    17      EQ \<Rightarrow> True |
    18      GT \<Rightarrow> isin r x)"
    19 
    20 lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
    21 by (induction t) (auto simp: elems_simps1)
    22 
    23 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
    24 by (induction t) (auto simp: elems_simps2)
    25 
    26 end