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