equal
deleted
inserted
replaced
13 fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option" |
13 fixes map_of :: "'m \<Rightarrow> 'a \<Rightarrow> 'b option" |
14 fixes invar :: "'m \<Rightarrow> bool" |
14 fixes invar :: "'m \<Rightarrow> bool" |
15 assumes "map_of empty = (\<lambda>_. None)" |
15 assumes "map_of empty = (\<lambda>_. None)" |
16 assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)" |
16 assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)" |
17 assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)" |
17 assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)" |
|
18 assumes "invar empty" |
18 assumes "invar m \<Longrightarrow> invar(update a b m)" |
19 assumes "invar m \<Longrightarrow> invar(update a b m)" |
19 assumes "invar m \<Longrightarrow> invar(delete a m)" |
20 assumes "invar m \<Longrightarrow> invar(delete a m)" |
20 |
21 |
21 locale Map_by_Ordered = |
22 locale Map_by_Ordered = |
22 fixes empty :: "'t" |
23 fixes empty :: "'t" |
30 lookup t a = map_of (inorder t) a" |
31 lookup t a = map_of (inorder t) a" |
31 assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> |
32 assumes update: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> |
32 inorder(update a b t) = upd_list a b (inorder t)" |
33 inorder(update a b t) = upd_list a b (inorder t)" |
33 assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> |
34 assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> |
34 inorder(delete a t) = del_list a (inorder t)" |
35 inorder(delete a t) = del_list a (inorder t)" |
|
36 assumes wf_empty: "wf empty" |
35 assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)" |
37 assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)" |
36 assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)" |
38 assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)" |
37 begin |
39 begin |
38 |
40 |
39 sublocale Map |
41 sublocale Map |
43 next |
45 next |
44 case 2 thus ?case by(simp add: update map_of_ins_list) |
46 case 2 thus ?case by(simp add: update map_of_ins_list) |
45 next |
47 next |
46 case 3 thus ?case by(simp add: delete map_of_del_list) |
48 case 3 thus ?case by(simp add: delete map_of_del_list) |
47 next |
49 next |
48 case 4 thus ?case by(simp add: update wf_insert sorted_upd_list) |
50 case 4 thus ?case by(simp add: empty wf_empty) |
49 next |
51 next |
50 case 5 thus ?case by (auto simp: delete wf_delete sorted_del_list) |
52 case 5 thus ?case by(simp add: update wf_insert sorted_upd_list) |
|
53 next |
|
54 case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list) |
51 qed |
55 qed |
52 |
56 |
53 end |
57 end |
54 |
58 |
55 end |
59 end |