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