section \<open>Function \textit{lookup} for Tree2\<close>
theory Lookup2 imports
Tree2
Cmp
Map_Specs begin
fun lookup :: "(('a::linorder * 'b) * 'c) tree \ 'a \ 'b option" where "lookup Leaf x = None" | "lookup (Node l ((a,b), _) r) x =
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
lemma lookup_map_of: "sorted1(inorder t) \ lookup t x = map_of (inorder t) x" by(induction t rule: tree2_induct) (auto simp: map_of_simps split: option.split)
end
¤ 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.0.12Bemerkung:
(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.
Eigene Datei ansehen
Die farbliche Syntaxdarstellung ist noch experimentell.
