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