src/HOL/Data_Structures/Isin2.thy
author haftmann
Sat, 11 Nov 2017 18:41:08 +0000
changeset 67051 e7e54a0b9197
parent 63411 e051eea34990
child 67929 30486b96274d
permissions -rw-r--r--
dedicated definition for coprimality

(* Author: Tobias Nipkow *)

section \<open>Function \textit{isin} for Tree2\<close>

theory Isin2
imports
  Tree2
  Cmp
  Set_by_Ordered
begin

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

lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
by (induction t) (auto simp: elems_simps1)

lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
by (induction t) (auto simp: elems_simps2)

end