1(* Author: Tobias Nipkow *) 2 3section \<open>Specifications of Map ADT\<close> 4 5theory Map_Specs 6imports AList_Upd_Del 7begin 8 9text \<open>The basic map interface with traditional \<open>set\<close>-based specification:\<close> 10 11locale Map = 12fixes empty :: "'m" 13fixes update :: "'a \<Rightarrow> 'b \<Rightarrow> 'm \<Rightarrow> 'm" 14fixes delete :: "'a \<Rightarrow> 'm \<Rightarrow> 'm" 15fixes lookup :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option" 16fixes invar :: "'m \<Rightarrow> bool" 17assumes map_empty: "lookup empty = (\<lambda>_. None)" 18and map_update: "invar m \<Longrightarrow> lookup(update a b m) = (lookup m)(a := Some b)" 19and map_delete: "invar m \<Longrightarrow> lookup(delete a m) = (lookup m)(a := None)" 20and invar_empty: "invar empty" 21and invar_update: "invar m \<Longrightarrow> invar(update a b m)" 22and invar_delete: "invar m \<Longrightarrow> invar(delete a m)" 23 24lemmas (in Map) map_specs = 25 map_empty map_update map_delete invar_empty invar_update invar_delete 26 27 28text \<open>The basic map interface with \<open>inorder\<close>-based specification:\<close> 29 30locale Map_by_Ordered = 31fixes empty :: "'t" 32fixes update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> 't \<Rightarrow> 't" 33fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't" 34fixes lookup :: "'t \<Rightarrow> 'a \<Rightarrow> 'b option" 35fixes inorder :: "'t \<Rightarrow> ('a * 'b) list" 36fixes inv :: "'t \<Rightarrow> bool" 37assumes inorder_empty: "inorder empty = []" 38and inorder_lookup: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> 39 lookup t a = map_of (inorder t) a" 40and inorder_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> 41 inorder(update a b t) = upd_list a b (inorder t)" 42and inorder_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> 43 inorder(delete a t) = del_list a (inorder t)" 44and inorder_inv_empty: "inv empty" 45and inorder_inv_update: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(update a b t)" 46and inorder_inv_delete: "inv t \<and> sorted1 (inorder t) \<Longrightarrow> inv(delete a t)" 47 48begin 49 50text \<open>It implements the traditional specification:\<close> 51 52definition invar :: "'t \<Rightarrow> bool" where 53"invar t == inv t \<and> sorted1 (inorder t)" 54 55sublocale Map 56 empty update delete lookup invar 57proof(standard, goal_cases) 58 case 1 show ?case by (auto simp: inorder_lookup inorder_empty inorder_inv_empty) 59next 60 case 2 thus ?case 61 by(simp add: fun_eq_iff inorder_update inorder_inv_update map_of_ins_list inorder_lookup 62 sorted_upd_list invar_def) 63next 64 case 3 thus ?case 65 by(simp add: fun_eq_iff inorder_delete inorder_inv_delete map_of_del_list inorder_lookup 66 sorted_del_list invar_def) 67next 68 case 4 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def) 69next 70 case 5 thus ?case by(simp add: inorder_update inorder_inv_update sorted_upd_list invar_def) 71next 72 case 6 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def) 73qed 74 75end 76 77end 78