1(* Author: Tobias Nipkow *)
2
3section \<open>Unbalanced Tree Implementation of Map\<close>
4
5theory Tree_Map
6imports
7  Tree_Set
8  Map_Specs
9begin
10
11fun lookup :: "('a::linorder*'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
16fun update :: "'a::linorder \<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
23fun delete :: "'a::linorder \<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') = split_min r in Node l ab' r')"
29
30
31subsection "Functional Correctness Proofs"
32
33lemma lookup_map_of:
34  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
35by (induction t) (auto simp: map_of_simps split: option.split)
36
37lemma inorder_update:
38  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
39by(induction t) (auto simp: upd_list_simps)
40
41lemma inorder_delete:
42  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
43by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
44
45interpretation M: Map_by_Ordered
46where empty = empty and lookup = lookup and update = update and delete = delete
47and inorder = inorder and inv = "\<lambda>_. True"
48proof (standard, goal_cases)
49  case 1 show ?case by (simp add: empty_def)
50next
51  case 2 thus ?case by(simp add: lookup_map_of)
52next
53  case 3 thus ?case by(simp add: inorder_update)
54next
55  case 4 thus ?case by(simp add: inorder_delete)
56qed auto
57
58end
59