1(* Author: Tobias Nipkow *) 2 3section \<open>1-2 Brother Tree Implementation of Maps\<close> 4 5theory Brother12_Map 6imports 7 Brother12_Set 8 Map_Specs 9begin 10 11fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where 12"lookup N0 x = None" | 13"lookup (N1 t) x = lookup t x" | 14"lookup (N2 l (a,b) r) x = 15 (case cmp x a of 16 LT \<Rightarrow> lookup l x | 17 EQ \<Rightarrow> Some b | 18 GT \<Rightarrow> lookup r x)" 19 20locale update = insert 21begin 22 23fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where 24"upd x y N0 = L2 (x,y)" | 25"upd x y (N1 t) = n1 (upd x y t)" | 26"upd x y (N2 l (a,b) r) = 27 (case cmp x a of 28 LT \<Rightarrow> n2 (upd x y l) (a,b) r | 29 EQ \<Rightarrow> N2 l (a,y) r | 30 GT \<Rightarrow> n2 l (a,b) (upd x y r))" 31 32definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where 33"update x y t = tree(upd x y t)" 34 35end 36 37context delete 38begin 39 40fun del :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where 41"del _ N0 = N0" | 42"del x (N1 t) = N1 (del x t)" | 43"del x (N2 l (a,b) r) = 44 (case cmp x a of 45 LT \<Rightarrow> n2 (del x l) (a,b) r | 46 GT \<Rightarrow> n2 l (a,b) (del x r) | 47 EQ \<Rightarrow> (case split_min r of 48 None \<Rightarrow> N1 l | 49 Some (ab, r') \<Rightarrow> n2 l ab r'))" 50 51definition delete :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where 52"delete a t = tree (del a t)" 53 54end 55 56subsection "Functional Correctness Proofs" 57 58subsubsection "Proofs for lookup" 59 60lemma lookup_map_of: "t \<in> T h \<Longrightarrow> 61 sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" 62by(induction h arbitrary: t) (auto simp: map_of_simps split: option.splits) 63 64subsubsection "Proofs for update" 65 66context update 67begin 68 69lemma inorder_upd: "t \<in> T h \<Longrightarrow> 70 sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)" 71by(induction h arbitrary: t) (auto simp: upd_list_simps inorder_n1 inorder_n2) 72 73lemma inorder_update: "t \<in> T h \<Longrightarrow> 74 sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" 75by(simp add: update_def inorder_upd inorder_tree) 76 77end 78 79subsubsection \<open>Proofs for deletion\<close> 80 81context delete 82begin 83 84lemma inorder_del: 85 "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" 86by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2 87 inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits) 88 89lemma inorder_delete: 90 "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" 91by(simp add: delete_def inorder_del inorder_tree) 92 93end 94 95 96subsection \<open>Invariant Proofs\<close> 97 98subsubsection \<open>Proofs for update\<close> 99 100context update 101begin 102 103lemma upd_type: 104 "(t \<in> B h \<longrightarrow> upd x y t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> upd x y t \<in> T h)" 105apply(induction h arbitrary: t) 106 apply (simp) 107apply (fastforce simp: Bp_if_B n2_type dest: n1_type) 108done 109 110lemma update_type: 111 "t \<in> B h \<Longrightarrow> update x y t \<in> B h \<union> B (Suc h)" 112unfolding update_def by (metis upd_type tree_type) 113 114end 115 116subsubsection "Proofs for deletion" 117 118context delete 119begin 120 121lemma del_type: 122 "t \<in> B h \<Longrightarrow> del x t \<in> T h" 123 "t \<in> U h \<Longrightarrow> del x t \<in> Um h" 124proof (induction h arbitrary: x t) 125 case (Suc h) 126 { case 1 127 then obtain l a b r where [simp]: "t = N2 l (a,b) r" and 128 lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto 129 have ?case if "x < a" 130 proof cases 131 assume "l \<in> B h" 132 from n2_type3[OF Suc.IH(1)[OF this] lr(2)] 133 show ?thesis using \<open>x<a\<close> by(simp) 134 next 135 assume "l \<notin> B h" 136 hence "l \<in> U h" "r \<in> B h" using lr by auto 137 from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)] 138 show ?thesis using \<open>x<a\<close> by(simp) 139 qed 140 moreover 141 have ?case if "x > a" 142 proof cases 143 assume "r \<in> B h" 144 from n2_type3[OF lr(1) Suc.IH(1)[OF this]] 145 show ?thesis using \<open>x>a\<close> by(simp) 146 next 147 assume "r \<notin> B h" 148 hence "l \<in> B h" "r \<in> U h" using lr by auto 149 from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]] 150 show ?thesis using \<open>x>a\<close> by(simp) 151 qed 152 moreover 153 have ?case if [simp]: "x=a" 154 proof (cases "split_min r") 155 case None 156 show ?thesis 157 proof cases 158 assume "r \<in> B h" 159 with split_minNoneN0[OF this None] lr show ?thesis by(simp) 160 next 161 assume "r \<notin> B h" 162 hence "r \<in> U h" using lr by auto 163 with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp) 164 qed 165 next 166 case [simp]: (Some br') 167 obtain b r' where [simp]: "br' = (b,r')" by fastforce 168 show ?thesis 169 proof cases 170 assume "r \<in> B h" 171 from split_min_type(1)[OF this] n2_type3[OF lr(1)] 172 show ?thesis by simp 173 next 174 assume "r \<notin> B h" 175 hence "l \<in> B h" and "r \<in> U h" using lr by auto 176 from split_min_type(2)[OF this(2)] n2_type2[OF this(1)] 177 show ?thesis by simp 178 qed 179 qed 180 ultimately show ?case by auto 181 } 182 { case 2 with Suc.IH(1) show ?case by auto } 183qed auto 184 185lemma delete_type: 186 "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)" 187unfolding delete_def 188by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1) 189 190end 191 192subsection "Overall correctness" 193 194interpretation Map_by_Ordered 195where empty = empty and lookup = lookup and update = update.update 196and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h" 197proof (standard, goal_cases) 198 case 2 thus ?case by(auto intro!: lookup_map_of) 199next 200 case 3 thus ?case by(auto intro!: update.inorder_update) 201next 202 case 4 thus ?case by(auto intro!: delete.inorder_delete) 203next 204 case 6 thus ?case using update.update_type by (metis Un_iff) 205next 206 case 7 thus ?case using delete.delete_type by blast 207qed (auto simp: empty_def) 208 209end 210