|
(* Author: Tobias Nipkow *)
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.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
