author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 70755 | 3fb16bed5d6c |
permissions | -rw-r--r-- |
61232 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section \<open>Function \textit{lookup} for Tree2\<close> |
|
4 |
||
5 |
theory Lookup2 |
|
6 |
imports |
|
7 |
Tree2 |
|
61693 | 8 |
Cmp |
67965 | 9 |
Map_Specs |
61232 | 10 |
begin |
11 |
||
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
12 |
fun lookup :: "(('a::linorder * 'b) * 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
61232 | 13 |
"lookup Leaf x = None" | |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
14 |
"lookup (Node l ((a,b), _) r) x = |
61693 | 15 |
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)" |
61232 | 16 |
|
61790 | 17 |
lemma lookup_map_of: |
18 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68413
diff
changeset
|
19 |
by(induction t rule: tree2_induct) (auto simp: map_of_simps split: option.split) |
61232 | 20 |
|
62390 | 21 |
end |