|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 section "AVL Tree Implementation of Maps" |
|
4 |
|
5 theory AVL_Map |
|
6 imports |
|
7 AVL_Set |
|
8 Lookup2 |
|
9 begin |
|
10 |
|
11 fun update :: "'a::order \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
|
12 "update x y Leaf = Node 1 Leaf (x,y) Leaf" | |
|
13 "update x y (Node h l (a,b) r) = |
|
14 (if x = a then Node h l (x,y) r else |
|
15 if x < a then node_bal_l (update x y l) (a,b) r |
|
16 else node_bal_r l (a,b) (update x y r))" |
|
17 |
|
18 fun delete :: "'a::order \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where |
|
19 "delete _ Leaf = Leaf" | |
|
20 "delete x (Node h l (a,b) r) = ( |
|
21 if x = a then delete_root (Node h l (a,b) r) else |
|
22 if x < a then node_bal_r (delete x l) (a,b) r |
|
23 else node_bal_l l (a,b) (delete x r))" |
|
24 |
|
25 |
|
26 subsection {* Functional Correctness Proofs *} |
|
27 |
|
28 theorem inorder_update: |
|
29 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
|
30 by (induct t) |
|
31 (auto simp: upd_list_simps inorder_node_bal_l inorder_node_bal_r) |
|
32 |
|
33 |
|
34 theorem inorder_delete: |
|
35 "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
|
36 by(induction t) |
|
37 (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r |
|
38 inorder_delete_root inorder_delete_maxD split: prod.splits) |
|
39 |
|
40 |
|
41 interpretation Map_by_Ordered |
|
42 where empty = Leaf and lookup = lookup and update = update and delete = delete |
|
43 and inorder = inorder and wf = "\<lambda>_. True" |
|
44 proof (standard, goal_cases) |
|
45 case 1 show ?case by simp |
|
46 next |
|
47 case 2 thus ?case by(simp add: lookup_eq) |
|
48 next |
|
49 case 3 thus ?case by(simp add: inorder_update) |
|
50 next |
|
51 case 4 thus ?case by(simp add: inorder_delete) |
|
52 qed (rule TrueI)+ |
|
53 |
|
54 end |