32 assumes vt_s: "vt s" |
32 assumes vt_s: "vt s" |
33 and threads_s: "th \<in> threads s" |
33 and threads_s: "th \<in> threads s" |
34 and highest: "preced th s = Max ((cp s)`threads s)" |
34 and highest: "preced th s = Max ((cp s)`threads s)" |
35 and preced_th: "preced th s = Prc prio tm" |
35 and preced_th: "preced th s = Prc prio tm" |
36 |
36 |
|
37 sublocale highest_gen < vat_s: valid_trace "s" |
|
38 by (unfold_locales, insert vt_s, simp) |
|
39 |
37 context highest_gen |
40 context highest_gen |
38 begin |
41 begin |
39 |
42 |
40 |
|
41 |
|
42 lemma lt_tm: "tm < length s" |
43 lemma lt_tm: "tm < length s" |
43 by (insert preced_tm_lt[OF threads_s preced_th], simp) |
44 by (insert preced_tm_lt[OF threads_s preced_th], simp) |
44 |
45 |
45 lemma eq_cp_s_th: "cp s th = preced th s" |
46 lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") |
46 proof - |
47 proof - |
47 from highest and max_cp_eq[OF vt_s] |
48 have "?L \<le> ?R" |
48 have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp |
49 by (unfold highest, rule Max_ge, |
49 have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s" |
50 auto simp:threads_s finite_threads[OF vt_s]) |
50 proof - |
51 moreover have "?R \<le> ?L" |
51 from threads_s and dependants_threads[OF vt_s, of th] |
52 by (unfold vat_s.cp_rec, rule Max_ge, |
52 show ?thesis by auto |
53 auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) |
53 qed |
54 ultimately show ?thesis by auto |
54 show ?thesis |
|
55 proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) |
|
56 show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp |
|
57 next |
|
58 fix y |
|
59 assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" |
|
60 then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)" |
|
61 and eq_y: "y = preced th1 s" by auto |
|
62 show "y \<le> preced th s" |
|
63 proof(unfold is_max, rule Max_ge) |
|
64 from finite_threads[OF vt_s] |
|
65 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp |
|
66 next |
|
67 from sbs th1_in and eq_y |
|
68 show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto |
|
69 qed |
|
70 next |
|
71 from sbs and finite_threads[OF vt_s] |
|
72 show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))" |
|
73 by (auto intro:finite_subset) |
|
74 qed |
|
75 qed |
55 qed |
76 |
56 |
77 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" |
57 lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" |
78 by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp) |
58 by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp) |
79 |
59 |
162 by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) |
152 by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) |
163 qed |
153 qed |
164 qed |
154 qed |
165 qed |
155 qed |
166 |
156 |
|
157 |
167 lemma th_kept: "th \<in> threads (t @ s) \<and> |
158 lemma th_kept: "th \<in> threads (t @ s) \<and> |
168 preced th (t@s) = preced th s" (is "?Q t") |
159 preced th (t@s) = preced th s" (is "?Q t") |
169 proof - |
160 proof - |
170 show ?thesis |
161 show ?thesis |
171 proof(induct rule:ind) |
162 proof(induct rule:ind) |
172 case Nil |
163 case Nil |
173 from threads_s |
164 from threads_s |
174 show "th \<in> threads ([] @ s) \<and> preced th ([] @ s) = preced th s" |
165 show ?case |
175 by auto |
166 by auto |
176 next |
167 next |
177 case (Cons e t) |
168 case (Cons e t) |
|
169 interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto |
|
170 interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto |
178 show ?case |
171 show ?case |
179 proof(cases e) |
172 proof(cases e) |
180 case (Create thread prio) |
173 case (Create thread prio) |
181 assume eq_e: " e = Create thread prio" |
|
182 show ?thesis |
174 show ?thesis |
183 proof - |
175 proof - |
184 from Cons and eq_e have "step (t@s) (Create thread prio)" by auto |
176 from Cons and Create have "step (t@s) (Create thread prio)" by auto |
185 hence "th \<noteq> thread" |
177 hence "th \<noteq> thread" |
186 proof(cases) |
178 proof(cases) |
187 assume "thread \<notin> threads (t @ s)" |
179 case thread_create |
188 with Cons show ?thesis by auto |
180 with Cons show ?thesis by auto |
189 qed |
181 qed |
190 hence "preced th ((e # t) @ s) = preced th (t @ s)" |
182 hence "preced th ((e # t) @ s) = preced th (t @ s)" |
191 by (unfold eq_e, auto simp:preced_def) |
183 by (unfold Create, auto simp:preced_def) |
192 moreover note Cons |
184 moreover note Cons |
193 ultimately show ?thesis |
185 ultimately show ?thesis |
194 by (auto simp:eq_e) |
186 by (auto simp:Create) |
195 qed |
187 qed |
196 next |
188 next |
197 case (Exit thread) |
189 case (Exit thread) |
198 assume eq_e: "e = Exit thread" |
190 from h_e.exit_diff and Exit |
199 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
|
200 from extend_highest_gen.exit_diff [OF this] and eq_e |
|
201 have neq_th: "thread \<noteq> th" by auto |
191 have neq_th: "thread \<noteq> th" by auto |
202 with Cons |
192 with Cons |
203 show ?thesis |
193 show ?thesis |
204 by (unfold eq_e, auto simp:preced_def) |
194 by (unfold Exit, auto simp:preced_def) |
205 next |
195 next |
206 case (P thread cs) |
196 case (P thread cs) |
207 assume eq_e: "e = P thread cs" |
|
208 with Cons |
197 with Cons |
209 show ?thesis |
198 show ?thesis |
210 by (auto simp:eq_e preced_def) |
199 by (auto simp:P preced_def) |
211 next |
200 next |
212 case (V thread cs) |
201 case (V thread cs) |
213 assume eq_e: "e = V thread cs" |
|
214 with Cons |
202 with Cons |
215 show ?thesis |
203 show ?thesis |
216 by (auto simp:eq_e preced_def) |
204 by (auto simp:V preced_def) |
217 next |
205 next |
218 case (Set thread prio') |
206 case (Set thread prio') |
219 assume eq_e: " e = Set thread prio'" |
|
220 show ?thesis |
207 show ?thesis |
221 proof - |
208 proof - |
222 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
209 from h_e.set_diff_low and Set |
223 from extend_highest_gen.set_diff_low[OF this] and eq_e |
|
224 have "th \<noteq> thread" by auto |
210 have "th \<noteq> thread" by auto |
225 hence "preced th ((e # t) @ s) = preced th (t @ s)" |
211 hence "preced th ((e # t) @ s) = preced th (t @ s)" |
226 by (unfold eq_e, auto simp:preced_def) |
212 by (unfold Set, auto simp:preced_def) |
227 moreover note Cons |
213 moreover note Cons |
228 ultimately show ?thesis |
214 ultimately show ?thesis |
229 by (auto simp:eq_e) |
215 by (auto simp:Set) |
230 qed |
216 qed |
231 qed |
217 qed |
232 qed |
218 qed |
233 qed |
219 qed |
234 |
220 |
235 lemma max_kept: "Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s))) = preced th s" |
221 lemma Max_remove_less: |
|
222 assumes "finite A" |
|
223 and "a \<in> A" |
|
224 and "b \<in> A" |
|
225 and "a \<noteq> b" |
|
226 and "inj_on f A" |
|
227 and "f a = Max (f ` A)" |
|
228 shows "Max (f ` (A - {b})) = (Max (f ` A))" |
|
229 proof - |
|
230 have "Max (f ` (A - {b})) = Max (f`A - {f b})" |
|
231 proof - |
|
232 have "f ` (A - {b}) = f ` A - f ` {b}" |
|
233 by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto) |
|
234 thus ?thesis by simp |
|
235 qed |
|
236 also have "... = |
|
237 (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))" |
|
238 proof(subst Max.remove) |
|
239 from assms show "f a \<in> f ` A - {f b}" |
|
240 by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff) |
|
241 next |
|
242 from assms(1) show "finite (f ` A - {f b})" by auto |
|
243 qed auto |
|
244 also have "... = Max (f ` A)" (is "?L = ?R") |
|
245 proof(cases "f ` A - {f b} - {f a} = {}") |
|
246 case True |
|
247 with assms show ?thesis by auto |
|
248 next |
|
249 case False |
|
250 hence "?L = max (f a) (Max (f ` A - {f b} - {f a}))" |
|
251 by simp |
|
252 also have "... = ?R" |
|
253 proof - |
|
254 from assms False |
|
255 have "(Max (f ` A - {f b} - {f a})) \<le> f a" by auto |
|
256 thus ?thesis by (simp add: assms(6) max_def) |
|
257 qed |
|
258 finally show ?thesis . |
|
259 qed |
|
260 finally show ?thesis . |
|
261 qed |
|
262 |
|
263 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" |
236 proof(induct rule:ind) |
264 proof(induct rule:ind) |
237 case Nil |
265 case Nil |
238 from highest_preced_thread |
266 from highest_preced_thread |
239 show "Max ((\<lambda>th'. preced th' ([] @ s)) ` threads ([] @ s)) = preced th s" |
267 show ?case |
240 by simp |
268 by (unfold the_preced_def, simp) |
241 next |
269 next |
242 case (Cons e t) |
270 case (Cons e t) |
|
271 interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto |
|
272 interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto |
243 show ?case |
273 show ?case |
244 proof(cases e) |
274 proof(cases e) |
245 case (Create thread prio') |
275 case (Create thread prio') |
246 assume eq_e: " e = Create thread prio'" |
276 from Cons(2)[unfolded this] |
247 from Cons and eq_e have stp: "step (t@s) (Create thread prio')" by auto |
277 have thread_not_in: "thread \<notin> threads (t@s)" by (cases, simp) |
248 hence neq_thread: "thread \<noteq> th" |
|
249 proof(cases) |
|
250 assume "thread \<notin> threads (t @ s)" |
|
251 moreover have "th \<in> threads (t@s)" |
|
252 proof - |
|
253 from Cons have "extend_highest_gen s th prio tm t" by auto |
|
254 from extend_highest_gen.th_kept[OF this] show ?thesis by (simp) |
|
255 qed |
|
256 ultimately show ?thesis by auto |
|
257 qed |
|
258 from Cons have "extend_highest_gen s th prio tm t" by auto |
|
259 from extend_highest_gen.th_kept[OF this] |
|
260 have h': " th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" |
|
261 by (auto) |
|
262 from stp |
|
263 have thread_ts: "thread \<notin> threads (t @ s)" |
|
264 by (cases, auto) |
|
265 show ?thesis (is "Max (?f ` ?A) = ?t") |
278 show ?thesis (is "Max (?f ` ?A) = ?t") |
266 proof - |
279 proof - |
267 have "Max (?f ` ?A) = Max(insert (?f thread) (?f ` (threads (t@s))))" |
280 have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))" |
268 by (unfold eq_e, simp) |
281 by (unfold Create, simp) |
269 moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))" |
282 moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))" |
270 proof(rule Max_insert) |
283 proof(rule Max.insert) |
271 from Cons have "vt (t @ s)" by auto |
284 from finite_threads[OF Cons(1)] |
272 from finite_threads[OF this] |
|
273 show "finite (?f ` (threads (t@s)))" by simp |
285 show "finite (?f ` (threads (t@s)))" by simp |
274 next |
286 qed (insert h_t.th_kept, auto) |
275 from h' show "(?f ` (threads (t@s))) \<noteq> {}" by auto |
287 moreover have "(Max (?f ` (threads (t@s)))) = ?t" |
276 qed |
|
277 moreover have "(Max (?f ` (threads (t@s)))) = ?t" |
|
278 proof - |
288 proof - |
279 have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) = |
289 have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) = |
280 (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" (is "?f1 ` ?B = ?f2 ` ?B") |
290 (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" |
281 proof - |
291 by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def) |
282 { fix th' |
292 with Cons show ?thesis by (auto simp:the_preced_def) |
283 assume "th' \<in> ?B" |
|
284 with thread_ts eq_e |
|
285 have "?f1 th' = ?f2 th'" by (auto simp:preced_def) |
|
286 } thus ?thesis |
|
287 apply (auto simp:Image_def) |
|
288 proof - |
|
289 fix th' |
|
290 assume h: "\<And>th'. th' \<in> threads (t @ s) \<Longrightarrow> |
|
291 preced th' (e # t @ s) = preced th' (t @ s)" |
|
292 and h1: "th' \<in> threads (t @ s)" |
|
293 show "preced th' (t @ s) \<in> (\<lambda>th'. preced th' (e # t @ s)) ` threads (t @ s)" |
|
294 proof - |
|
295 from h1 have "?f1 th' \<in> ?f1 ` ?B" by auto |
|
296 moreover from h[OF h1] have "?f1 th' = ?f2 th'" by simp |
|
297 ultimately show ?thesis by simp |
|
298 qed |
|
299 qed |
|
300 qed |
|
301 with Cons show ?thesis by auto |
|
302 qed |
293 qed |
303 moreover have "?f thread < ?t" |
294 moreover have "?f thread < ?t" |
304 proof - |
295 proof - |
305 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
296 from h_e.create_low and Create |
306 from extend_highest_gen.create_low[OF this] and eq_e |
|
307 have "prio' \<le> prio" by auto |
297 have "prio' \<le> prio" by auto |
308 thus ?thesis |
298 thus ?thesis |
309 by (unfold preced_th, unfold eq_e, insert lt_tm, |
299 by (unfold preced_th, unfold Create, insert lt_tm, |
310 auto simp:preced_def precedence_less_def preced_th) |
300 auto simp:preced_def precedence_less_def preced_th the_preced_def) |
311 qed |
301 qed |
312 ultimately show ?thesis by (auto simp:max_def) |
302 ultimately show ?thesis by (auto simp:max_def) |
313 qed |
303 qed |
314 next |
304 next |
315 case (Exit thread) |
305 case (Exit thread) |
316 assume eq_e: "e = Exit thread" |
306 show ?thesis |
317 from Cons have vt_e: "vt (e#(t @ s))" by auto |
|
318 from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto |
|
319 from stp have thread_ts: "thread \<in> threads (t @ s)" |
|
320 by(cases, unfold runing_def readys_def, auto) |
|
321 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
|
322 from extend_highest_gen.exit_diff[OF this] and eq_e |
|
323 have neq_thread: "thread \<noteq> th" by auto |
|
324 from Cons have "extend_highest_gen s th prio tm t" by auto |
|
325 from extend_highest_gen.th_kept[OF this] |
|
326 have h': "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" . |
|
327 show ?thesis (is "Max (?f ` ?A) = ?t") |
|
328 proof - |
307 proof - |
329 have "threads (t@s) = insert thread ?A" |
308 have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = |
330 by (insert stp thread_ts, unfold eq_e, auto) |
309 Max (the_preced (t @ s) ` (threads (t @ s)))" |
331 hence "Max (?f ` (threads (t@s))) = Max (?f ` \<dots>)" by simp |
310 proof(rule Max_remove_less) |
332 also from this have "\<dots> = Max (insert (?f thread) (?f ` ?A))" by simp |
311 show "th \<noteq> thread" using Exit h_e.exit_diff by auto |
333 also have "\<dots> = max (?f thread) (Max (?f ` ?A))" |
312 next |
334 proof(rule Max_insert) |
313 from Cons(2)[unfolded Exit] |
335 from finite_threads [OF vt_e] |
314 show "thread \<in> threads (t @ s)" |
336 show "finite (?f ` ?A)" by simp |
315 by (cases, simp add: readys_def runing_def) |
337 next |
316 next |
338 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
317 show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t) |
339 from extend_highest_gen.th_kept[OF this] |
318 next |
340 show "?f ` ?A \<noteq> {}" by auto |
319 show "th \<in> threads (t @ s)" by (simp add: h_t.th_kept) |
341 qed |
320 next |
342 finally have "Max (?f ` (threads (t@s))) = max (?f thread) (Max (?f ` ?A))" . |
321 show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced) |
343 moreover have "Max (?f ` (threads (t@s))) = ?t" |
322 next |
344 proof - |
323 show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))" |
345 from Cons show ?thesis |
324 by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def) |
346 by (unfold eq_e, auto simp:preced_def) |
325 qed |
347 qed |
326 from this[unfolded Cons(5)] |
348 ultimately have "max (?f thread) (Max (?f ` ?A)) = ?t" by simp |
327 have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" . |
349 moreover have "?f thread < ?t" |
328 moreover have "the_preced ((e # t) @ s) = the_preced (t@s)" |
350 proof(unfold eq_e, simp add:preced_def, fold preced_def) |
329 by (auto simp:Exit the_preced_def preced_def) |
351 show "preced thread (t @ s) < ?t" |
330 ultimately show ?thesis by (simp add:Exit) |
352 proof - |
|
353 have "preced thread (t @ s) \<le> ?t" |
|
354 proof - |
|
355 from Cons |
|
356 have "?t = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" |
|
357 (is "?t = Max (?g ` ?B)") by simp |
|
358 moreover have "?g thread \<le> \<dots>" |
|
359 proof(rule Max_ge) |
|
360 have "vt (t@s)" by fact |
|
361 from finite_threads [OF this] |
|
362 show "finite (?g ` ?B)" by simp |
|
363 next |
|
364 from thread_ts |
|
365 show "?g thread \<in> (?g ` ?B)" by auto |
|
366 qed |
|
367 ultimately show ?thesis by auto |
|
368 qed |
|
369 moreover have "preced thread (t @ s) \<noteq> ?t" |
|
370 proof |
|
371 assume "preced thread (t @ s) = preced th s" |
|
372 with h' have "preced thread (t @ s) = preced th (t@s)" by simp |
|
373 from preced_unique [OF this] have "thread = th" |
|
374 proof |
|
375 from h' show "th \<in> threads (t @ s)" by simp |
|
376 next |
|
377 from thread_ts show "thread \<in> threads (t @ s)" . |
|
378 qed(simp) |
|
379 with neq_thread show "False" by simp |
|
380 qed |
|
381 ultimately show ?thesis by auto |
|
382 qed |
|
383 qed |
|
384 ultimately show ?thesis |
|
385 by (auto simp:max_def split:if_splits) |
|
386 qed |
331 qed |
387 next |
332 next |
388 case (P thread cs) |
333 case (P thread cs) |
389 with Cons |
334 with Cons |
390 show ?thesis by (auto simp:preced_def) |
335 show ?thesis by (auto simp:preced_def the_preced_def) |
391 next |
336 next |
392 case (V thread cs) |
337 case (V thread cs) |
393 with Cons |
338 with Cons |
394 show ?thesis by (auto simp:preced_def) |
339 show ?thesis by (auto simp:preced_def the_preced_def) |
395 next |
340 next (* ccc *) |
396 case (Set thread prio') |
341 case (Set thread prio') |
397 show ?thesis (is "Max (?f ` ?A) = ?t") |
342 show ?thesis |
|
343 apply (unfold Set, simp, insert Cons(5)) (* ccc *) |
|
344 find_theorems priority Set |
|
345 find_theorems preced Set |
398 proof - |
346 proof - |
399 let ?B = "threads (t@s)" |
347 let ?B = "threads (t@s)" |
400 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
348 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto |
401 from extend_highest_gen.set_diff_low[OF this] and Set |
349 from extend_highest_gen.set_diff_low[OF this] and Set |
402 have neq_thread: "thread \<noteq> th" and le_p: "prio' \<le> prio" by auto |
350 have neq_thread: "thread \<noteq> th" and le_p: "prio' \<le> prio" by auto |