61640
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section {* Unbalanced Tree as Map *}
|
|
4 |
|
|
5 |
theory Tree_Map
|
|
6 |
imports
|
|
7 |
Tree_Set
|
|
8 |
Map_by_Ordered
|
|
9 |
begin
|
|
10 |
|
|
11 |
fun lookup :: "('a::cmp*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
|
|
12 |
"lookup Leaf x = None" |
|
|
13 |
"lookup (Node l (a,b) r) x =
|
|
14 |
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"
|
|
15 |
|
|
16 |
fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
|
|
17 |
"update x y Leaf = Node Leaf (x,y) Leaf" |
|
|
18 |
"update x y (Node l (a,b) r) = (case cmp x a of
|
|
19 |
LT \<Rightarrow> Node (update x y l) (a,b) r |
|
|
20 |
EQ \<Rightarrow> Node l (x,y) r |
|
|
21 |
GT \<Rightarrow> Node l (a,b) (update x y r))"
|
|
22 |
|
|
23 |
fun delete :: "'a::cmp \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
|
|
24 |
"delete x Leaf = Leaf" |
|
|
25 |
"delete x (Node l (a,b) r) = (case cmp x a of
|
|
26 |
LT \<Rightarrow> Node (delete x l) (a,b) r |
|
|
27 |
GT \<Rightarrow> Node l (a,b) (delete x r) |
|
|
28 |
EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
|
|
29 |
|
|
30 |
|
|
31 |
subsection "Functional Correctness Proofs"
|
|
32 |
|
|
33 |
lemma lookup_eq:
|
|
34 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
|
|
35 |
by (induction t) (auto simp: map_of_simps split: option.split)
|
|
36 |
|
|
37 |
|
|
38 |
lemma inorder_update:
|
|
39 |
"sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
|
|
40 |
by(induction t) (auto simp: upd_list_simps)
|
|
41 |
|
|
42 |
|
|
43 |
lemma del_minD:
|
|
44 |
"del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
|
|
45 |
x # inorder t' = inorder t"
|
|
46 |
by(induction t arbitrary: t' rule: del_min.induct)
|
61647
|
47 |
(auto simp: del_list_simps split: prod.splits if_splits)
|
61640
|
48 |
|
|
49 |
lemma inorder_delete:
|
|
50 |
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
|
|
51 |
by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
|
|
52 |
|
|
53 |
interpretation Map_by_Ordered
|
|
54 |
where empty = Leaf and lookup = lookup and update = update and delete = delete
|
|
55 |
and inorder = inorder and wf = "\<lambda>_. True"
|
|
56 |
proof (standard, goal_cases)
|
|
57 |
case 1 show ?case by simp
|
|
58 |
next
|
|
59 |
case 2 thus ?case by(simp add: lookup_eq)
|
|
60 |
next
|
|
61 |
case 3 thus ?case by(simp add: inorder_update)
|
|
62 |
next
|
|
63 |
case 4 thus ?case by(simp add: inorder_delete)
|
|
64 |
qed (rule TrueI)+
|
|
65 |
|
|
66 |
end
|