|
13020
|
1 |
|
|
|
2 |
header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
|
|
|
3 |
|
|
|
4 |
\section {Formalization of the Memory} *}
|
|
|
5 |
|
|
|
6 |
theory Graph = Main:
|
|
|
7 |
|
|
|
8 |
datatype node = Black | White
|
|
|
9 |
|
|
|
10 |
types
|
|
|
11 |
nodes = "node list"
|
|
|
12 |
edge = "nat \<times> nat"
|
|
|
13 |
edges = "edge list"
|
|
|
14 |
|
|
|
15 |
consts Roots :: "nat set"
|
|
|
16 |
|
|
|
17 |
constdefs
|
|
|
18 |
Proper_Roots :: "nodes \<Rightarrow> bool"
|
|
|
19 |
"Proper_Roots M \<equiv> Roots\<noteq>{} \<and> Roots \<subseteq> {i. i<length M}"
|
|
|
20 |
|
|
|
21 |
Proper_Edges :: "(nodes \<times> edges) \<Rightarrow> bool"
|
|
|
22 |
"Proper_Edges \<equiv> (\<lambda>(M,E). \<forall>i<length E. fst(E!i)<length M \<and> snd(E!i)<length M)"
|
|
|
23 |
|
|
|
24 |
BtoW :: "(edge \<times> nodes) \<Rightarrow> bool"
|
|
|
25 |
"BtoW \<equiv> (\<lambda>(e,M). (M!fst e)=Black \<and> (M!snd e)\<noteq>Black)"
|
|
|
26 |
|
|
|
27 |
Blacks :: "nodes \<Rightarrow> nat set"
|
|
|
28 |
"Blacks M \<equiv> {i. i<length M \<and> M!i=Black}"
|
|
|
29 |
|
|
|
30 |
Reach :: "edges \<Rightarrow> nat set"
|
|
|
31 |
"Reach E \<equiv> {x. (\<exists>path. 1<length path \<and> path!(length path - 1)\<in>Roots \<and> x=path!0
|
|
|
32 |
\<and> (\<forall>i<length path - 1. (\<exists>j<length E. E!j=(path!(i+1), path!i))))
|
|
|
33 |
\<or> x\<in>Roots}"
|
|
|
34 |
|
|
|
35 |
text{* Reach: the set of reachable nodes is the set of Roots together with the
|
|
|
36 |
nodes reachable from some Root by a path represented by a list of
|
|
|
37 |
nodes (at least two since we traverse at least one edge), where two
|
|
|
38 |
consecutive nodes correspond to an edge in E. *}
|
|
|
39 |
|
|
|
40 |
subsection {* Proofs about Graphs *}
|
|
|
41 |
|
|
|
42 |
lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
|
|
|
43 |
declare Graph_defs [simp]
|
|
|
44 |
|
|
|
45 |
subsubsection{* Graph 1. *}
|
|
|
46 |
|
|
|
47 |
lemma Graph1_aux [rule_format]:
|
|
|
48 |
"\<lbrakk> Roots\<subseteq>Blacks M; \<forall>i<length E. \<not>BtoW(E!i,M)\<rbrakk>
|
|
|
49 |
\<Longrightarrow> 1< length path \<longrightarrow> (path!(length path - 1))\<in>Roots \<longrightarrow>
|
|
|
50 |
(\<forall>i<length path - 1. (\<exists>j. j < length E \<and> E!j=(path!(Suc i), path!i)))
|
|
|
51 |
\<longrightarrow> M!(path!0) = Black"
|
|
|
52 |
apply(induct_tac "path")
|
|
|
53 |
apply force
|
|
|
54 |
apply clarify
|
|
|
55 |
apply simp
|
|
|
56 |
apply(case_tac "list")
|
|
|
57 |
apply force
|
|
|
58 |
apply simp
|
|
|
59 |
apply(rotate_tac -1)
|
|
|
60 |
apply(erule_tac x = "0" in all_dupE)
|
|
|
61 |
apply simp
|
|
|
62 |
apply clarify
|
|
|
63 |
apply(erule allE , erule (1) notE impE)
|
|
|
64 |
apply simp
|
|
|
65 |
apply(erule mp)
|
|
|
66 |
apply(case_tac "lista")
|
|
|
67 |
apply force
|
|
|
68 |
apply simp
|
|
|
69 |
apply(erule mp)
|
|
|
70 |
apply clarify
|
|
|
71 |
apply(erule_tac x = "Suc i" in allE)
|
|
|
72 |
apply force
|
|
|
73 |
done
|
|
|
74 |
|
|
|
75 |
lemma Graph1:
|
|
|
76 |
"\<lbrakk>Roots\<subseteq>Blacks M; Proper_Edges(M, E); \<forall>i<length E. \<not>BtoW(E!i,M) \<rbrakk>
|
|
|
77 |
\<Longrightarrow> Reach E\<subseteq>Blacks M"
|
|
|
78 |
apply (unfold Reach_def)
|
|
|
79 |
apply simp
|
|
|
80 |
apply clarify
|
|
|
81 |
apply(erule disjE)
|
|
|
82 |
apply clarify
|
|
|
83 |
apply(rule conjI)
|
|
|
84 |
apply(subgoal_tac "0< length path - Suc 0")
|
|
|
85 |
apply(erule allE , erule (1) notE impE)
|
|
|
86 |
apply force
|
|
|
87 |
apply simp
|
|
|
88 |
apply(rule Graph1_aux)
|
|
|
89 |
apply auto
|
|
|
90 |
done
|
|
|
91 |
|
|
|
92 |
subsubsection{* Graph 2. *}
|
|
|
93 |
|
|
|
94 |
lemma Ex_first_occurrence [rule_format]:
|
|
|
95 |
"P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))";
|
|
|
96 |
apply(rule nat_less_induct)
|
|
|
97 |
apply clarify
|
|
|
98 |
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
|
|
|
99 |
apply auto
|
|
|
100 |
done
|
|
|
101 |
|
|
|
102 |
lemma Compl_lemma: "(n::nat)\<le>l \<Longrightarrow> (\<exists>m. m\<le>l \<and> n=l - m)"
|
|
|
103 |
apply(rule_tac x = "l - n" in exI)
|
|
|
104 |
apply arith
|
|
|
105 |
done
|
|
|
106 |
|
|
|
107 |
lemma Ex_last_occurrence:
|
|
|
108 |
"\<lbrakk>P (n::nat); n\<le>l\<rbrakk> \<Longrightarrow> (\<exists>m. P (l - m) \<and> (\<forall>i. i<m \<longrightarrow> \<not>P (l - i)))"
|
|
|
109 |
apply(drule Compl_lemma)
|
|
|
110 |
apply clarify
|
|
|
111 |
apply(erule Ex_first_occurrence)
|
|
|
112 |
done
|
|
|
113 |
|
|
|
114 |
lemma Graph2:
|
|
|
115 |
"\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
|
|
|
116 |
apply (unfold Reach_def)
|
|
|
117 |
apply clarify
|
|
|
118 |
apply simp
|
|
|
119 |
apply(case_tac "\<forall>z<length path. fst(E!R)\<noteq>path!z")
|
|
|
120 |
apply(rule_tac x = "path" in exI)
|
|
|
121 |
apply simp
|
|
|
122 |
apply clarify
|
|
|
123 |
apply(erule allE , erule (1) notE impE)
|
|
|
124 |
apply clarify
|
|
|
125 |
apply(rule_tac x = "j" in exI)
|
|
|
126 |
apply(case_tac "j=R")
|
|
|
127 |
apply(erule_tac x = "Suc i" in allE)
|
|
|
128 |
apply simp
|
|
|
129 |
apply arith
|
|
|
130 |
apply (force simp add:nth_list_update)
|
|
|
131 |
apply simp
|
|
|
132 |
apply(erule exE)
|
|
|
133 |
apply(subgoal_tac "z \<le> length path - Suc 0")
|
|
|
134 |
prefer 2 apply arith
|
|
|
135 |
apply(drule_tac P = "\<lambda>m. m<length path \<and> fst(E!R)=path!m" in Ex_last_occurrence)
|
|
|
136 |
apply assumption
|
|
|
137 |
apply clarify
|
|
|
138 |
apply simp
|
|
|
139 |
apply(rule_tac x = "(path!0)#(drop (length path - Suc m) path)" in exI)
|
|
|
140 |
apply simp
|
|
|
141 |
apply(case_tac "length path - (length path - Suc m)")
|
|
|
142 |
apply arith
|
|
|
143 |
apply simp
|
|
|
144 |
apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
|
|
|
145 |
prefer 2 apply arith
|
|
|
146 |
apply(drule nth_drop)
|
|
|
147 |
apply simp
|
|
|
148 |
apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
|
|
|
149 |
prefer 2 apply arith
|
|
|
150 |
apply simp
|
|
|
151 |
apply clarify
|
|
|
152 |
apply(case_tac "i")
|
|
|
153 |
apply(force simp add: nth_list_update)
|
|
|
154 |
apply simp
|
|
|
155 |
apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
|
|
|
156 |
prefer 2 apply arith
|
|
|
157 |
apply simp
|
|
|
158 |
apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
|
|
|
159 |
prefer 2 apply arith
|
|
|
160 |
apply simp
|
|
|
161 |
apply(erule_tac x = "length path - Suc m + nata" in allE)
|
|
|
162 |
apply simp
|
|
|
163 |
apply clarify
|
|
|
164 |
apply(rule_tac x = "j" in exI)
|
|
|
165 |
apply(case_tac "R=j")
|
|
|
166 |
prefer 2 apply force
|
|
|
167 |
apply simp
|
|
|
168 |
apply(drule_tac t = "path ! (length path - Suc m)" in sym)
|
|
|
169 |
apply simp
|
|
|
170 |
apply(case_tac " length path - Suc 0 < m")
|
|
|
171 |
apply(subgoal_tac "(length path - Suc m)=0")
|
|
|
172 |
prefer 2 apply arith
|
|
|
173 |
apply(rotate_tac -1)
|
|
|
174 |
apply(simp del: diff_is_0_eq)
|
|
|
175 |
apply(subgoal_tac "Suc nata\<le>nat")
|
|
|
176 |
prefer 2 apply arith
|
|
|
177 |
apply(drule_tac n = "Suc nata" in Compl_lemma)
|
|
|
178 |
apply clarify
|
|
|
179 |
apply force
|
|
|
180 |
apply(drule leI)
|
|
|
181 |
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
|
|
|
182 |
apply(erule_tac x = "m - (Suc nata)" in allE)
|
|
|
183 |
apply(case_tac "m")
|
|
|
184 |
apply simp
|
|
|
185 |
apply simp
|
|
|
186 |
apply(subgoal_tac "natb - nata < Suc natb")
|
|
|
187 |
prefer 2 apply(erule thin_rl)+ apply arith
|
|
|
188 |
apply simp
|
|
|
189 |
apply(case_tac "length path")
|
|
|
190 |
apply force
|
|
|
191 |
apply simp
|
|
|
192 |
apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
|
|
|
193 |
apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
|
|
|
194 |
apply simp
|
|
|
195 |
apply arith
|
|
|
196 |
done
|
|
|
197 |
|
|
|
198 |
|
|
|
199 |
subsubsection{* Graph 3. *}
|
|
|
200 |
|
|
|
201 |
lemma Graph3:
|
|
|
202 |
"\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
|
|
|
203 |
apply (unfold Reach_def)
|
|
|
204 |
apply clarify
|
|
|
205 |
apply simp
|
|
|
206 |
apply(case_tac "\<exists>i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)")
|
|
|
207 |
--{* the changed edge is part of the path *}
|
|
|
208 |
apply(erule exE)
|
|
|
209 |
apply(drule_tac P = "\<lambda>i. i<length path - 1 \<and> (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence)
|
|
|
210 |
apply clarify
|
|
|
211 |
apply(erule disjE)
|
|
|
212 |
--{* T is NOT a root *}
|
|
|
213 |
apply clarify
|
|
|
214 |
apply(rule_tac x = "(take m path)@patha" in exI)
|
|
|
215 |
apply(subgoal_tac "\<not>(length path\<le>m)")
|
|
|
216 |
prefer 2 apply arith
|
|
|
217 |
apply(simp add: min_def)
|
|
|
218 |
apply(rule conjI)
|
|
|
219 |
apply(subgoal_tac "\<not>(m + length patha - 1 < m)")
|
|
|
220 |
prefer 2 apply arith
|
|
|
221 |
apply(simp add: nth_append min_def)
|
|
|
222 |
apply(rule conjI)
|
|
|
223 |
apply(case_tac "m")
|
|
|
224 |
apply force
|
|
|
225 |
apply(case_tac "path")
|
|
|
226 |
apply force
|
|
|
227 |
apply force
|
|
|
228 |
apply clarify
|
|
|
229 |
apply(case_tac "Suc i\<le>m")
|
|
|
230 |
apply(erule_tac x = "i" in allE)
|
|
|
231 |
apply simp
|
|
|
232 |
apply clarify
|
|
|
233 |
apply(rule_tac x = "j" in exI)
|
|
|
234 |
apply(case_tac "Suc i<m")
|
|
|
235 |
apply(simp add: nth_append min_def)
|
|
|
236 |
apply(case_tac "R=j")
|
|
|
237 |
apply(simp add: nth_list_update)
|
|
|
238 |
apply(case_tac "i=m")
|
|
|
239 |
apply force
|
|
|
240 |
apply(erule_tac x = "i" in allE)
|
|
|
241 |
apply force
|
|
|
242 |
apply(force simp add: nth_list_update)
|
|
|
243 |
apply(simp add: nth_append min_def)
|
|
|
244 |
apply(subgoal_tac "i=m - 1")
|
|
|
245 |
prefer 2 apply arith
|
|
|
246 |
apply(case_tac "R=j")
|
|
|
247 |
apply(erule_tac x = "m - 1" in allE)
|
|
|
248 |
apply(simp add: nth_list_update)
|
|
|
249 |
apply(force simp add: nth_list_update)
|
|
|
250 |
apply(simp add: nth_append min_def)
|
|
|
251 |
apply(rotate_tac -4)
|
|
|
252 |
apply(erule_tac x = "i - m" in allE)
|
|
|
253 |
apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
|
|
|
254 |
prefer 2 apply arith
|
|
|
255 |
apply simp
|
|
|
256 |
apply(erule mp)
|
|
|
257 |
apply arith
|
|
|
258 |
--{* T is a root *}
|
|
|
259 |
apply(case_tac "m=0")
|
|
|
260 |
apply force
|
|
|
261 |
apply(rule_tac x = "take (Suc m) path" in exI)
|
|
|
262 |
apply(subgoal_tac "\<not>(length path\<le>Suc m)" )
|
|
|
263 |
prefer 2 apply arith
|
|
|
264 |
apply(simp add: min_def)
|
|
|
265 |
apply clarify
|
|
|
266 |
apply(erule_tac x = "i" in allE)
|
|
|
267 |
apply simp
|
|
|
268 |
apply clarify
|
|
|
269 |
apply(case_tac "R=j")
|
|
|
270 |
apply(force simp add: nth_list_update)
|
|
|
271 |
apply(force simp add: nth_list_update)
|
|
|
272 |
--{* the changed edge is not part of the path *}
|
|
|
273 |
apply(rule_tac x = "path" in exI)
|
|
|
274 |
apply simp
|
|
|
275 |
apply clarify
|
|
|
276 |
apply(erule_tac x = "i" in allE)
|
|
|
277 |
apply clarify
|
|
|
278 |
apply(case_tac "R=j")
|
|
|
279 |
apply(erule_tac x = "i" in allE)
|
|
|
280 |
apply simp
|
|
|
281 |
apply(force simp add: nth_list_update)
|
|
|
282 |
done
|
|
|
283 |
|
|
|
284 |
subsubsection{* Graph 4. *}
|
|
|
285 |
|
|
|
286 |
lemma Graph4:
|
|
|
287 |
"\<lbrakk>T \<in> Reach E; Roots\<subseteq>Blacks M; I\<le>length E; T<length M; R<length E;
|
|
|
288 |
\<forall>i<I. \<not>BtoW(E!i,M); R<I; M!fst(E!R)=Black; M!T\<noteq>Black\<rbrakk> \<Longrightarrow>
|
|
|
289 |
(\<exists>r. I\<le>r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
|
|
|
290 |
apply (unfold Reach_def)
|
|
|
291 |
apply simp
|
|
|
292 |
apply(erule disjE)
|
|
|
293 |
prefer 2 apply force
|
|
|
294 |
apply clarify
|
|
|
295 |
--{* there exist a black node in the path to T *}
|
|
|
296 |
apply(case_tac "\<exists>m<length path. M!(path!m)=Black")
|
|
|
297 |
apply(erule exE)
|
|
|
298 |
apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence)
|
|
|
299 |
apply clarify
|
|
|
300 |
apply(case_tac "ma")
|
|
|
301 |
apply force
|
|
|
302 |
apply simp
|
|
|
303 |
apply(case_tac "length path")
|
|
|
304 |
apply force
|
|
|
305 |
apply simp
|
|
|
306 |
apply(rotate_tac -5)
|
|
|
307 |
apply(erule_tac x = "nat" in allE)
|
|
|
308 |
apply simp
|
|
|
309 |
apply clarify
|
|
|
310 |
apply(erule_tac x = "nat" in allE)
|
|
|
311 |
apply simp
|
|
|
312 |
apply(case_tac "j<I")
|
|
|
313 |
apply(erule_tac x = "j" in allE)
|
|
|
314 |
apply force
|
|
|
315 |
apply(rule_tac x = "j" in exI)
|
|
|
316 |
apply(force simp add: nth_list_update)
|
|
|
317 |
apply simp
|
|
|
318 |
apply(rotate_tac -1)
|
|
|
319 |
apply(erule_tac x = "length path - 1" in allE)
|
|
|
320 |
apply(case_tac "length path")
|
|
|
321 |
apply force
|
|
|
322 |
apply force
|
|
|
323 |
done
|
|
|
324 |
|
|
|
325 |
subsubsection {* Graph 5. *}
|
|
|
326 |
|
|
|
327 |
lemma Graph5:
|
|
|
328 |
"\<lbrakk> T \<in> Reach E ; Roots \<subseteq> Blacks M; \<forall>i<R. \<not>BtoW(E!i,M); T<length M;
|
|
|
329 |
R<length E; M!fst(E!R)=Black; M!snd(E!R)=Black; M!T \<noteq> Black\<rbrakk>
|
|
|
330 |
\<Longrightarrow> (\<exists>r. R<r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
|
|
|
331 |
apply (unfold Reach_def)
|
|
|
332 |
apply simp
|
|
|
333 |
apply(erule disjE)
|
|
|
334 |
prefer 2 apply force
|
|
|
335 |
apply clarify
|
|
|
336 |
--{* there exist a black node in the path to T*}
|
|
|
337 |
apply(case_tac "\<exists>m<length path. M!(path!m)=Black")
|
|
|
338 |
apply(erule exE)
|
|
|
339 |
apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence)
|
|
|
340 |
apply clarify
|
|
|
341 |
apply(case_tac "ma")
|
|
|
342 |
apply force
|
|
|
343 |
apply simp
|
|
|
344 |
apply(case_tac "length path")
|
|
|
345 |
apply force
|
|
|
346 |
apply simp
|
|
|
347 |
apply(rotate_tac -5)
|
|
|
348 |
apply(erule_tac x = "nat" in allE)
|
|
|
349 |
apply simp
|
|
|
350 |
apply clarify
|
|
|
351 |
apply(erule_tac x = "nat" in allE)
|
|
|
352 |
apply simp
|
|
|
353 |
apply(case_tac "j\<le>R")
|
|
|
354 |
apply(drule le_imp_less_or_eq)
|
|
|
355 |
apply(erule disjE)
|
|
|
356 |
apply(erule allE , erule (1) notE impE)
|
|
|
357 |
apply force
|
|
|
358 |
apply force
|
|
|
359 |
apply(rule_tac x = "j" in exI)
|
|
|
360 |
apply(force simp add: nth_list_update)
|
|
|
361 |
apply simp
|
|
|
362 |
apply(rotate_tac -1)
|
|
|
363 |
apply(erule_tac x = "length path - 1" in allE)
|
|
|
364 |
apply(case_tac "length path")
|
|
|
365 |
apply force
|
|
|
366 |
apply force
|
|
|
367 |
done
|
|
|
368 |
|
|
|
369 |
subsubsection {* Graph 6, 7, 8. *}
|
|
|
370 |
|
|
|
371 |
lemma Graph6:
|
|
|
372 |
"\<lbrakk>Proper_Edges(M,E); R<length E ; T<length M\<rbrakk> \<Longrightarrow> Proper_Edges(M,E[R:=(fst(E!R),T)])"
|
|
|
373 |
apply (unfold Proper_Edges_def)
|
|
|
374 |
apply(force simp add: nth_list_update)
|
|
|
375 |
done
|
|
|
376 |
|
|
|
377 |
lemma Graph7:
|
|
|
378 |
"\<lbrakk>Proper_Edges(M,E)\<rbrakk> \<Longrightarrow> Proper_Edges(M[T:=a],E)"
|
|
|
379 |
apply (unfold Proper_Edges_def)
|
|
|
380 |
apply force
|
|
|
381 |
done
|
|
|
382 |
|
|
|
383 |
lemma Graph8:
|
|
|
384 |
"\<lbrakk>Proper_Roots(M)\<rbrakk> \<Longrightarrow> Proper_Roots(M[T:=a])"
|
|
|
385 |
apply (unfold Proper_Roots_def)
|
|
|
386 |
apply force
|
|
|
387 |
done
|
|
|
388 |
|
|
|
389 |
text{* Some specific lemmata for the verification of garbage collection algorithms. *}
|
|
|
390 |
|
|
|
391 |
lemma Graph9: "j<length M \<Longrightarrow> Blacks M\<subseteq>Blacks (M[j := Black])"
|
|
|
392 |
apply (unfold Blacks_def)
|
|
|
393 |
apply(force simp add: nth_list_update)
|
|
|
394 |
done
|
|
|
395 |
|
|
|
396 |
lemma Graph10 [rule_format (no_asm)]: "\<forall>i. M!i=a \<longrightarrow>M[i:=a]=M"
|
|
|
397 |
apply(induct_tac "M")
|
|
|
398 |
apply auto
|
|
|
399 |
apply(case_tac "i")
|
|
|
400 |
apply auto
|
|
|
401 |
done
|
|
|
402 |
|
|
|
403 |
lemma Graph11 [rule_format (no_asm)]:
|
|
|
404 |
"\<lbrakk> M!j\<noteq>Black;j<length M\<rbrakk> \<Longrightarrow> Blacks M \<subset> Blacks (M[j := Black])"
|
|
|
405 |
apply (unfold Blacks_def)
|
|
|
406 |
apply(rule psubsetI)
|
|
|
407 |
apply(force simp add: nth_list_update)
|
|
|
408 |
apply safe
|
|
|
409 |
apply(erule_tac c = "j" in equalityCE)
|
|
|
410 |
apply auto
|
|
|
411 |
done
|
|
|
412 |
|
|
|
413 |
lemma Graph12: "\<lbrakk>a\<subseteq>Blacks M;j<length M\<rbrakk> \<Longrightarrow> a\<subseteq>Blacks (M[j := Black])"
|
|
|
414 |
apply (unfold Blacks_def)
|
|
|
415 |
apply(force simp add: nth_list_update)
|
|
|
416 |
done
|
|
|
417 |
|
|
|
418 |
lemma Graph13: "\<lbrakk>a\<subset> Blacks M;j<length M\<rbrakk> \<Longrightarrow> a \<subset> Blacks (M[j := Black])"
|
|
|
419 |
apply (unfold Blacks_def)
|
|
|
420 |
apply(erule psubset_subset_trans)
|
|
|
421 |
apply(force simp add: nth_list_update)
|
|
|
422 |
done
|
|
|
423 |
|
|
|
424 |
declare Graph_defs [simp del]
|
|
|
425 |
|
|
|
426 |
end
|