71 |
71 |
72 abbreviation |
72 abbreviation |
73 "release qs \<equiv> case qs of |
73 "release qs \<equiv> case qs of |
74 [] => [] |
74 [] => [] |
75 | (_ # qs) => SOME q. distinct q \<and> set q = set qs" |
75 | (_ # qs) => SOME q. distinct q \<and> set q = set qs" |
|
76 |
|
77 lemma [simp]: |
|
78 "(SOME q. distinct q \<and> q = []) = []" |
|
79 by auto |
|
80 |
|
81 lemma [simp]: |
|
82 "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)" |
|
83 apply(auto) |
|
84 apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
|
85 by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
|
86 |
|
87 abbreviation |
|
88 "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)" |
|
89 |
76 |
90 |
77 fun schs :: "state \<Rightarrow> schedule_state" |
91 fun schs :: "state \<Rightarrow> schedule_state" |
78 where |
92 where |
79 "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" |
93 "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" |
80 | "schs (Create th prio # s) = |
94 | "schs (Create th prio # s) = |
167 lemma readys_threads: |
179 lemma readys_threads: |
168 shows "readys s \<subseteq> threads s" |
180 shows "readys s \<subseteq> threads s" |
169 unfolding readys_def |
181 unfolding readys_def |
170 by auto |
182 by auto |
171 |
183 |
|
184 lemma wq_threads: |
|
185 assumes vt: "vt s" |
|
186 and h: "th \<in> set (wq s cs)" |
|
187 shows "th \<in> threads s" |
|
188 using assms |
|
189 apply(induct) |
|
190 apply(simp add: wq_def) |
|
191 apply(erule step.cases) |
|
192 apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) |
|
193 apply(simp add: waits_def) |
|
194 apply(auto simp add: waits_def split: if_splits)[1] |
|
195 apply(auto split: if_splits) |
|
196 apply(simp only: waits_def) |
|
197 by (metis insert_iff set_simps(2)) |
|
198 |
|
199 |
|
200 |
|
201 lemma Domain_RAG_threads: |
|
202 assumes vt: "vt s" |
|
203 and in_dom: "(Th th) \<in> Domain (RAG2 s)" |
|
204 shows "th \<in> threads s" |
|
205 proof - |
|
206 from in_dom obtain n where "(Th th, n) \<in> RAG2 s" by auto |
|
207 then obtain cs where "n = Cs cs" "(Th th, Cs cs) \<in> RAG2 s" |
|
208 unfolding RAG2_def RAG_def by auto |
|
209 then have "th \<in> set (wq s cs)" |
|
210 unfolding wq_def RAG_def RAG2_def waits_def by auto |
|
211 with wq_threads [OF vt] show ?thesis . |
|
212 qed |
|
213 |
|
214 lemma dependants_threads: |
|
215 assumes vt: "vt s" |
|
216 shows "dependants2 s th \<subseteq> threads s" |
|
217 proof |
|
218 fix th1 |
|
219 assume "th1 \<in> dependants2 s th" |
|
220 then have h: "(Th th1, Th th) \<in> (RAG2 s)\<^sup>+" |
|
221 unfolding dependants2_def dependants_def RAG2_def by simp |
|
222 then have "Th th1 \<in> Domain ((RAG2 s)\<^sup>+)" unfolding Domain_def by auto |
|
223 then have "Th th1 \<in> Domain (RAG2 s)" using trancl_domain by simp |
|
224 then show "th1 \<in> threads s" using vt by (rule_tac Domain_RAG_threads) |
|
225 qed |
|
226 |
|
227 lemma finite_threads: |
|
228 assumes vt: "vt s" |
|
229 shows "finite (threads s)" |
|
230 using vt by (induct) (auto elim: step.cases) |
|
231 |
|
232 |
|
233 section {* Distinctness of @{const wq} *} |
|
234 |
172 lemma wq_distinct_step: |
235 lemma wq_distinct_step: |
173 assumes "step s e" "distinct (wq s cs)" |
236 assumes "step s e" "distinct (wq s cs)" |
174 shows "distinct (wq (e # s) cs)" |
237 shows "distinct (wq (e # s) cs)" |
175 using assms |
238 using assms |
176 unfolding wq_def |
239 unfolding wq_def |
177 apply(induct) |
240 apply(erule_tac step.cases) |
178 apply(auto simp add: RAG2_def RAG_def Let_def)[1] |
241 apply(auto simp add: RAG2_def RAG_def Let_def)[1] |
179 apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def) |
242 apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def) |
180 apply(auto split: list.split) |
243 apply(auto split: list.split) |
181 apply(rule someI2) |
244 apply(rule someI2) |
182 apply(auto) |
245 apply(auto) |
189 apply(induct) |
252 apply(induct) |
190 apply(simp add: wq_def) |
253 apply(simp add: wq_def) |
191 apply(simp add: wq_distinct_step) |
254 apply(simp add: wq_distinct_step) |
192 done |
255 done |
193 |
256 |
194 lemma RAG_set_unchanged[simp]: |
257 |
195 shows "RAG2 (Set th prio # s) = RAG2 s" |
258 section {* Single_Valuedness of @{const waits2}, @{const holds2}, @{const RAG2} *} |
196 unfolding RAG2_def |
|
197 by (simp add: Let_def) |
|
198 |
|
199 lemma RAG_create_unchanged[simp]: |
|
200 "RAG2 (Create th prio # s) = RAG2 s" |
|
201 unfolding RAG2_def |
|
202 by (simp add: Let_def) |
|
203 |
|
204 lemma RAG_exit_unchanged[simp]: |
|
205 shows "RAG2 (Exit th # s) = RAG2 s" |
|
206 unfolding RAG2_def |
|
207 by (simp add: Let_def) |
|
208 |
|
209 lemma RAG_p1: |
|
210 assumes "wq s cs = []" |
|
211 shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}" |
|
212 using assms |
|
213 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def |
|
214 by (auto simp add: Let_def) |
|
215 |
|
216 |
|
217 lemma RAG_p2: |
|
218 assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []" |
|
219 shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}" |
|
220 using assms |
|
221 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def |
|
222 by (auto simp add: Let_def) |
|
223 |
|
224 lemma [simp]: "(SOME q. distinct q \<and> q = []) = []" |
|
225 by auto |
|
226 |
|
227 lemma [simp]: "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)" |
|
228 apply auto |
|
229 apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
|
230 by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
|
231 |
|
232 lemma RAG_v1: |
|
233 assumes vt: "wq s cs = [th]" |
|
234 shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" |
|
235 using assms |
|
236 unfolding RAG2_def RAG_def waits_def holds_def wq_def |
|
237 by (auto simp add: Let_def) |
|
238 |
|
239 lemma RAG_v2: |
|
240 assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []" |
|
241 shows "RAG2 (V th cs # s) \<subseteq> |
|
242 RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}" |
|
243 unfolding RAG2_def RAG_def waits_def holds_def |
|
244 using assms wq_distinct[OF vt(1), of"cs"] |
|
245 by (auto simp add: Let_def wq_def) |
|
246 |
|
247 (* |
|
248 lemma single_valued_waits2: |
|
249 assumes "vt s" |
|
250 shows "single_valuedP (waits2 s)" |
|
251 using assms |
|
252 apply(induct) |
|
253 apply(simp add: waits2_def waits_def) |
|
254 apply(erule step.cases) |
|
255 apply(auto simp add: Let_def waits2_def) |
|
256 unfolding single_valued_def waits2_def waits_def |
|
257 apply(auto) |
|
258 *) |
|
259 |
|
260 |
259 |
261 lemma waits2_unique: |
260 lemma waits2_unique: |
262 assumes "vt s" |
261 assumes "vt s" |
263 and "waits2 s th cs1" |
262 and "waits2 s th cs1" |
264 and "waits2 s th cs2" |
263 and "waits2 s th cs2" |
272 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
271 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
273 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
272 apply (metis Nil_is_append_conv hd_append2 list.distinct(1) split_list) |
274 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
273 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
275 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
274 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct) |
276 |
275 |
|
276 lemma single_valued_waits2: |
|
277 assumes "vt s" |
|
278 shows "single_valuedP (waits2 s)" |
|
279 using assms |
|
280 unfolding single_valued_def |
|
281 by (metis Collect_splitD fst_eqD sndI waits2_unique) |
|
282 |
277 lemma single_valued_holds2: |
283 lemma single_valued_holds2: |
278 assumes "vt s" |
284 assumes "vt s" |
279 shows "single_valuedP (\<lambda>cs th. holds2 s th cs)" |
285 shows "single_valuedP (\<lambda>cs th. holds2 s th cs)" |
280 unfolding single_valued_def holds2_def holds_def by simp |
286 unfolding single_valued_def holds2_def holds_def by simp |
281 |
287 |
282 |
|
283 lemma holds2_unique: |
|
284 assumes "holds2 s th1 cs" |
|
285 and "holds2 s th2 cs" |
|
286 shows "th1 = th2" |
|
287 using assms |
|
288 unfolding holds2_def holds_def by auto |
|
289 |
|
290 lemma single_valued_waits2: |
|
291 assumes "vt s" |
|
292 shows "single_valuedP (waits2 s)" |
|
293 by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique) |
|
294 |
|
295 |
|
296 (* was unique_RAG2 *) |
|
297 lemma single_valued_RAG2: |
288 lemma single_valued_RAG2: |
298 assumes "vt s" |
289 assumes "vt s" |
299 shows "single_valued (RAG2 s)" |
290 shows "single_valued (RAG2 s)" |
300 using single_valued_waits2[OF assms] single_valued_holds2[OF assms] |
291 using single_valued_waits2[OF assms] single_valued_holds2[OF assms] |
301 unfolding RAG2_def RAG_def |
292 unfolding RAG2_def RAG_def |
302 unfolding single_valued_def |
293 apply(rule_tac single_valued_union) |
303 unfolding holds2_def waits2_def |
294 unfolding holds2_def[symmetric] waits2_def[symmetric] |
304 by auto |
295 apply(rule single_valued_Collect) |
|
296 apply(simp) |
|
297 apply(simp add: inj_on_def) |
|
298 apply(rule single_valued_Collect) |
|
299 apply(simp) |
|
300 apply(simp add: inj_on_def) |
|
301 apply(auto) |
|
302 done |
|
303 |
|
304 |
|
305 section {* Properties of @{const RAG2} under events *} |
|
306 |
|
307 lemma RAG_Set [simp]: |
|
308 shows "RAG2 (Set th prio # s) = RAG2 s" |
|
309 unfolding RAG2_def |
|
310 by (simp add: Let_def) |
|
311 |
|
312 lemma RAG_Create [simp]: |
|
313 "RAG2 (Create th prio # s) = RAG2 s" |
|
314 unfolding RAG2_def |
|
315 by (simp add: Let_def) |
|
316 |
|
317 lemma RAG_Exit [simp]: |
|
318 shows "RAG2 (Exit th # s) = RAG2 s" |
|
319 unfolding RAG2_def |
|
320 by (simp add: Let_def) |
|
321 |
|
322 lemma RAG_P1: |
|
323 assumes "wq s cs = []" |
|
324 shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}" |
|
325 using assms |
|
326 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def |
|
327 by (auto simp add: Let_def) |
|
328 |
|
329 lemma RAG_P2: |
|
330 assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []" |
|
331 shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}" |
|
332 using assms |
|
333 unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def |
|
334 by (auto simp add: Let_def) |
|
335 |
|
336 |
|
337 lemma RAG_V1: |
|
338 assumes vt: "wq s cs = [th]" |
|
339 shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" |
|
340 using assms |
|
341 unfolding RAG2_def RAG_def waits_def holds_def wq_def |
|
342 by (auto simp add: Let_def) |
|
343 |
|
344 lemma RAG_V2: |
|
345 assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []" |
|
346 shows "RAG2 (V th cs # s) \<subseteq> |
|
347 RAG2 s - {(Cs cs, Th th), (Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}" |
|
348 unfolding RAG2_def RAG_def waits_def holds_def |
|
349 using assms wq_distinct[OF vt(1), of"cs"] |
|
350 by (auto simp add: Let_def wq_def) |
|
351 |
|
352 |
|
353 |
|
354 section {* Acyclicity of @{const RAG2} *} |
305 |
355 |
306 lemma acyclic_RAG_step: |
356 lemma acyclic_RAG_step: |
307 assumes vt: "vt s" |
357 assumes vt: "vt s" |
308 and stp: "step s e" |
358 and stp: "step s e" |
309 and ac: "acyclic (RAG2 s)" |
359 and ac: "acyclic (RAG2 s)" |
319 assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" |
369 assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" |
320 then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis |
370 then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis |
321 with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def) |
371 with wq_empty show False by (auto simp: RAG2_def RAG_def wq_def waits_def) |
322 qed |
372 qed |
323 with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp |
373 with ac have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp |
324 then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF wq_empty] |
374 then have "acyclic (RAG2 (P th cs # s))" using RAG_P1[OF wq_empty] |
325 by (rule acyclic_subset) |
375 by (rule acyclic_subset) |
326 } |
376 } |
327 moreover |
377 moreover |
328 { assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty" |
378 { assume wq_not_empty: "wq s cs \<noteq> []" -- "case waiting queue is not empty" |
329 from ac ds |
379 from ac ds |
330 have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp |
380 have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by simp |
331 then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds wq_not_empty] |
381 then have "acyclic (RAG2 (P th cs # s))" using RAG_P2[OF ds wq_not_empty] |
332 by (rule acyclic_subset) |
382 by (rule acyclic_subset) |
333 } |
383 } |
334 ultimately show "acyclic (RAG2 (P th cs # s))" by metis |
384 ultimately show "acyclic (RAG2 (P th cs # s))" by metis |
335 next |
385 next |
336 case (step_V th s cs) -- "case for release of a lock" |
386 case (step_V th s cs) -- "case for release of a lock" |
341 from hd have "th \<in> set (wq s cs)" "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto |
391 from hd have "th \<in> set (wq s cs)" "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto |
342 then obtain wts where eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto) |
392 then obtain wts where eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto) |
343 -- "case no thread present in the waiting queue to take over" |
393 -- "case no thread present in the waiting queue to take over" |
344 { assume "wts = []" |
394 { assume "wts = []" |
345 with eq_wq have "wq s cs = [th]" by simp |
395 with eq_wq have "wq s cs = [th]" by simp |
346 then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1) |
396 then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_V1) |
347 moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset) |
397 moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset) |
348 ultimately |
398 ultimately |
349 have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) |
399 have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset) |
350 } |
400 } |
351 moreover |
401 moreover |
352 -- "at least one thread present to take over" |
402 -- "at least one thread present to take over" |
353 { def nth \<equiv> "next_to_run wts" |
403 { def nth \<equiv> "next_to_run wts" |
354 assume wq_not_empty: "wts \<noteq> []" |
404 assume wq_not_empty: "wts \<noteq> []" |
355 have waits2_cs: "waits2 s nth cs" |
405 have "waits2 s nth cs" |
356 using eq_wq wq_not_empty wq_distinct |
406 using eq_wq wq_not_empty wq_distinct |
357 unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto |
407 unfolding nth_def waits2_def waits_def wq_def[symmetric] by auto |
|
408 then have cs_in_RAG: "(Th nth, Cs cs) \<in> RAG2 s" |
|
409 unfolding RAG2_def RAG_def waits2_def by auto |
358 have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" |
410 have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}" |
359 unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_v2) (auto) |
411 unfolding nth_def using vt wq_not_empty eq_wq by (rule_tac RAG_V2) (auto) |
360 moreover |
412 moreover |
361 have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)})" |
413 have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth)})" |
362 proof - |
414 proof - |
363 have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset) |
415 have "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset) |
364 moreover |
416 moreover |
366 proof (rule notI) |
418 proof (rule notI) |
367 assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" |
419 assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})\<^sup>+" |
368 then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" |
420 then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)})" |
369 by (metis converse_tranclE) |
421 by (metis converse_tranclE) |
370 then have "(Th nth, z) \<in> RAG2 s" by simp |
422 then have "(Th nth, z) \<in> RAG2 s" by simp |
371 then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s" |
423 then have "z = Cs cs" using cs_in_RAG single_valued_RAG2[OF vt] |
372 unfolding RAG2_def RAG_def by auto |
424 by (simp add: single_valued_def) |
373 moreover |
425 then show "False" using a by simp |
374 have "waits2 s nth cs'" |
|
375 using b(2) unfolding RAG2_def RAG_def waits2_def by simp |
|
376 ultimately have "cs = cs'" |
|
377 by (rule_tac waits2_unique[OF vt waits2_cs]) |
|
378 then show "False" using a b(1) by simp |
|
379 qed |
426 qed |
380 ultimately |
427 ultimately |
381 show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp |
428 show "acyclic (RAG2 s - {(Cs cs, Th th), (Th nth, Cs cs)} \<union> {(Cs cs, Th nth) })" by simp |
382 qed |
429 qed |
383 ultimately have "acyclic (RAG2 (V th cs # s))" |
430 ultimately have "acyclic (RAG2 (V th cs # s))" |
395 apply(simp add: RAG2_def RAG_def waits_def holds_def) |
442 apply(simp add: RAG2_def RAG_def waits_def holds_def) |
396 apply(erule step.cases) |
443 apply(erule step.cases) |
397 apply(auto) |
444 apply(auto) |
398 apply(case_tac "wq sa cs = []") |
445 apply(case_tac "wq sa cs = []") |
399 apply(rule finite_subset) |
446 apply(rule finite_subset) |
400 apply(rule RAG_p1) |
447 apply(rule RAG_P1) |
401 apply(simp) |
448 apply(simp) |
402 apply(simp) |
449 apply(simp) |
403 apply(rule finite_subset) |
450 apply(rule finite_subset) |
404 apply(rule RAG_p2) |
451 apply(rule RAG_P2) |
405 apply(simp) |
452 apply(simp) |
406 apply(simp) |
453 apply(simp) |
407 apply(simp) |
454 apply(simp) |
408 apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts") |
455 apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts") |
409 apply(erule exE) |
456 apply(erule exE) |
410 apply(case_tac "wts = []") |
457 apply(case_tac "wts = []") |
411 apply(rule finite_subset) |
458 apply(rule finite_subset) |
412 apply(rule RAG_v1) |
459 apply(rule RAG_V1) |
413 apply(simp) |
460 apply(simp) |
414 apply(simp) |
461 apply(simp) |
415 apply(rule finite_subset) |
462 apply(rule finite_subset) |
416 apply(rule RAG_v2) |
463 apply(rule RAG_V2) |
417 apply(simp) |
464 apply(simp) |
418 apply(simp) |
465 apply(simp) |
419 apply(simp) |
466 apply(simp) |
420 apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") |
467 apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") |
421 apply(case_tac "wq sa cs") |
468 apply(case_tac "wq sa cs") |
422 apply(auto)[2] |
469 apply(auto)[2] |
423 apply(auto simp add: holds2_def holds_def wq_def) |
470 apply(auto simp add: holds2_def holds_def wq_def) |
424 done |
471 done |
425 |
|
426 lemma wq_threads: |
|
427 assumes vt: "vt s" |
|
428 and h: "th \<in> set (wq s cs)" |
|
429 shows "th \<in> threads s" |
|
430 using assms |
|
431 apply(induct) |
|
432 apply(simp add: wq_def) |
|
433 apply(erule step.cases) |
|
434 apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def) |
|
435 apply(simp add: waits_def) |
|
436 apply(auto simp add: waits_def split: if_splits)[1] |
|
437 apply(auto split: if_splits) |
|
438 apply(simp only: waits_def) |
|
439 by (metis insert_iff set_simps(2)) |
|
440 |
|
441 lemma max_cpreceds_readys_threads: |
|
442 assumes vt: "vt s" |
|
443 shows "Max (cpreceds2 s (readys s)) = Max (cpreceds2 s (threads s))" |
|
444 apply(case_tac "threads s = {}") |
|
445 apply(simp add: readys_def) |
|
446 using vt |
|
447 apply(induct) |
|
448 apply(simp) |
|
449 apply(erule step.cases) |
|
450 apply(auto simp add: readys_def waits2_def waits_def Let_def holding_def runing_def holds2_def) |
|
451 defer |
|
452 defer |
|
453 oops |
|
454 |
|
455 |
|
456 |
|
457 |
472 |
458 |
473 |
459 |
474 |
460 lemma dchain_unique: |
475 lemma dchain_unique: |
461 assumes vt: "vt s" |
476 assumes vt: "vt s" |
464 and th2_d: "(n, Th th2) \<in> (RAG2 s)^+" |
479 and th2_d: "(n, Th th2) \<in> (RAG2 s)^+" |
465 and th2_r: "th2 \<in> readys s" |
480 and th2_r: "th2 \<in> readys s" |
466 shows "th1 = th2" |
481 shows "th1 = th2" |
467 proof(rule ccontr) |
482 proof(rule ccontr) |
468 assume neq: "th1 \<noteq> th2" |
483 assume neq: "th1 \<noteq> th2" |
469 hence "Th th1 \<noteq> Th th2" by simp |
484 with single_valued_confluent2 [OF single_valued_RAG2 [OF vt]] th1_d th2_d |
470 from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt] |
485 have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" by auto |
471 have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" |
486 moreover |
472 unfolding single_valued_def by auto |
487 { assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+" |
473 then show "False" |
488 then obtain n where dd: "(Th th1, n) \<in> RAG2 s" by (metis converse_tranclE) |
474 proof |
|
475 assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+" |
|
476 from trancl_split [OF this] |
|
477 obtain n where dd: "(Th th1, n) \<in> RAG2 s" by auto |
|
478 then obtain cs where eq_n: "n = Cs cs" |
489 then obtain cs where eq_n: "n = Cs cs" |
479 unfolding RAG2_def RAG_def by (case_tac n) (auto) |
490 unfolding RAG2_def RAG_def by (case_tac n) (auto) |
480 from dd eq_n have "th1 \<notin> readys s" |
491 from dd eq_n have "th1 \<notin> readys s" |
481 unfolding RAG2_def RAG_def waits2_def readys_def by (auto) |
492 unfolding RAG2_def RAG_def waits2_def readys_def by (auto) |
482 with th1_r show ?thesis by auto |
493 with th1_r have "False" by auto |
483 next |
494 } |
484 assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" |
495 moreover |
485 from trancl_split [OF this] |
496 { assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" |
486 obtain n where dd: "(Th th2, n) \<in> RAG2 s" by auto |
497 then obtain n where dd: "(Th th2, n) \<in> RAG2 s" by (metis converse_tranclE) |
487 then obtain cs where eq_n: "n = Cs cs" |
498 then obtain cs where eq_n: "n = Cs cs" |
488 unfolding RAG2_def RAG_def by (case_tac n) (auto) |
499 unfolding RAG2_def RAG_def by (case_tac n) (auto) |
489 from dd eq_n have "th2 \<notin> readys s" |
500 from dd eq_n have "th2 \<notin> readys s" |
490 unfolding RAG2_def RAG_def waits2_def readys_def by (auto) |
501 unfolding RAG2_def RAG_def waits2_def readys_def by (auto) |
491 with th2_r show ?thesis by auto |
502 with th2_r have "False" by auto |
492 qed |
503 } |
|
504 ultimately show "False" by metis |
493 qed |
505 qed |
494 |
506 |
|
507 lemma max_cpreceds_readys_threads: |
|
508 assumes vt: "vt s" |
|
509 shows "Max (cpreceds2 s (readys s)) = Max (cpreceds2 s (threads s))" |
|
510 apply(case_tac "threads s = {}") |
|
511 apply(simp add: readys_def) |
|
512 using vt |
|
513 apply(induct) |
|
514 apply(simp) |
|
515 apply(erule step.cases) |
|
516 apply(auto simp add: readys_def waits2_def waits_def Let_def holding_def runing_def holds2_def) |
|
517 defer |
|
518 defer |
|
519 oops |
|
520 |
|
521 lemma readys_Exit: |
|
522 shows "readys (Exit th # s) \<subseteq> readys s" |
|
523 by (auto simp add: readys_def waits2_def Let_def) |
|
524 |
|
525 lemma readys_Create: |
|
526 shows "readys (Create th prio # s) \<subseteq> {th} \<union> readys s" |
|
527 by (auto simp add: readys_def waits2_def Let_def) |
|
528 |
|
529 lemma readys_Set: |
|
530 shows "readys (Set th prio # s) \<subseteq> readys s" |
|
531 by (auto simp add: readys_def waits2_def Let_def) |
|
532 |
|
533 |
|
534 lemma readys_P: |
|
535 shows "readys (P th cs # s) \<subseteq> readys s" |
|
536 apply(auto simp add: readys_def waits2_def Let_def) |
|
537 apply(simp add: waits_def) |
|
538 apply(case_tac "csa = cs") |
|
539 apply(simp) |
|
540 apply(drule_tac x="cs" in spec) |
|
541 apply(simp) |
|
542 apply (metis hd_append2 in_set_insert insert_Nil list.sel(1)) |
|
543 apply(drule_tac x="csa" in spec) |
|
544 apply(simp) |
|
545 done |
|
546 |
|
547 lemma readys_V: |
|
548 shows "readys (V th cs # s) \<subseteq> readys s \<union> set (wq s cs)" |
|
549 apply(auto simp add: readys_def waits2_def waits_def Let_def wq_def) |
|
550 done |
|
551 |
|
552 lemma |
|
553 assumes "vt s" |
|
554 shows "card (runing s) \<le> 1" |
|
555 proof (rule ccontr) |
|
556 assume "\<not> card (runing s) \<le> 1" |
|
557 then have "2 \<le> card (runing s)" by auto |
|
558 moreover |
|
559 have "finite (runing s)" sorry |
|
560 ultimately obtain th1 th2 where "th1 \<noteq> th2" "th1 \<in> runing s" "th2 \<in> runing s" |
|
561 by (auto simp add: numerals card_le_Suc_iff) (blast) |
|
562 |
|
563 show "False" |
|
564 apply(simp) |
|
565 oops |
495 |
566 |
496 |
567 |
497 end |
568 end |