section \<open>Function \textit{isin} for Tree2\<close>
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 \<Rightarrow> isin l x |
EQ \<Rightarrow> True |
GT \<Rightarrow> 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
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
