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