2312 by (unfold fsubtree_def fsubtree_axioms_def,auto) |
2408 by (unfold fsubtree_def fsubtree_axioms_def,auto) |
2313 qed |
2409 qed |
2314 from this[folded tRAG_def] show "fsubtree (tRAG s)" . |
2410 from this[folded tRAG_def] show "fsubtree (tRAG s)" . |
2315 qed |
2411 qed |
2316 |
2412 |
2317 |
|
2318 (* ccc *) |
|
2319 |
|
2320 context valid_trace_p |
|
2321 begin |
|
2322 |
|
2323 lemma ready_th_s: "th \<in> readys s" |
|
2324 using runing_th_s |
|
2325 by (unfold runing_def, auto) |
|
2326 |
|
2327 lemma live_th_s: "th \<in> threads s" |
|
2328 using readys_threads ready_th_s by auto |
|
2329 |
|
2330 lemma live_th_es: "th \<in> threads (e#s)" |
|
2331 using live_th_s |
|
2332 by (unfold is_p, simp) |
|
2333 |
|
2334 |
|
2335 lemma waiting_neq_th: |
|
2336 assumes "waiting s t c" |
|
2337 shows "t \<noteq> th" |
|
2338 using assms using th_not_waiting by blast |
|
2339 |
|
2340 end |
|
2341 |
|
2342 context valid_trace_v |
|
2343 begin |
|
2344 |
|
2345 lemma th_not_waiting: |
|
2346 "\<not> waiting s th c" |
|
2347 proof - |
|
2348 have "th \<in> readys s" |
|
2349 using runing_ready runing_th_s by blast |
|
2350 thus ?thesis |
|
2351 by (unfold readys_def, auto) |
|
2352 qed |
|
2353 |
|
2354 lemma waiting_neq_th: |
|
2355 assumes "waiting s t c" |
|
2356 shows "t \<noteq> th" |
|
2357 using assms using th_not_waiting by blast |
|
2358 |
|
2359 end |
|
2360 |
|
2361 |
|
2362 context valid_trace_e |
|
2363 begin |
|
2364 |
|
2365 lemma actor_inv: |
|
2366 assumes "\<not> isCreate e" |
|
2367 shows "actor e \<in> runing s" |
|
2368 using pip_e assms |
|
2369 by (induct, auto) |
|
2370 |
|
2371 end |
|
2372 |
|
2373 |
|
2374 (* ccc *) |
|
2375 |
|
2376 (* drag more from before to here *) |
|
2377 |
|
2378 |
|
2379 section {* ccc *} |
|
2380 |
|
2381 |
|
2382 context valid_trace |
|
2383 begin |
|
2384 |
|
2385 lemma finite_subtree_threads: |
|
2386 "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A") |
|
2387 proof - |
|
2388 have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}" |
|
2389 by (auto, insert image_iff, fastforce) |
|
2390 moreover have "finite {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}" |
|
2391 (is "finite ?B") |
|
2392 proof - |
|
2393 have "?B = (subtree (RAG s) (Th th)) \<inter> {Th th' | th'. True}" |
|
2394 by auto |
|
2395 moreover have "... \<subseteq> (subtree (RAG s) (Th th))" by auto |
|
2396 moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) |
|
2397 ultimately show ?thesis by auto |
|
2398 qed |
|
2399 ultimately show ?thesis by auto |
|
2400 qed |
|
2401 |
|
2402 lemma le_cp: |
|
2403 shows "preced th s \<le> cp s th" |
|
2404 proof(unfold cp_alt_def, rule Max_ge) |
|
2405 show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
2406 by (simp add: finite_subtree_threads) |
|
2407 next |
|
2408 show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
2409 by (simp add: subtree_def the_preced_def) |
|
2410 qed |
|
2411 |
|
2412 lemma finite_threads: |
|
2413 shows "finite (threads s)" |
|
2414 using vt by (induct) (auto elim: step.cases) |
|
2415 |
|
2416 lemma cp_le: |
|
2417 assumes th_in: "th \<in> threads s" |
|
2418 shows "cp s th \<le> Max (the_preced s ` threads s)" |
|
2419 proof(unfold cp_alt_def, rule Max_f_mono) |
|
2420 show "finite (threads s)" by (simp add: finite_threads) |
|
2421 next |
|
2422 show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}" |
|
2423 using subtree_def by fastforce |
|
2424 next |
|
2425 show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s" |
|
2426 using assms |
|
2427 by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq |
|
2428 node.inject(1) rtranclD subsetI subtree_def trancl_domain) |
|
2429 qed |
|
2430 |
|
2431 lemma max_cp_eq: |
|
2432 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" |
|
2433 (is "?L = ?R") |
|
2434 proof - |
|
2435 have "?L \<le> ?R" |
|
2436 proof(cases "threads s = {}") |
|
2437 case False |
|
2438 show ?thesis |
|
2439 by (rule Max.boundedI, |
|
2440 insert cp_le, |
|
2441 auto simp:finite_threads False) |
|
2442 qed auto |
|
2443 moreover have "?R \<le> ?L" |
|
2444 by (rule Max_fg_mono, |
|
2445 simp add: finite_threads, |
|
2446 simp add: le_cp the_preced_def) |
|
2447 ultimately show ?thesis by auto |
|
2448 qed |
|
2449 |
|
2450 lemma chain_building: |
|
2451 assumes "node \<in> Domain (RAG s)" |
|
2452 obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+" |
|
2453 proof - |
|
2454 from assms have "node \<in> Range ((RAG s)^-1)" by auto |
|
2455 from wf_base[OF wf_RAG_converse this] |
|
2456 obtain b where h_b: "(b, node) \<in> ((RAG s)\<inverse>)\<^sup>+" "\<forall>c. (c, b) \<notin> (RAG s)\<inverse>" by auto |
|
2457 obtain th' where eq_b: "b = Th th'" |
|
2458 proof(cases b) |
|
2459 case (Cs cs) |
|
2460 from h_b(1)[unfolded trancl_converse] |
|
2461 have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto |
|
2462 from tranclE[OF this] |
|
2463 obtain n where "(n, b) \<in> RAG s" by auto |
|
2464 from this[unfolded Cs] |
|
2465 obtain th1 where "waiting s th1 cs" |
|
2466 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
2467 from waiting_holding[OF this] |
|
2468 obtain th2 where "holding s th2 cs" . |
|
2469 hence "(Cs cs, Th th2) \<in> RAG s" |
|
2470 by (unfold s_RAG_def, fold holding_eq, auto) |
|
2471 with h_b(2)[unfolded Cs, rule_format] |
|
2472 have False by auto |
|
2473 thus ?thesis by auto |
|
2474 qed auto |
|
2475 have "th' \<in> readys s" |
|
2476 proof - |
|
2477 from h_b(2)[unfolded eq_b] |
|
2478 have "\<forall>cs. \<not> waiting s th' cs" |
|
2479 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
2480 moreover have "th' \<in> threads s" |
|
2481 proof(rule rg_RAG_threads) |
|
2482 from tranclD[OF h_b(1), unfolded eq_b] |
|
2483 obtain z where "(z, Th th') \<in> (RAG s)" by auto |
|
2484 thus "Th th' \<in> Range (RAG s)" by auto |
|
2485 qed |
|
2486 ultimately show ?thesis by (auto simp:readys_def) |
|
2487 qed |
|
2488 moreover have "(node, Th th') \<in> (RAG s)^+" |
|
2489 using h_b(1)[unfolded trancl_converse] eq_b by auto |
|
2490 ultimately show ?thesis using that by metis |
|
2491 qed |
|
2492 |
|
2493 text {* \noindent |
|
2494 The following is just an instance of @{text "chain_building"}. |
|
2495 *} |
|
2496 lemma th_chain_to_ready: |
|
2497 assumes th_in: "th \<in> threads s" |
|
2498 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)" |
|
2499 proof(cases "th \<in> readys s") |
|
2500 case True |
|
2501 thus ?thesis by auto |
|
2502 next |
|
2503 case False |
|
2504 from False and th_in have "Th th \<in> Domain (RAG s)" |
|
2505 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) |
|
2506 from chain_building [rule_format, OF this] |
|
2507 show ?thesis by auto |
|
2508 qed |
|
2509 |
|
2510 end |
|
2511 |
|
2512 lemma count_rec1 [simp]: |
|
2513 assumes "Q e" |
|
2514 shows "count Q (e#es) = Suc (count Q es)" |
|
2515 using assms |
|
2516 by (unfold count_def, auto) |
|
2517 |
|
2518 lemma count_rec2 [simp]: |
|
2519 assumes "\<not>Q e" |
|
2520 shows "count Q (e#es) = (count Q es)" |
|
2521 using assms |
|
2522 by (unfold count_def, auto) |
|
2523 |
|
2524 lemma count_rec3 [simp]: |
|
2525 shows "count Q [] = 0" |
|
2526 by (unfold count_def, auto) |
|
2527 |
|
2528 lemma cntP_simp1[simp]: |
|
2529 "cntP (P th cs'#s) th = cntP s th + 1" |
|
2530 by (unfold cntP_def, simp) |
|
2531 |
|
2532 lemma cntP_simp2[simp]: |
|
2533 assumes "th' \<noteq> th" |
|
2534 shows "cntP (P th cs'#s) th' = cntP s th'" |
|
2535 using assms |
|
2536 by (unfold cntP_def, simp) |
|
2537 |
|
2538 lemma cntP_simp3[simp]: |
|
2539 assumes "\<not> isP e" |
|
2540 shows "cntP (e#s) th' = cntP s th'" |
|
2541 using assms |
|
2542 by (unfold cntP_def, cases e, simp+) |
|
2543 |
|
2544 lemma cntV_simp1[simp]: |
|
2545 "cntV (V th cs'#s) th = cntV s th + 1" |
|
2546 by (unfold cntV_def, simp) |
|
2547 |
|
2548 lemma cntV_simp2[simp]: |
|
2549 assumes "th' \<noteq> th" |
|
2550 shows "cntV (V th cs'#s) th' = cntV s th'" |
|
2551 using assms |
|
2552 by (unfold cntV_def, simp) |
|
2553 |
|
2554 lemma cntV_simp3[simp]: |
|
2555 assumes "\<not> isV e" |
|
2556 shows "cntV (e#s) th' = cntV s th'" |
|
2557 using assms |
|
2558 by (unfold cntV_def, cases e, simp+) |
|
2559 |
|
2560 lemma cntP_diff_inv: |
|
2561 assumes "cntP (e#s) th \<noteq> cntP s th" |
|
2562 shows "isP e \<and> actor e = th" |
|
2563 proof(cases e) |
|
2564 case (P th' pty) |
|
2565 show ?thesis |
|
2566 by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", |
|
2567 insert assms P, auto simp:cntP_def) |
|
2568 qed (insert assms, auto simp:cntP_def) |
|
2569 |
|
2570 lemma cntV_diff_inv: |
|
2571 assumes "cntV (e#s) th \<noteq> cntV s th" |
|
2572 shows "isV e \<and> actor e = th" |
|
2573 proof(cases e) |
|
2574 case (V th' pty) |
|
2575 show ?thesis |
|
2576 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", |
|
2577 insert assms V, auto simp:cntV_def) |
|
2578 qed (insert assms, auto simp:cntV_def) |
|
2579 |
|
2580 lemma children_RAG_alt_def: |
|
2581 "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}" |
|
2582 by (unfold s_RAG_def, auto simp:children_def holding_eq) |
|
2583 |
|
2584 lemma holdents_alt_def: |
|
2585 "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))" |
|
2586 by (unfold children_RAG_alt_def holdents_def, simp add: image_image) |
|
2587 |
|
2588 lemma cntCS_alt_def: |
|
2589 "cntCS s th = card (children (RAG s) (Th th))" |
|
2590 apply (unfold children_RAG_alt_def cntCS_def holdents_def) |
|
2591 by (rule card_image[symmetric], auto simp:inj_on_def) |
|
2592 |
|
2593 |
|
2594 context valid_trace_p_w |
|
2595 begin |
|
2596 |
|
2597 lemma holding_s_holder: "holding s holder cs" |
|
2598 by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) |
|
2599 |
|
2600 lemma holding_es_holder: "holding (e#s) holder cs" |
|
2601 by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto) |
|
2602 |
|
2603 lemma holdents_es: |
|
2604 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
2605 proof - |
|
2606 { fix cs' |
|
2607 assume "cs' \<in> ?L" |
|
2608 hence h: "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
2609 have "holding s th' cs'" |
|
2610 proof(cases "cs' = cs") |
|
2611 case True |
|
2612 from held_unique[OF h[unfolded True] holding_es_holder] |
|
2613 have "th' = holder" . |
|
2614 thus ?thesis |
|
2615 by (unfold True holdents_def, insert holding_s_holder, simp) |
|
2616 next |
|
2617 case False |
|
2618 hence "wq (e#s) cs' = wq s cs'" by simp |
|
2619 from h[unfolded s_holding_def, folded wq_def, unfolded this] |
|
2620 show ?thesis |
|
2621 by (unfold s_holding_def, fold wq_def, auto) |
|
2622 qed |
|
2623 hence "cs' \<in> ?R" by (auto simp:holdents_def) |
|
2624 } moreover { |
|
2625 fix cs' |
|
2626 assume "cs' \<in> ?R" |
|
2627 hence h: "holding s th' cs'" by (auto simp:holdents_def) |
|
2628 have "holding (e#s) th' cs'" |
|
2629 proof(cases "cs' = cs") |
|
2630 case True |
|
2631 from held_unique[OF h[unfolded True] holding_s_holder] |
|
2632 have "th' = holder" . |
|
2633 thus ?thesis |
|
2634 by (unfold True holdents_def, insert holding_es_holder, simp) |
|
2635 next |
|
2636 case False |
|
2637 hence "wq s cs' = wq (e#s) cs'" by simp |
|
2638 from h[unfolded s_holding_def, folded wq_def, unfolded this] |
|
2639 show ?thesis |
|
2640 by (unfold s_holding_def, fold wq_def, auto) |
|
2641 qed |
|
2642 hence "cs' \<in> ?L" by (auto simp:holdents_def) |
|
2643 } ultimately show ?thesis by auto |
|
2644 qed |
|
2645 |
|
2646 lemma cntCS_es_th[simp]: "cntCS (e#s) th' = cntCS s th'" |
|
2647 by (unfold cntCS_def holdents_es, simp) |
|
2648 |
|
2649 lemma th_not_ready_es: |
|
2650 shows "th \<notin> readys (e#s)" |
|
2651 using waiting_es_th_cs |
|
2652 by (unfold readys_def, auto) |
|
2653 |
|
2654 end |
|
2655 |
|
2656 lemma (in valid_trace) finite_holdents: "finite (holdents s th)" |
|
2657 by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto) |
|
2658 |
|
2659 context valid_trace_p_h |
|
2660 begin |
|
2661 |
|
2662 lemma th_not_waiting': |
|
2663 "\<not> waiting (e#s) th cs'" |
|
2664 proof(cases "cs' = cs") |
|
2665 case True |
|
2666 show ?thesis |
|
2667 by (unfold True s_waiting_def, fold wq_def, unfold wq_es_cs', auto) |
|
2668 next |
|
2669 case False |
|
2670 from th_not_waiting[of cs', unfolded s_waiting_def, folded wq_def] |
|
2671 show ?thesis |
|
2672 by (unfold s_waiting_def, fold wq_def, insert False, simp) |
|
2673 qed |
|
2674 |
|
2675 lemma ready_th_es: |
|
2676 shows "th \<in> readys (e#s)" |
|
2677 using th_not_waiting' |
|
2678 by (unfold readys_def, insert live_th_es, auto) |
|
2679 |
|
2680 lemma holdents_es_th: |
|
2681 "holdents (e#s) th = (holdents s th) \<union> {cs}" (is "?L = ?R") |
|
2682 proof - |
|
2683 { fix cs' |
|
2684 assume "cs' \<in> ?L" |
|
2685 hence "holding (e#s) th cs'" |
|
2686 by (unfold holdents_def, auto) |
|
2687 hence "cs' \<in> ?R" |
|
2688 by (cases rule:holding_esE, auto simp:holdents_def) |
|
2689 } moreover { |
|
2690 fix cs' |
|
2691 assume "cs' \<in> ?R" |
|
2692 hence "holding s th cs' \<or> cs' = cs" |
|
2693 by (auto simp:holdents_def) |
|
2694 hence "cs' \<in> ?L" |
|
2695 proof |
|
2696 assume "holding s th cs'" |
|
2697 from holding_kept[OF this] |
|
2698 show ?thesis by (auto simp:holdents_def) |
|
2699 next |
|
2700 assume "cs' = cs" |
|
2701 thus ?thesis using holding_es_th_cs |
|
2702 by (unfold holdents_def, auto) |
|
2703 qed |
|
2704 } ultimately show ?thesis by auto |
|
2705 qed |
|
2706 |
|
2707 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" |
|
2708 proof - |
|
2709 have "card (holdents s th \<union> {cs}) = card (holdents s th) + 1" |
|
2710 proof(subst card_Un_disjoint) |
|
2711 show "holdents s th \<inter> {cs} = {}" |
|
2712 using not_holding_s_th_cs by (auto simp:holdents_def) |
|
2713 qed (auto simp:finite_holdents) |
|
2714 thus ?thesis |
|
2715 by (unfold cntCS_def holdents_es_th, simp) |
|
2716 qed |
|
2717 |
|
2718 lemma no_holder: |
|
2719 "\<not> holding s th' cs" |
|
2720 proof |
|
2721 assume otherwise: "holding s th' cs" |
|
2722 from this[unfolded s_holding_def, folded wq_def, unfolded we] |
|
2723 show False by auto |
|
2724 qed |
|
2725 |
|
2726 lemma holdents_es_th': |
|
2727 assumes "th' \<noteq> th" |
|
2728 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
2729 proof - |
|
2730 { fix cs' |
|
2731 assume "cs' \<in> ?L" |
|
2732 hence h_e: "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
2733 have "cs' \<noteq> cs" |
|
2734 proof |
|
2735 assume "cs' = cs" |
|
2736 from held_unique[OF h_e[unfolded this] holding_es_th_cs] |
|
2737 have "th' = th" . |
|
2738 with assms show False by simp |
|
2739 qed |
|
2740 from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]] |
|
2741 have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" . |
|
2742 hence "cs' \<in> ?R" |
|
2743 by (unfold holdents_def s_holding_def, fold wq_def, auto) |
|
2744 } moreover { |
|
2745 fix cs' |
|
2746 assume "cs' \<in> ?R" |
|
2747 hence "holding s th' cs'" by (auto simp:holdents_def) |
|
2748 from holding_kept[OF this] |
|
2749 have "holding (e # s) th' cs'" . |
|
2750 hence "cs' \<in> ?L" |
|
2751 by (unfold holdents_def, auto) |
|
2752 } ultimately show ?thesis by auto |
|
2753 qed |
|
2754 |
|
2755 lemma cntCS_es_th'[simp]: |
|
2756 assumes "th' \<noteq> th" |
|
2757 shows "cntCS (e#s) th' = cntCS s th'" |
|
2758 by (unfold cntCS_def holdents_es_th'[OF assms], simp) |
|
2759 |
|
2760 end |
|
2761 |
|
2762 context valid_trace_p |
|
2763 begin |
|
2764 |
|
2765 lemma readys_kept1: |
|
2766 assumes "th' \<noteq> th" |
|
2767 and "th' \<in> readys (e#s)" |
|
2768 shows "th' \<in> readys s" |
|
2769 proof - |
|
2770 { fix cs' |
|
2771 assume wait: "waiting s th' cs'" |
|
2772 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
2773 using assms(2)[unfolded readys_def] by auto |
|
2774 have False |
|
2775 proof(cases "cs' = cs") |
|
2776 case False |
|
2777 with n_wait wait |
|
2778 show ?thesis |
|
2779 by (unfold s_waiting_def, fold wq_def, auto) |
|
2780 next |
|
2781 case True |
|
2782 show ?thesis |
|
2783 proof(cases "wq s cs = []") |
|
2784 case True |
|
2785 then interpret vt: valid_trace_p_h |
|
2786 by (unfold_locales, simp) |
|
2787 show ?thesis using n_wait wait waiting_kept by auto |
|
2788 next |
|
2789 case False |
|
2790 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
2791 show ?thesis using n_wait wait waiting_kept by blast |
|
2792 qed |
|
2793 qed |
|
2794 } with assms(2) show ?thesis |
|
2795 by (unfold readys_def, auto) |
|
2796 qed |
|
2797 |
|
2798 lemma readys_kept2: |
|
2799 assumes "th' \<noteq> th" |
|
2800 and "th' \<in> readys s" |
|
2801 shows "th' \<in> readys (e#s)" |
|
2802 proof - |
|
2803 { fix cs' |
|
2804 assume wait: "waiting (e#s) th' cs'" |
|
2805 have n_wait: "\<not> waiting s th' cs'" |
|
2806 using assms(2)[unfolded readys_def] by auto |
|
2807 have False |
|
2808 proof(cases "cs' = cs") |
|
2809 case False |
|
2810 with n_wait wait |
|
2811 show ?thesis |
|
2812 by (unfold s_waiting_def, fold wq_def, auto) |
|
2813 next |
|
2814 case True |
|
2815 show ?thesis |
|
2816 proof(cases "wq s cs = []") |
|
2817 case True |
|
2818 then interpret vt: valid_trace_p_h |
|
2819 by (unfold_locales, simp) |
|
2820 show ?thesis using n_wait vt.waiting_esE wait by blast |
|
2821 next |
|
2822 case False |
|
2823 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
2824 show ?thesis using assms(1) n_wait vt.waiting_esE wait by auto |
|
2825 qed |
|
2826 qed |
|
2827 } with assms(2) show ?thesis |
|
2828 by (unfold readys_def, auto) |
|
2829 qed |
|
2830 |
|
2831 lemma readys_simp [simp]: |
|
2832 assumes "th' \<noteq> th" |
|
2833 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
2834 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
2835 by metis |
|
2836 |
|
2837 lemma cnp_cnv_cncs_kept: (* ddd *) |
|
2838 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
2839 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
2840 proof(cases "th' = th") |
|
2841 case True |
|
2842 note eq_th' = this |
|
2843 show ?thesis |
|
2844 proof(cases "wq s cs = []") |
|
2845 case True |
|
2846 then interpret vt: valid_trace_p_h by (unfold_locales, simp) |
|
2847 show ?thesis |
|
2848 using assms eq_th' is_p ready_th_s vt.cntCS_es_th vt.ready_th_es pvD_def by auto |
|
2849 next |
|
2850 case False |
|
2851 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
2852 show ?thesis |
|
2853 using add.commute add.left_commute assms eq_th' is_p live_th_s |
|
2854 ready_th_s vt.th_not_ready_es pvD_def |
|
2855 apply (auto) |
|
2856 by (fold is_p, simp) |
|
2857 qed |
|
2858 next |
|
2859 case False |
|
2860 note h_False = False |
|
2861 thus ?thesis |
|
2862 proof(cases "wq s cs = []") |
|
2863 case True |
|
2864 then interpret vt: valid_trace_p_h by (unfold_locales, simp) |
|
2865 show ?thesis using assms |
|
2866 by (insert True h_False pvD_def, auto split:if_splits,unfold is_p, auto) |
|
2867 next |
|
2868 case False |
|
2869 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
2870 show ?thesis using assms |
|
2871 by (insert False h_False pvD_def, auto split:if_splits,unfold is_p, auto) |
|
2872 qed |
|
2873 qed |
|
2874 |
|
2875 end |
|
2876 |
|
2877 |
|
2878 context valid_trace_v |
|
2879 begin |
|
2880 |
|
2881 lemma holding_th_cs_s: |
|
2882 "holding s th cs" |
|
2883 by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) |
|
2884 |
|
2885 lemma th_ready_s [simp]: "th \<in> readys s" |
|
2886 using runing_th_s |
|
2887 by (unfold runing_def readys_def, auto) |
|
2888 |
|
2889 lemma th_live_s [simp]: "th \<in> threads s" |
|
2890 using th_ready_s by (unfold readys_def, auto) |
|
2891 |
|
2892 lemma th_ready_es [simp]: "th \<in> readys (e#s)" |
|
2893 using runing_th_s neq_t_th |
|
2894 by (unfold is_v runing_def readys_def, auto) |
|
2895 |
|
2896 lemma th_live_es [simp]: "th \<in> threads (e#s)" |
|
2897 using th_ready_es by (unfold readys_def, auto) |
|
2898 |
|
2899 lemma pvD_th_s[simp]: "pvD s th = 0" |
|
2900 by (unfold pvD_def, simp) |
|
2901 |
|
2902 lemma pvD_th_es[simp]: "pvD (e#s) th = 0" |
|
2903 by (unfold pvD_def, simp) |
|
2904 |
|
2905 lemma cntCS_s_th [simp]: "cntCS s th > 0" |
|
2906 proof - |
|
2907 have "cs \<in> holdents s th" using holding_th_cs_s |
|
2908 by (unfold holdents_def, simp) |
|
2909 moreover have "finite (holdents s th)" using finite_holdents (* ccc *) |
|
2910 by simp |
|
2911 ultimately show ?thesis |
|
2912 by (unfold cntCS_def, |
|
2913 auto intro!:card_gt_0_iff[symmetric, THEN iffD1]) |
|
2914 qed |
|
2915 |
|
2916 end |
|
2917 |
|
2918 context valid_trace_v_n |
|
2919 begin |
|
2920 |
|
2921 lemma not_ready_taker_s[simp]: |
|
2922 "taker \<notin> readys s" |
|
2923 using waiting_taker |
|
2924 by (unfold readys_def, auto) |
|
2925 |
|
2926 lemma taker_live_s [simp]: "taker \<in> threads s" |
|
2927 proof - |
|
2928 have "taker \<in> set wq'" by (simp add: eq_wq') |
|
2929 from th'_in_inv[OF this] |
|
2930 have "taker \<in> set rest" . |
|
2931 hence "taker \<in> set (wq s cs)" by (simp add: wq_s_cs) |
|
2932 thus ?thesis using wq_threads by auto |
|
2933 qed |
|
2934 |
|
2935 lemma taker_live_es [simp]: "taker \<in> threads (e#s)" |
|
2936 using taker_live_s threads_es by blast |
|
2937 |
|
2938 lemma taker_ready_es [simp]: |
|
2939 shows "taker \<in> readys (e#s)" |
|
2940 proof - |
|
2941 { fix cs' |
|
2942 assume "waiting (e#s) taker cs'" |
|
2943 hence False |
|
2944 proof(cases rule:waiting_esE) |
|
2945 case 1 |
|
2946 thus ?thesis using waiting_taker waiting_unique by auto |
|
2947 qed simp |
|
2948 } thus ?thesis by (unfold readys_def, auto) |
|
2949 qed |
|
2950 |
|
2951 lemma neq_taker_th: "taker \<noteq> th" |
|
2952 using th_not_waiting waiting_taker by blast |
|
2953 |
|
2954 lemma not_holding_taker_s_cs: |
|
2955 shows "\<not> holding s taker cs" |
|
2956 using holding_cs_eq_th neq_taker_th by auto |
|
2957 |
|
2958 lemma holdents_es_taker: |
|
2959 "holdents (e#s) taker = holdents s taker \<union> {cs}" (is "?L = ?R") |
|
2960 proof - |
|
2961 { fix cs' |
|
2962 assume "cs' \<in> ?L" |
|
2963 hence "holding (e#s) taker cs'" by (auto simp:holdents_def) |
|
2964 hence "cs' \<in> ?R" |
|
2965 proof(cases rule:holding_esE) |
|
2966 case 2 |
|
2967 thus ?thesis by (auto simp:holdents_def) |
|
2968 qed auto |
|
2969 } moreover { |
|
2970 fix cs' |
|
2971 assume "cs' \<in> ?R" |
|
2972 hence "holding s taker cs' \<or> cs' = cs" by (auto simp:holdents_def) |
|
2973 hence "cs' \<in> ?L" |
|
2974 proof |
|
2975 assume "holding s taker cs'" |
|
2976 hence "holding (e#s) taker cs'" |
|
2977 using holding_esI2 holding_taker by fastforce |
|
2978 thus ?thesis by (auto simp:holdents_def) |
|
2979 next |
|
2980 assume "cs' = cs" |
|
2981 with holding_taker |
|
2982 show ?thesis by (auto simp:holdents_def) |
|
2983 qed |
|
2984 } ultimately show ?thesis by auto |
|
2985 qed |
|
2986 |
|
2987 lemma cntCS_es_taker [simp]: "cntCS (e#s) taker = cntCS s taker + 1" |
|
2988 proof - |
|
2989 have "card (holdents s taker \<union> {cs}) = card (holdents s taker) + 1" |
|
2990 proof(subst card_Un_disjoint) |
|
2991 show "holdents s taker \<inter> {cs} = {}" |
|
2992 using not_holding_taker_s_cs by (auto simp:holdents_def) |
|
2993 qed (auto simp:finite_holdents) |
|
2994 thus ?thesis |
|
2995 by (unfold cntCS_def, insert holdents_es_taker, simp) |
|
2996 qed |
|
2997 |
|
2998 lemma pvD_taker_s[simp]: "pvD s taker = 1" |
|
2999 by (unfold pvD_def, simp) |
|
3000 |
|
3001 lemma pvD_taker_es[simp]: "pvD (e#s) taker = 0" |
|
3002 by (unfold pvD_def, simp) |
|
3003 |
|
3004 lemma pvD_th_s[simp]: "pvD s th = 0" |
|
3005 by (unfold pvD_def, simp) |
|
3006 |
|
3007 lemma pvD_th_es[simp]: "pvD (e#s) th = 0" |
|
3008 by (unfold pvD_def, simp) |
|
3009 |
|
3010 lemma holdents_es_th: |
|
3011 "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R") |
|
3012 proof - |
|
3013 { fix cs' |
|
3014 assume "cs' \<in> ?L" |
|
3015 hence "holding (e#s) th cs'" by (auto simp:holdents_def) |
|
3016 hence "cs' \<in> ?R" |
|
3017 proof(cases rule:holding_esE) |
|
3018 case 2 |
|
3019 thus ?thesis by (auto simp:holdents_def) |
|
3020 qed (insert neq_taker_th, auto) |
|
3021 } moreover { |
|
3022 fix cs' |
|
3023 assume "cs' \<in> ?R" |
|
3024 hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def) |
|
3025 from holding_esI2[OF this] |
|
3026 have "cs' \<in> ?L" by (auto simp:holdents_def) |
|
3027 } ultimately show ?thesis by auto |
|
3028 qed |
|
3029 |
|
3030 lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1" |
|
3031 proof - |
|
3032 have "card (holdents s th - {cs}) = card (holdents s th) - 1" |
|
3033 proof - |
|
3034 have "cs \<in> holdents s th" using holding_th_cs_s |
|
3035 by (auto simp:holdents_def) |
|
3036 moreover have "finite (holdents s th)" |
|
3037 by (simp add: finite_holdents) |
|
3038 ultimately show ?thesis by auto |
|
3039 qed |
|
3040 thus ?thesis by (unfold cntCS_def holdents_es_th) |
|
3041 qed |
|
3042 |
|
3043 lemma holdents_kept: |
|
3044 assumes "th' \<noteq> taker" |
|
3045 and "th' \<noteq> th" |
|
3046 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3047 proof - |
|
3048 { fix cs' |
|
3049 assume h: "cs' \<in> ?L" |
|
3050 have "cs' \<in> ?R" |
|
3051 proof(cases "cs' = cs") |
|
3052 case False |
|
3053 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3054 from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
3055 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3056 show ?thesis |
|
3057 by (unfold holdents_def s_holding_def, fold wq_def, auto) |
|
3058 next |
|
3059 case True |
|
3060 from h[unfolded this] |
|
3061 have "holding (e#s) th' cs" by (auto simp:holdents_def) |
|
3062 from held_unique[OF this holding_taker] |
|
3063 have "th' = taker" . |
|
3064 with assms show ?thesis by auto |
|
3065 qed |
|
3066 } moreover { |
|
3067 fix cs' |
|
3068 assume h: "cs' \<in> ?R" |
|
3069 have "cs' \<in> ?L" |
|
3070 proof(cases "cs' = cs") |
|
3071 case False |
|
3072 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3073 from h have "holding s th' cs'" by (auto simp:holdents_def) |
|
3074 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3075 show ?thesis |
|
3076 by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) |
|
3077 next |
|
3078 case True |
|
3079 from h[unfolded this] |
|
3080 have "holding s th' cs" by (auto simp:holdents_def) |
|
3081 from held_unique[OF this holding_th_cs_s] |
|
3082 have "th' = th" . |
|
3083 with assms show ?thesis by auto |
|
3084 qed |
|
3085 } ultimately show ?thesis by auto |
|
3086 qed |
|
3087 |
|
3088 lemma cntCS_kept [simp]: |
|
3089 assumes "th' \<noteq> taker" |
|
3090 and "th' \<noteq> th" |
|
3091 shows "cntCS (e#s) th' = cntCS s th'" |
|
3092 by (unfold cntCS_def holdents_kept[OF assms], simp) |
|
3093 |
|
3094 lemma readys_kept1: |
|
3095 assumes "th' \<noteq> taker" |
|
3096 and "th' \<in> readys (e#s)" |
|
3097 shows "th' \<in> readys s" |
|
3098 proof - |
|
3099 { fix cs' |
|
3100 assume wait: "waiting s th' cs'" |
|
3101 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3102 using assms(2)[unfolded readys_def] by auto |
|
3103 have False |
|
3104 proof(cases "cs' = cs") |
|
3105 case False |
|
3106 with n_wait wait |
|
3107 show ?thesis |
|
3108 by (unfold s_waiting_def, fold wq_def, auto) |
|
3109 next |
|
3110 case True |
|
3111 have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" |
|
3112 using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . |
|
3113 moreover have "\<not> (th' \<in> set rest \<and> th' \<noteq> hd (taker # rest'))" |
|
3114 using n_wait[unfolded True s_waiting_def, folded wq_def, |
|
3115 unfolded wq_es_cs set_wq', unfolded eq_wq'] . |
|
3116 ultimately have "th' = taker" by auto |
|
3117 with assms(1) |
|
3118 show ?thesis by simp |
|
3119 qed |
|
3120 } with assms(2) show ?thesis |
|
3121 by (unfold readys_def, auto) |
|
3122 qed |
|
3123 |
|
3124 lemma readys_kept2: |
|
3125 assumes "th' \<noteq> taker" |
|
3126 and "th' \<in> readys s" |
|
3127 shows "th' \<in> readys (e#s)" |
|
3128 proof - |
|
3129 { fix cs' |
|
3130 assume wait: "waiting (e#s) th' cs'" |
|
3131 have n_wait: "\<not> waiting s th' cs'" |
|
3132 using assms(2)[unfolded readys_def] by auto |
|
3133 have False |
|
3134 proof(cases "cs' = cs") |
|
3135 case False |
|
3136 with n_wait wait |
|
3137 show ?thesis |
|
3138 by (unfold s_waiting_def, fold wq_def, auto) |
|
3139 next |
|
3140 case True |
|
3141 have "th' \<in> set rest \<and> th' \<noteq> hd (taker # rest')" |
|
3142 using wait [unfolded True s_waiting_def, folded wq_def, |
|
3143 unfolded wq_es_cs set_wq', unfolded eq_wq'] . |
|
3144 moreover have "\<not> (th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest))" |
|
3145 using n_wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . |
|
3146 ultimately have "th' = taker" by auto |
|
3147 with assms(1) |
|
3148 show ?thesis by simp |
|
3149 qed |
|
3150 } with assms(2) show ?thesis |
|
3151 by (unfold readys_def, auto) |
|
3152 qed |
|
3153 |
|
3154 lemma readys_simp [simp]: |
|
3155 assumes "th' \<noteq> taker" |
|
3156 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3157 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3158 by metis |
|
3159 |
|
3160 lemma cnp_cnv_cncs_kept: |
|
3161 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3162 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3163 proof - |
|
3164 { assume eq_th': "th' = taker" |
|
3165 have ?thesis |
|
3166 apply (unfold eq_th' pvD_taker_es cntCS_es_taker) |
|
3167 by (insert neq_taker_th assms[unfolded eq_th'], unfold is_v, simp) |
|
3168 } moreover { |
|
3169 assume eq_th': "th' = th" |
|
3170 have ?thesis |
|
3171 apply (unfold eq_th' pvD_th_es cntCS_es_th) |
|
3172 by (insert assms[unfolded eq_th'], unfold is_v, simp) |
|
3173 } moreover { |
|
3174 assume h: "th' \<noteq> taker" "th' \<noteq> th" |
|
3175 have ?thesis using assms |
|
3176 apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp) |
|
3177 by (fold is_v, unfold pvD_def, simp) |
|
3178 } ultimately show ?thesis by metis |
|
3179 qed |
|
3180 |
|
3181 end |
|
3182 |
|
3183 context valid_trace_v_e |
|
3184 begin |
|
3185 |
|
3186 lemma holdents_es_th: |
|
3187 "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R") |
|
3188 proof - |
|
3189 { fix cs' |
|
3190 assume "cs' \<in> ?L" |
|
3191 hence "holding (e#s) th cs'" by (auto simp:holdents_def) |
|
3192 hence "cs' \<in> ?R" |
|
3193 proof(cases rule:holding_esE) |
|
3194 case 1 |
|
3195 thus ?thesis by (auto simp:holdents_def) |
|
3196 qed |
|
3197 } moreover { |
|
3198 fix cs' |
|
3199 assume "cs' \<in> ?R" |
|
3200 hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def) |
|
3201 from holding_esI2[OF this] |
|
3202 have "cs' \<in> ?L" by (auto simp:holdents_def) |
|
3203 } ultimately show ?thesis by auto |
|
3204 qed |
|
3205 |
|
3206 lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1" |
|
3207 proof - |
|
3208 have "card (holdents s th - {cs}) = card (holdents s th) - 1" |
|
3209 proof - |
|
3210 have "cs \<in> holdents s th" using holding_th_cs_s |
|
3211 by (auto simp:holdents_def) |
|
3212 moreover have "finite (holdents s th)" |
|
3213 by (simp add: finite_holdents) |
|
3214 ultimately show ?thesis by auto |
|
3215 qed |
|
3216 thus ?thesis by (unfold cntCS_def holdents_es_th) |
|
3217 qed |
|
3218 |
|
3219 lemma holdents_kept: |
|
3220 assumes "th' \<noteq> th" |
|
3221 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3222 proof - |
|
3223 { fix cs' |
|
3224 assume h: "cs' \<in> ?L" |
|
3225 have "cs' \<in> ?R" |
|
3226 proof(cases "cs' = cs") |
|
3227 case False |
|
3228 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3229 from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
3230 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3231 show ?thesis |
|
3232 by (unfold holdents_def s_holding_def, fold wq_def, auto) |
|
3233 next |
|
3234 case True |
|
3235 from h[unfolded this] |
|
3236 have "holding (e#s) th' cs" by (auto simp:holdents_def) |
|
3237 from this[unfolded s_holding_def, folded wq_def, |
|
3238 unfolded wq_es_cs nil_wq'] |
|
3239 show ?thesis by auto |
|
3240 qed |
|
3241 } moreover { |
|
3242 fix cs' |
|
3243 assume h: "cs' \<in> ?R" |
|
3244 have "cs' \<in> ?L" |
|
3245 proof(cases "cs' = cs") |
|
3246 case False |
|
3247 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3248 from h have "holding s th' cs'" by (auto simp:holdents_def) |
|
3249 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3250 show ?thesis |
|
3251 by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) |
|
3252 next |
|
3253 case True |
|
3254 from h[unfolded this] |
|
3255 have "holding s th' cs" by (auto simp:holdents_def) |
|
3256 from held_unique[OF this holding_th_cs_s] |
|
3257 have "th' = th" . |
|
3258 with assms show ?thesis by auto |
|
3259 qed |
|
3260 } ultimately show ?thesis by auto |
|
3261 qed |
|
3262 |
|
3263 lemma cntCS_kept [simp]: |
|
3264 assumes "th' \<noteq> th" |
|
3265 shows "cntCS (e#s) th' = cntCS s th'" |
|
3266 by (unfold cntCS_def holdents_kept[OF assms], simp) |
|
3267 |
|
3268 lemma readys_kept1: |
|
3269 assumes "th' \<in> readys (e#s)" |
|
3270 shows "th' \<in> readys s" |
|
3271 proof - |
|
3272 { fix cs' |
|
3273 assume wait: "waiting s th' cs'" |
|
3274 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3275 using assms(1)[unfolded readys_def] by auto |
|
3276 have False |
|
3277 proof(cases "cs' = cs") |
|
3278 case False |
|
3279 with n_wait wait |
|
3280 show ?thesis |
|
3281 by (unfold s_waiting_def, fold wq_def, auto) |
|
3282 next |
|
3283 case True |
|
3284 have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" |
|
3285 using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . |
|
3286 hence "th' \<in> set rest" by auto |
|
3287 with set_wq' have "th' \<in> set wq'" by metis |
|
3288 with nil_wq' show ?thesis by simp |
|
3289 qed |
|
3290 } thus ?thesis using assms |
|
3291 by (unfold readys_def, auto) |
|
3292 qed |
|
3293 |
|
3294 lemma readys_kept2: |
|
3295 assumes "th' \<in> readys s" |
|
3296 shows "th' \<in> readys (e#s)" |
|
3297 proof - |
|
3298 { fix cs' |
|
3299 assume wait: "waiting (e#s) th' cs'" |
|
3300 have n_wait: "\<not> waiting s th' cs'" |
|
3301 using assms[unfolded readys_def] by auto |
|
3302 have False |
|
3303 proof(cases "cs' = cs") |
|
3304 case False |
|
3305 with n_wait wait |
|
3306 show ?thesis |
|
3307 by (unfold s_waiting_def, fold wq_def, auto) |
|
3308 next |
|
3309 case True |
|
3310 have "th' \<in> set [] \<and> th' \<noteq> hd []" |
|
3311 using wait[unfolded True s_waiting_def, folded wq_def, |
|
3312 unfolded wq_es_cs nil_wq'] . |
|
3313 thus ?thesis by simp |
|
3314 qed |
|
3315 } with assms show ?thesis |
|
3316 by (unfold readys_def, auto) |
|
3317 qed |
|
3318 |
|
3319 lemma readys_simp [simp]: |
|
3320 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3321 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3322 by metis |
|
3323 |
|
3324 lemma cnp_cnv_cncs_kept: |
|
3325 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3326 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3327 proof - |
|
3328 { |
|
3329 assume eq_th': "th' = th" |
|
3330 have ?thesis |
|
3331 apply (unfold eq_th' pvD_th_es cntCS_es_th) |
|
3332 by (insert assms[unfolded eq_th'], unfold is_v, simp) |
|
3333 } moreover { |
|
3334 assume h: "th' \<noteq> th" |
|
3335 have ?thesis using assms |
|
3336 apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp) |
|
3337 by (fold is_v, unfold pvD_def, simp) |
|
3338 } ultimately show ?thesis by metis |
|
3339 qed |
|
3340 |
|
3341 end |
|
3342 |
|
3343 context valid_trace_v |
|
3344 begin |
|
3345 |
|
3346 lemma cnp_cnv_cncs_kept: |
|
3347 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3348 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3349 proof(cases "rest = []") |
|
3350 case True |
|
3351 then interpret vt: valid_trace_v_e by (unfold_locales, simp) |
|
3352 show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast |
|
3353 next |
|
3354 case False |
|
3355 then interpret vt: valid_trace_v_n by (unfold_locales, simp) |
|
3356 show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast |
|
3357 qed |
|
3358 |
|
3359 end |
|
3360 |
|
3361 context valid_trace_create |
|
3362 begin |
|
3363 |
|
3364 lemma th_not_live_s [simp]: "th \<notin> threads s" |
|
3365 proof - |
|
3366 from pip_e[unfolded is_create] |
|
3367 show ?thesis by (cases, simp) |
|
3368 qed |
|
3369 |
|
3370 lemma th_not_ready_s [simp]: "th \<notin> readys s" |
|
3371 using th_not_live_s by (unfold readys_def, simp) |
|
3372 |
|
3373 lemma th_live_es [simp]: "th \<in> threads (e#s)" |
|
3374 by (unfold is_create, simp) |
|
3375 |
|
3376 lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'" |
|
3377 proof |
|
3378 assume "waiting s th cs'" |
|
3379 from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3380 have "th \<in> set (wq s cs')" by auto |
|
3381 from wq_threads[OF this] have "th \<in> threads s" . |
|
3382 with th_not_live_s show False by simp |
|
3383 qed |
|
3384 |
|
3385 lemma not_holding_th_s [simp]: "\<not> holding s th cs'" |
|
3386 proof |
|
3387 assume "holding s th cs'" |
|
3388 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] |
|
3389 have "th \<in> set (wq s cs')" by auto |
|
3390 from wq_threads[OF this] have "th \<in> threads s" . |
|
3391 with th_not_live_s show False by simp |
|
3392 qed |
|
3393 |
|
3394 lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'" |
|
3395 proof |
|
3396 assume "waiting (e # s) th cs'" |
|
3397 from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3398 have "th \<in> set (wq s cs')" by auto |
|
3399 from wq_threads[OF this] have "th \<in> threads s" . |
|
3400 with th_not_live_s show False by simp |
|
3401 qed |
|
3402 |
|
3403 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'" |
|
3404 proof |
|
3405 assume "holding (e # s) th cs'" |
|
3406 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] |
|
3407 have "th \<in> set (wq s cs')" by auto |
|
3408 from wq_threads[OF this] have "th \<in> threads s" . |
|
3409 with th_not_live_s show False by simp |
|
3410 qed |
|
3411 |
|
3412 lemma ready_th_es [simp]: "th \<in> readys (e#s)" |
|
3413 by (simp add:readys_def) |
|
3414 |
|
3415 lemma holdents_th_s: "holdents s th = {}" |
|
3416 by (unfold holdents_def, auto) |
|
3417 |
|
3418 lemma holdents_th_es: "holdents (e#s) th = {}" |
|
3419 by (unfold holdents_def, auto) |
|
3420 |
|
3421 lemma cntCS_th_s [simp]: "cntCS s th = 0" |
|
3422 by (unfold cntCS_def, simp add:holdents_th_s) |
|
3423 |
|
3424 lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0" |
|
3425 by (unfold cntCS_def, simp add:holdents_th_es) |
|
3426 |
|
3427 lemma pvD_th_s [simp]: "pvD s th = 0" |
|
3428 by (unfold pvD_def, simp) |
|
3429 |
|
3430 lemma pvD_th_es [simp]: "pvD (e#s) th = 0" |
|
3431 by (unfold pvD_def, simp) |
|
3432 |
|
3433 lemma holdents_kept: |
|
3434 assumes "th' \<noteq> th" |
|
3435 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3436 proof - |
|
3437 { fix cs' |
|
3438 assume h: "cs' \<in> ?L" |
|
3439 hence "cs' \<in> ?R" |
|
3440 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3441 unfold wq_kept, auto) |
|
3442 } moreover { |
|
3443 fix cs' |
|
3444 assume h: "cs' \<in> ?R" |
|
3445 hence "cs' \<in> ?L" |
|
3446 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3447 unfold wq_kept, auto) |
|
3448 } ultimately show ?thesis by auto |
|
3449 qed |
|
3450 |
|
3451 lemma cntCS_kept [simp]: |
|
3452 assumes "th' \<noteq> th" |
|
3453 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R") |
|
3454 using holdents_kept[OF assms] |
|
3455 by (unfold cntCS_def, simp) |
|
3456 |
|
3457 lemma readys_kept1: |
|
3458 assumes "th' \<noteq> th" |
|
3459 and "th' \<in> readys (e#s)" |
|
3460 shows "th' \<in> readys s" |
|
3461 proof - |
|
3462 { fix cs' |
|
3463 assume wait: "waiting s th' cs'" |
|
3464 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3465 using assms by (auto simp:readys_def) |
|
3466 from wait[unfolded s_waiting_def, folded wq_def] |
|
3467 n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3468 have False by auto |
|
3469 } thus ?thesis using assms |
|
3470 by (unfold readys_def, auto) |
|
3471 qed |
|
3472 |
|
3473 lemma readys_kept2: |
|
3474 assumes "th' \<noteq> th" |
|
3475 and "th' \<in> readys s" |
|
3476 shows "th' \<in> readys (e#s)" |
|
3477 proof - |
|
3478 { fix cs' |
|
3479 assume wait: "waiting (e#s) th' cs'" |
|
3480 have n_wait: "\<not> waiting s th' cs'" |
|
3481 using assms(2) by (auto simp:readys_def) |
|
3482 from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3483 n_wait[unfolded s_waiting_def, folded wq_def] |
|
3484 have False by auto |
|
3485 } with assms show ?thesis |
|
3486 by (unfold readys_def, auto) |
|
3487 qed |
|
3488 |
|
3489 lemma readys_simp [simp]: |
|
3490 assumes "th' \<noteq> th" |
|
3491 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3492 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3493 by metis |
|
3494 |
|
3495 lemma pvD_kept [simp]: |
|
3496 assumes "th' \<noteq> th" |
|
3497 shows "pvD (e#s) th' = pvD s th'" |
|
3498 using assms |
|
3499 by (unfold pvD_def, simp) |
|
3500 |
|
3501 lemma cnp_cnv_cncs_kept: |
|
3502 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3503 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3504 proof - |
|
3505 { |
|
3506 assume eq_th': "th' = th" |
|
3507 have ?thesis using assms |
|
3508 by (unfold eq_th', simp, unfold is_create, simp) |
|
3509 } moreover { |
|
3510 assume h: "th' \<noteq> th" |
|
3511 hence ?thesis using assms |
|
3512 by (simp, simp add:is_create) |
|
3513 } ultimately show ?thesis by metis |
|
3514 qed |
|
3515 |
|
3516 end |
|
3517 |
|
3518 context valid_trace_exit |
|
3519 begin |
|
3520 |
|
3521 lemma th_live_s [simp]: "th \<in> threads s" |
|
3522 proof - |
|
3523 from pip_e[unfolded is_exit] |
|
3524 show ?thesis |
|
3525 by (cases, unfold runing_def readys_def, simp) |
|
3526 qed |
|
3527 |
|
3528 lemma th_ready_s [simp]: "th \<in> readys s" |
|
3529 proof - |
|
3530 from pip_e[unfolded is_exit] |
|
3531 show ?thesis |
|
3532 by (cases, unfold runing_def, simp) |
|
3533 qed |
|
3534 |
|
3535 lemma th_not_live_es [simp]: "th \<notin> threads (e#s)" |
|
3536 by (unfold is_exit, simp) |
|
3537 |
|
3538 lemma not_holding_th_s [simp]: "\<not> holding s th cs'" |
|
3539 proof - |
|
3540 from pip_e[unfolded is_exit] |
|
3541 show ?thesis |
|
3542 by (cases, unfold holdents_def, auto) |
|
3543 qed |
|
3544 |
|
3545 lemma cntCS_th_s [simp]: "cntCS s th = 0" |
|
3546 proof - |
|
3547 from pip_e[unfolded is_exit] |
|
3548 show ?thesis |
|
3549 by (cases, unfold cntCS_def, simp) |
|
3550 qed |
|
3551 |
|
3552 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'" |
|
3553 proof |
|
3554 assume "holding (e # s) th cs'" |
|
3555 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] |
|
3556 have "holding s th cs'" |
|
3557 by (unfold s_holding_def, fold wq_def, auto) |
|
3558 with not_holding_th_s |
|
3559 show False by simp |
|
3560 qed |
|
3561 |
|
3562 lemma ready_th_es [simp]: "th \<notin> readys (e#s)" |
|
3563 by (simp add:readys_def) |
|
3564 |
|
3565 lemma holdents_th_s: "holdents s th = {}" |
|
3566 by (unfold holdents_def, auto) |
|
3567 |
|
3568 lemma holdents_th_es: "holdents (e#s) th = {}" |
|
3569 by (unfold holdents_def, auto) |
|
3570 |
|
3571 lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0" |
|
3572 by (unfold cntCS_def, simp add:holdents_th_es) |
|
3573 |
|
3574 lemma pvD_th_s [simp]: "pvD s th = 0" |
|
3575 by (unfold pvD_def, simp) |
|
3576 |
|
3577 lemma pvD_th_es [simp]: "pvD (e#s) th = 0" |
|
3578 by (unfold pvD_def, simp) |
|
3579 |
|
3580 lemma holdents_kept: |
|
3581 assumes "th' \<noteq> th" |
|
3582 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3583 proof - |
|
3584 { fix cs' |
|
3585 assume h: "cs' \<in> ?L" |
|
3586 hence "cs' \<in> ?R" |
|
3587 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3588 unfold wq_kept, auto) |
|
3589 } moreover { |
|
3590 fix cs' |
|
3591 assume h: "cs' \<in> ?R" |
|
3592 hence "cs' \<in> ?L" |
|
3593 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3594 unfold wq_kept, auto) |
|
3595 } ultimately show ?thesis by auto |
|
3596 qed |
|
3597 |
|
3598 lemma cntCS_kept [simp]: |
|
3599 assumes "th' \<noteq> th" |
|
3600 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R") |
|
3601 using holdents_kept[OF assms] |
|
3602 by (unfold cntCS_def, simp) |
|
3603 |
|
3604 lemma readys_kept1: |
|
3605 assumes "th' \<noteq> th" |
|
3606 and "th' \<in> readys (e#s)" |
|
3607 shows "th' \<in> readys s" |
|
3608 proof - |
|
3609 { fix cs' |
|
3610 assume wait: "waiting s th' cs'" |
|
3611 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3612 using assms by (auto simp:readys_def) |
|
3613 from wait[unfolded s_waiting_def, folded wq_def] |
|
3614 n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3615 have False by auto |
|
3616 } thus ?thesis using assms |
|
3617 by (unfold readys_def, auto) |
|
3618 qed |
|
3619 |
|
3620 lemma readys_kept2: |
|
3621 assumes "th' \<noteq> th" |
|
3622 and "th' \<in> readys s" |
|
3623 shows "th' \<in> readys (e#s)" |
|
3624 proof - |
|
3625 { fix cs' |
|
3626 assume wait: "waiting (e#s) th' cs'" |
|
3627 have n_wait: "\<not> waiting s th' cs'" |
|
3628 using assms(2) by (auto simp:readys_def) |
|
3629 from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3630 n_wait[unfolded s_waiting_def, folded wq_def] |
|
3631 have False by auto |
|
3632 } with assms show ?thesis |
|
3633 by (unfold readys_def, auto) |
|
3634 qed |
|
3635 |
|
3636 lemma readys_simp [simp]: |
|
3637 assumes "th' \<noteq> th" |
|
3638 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3639 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3640 by metis |
|
3641 |
|
3642 lemma pvD_kept [simp]: |
|
3643 assumes "th' \<noteq> th" |
|
3644 shows "pvD (e#s) th' = pvD s th'" |
|
3645 using assms |
|
3646 by (unfold pvD_def, simp) |
|
3647 |
|
3648 lemma cnp_cnv_cncs_kept: |
|
3649 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3650 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3651 proof - |
|
3652 { |
|
3653 assume eq_th': "th' = th" |
|
3654 have ?thesis using assms |
|
3655 by (unfold eq_th', simp, unfold is_exit, simp) |
|
3656 } moreover { |
|
3657 assume h: "th' \<noteq> th" |
|
3658 hence ?thesis using assms |
|
3659 by (simp, simp add:is_exit) |
|
3660 } ultimately show ?thesis by metis |
|
3661 qed |
|
3662 |
|
3663 end |
|
3664 |
|
3665 context valid_trace_set |
|
3666 begin |
|
3667 |
|
3668 lemma th_live_s [simp]: "th \<in> threads s" |
|
3669 proof - |
|
3670 from pip_e[unfolded is_set] |
|
3671 show ?thesis |
|
3672 by (cases, unfold runing_def readys_def, simp) |
|
3673 qed |
|
3674 |
|
3675 lemma th_ready_s [simp]: "th \<in> readys s" |
|
3676 proof - |
|
3677 from pip_e[unfolded is_set] |
|
3678 show ?thesis |
|
3679 by (cases, unfold runing_def, simp) |
|
3680 qed |
|
3681 |
|
3682 lemma th_not_live_es [simp]: "th \<in> threads (e#s)" |
|
3683 by (unfold is_set, simp) |
|
3684 |
|
3685 |
|
3686 lemma holdents_kept: |
|
3687 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3688 proof - |
|
3689 { fix cs' |
|
3690 assume h: "cs' \<in> ?L" |
|
3691 hence "cs' \<in> ?R" |
|
3692 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3693 unfold wq_kept, auto) |
|
3694 } moreover { |
|
3695 fix cs' |
|
3696 assume h: "cs' \<in> ?R" |
|
3697 hence "cs' \<in> ?L" |
|
3698 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3699 unfold wq_kept, auto) |
|
3700 } ultimately show ?thesis by auto |
|
3701 qed |
|
3702 |
|
3703 lemma cntCS_kept [simp]: |
|
3704 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R") |
|
3705 using holdents_kept |
|
3706 by (unfold cntCS_def, simp) |
|
3707 |
|
3708 lemma threads_kept[simp]: |
|
3709 "threads (e#s) = threads s" |
|
3710 by (unfold is_set, simp) |
|
3711 |
|
3712 lemma readys_kept1: |
|
3713 assumes "th' \<in> readys (e#s)" |
|
3714 shows "th' \<in> readys s" |
|
3715 proof - |
|
3716 { fix cs' |
|
3717 assume wait: "waiting s th' cs'" |
|
3718 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3719 using assms by (auto simp:readys_def) |
|
3720 from wait[unfolded s_waiting_def, folded wq_def] |
|
3721 n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3722 have False by auto |
|
3723 } moreover have "th' \<in> threads s" |
|
3724 using assms[unfolded readys_def] by auto |
|
3725 ultimately show ?thesis |
|
3726 by (unfold readys_def, auto) |
|
3727 qed |
|
3728 |
|
3729 lemma readys_kept2: |
|
3730 assumes "th' \<in> readys s" |
|
3731 shows "th' \<in> readys (e#s)" |
|
3732 proof - |
|
3733 { fix cs' |
|
3734 assume wait: "waiting (e#s) th' cs'" |
|
3735 have n_wait: "\<not> waiting s th' cs'" |
|
3736 using assms by (auto simp:readys_def) |
|
3737 from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3738 n_wait[unfolded s_waiting_def, folded wq_def] |
|
3739 have False by auto |
|
3740 } with assms show ?thesis |
|
3741 by (unfold readys_def, auto) |
|
3742 qed |
|
3743 |
|
3744 lemma readys_simp [simp]: |
|
3745 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3746 using readys_kept1 readys_kept2 |
|
3747 by metis |
|
3748 |
|
3749 lemma pvD_kept [simp]: |
|
3750 shows "pvD (e#s) th' = pvD s th'" |
|
3751 by (unfold pvD_def, simp) |
|
3752 |
|
3753 lemma cnp_cnv_cncs_kept: |
|
3754 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3755 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3756 using assms |
|
3757 by (unfold is_set, simp, fold is_set, simp) |
|
3758 |
|
3759 end |
|
3760 |
|
3761 context valid_trace |
|
3762 begin |
|
3763 |
|
3764 lemma cnp_cnv_cncs: "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3765 proof(induct rule:ind) |
|
3766 case Nil |
|
3767 thus ?case |
|
3768 by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def |
|
3769 s_holding_def, simp) |
|
3770 next |
|
3771 case (Cons s e) |
|
3772 interpret vt_e: valid_trace_e s e using Cons by simp |
|
3773 show ?case |
|
3774 proof(cases e) |
|
3775 case (Create th prio) |
|
3776 interpret vt_create: valid_trace_create s e th prio |
|
3777 using Create by (unfold_locales, simp) |
|
3778 show ?thesis using Cons by (simp add: vt_create.cnp_cnv_cncs_kept) |
|
3779 next |
|
3780 case (Exit th) |
|
3781 interpret vt_exit: valid_trace_exit s e th |
|
3782 using Exit by (unfold_locales, simp) |
|
3783 show ?thesis using Cons by (simp add: vt_exit.cnp_cnv_cncs_kept) |
|
3784 next |
|
3785 case (P th cs) |
|
3786 interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp) |
|
3787 show ?thesis using Cons by (simp add: vt_p.cnp_cnv_cncs_kept) |
|
3788 next |
|
3789 case (V th cs) |
|
3790 interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp) |
|
3791 show ?thesis using Cons by (simp add: vt_v.cnp_cnv_cncs_kept) |
|
3792 next |
|
3793 case (Set th prio) |
|
3794 interpret vt_set: valid_trace_set s e th prio |
|
3795 using Set by (unfold_locales, simp) |
|
3796 show ?thesis using Cons by (simp add: vt_set.cnp_cnv_cncs_kept) |
|
3797 qed |
|
3798 qed |
|
3799 |
|
3800 lemma not_thread_holdents: |
|
3801 assumes not_in: "th \<notin> threads s" |
|
3802 shows "holdents s th = {}" |
|
3803 proof - |
|
3804 { fix cs |
|
3805 assume "cs \<in> holdents s th" |
|
3806 hence "holding s th cs" by (auto simp:holdents_def) |
|
3807 from this[unfolded s_holding_def, folded wq_def] |
|
3808 have "th \<in> set (wq s cs)" by auto |
|
3809 with wq_threads have "th \<in> threads s" by auto |
|
3810 with assms |
|
3811 have False by simp |
|
3812 } thus ?thesis by auto |
|
3813 qed |
|
3814 |
|
3815 lemma not_thread_cncs: |
|
3816 assumes not_in: "th \<notin> threads s" |
|
3817 shows "cntCS s th = 0" |
|
3818 using not_thread_holdents[OF assms] |
|
3819 by (simp add:cntCS_def) |
|
3820 |
|
3821 lemma cnp_cnv_eq: |
|
3822 assumes "th \<notin> threads s" |
|
3823 shows "cntP s th = cntV s th" |
|
3824 using assms cnp_cnv_cncs not_thread_cncs pvD_def |
|
3825 by (auto) |
|
3826 |
|
3827 lemma runing_unique: |
|
3828 assumes runing_1: "th1 \<in> runing s" |
|
3829 and runing_2: "th2 \<in> runing s" |
|
3830 shows "th1 = th2" |
|
3831 proof - |
|
3832 from runing_1 and runing_2 have "cp s th1 = cp s th2" |
|
3833 unfolding runing_def by auto |
|
3834 from this[unfolded cp_alt_def] |
|
3835 have eq_max: |
|
3836 "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) = |
|
3837 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})" |
|
3838 (is "Max ?L = Max ?R") . |
|
3839 have "Max ?L \<in> ?L" |
|
3840 proof(rule Max_in) |
|
3841 show "finite ?L" by (simp add: finite_subtree_threads) |
|
3842 next |
|
3843 show "?L \<noteq> {}" using subtree_def by fastforce |
|
3844 qed |
|
3845 then obtain th1' where |
|
3846 h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L" |
|
3847 by auto |
|
3848 have "Max ?R \<in> ?R" |
|
3849 proof(rule Max_in) |
|
3850 show "finite ?R" by (simp add: finite_subtree_threads) |
|
3851 next |
|
3852 show "?R \<noteq> {}" using subtree_def by fastforce |
|
3853 qed |
|
3854 then obtain th2' where |
|
3855 h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R" |
|
3856 by auto |
|
3857 have "th1' = th2'" |
|
3858 proof(rule preced_unique) |
|
3859 from h_1(1) |
|
3860 show "th1' \<in> threads s" |
|
3861 proof(cases rule:subtreeE) |
|
3862 case 1 |
|
3863 hence "th1' = th1" by simp |
|
3864 with runing_1 show ?thesis by (auto simp:runing_def readys_def) |
|
3865 next |
|
3866 case 2 |
|
3867 from this(2) |
|
3868 have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
3869 from tranclD[OF this] |
|
3870 have "(Th th1') \<in> Domain (RAG s)" by auto |
|
3871 from dm_RAG_threads[OF this] show ?thesis . |
|
3872 qed |
|
3873 next |
|
3874 from h_2(1) |
|
3875 show "th2' \<in> threads s" |
|
3876 proof(cases rule:subtreeE) |
|
3877 case 1 |
|
3878 hence "th2' = th2" by simp |
|
3879 with runing_2 show ?thesis by (auto simp:runing_def readys_def) |
|
3880 next |
|
3881 case 2 |
|
3882 from this(2) |
|
3883 have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
3884 from tranclD[OF this] |
|
3885 have "(Th th2') \<in> Domain (RAG s)" by auto |
|
3886 from dm_RAG_threads[OF this] show ?thesis . |
|
3887 qed |
|
3888 next |
|
3889 have "the_preced s th1' = the_preced s th2'" |
|
3890 using eq_max h_1(2) h_2(2) by metis |
|
3891 thus "preced th1' s = preced th2' s" by (simp add:the_preced_def) |
|
3892 qed |
|
3893 from h_1(1)[unfolded this] |
|
3894 have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def) |
|
3895 from h_2(1)[unfolded this] |
|
3896 have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def) |
|
3897 from star_rpath[OF star1] obtain xs1 |
|
3898 where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)" |
|
3899 by auto |
|
3900 from star_rpath[OF star2] obtain xs2 |
|
3901 where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)" |
|
3902 by auto |
|
3903 from rp1 rp2 |
|
3904 show ?thesis |
|
3905 proof(cases) |
|
3906 case (less_1 xs') |
|
3907 moreover have "xs' = []" |
|
3908 proof(rule ccontr) |
|
3909 assume otherwise: "xs' \<noteq> []" |
|
3910 from rpath_plus[OF less_1(3) this] |
|
3911 have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" . |
|
3912 from tranclD[OF this] |
|
3913 obtain cs where "waiting s th1 cs" |
|
3914 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
3915 with runing_1 show False |
|
3916 by (unfold runing_def readys_def, auto) |
|
3917 qed |
|
3918 ultimately have "xs2 = xs1" by simp |
|
3919 from rpath_dest_eq[OF rp1 rp2[unfolded this]] |
|
3920 show ?thesis by simp |
|
3921 next |
|
3922 case (less_2 xs') |
|
3923 moreover have "xs' = []" |
|
3924 proof(rule ccontr) |
|
3925 assume otherwise: "xs' \<noteq> []" |
|
3926 from rpath_plus[OF less_2(3) this] |
|
3927 have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" . |
|
3928 from tranclD[OF this] |
|
3929 obtain cs where "waiting s th2 cs" |
|
3930 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
3931 with runing_2 show False |
|
3932 by (unfold runing_def readys_def, auto) |
|
3933 qed |
|
3934 ultimately have "xs2 = xs1" by simp |
|
3935 from rpath_dest_eq[OF rp1 rp2[unfolded this]] |
|
3936 show ?thesis by simp |
|
3937 qed |
|
3938 qed |
|
3939 |
|
3940 lemma card_runing: "card (runing s) \<le> 1" |
|
3941 proof(cases "runing s = {}") |
|
3942 case True |
|
3943 thus ?thesis by auto |
|
3944 next |
|
3945 case False |
|
3946 then obtain th where [simp]: "th \<in> runing s" by auto |
|
3947 from runing_unique[OF this] |
|
3948 have "runing s = {th}" by auto |
|
3949 thus ?thesis by auto |
|
3950 qed |
|
3951 |
|
3952 lemma create_pre: |
|
3953 assumes stp: "step s e" |
|
3954 and not_in: "th \<notin> threads s" |
|
3955 and is_in: "th \<in> threads (e#s)" |
|
3956 obtains prio where "e = Create th prio" |
|
3957 proof - |
|
3958 from assms |
|
3959 show ?thesis |
|
3960 proof(cases) |
|
3961 case (thread_create thread prio) |
|
3962 with is_in not_in have "e = Create th prio" by simp |
|
3963 from that[OF this] show ?thesis . |
|
3964 next |
|
3965 case (thread_exit thread) |
|
3966 with assms show ?thesis by (auto intro!:that) |
|
3967 next |
|
3968 case (thread_P thread) |
|
3969 with assms show ?thesis by (auto intro!:that) |
|
3970 next |
|
3971 case (thread_V thread) |
|
3972 with assms show ?thesis by (auto intro!:that) |
|
3973 next |
|
3974 case (thread_set thread) |
|
3975 with assms show ?thesis by (auto intro!:that) |
|
3976 qed |
|
3977 qed |
|
3978 |
|
3979 lemma eq_pv_children: |
|
3980 assumes eq_pv: "cntP s th = cntV s th" |
|
3981 shows "children (RAG s) (Th th) = {}" |
|
3982 proof - |
|
3983 from cnp_cnv_cncs and eq_pv |
|
3984 have "cntCS s th = 0" |
|
3985 by (auto split:if_splits) |
|
3986 from this[unfolded cntCS_def holdents_alt_def] |
|
3987 have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" . |
|
3988 have "finite (the_cs ` children (RAG s) (Th th))" |
|
3989 by (simp add: fsbtRAGs.finite_children) |
|
3990 from card_0[unfolded card_0_eq[OF this]] |
|
3991 show ?thesis by auto |
|
3992 qed |
|
3993 |
|
3994 lemma eq_pv_holdents: |
|
3995 assumes eq_pv: "cntP s th = cntV s th" |
|
3996 shows "holdents s th = {}" |
|
3997 by (unfold holdents_alt_def eq_pv_children[OF assms], simp) |
|
3998 |
|
3999 lemma eq_pv_subtree: |
|
4000 assumes eq_pv: "cntP s th = cntV s th" |
|
4001 shows "subtree (RAG s) (Th th) = {Th th}" |
|
4002 using eq_pv_children[OF assms] |
|
4003 by (unfold subtree_children, simp) |
|
4004 |
|
4005 end |
|
4006 |
|
4007 lemma cp_gen_alt_def: |
|
4008 "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))" |
|
4009 by (auto simp:cp_gen_def) |
|
4010 |
|
4011 lemma tRAG_nodeE: |
2413 lemma tRAG_nodeE: |
4012 assumes "(n1, n2) \<in> tRAG s" |
2414 assumes "(n1, n2) \<in> tRAG s" |
4013 obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" |
2415 obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" |
4014 using assms |
2416 using assms |
4015 by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) |
2417 by (auto simp: tRAG_def wRAG_def hRAG_def) |
4016 |
2418 |
|
2419 lemma tRAG_ancestorsE: |
|
2420 assumes "x \<in> ancestors (tRAG s) u" |
|
2421 obtains th where "x = Th th" |
|
2422 proof - |
|
2423 from assms have "(u, x) \<in> (tRAG s)^+" |
|
2424 by (unfold ancestors_def, auto) |
|
2425 from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto |
|
2426 then obtain th where "x = Th th" |
|
2427 by (unfold tRAG_alt_def, auto) |
|
2428 from that[OF this] show ?thesis . |
|
2429 qed |
|
2430 |
4017 lemma subtree_nodeE: |
2431 lemma subtree_nodeE: |
4018 assumes "n \<in> subtree (tRAG s) (Th th)" |
2432 assumes "n \<in> subtree (tRAG s) (Th th)" |
4019 obtains th1 where "n = Th th1" |
2433 obtains th1 where "n = Th th1" |
4020 proof - |
2434 proof - |
4021 show ?thesis |
2435 show ?thesis |
4135 lemma tRAG_trancl_eq_Th: |
2549 lemma tRAG_trancl_eq_Th: |
4136 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
2550 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
4137 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
2551 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
4138 using tRAG_trancl_eq by auto |
2552 using tRAG_trancl_eq by auto |
4139 |
2553 |
|
2554 |
|
2555 lemma tRAG_Field: |
|
2556 "Field (tRAG s) \<subseteq> Field (RAG s)" |
|
2557 by (unfold tRAG_alt_def Field_def, auto) |
|
2558 |
|
2559 lemma tRAG_mono: |
|
2560 assumes "RAG s' \<subseteq> RAG s" |
|
2561 shows "tRAG s' \<subseteq> tRAG s" |
|
2562 using assms |
|
2563 by (unfold tRAG_alt_def, auto) |
|
2564 |
|
2565 lemma tRAG_subtree_eq: |
|
2566 "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}" |
|
2567 (is "?L = ?R") |
|
2568 proof - |
|
2569 { fix n |
|
2570 assume h: "n \<in> ?L" |
|
2571 hence "n \<in> ?R" |
|
2572 by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) |
|
2573 } moreover { |
|
2574 fix n |
|
2575 assume "n \<in> ?R" |
|
2576 then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*" |
|
2577 by (auto simp:subtree_def) |
|
2578 from rtranclD[OF this(2)] |
|
2579 have "n \<in> ?L" |
|
2580 proof |
|
2581 assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+" |
|
2582 with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto |
|
2583 thus ?thesis using subtree_def tRAG_trancl_eq by fastforce |
|
2584 qed (insert h, auto simp:subtree_def) |
|
2585 } ultimately show ?thesis by auto |
|
2586 qed |
|
2587 |
|
2588 lemma threads_set_eq: |
|
2589 "the_thread ` (subtree (tRAG s) (Th th)) = |
|
2590 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") |
|
2591 by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) |
|
2592 |
4140 lemma dependants_alt_def: |
2593 lemma dependants_alt_def: |
4141 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
2594 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
4142 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
2595 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
4143 |
2596 |
4144 lemma dependants_alt_def1: |
2597 lemma dependants_alt_def1: |
4145 "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}" |
2598 "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}" |
4146 using dependants_alt_def tRAG_trancl_eq by auto |
2599 using dependants_alt_def tRAG_trancl_eq by auto |
4147 |
2600 |
|
2601 section {* Chain to readys *} |
|
2602 |
4148 context valid_trace |
2603 context valid_trace |
4149 begin |
2604 begin |
|
2605 |
|
2606 lemma chain_building: |
|
2607 assumes "node \<in> Domain (RAG s)" |
|
2608 obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+" |
|
2609 proof - |
|
2610 from assms have "node \<in> Range ((RAG s)^-1)" by auto |
|
2611 from wf_base[OF wf_RAG_converse this] |
|
2612 obtain b where h_b: "(b, node) \<in> ((RAG s)\<inverse>)\<^sup>+" "\<forall>c. (c, b) \<notin> (RAG s)\<inverse>" by auto |
|
2613 obtain th' where eq_b: "b = Th th'" |
|
2614 proof(cases b) |
|
2615 case (Cs cs) |
|
2616 from h_b(1)[unfolded trancl_converse] |
|
2617 have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto |
|
2618 from tranclE[OF this] |
|
2619 obtain n where "(n, b) \<in> RAG s" by auto |
|
2620 from this[unfolded Cs] |
|
2621 obtain th1 where "waiting s th1 cs" |
|
2622 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
2623 from waiting_holding[OF this] |
|
2624 obtain th2 where "holding s th2 cs" . |
|
2625 hence "(Cs cs, Th th2) \<in> RAG s" |
|
2626 by (unfold s_RAG_def, fold holding_eq, auto) |
|
2627 with h_b(2)[unfolded Cs, rule_format] |
|
2628 have False by auto |
|
2629 thus ?thesis by auto |
|
2630 qed auto |
|
2631 have "th' \<in> readys s" |
|
2632 proof - |
|
2633 from h_b(2)[unfolded eq_b] |
|
2634 have "\<forall>cs. \<not> waiting s th' cs" |
|
2635 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
2636 moreover have "th' \<in> threads s" |
|
2637 proof(rule rg_RAG_threads) |
|
2638 from tranclD[OF h_b(1), unfolded eq_b] |
|
2639 obtain z where "(z, Th th') \<in> (RAG s)" by auto |
|
2640 thus "Th th' \<in> Range (RAG s)" by auto |
|
2641 qed |
|
2642 ultimately show ?thesis by (auto simp:readys_def) |
|
2643 qed |
|
2644 moreover have "(node, Th th') \<in> (RAG s)^+" |
|
2645 using h_b(1)[unfolded trancl_converse] eq_b by auto |
|
2646 ultimately show ?thesis using that by metis |
|
2647 qed |
|
2648 |
|
2649 text {* \noindent |
|
2650 The following is just an instance of @{text "chain_building"}. |
|
2651 *} |
|
2652 lemma th_chain_to_ready: |
|
2653 assumes th_in: "th \<in> threads s" |
|
2654 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)" |
|
2655 proof(cases "th \<in> readys s") |
|
2656 case True |
|
2657 thus ?thesis by auto |
|
2658 next |
|
2659 case False |
|
2660 from False and th_in have "Th th \<in> Domain (RAG s)" |
|
2661 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) |
|
2662 from chain_building [rule_format, OF this] |
|
2663 show ?thesis by auto |
|
2664 qed |
|
2665 |
|
2666 lemma finite_subtree_threads: |
|
2667 "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A") |
|
2668 proof - |
|
2669 have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}" |
|
2670 by (auto, insert image_iff, fastforce) |
|
2671 moreover have "finite {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}" |
|
2672 (is "finite ?B") |
|
2673 proof - |
|
2674 have "?B = (subtree (RAG s) (Th th)) \<inter> {Th th' | th'. True}" |
|
2675 by auto |
|
2676 moreover have "... \<subseteq> (subtree (RAG s) (Th th))" by auto |
|
2677 moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) |
|
2678 ultimately show ?thesis by auto |
|
2679 qed |
|
2680 ultimately show ?thesis by auto |
|
2681 qed |
|
2682 |
|
2683 lemma runing_unique: |
|
2684 assumes runing_1: "th1 \<in> runing s" |
|
2685 and runing_2: "th2 \<in> runing s" |
|
2686 shows "th1 = th2" |
|
2687 proof - |
|
2688 from runing_1 and runing_2 have "cp s th1 = cp s th2" |
|
2689 unfolding runing_def by auto |
|
2690 from this[unfolded cp_alt_def] |
|
2691 have eq_max: |
|
2692 "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) = |
|
2693 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})" |
|
2694 (is "Max ?L = Max ?R") . |
|
2695 have "Max ?L \<in> ?L" |
|
2696 proof(rule Max_in) |
|
2697 show "finite ?L" by (simp add: finite_subtree_threads) |
|
2698 next |
|
2699 show "?L \<noteq> {}" using subtree_def by fastforce |
|
2700 qed |
|
2701 then obtain th1' where |
|
2702 h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L" |
|
2703 by auto |
|
2704 have "Max ?R \<in> ?R" |
|
2705 proof(rule Max_in) |
|
2706 show "finite ?R" by (simp add: finite_subtree_threads) |
|
2707 next |
|
2708 show "?R \<noteq> {}" using subtree_def by fastforce |
|
2709 qed |
|
2710 then obtain th2' where |
|
2711 h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R" |
|
2712 by auto |
|
2713 have "th1' = th2'" |
|
2714 proof(rule preced_unique) |
|
2715 from h_1(1) |
|
2716 show "th1' \<in> threads s" |
|
2717 proof(cases rule:subtreeE) |
|
2718 case 1 |
|
2719 hence "th1' = th1" by simp |
|
2720 with runing_1 show ?thesis by (auto simp:runing_def readys_def) |
|
2721 next |
|
2722 case 2 |
|
2723 from this(2) |
|
2724 have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
2725 from tranclD[OF this] |
|
2726 have "(Th th1') \<in> Domain (RAG s)" by auto |
|
2727 from dm_RAG_threads[OF this] show ?thesis . |
|
2728 qed |
|
2729 next |
|
2730 from h_2(1) |
|
2731 show "th2' \<in> threads s" |
|
2732 proof(cases rule:subtreeE) |
|
2733 case 1 |
|
2734 hence "th2' = th2" by simp |
|
2735 with runing_2 show ?thesis by (auto simp:runing_def readys_def) |
|
2736 next |
|
2737 case 2 |
|
2738 from this(2) |
|
2739 have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
2740 from tranclD[OF this] |
|
2741 have "(Th th2') \<in> Domain (RAG s)" by auto |
|
2742 from dm_RAG_threads[OF this] show ?thesis . |
|
2743 qed |
|
2744 next |
|
2745 have "the_preced s th1' = the_preced s th2'" |
|
2746 using eq_max h_1(2) h_2(2) by metis |
|
2747 thus "preced th1' s = preced th2' s" by (simp add:the_preced_def) |
|
2748 qed |
|
2749 from h_1(1)[unfolded this] |
|
2750 have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def) |
|
2751 from h_2(1)[unfolded this] |
|
2752 have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def) |
|
2753 from star_rpath[OF star1] obtain xs1 |
|
2754 where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)" |
|
2755 by auto |
|
2756 from star_rpath[OF star2] obtain xs2 |
|
2757 where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)" |
|
2758 by auto |
|
2759 from rp1 rp2 |
|
2760 show ?thesis |
|
2761 proof(cases) |
|
2762 case (less_1 xs') |
|
2763 moreover have "xs' = []" |
|
2764 proof(rule ccontr) |
|
2765 assume otherwise: "xs' \<noteq> []" |
|
2766 from rpath_plus[OF less_1(3) this] |
|
2767 have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" . |
|
2768 from tranclD[OF this] |
|
2769 obtain cs where "waiting s th1 cs" |
|
2770 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
2771 with runing_1 show False |
|
2772 by (unfold runing_def readys_def, auto) |
|
2773 qed |
|
2774 ultimately have "xs2 = xs1" by simp |
|
2775 from rpath_dest_eq[OF rp1 rp2[unfolded this]] |
|
2776 show ?thesis by simp |
|
2777 next |
|
2778 case (less_2 xs') |
|
2779 moreover have "xs' = []" |
|
2780 proof(rule ccontr) |
|
2781 assume otherwise: "xs' \<noteq> []" |
|
2782 from rpath_plus[OF less_2(3) this] |
|
2783 have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" . |
|
2784 from tranclD[OF this] |
|
2785 obtain cs where "waiting s th2 cs" |
|
2786 by (unfold s_RAG_def, fold waiting_eq, auto) |
|
2787 with runing_2 show False |
|
2788 by (unfold runing_def readys_def, auto) |
|
2789 qed |
|
2790 ultimately have "xs2 = xs1" by simp |
|
2791 from rpath_dest_eq[OF rp1 rp2[unfolded this]] |
|
2792 show ?thesis by simp |
|
2793 qed |
|
2794 qed |
|
2795 |
|
2796 lemma card_runing: "card (runing s) \<le> 1" |
|
2797 proof(cases "runing s = {}") |
|
2798 case True |
|
2799 thus ?thesis by auto |
|
2800 next |
|
2801 case False |
|
2802 then obtain th where [simp]: "th \<in> runing s" by auto |
|
2803 from runing_unique[OF this] |
|
2804 have "runing s = {th}" by auto |
|
2805 thus ?thesis by auto |
|
2806 qed |
|
2807 |
|
2808 end |
|
2809 |
|
2810 |
|
2811 section {* Relating @{term cp} and @{term the_preced} and @{term preced} *} |
|
2812 |
|
2813 context valid_trace |
|
2814 begin |
|
2815 |
|
2816 lemma le_cp: |
|
2817 shows "preced th s \<le> cp s th" |
|
2818 proof(unfold cp_alt_def, rule Max_ge) |
|
2819 show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
2820 by (simp add: finite_subtree_threads) |
|
2821 next |
|
2822 show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
2823 by (simp add: subtree_def the_preced_def) |
|
2824 qed |
|
2825 |
|
2826 |
|
2827 lemma cp_le: |
|
2828 assumes th_in: "th \<in> threads s" |
|
2829 shows "cp s th \<le> Max (the_preced s ` threads s)" |
|
2830 proof(unfold cp_alt_def, rule Max_f_mono) |
|
2831 show "finite (threads s)" by (simp add: finite_threads) |
|
2832 next |
|
2833 show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}" |
|
2834 using subtree_def by fastforce |
|
2835 next |
|
2836 show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s" |
|
2837 using assms |
|
2838 by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq |
|
2839 node.inject(1) rtranclD subsetI subtree_def trancl_domain) |
|
2840 qed |
|
2841 |
|
2842 lemma max_cp_eq: |
|
2843 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" |
|
2844 (is "?L = ?R") |
|
2845 proof - |
|
2846 have "?L \<le> ?R" |
|
2847 proof(cases "threads s = {}") |
|
2848 case False |
|
2849 show ?thesis |
|
2850 by (rule Max.boundedI, |
|
2851 insert cp_le, |
|
2852 auto simp:finite_threads False) |
|
2853 qed auto |
|
2854 moreover have "?R \<le> ?L" |
|
2855 by (rule Max_fg_mono, |
|
2856 simp add: finite_threads, |
|
2857 simp add: le_cp the_preced_def) |
|
2858 ultimately show ?thesis by auto |
|
2859 qed |
|
2860 |
|
2861 end |
|
2862 |
|
2863 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *} |
|
2864 |
|
2865 context valid_trace_p_w |
|
2866 begin |
|
2867 |
|
2868 lemma holding_s_holder: "holding s holder cs" |
|
2869 by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) |
|
2870 |
|
2871 lemma holding_es_holder: "holding (e#s) holder cs" |
|
2872 by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto) |
|
2873 |
|
2874 lemma holdents_es: |
|
2875 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
2876 proof - |
|
2877 { fix cs' |
|
2878 assume "cs' \<in> ?L" |
|
2879 hence h: "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
2880 have "holding s th' cs'" |
|
2881 proof(cases "cs' = cs") |
|
2882 case True |
|
2883 from held_unique[OF h[unfolded True] holding_es_holder] |
|
2884 have "th' = holder" . |
|
2885 thus ?thesis |
|
2886 by (unfold True holdents_def, insert holding_s_holder, simp) |
|
2887 next |
|
2888 case False |
|
2889 hence "wq (e#s) cs' = wq s cs'" by simp |
|
2890 from h[unfolded s_holding_def, folded wq_def, unfolded this] |
|
2891 show ?thesis |
|
2892 by (unfold s_holding_def, fold wq_def, auto) |
|
2893 qed |
|
2894 hence "cs' \<in> ?R" by (auto simp:holdents_def) |
|
2895 } moreover { |
|
2896 fix cs' |
|
2897 assume "cs' \<in> ?R" |
|
2898 hence h: "holding s th' cs'" by (auto simp:holdents_def) |
|
2899 have "holding (e#s) th' cs'" |
|
2900 proof(cases "cs' = cs") |
|
2901 case True |
|
2902 from held_unique[OF h[unfolded True] holding_s_holder] |
|
2903 have "th' = holder" . |
|
2904 thus ?thesis |
|
2905 by (unfold True holdents_def, insert holding_es_holder, simp) |
|
2906 next |
|
2907 case False |
|
2908 hence "wq s cs' = wq (e#s) cs'" by simp |
|
2909 from h[unfolded s_holding_def, folded wq_def, unfolded this] |
|
2910 show ?thesis |
|
2911 by (unfold s_holding_def, fold wq_def, auto) |
|
2912 qed |
|
2913 hence "cs' \<in> ?L" by (auto simp:holdents_def) |
|
2914 } ultimately show ?thesis by auto |
|
2915 qed |
|
2916 |
|
2917 lemma cntCS_es_th[simp]: "cntCS (e#s) th' = cntCS s th'" |
|
2918 by (unfold cntCS_def holdents_es, simp) |
|
2919 |
|
2920 lemma th_not_ready_es: |
|
2921 shows "th \<notin> readys (e#s)" |
|
2922 using waiting_es_th_cs |
|
2923 by (unfold readys_def, auto) |
|
2924 |
|
2925 end |
|
2926 |
|
2927 lemma (in valid_trace) finite_holdents: "finite (holdents s th)" |
|
2928 by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto) |
|
2929 |
|
2930 context valid_trace_p |
|
2931 begin |
|
2932 |
|
2933 lemma ready_th_s: "th \<in> readys s" |
|
2934 using runing_th_s |
|
2935 by (unfold runing_def, auto) |
|
2936 |
|
2937 lemma live_th_s: "th \<in> threads s" |
|
2938 using readys_threads ready_th_s by auto |
|
2939 |
|
2940 lemma live_th_es: "th \<in> threads (e#s)" |
|
2941 using live_th_s |
|
2942 by (unfold is_p, simp) |
|
2943 |
|
2944 lemma waiting_neq_th: |
|
2945 assumes "waiting s t c" |
|
2946 shows "t \<noteq> th" |
|
2947 using assms using th_not_waiting by blast |
|
2948 |
|
2949 end |
|
2950 |
|
2951 context valid_trace_p_h |
|
2952 begin |
|
2953 |
|
2954 lemma th_not_waiting': |
|
2955 "\<not> waiting (e#s) th cs'" |
|
2956 proof(cases "cs' = cs") |
|
2957 case True |
|
2958 show ?thesis |
|
2959 by (unfold True s_waiting_def, fold wq_def, unfold wq_es_cs', auto) |
|
2960 next |
|
2961 case False |
|
2962 from th_not_waiting[of cs', unfolded s_waiting_def, folded wq_def] |
|
2963 show ?thesis |
|
2964 by (unfold s_waiting_def, fold wq_def, insert False, simp) |
|
2965 qed |
|
2966 |
|
2967 lemma ready_th_es: |
|
2968 shows "th \<in> readys (e#s)" |
|
2969 using th_not_waiting' |
|
2970 by (unfold readys_def, insert live_th_es, auto) |
|
2971 |
|
2972 lemma holdents_es_th: |
|
2973 "holdents (e#s) th = (holdents s th) \<union> {cs}" (is "?L = ?R") |
|
2974 proof - |
|
2975 { fix cs' |
|
2976 assume "cs' \<in> ?L" |
|
2977 hence "holding (e#s) th cs'" |
|
2978 by (unfold holdents_def, auto) |
|
2979 hence "cs' \<in> ?R" |
|
2980 by (cases rule:holding_esE, auto simp:holdents_def) |
|
2981 } moreover { |
|
2982 fix cs' |
|
2983 assume "cs' \<in> ?R" |
|
2984 hence "holding s th cs' \<or> cs' = cs" |
|
2985 by (auto simp:holdents_def) |
|
2986 hence "cs' \<in> ?L" |
|
2987 proof |
|
2988 assume "holding s th cs'" |
|
2989 from holding_kept[OF this] |
|
2990 show ?thesis by (auto simp:holdents_def) |
|
2991 next |
|
2992 assume "cs' = cs" |
|
2993 thus ?thesis using holding_es_th_cs |
|
2994 by (unfold holdents_def, auto) |
|
2995 qed |
|
2996 } ultimately show ?thesis by auto |
|
2997 qed |
|
2998 |
|
2999 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" |
|
3000 proof - |
|
3001 have "card (holdents s th \<union> {cs}) = card (holdents s th) + 1" |
|
3002 proof(subst card_Un_disjoint) |
|
3003 show "holdents s th \<inter> {cs} = {}" |
|
3004 using not_holding_s_th_cs by (auto simp:holdents_def) |
|
3005 qed (auto simp:finite_holdents) |
|
3006 thus ?thesis |
|
3007 by (unfold cntCS_def holdents_es_th, simp) |
|
3008 qed |
|
3009 |
|
3010 lemma no_holder: |
|
3011 "\<not> holding s th' cs" |
|
3012 proof |
|
3013 assume otherwise: "holding s th' cs" |
|
3014 from this[unfolded s_holding_def, folded wq_def, unfolded we] |
|
3015 show False by auto |
|
3016 qed |
|
3017 |
|
3018 lemma holdents_es_th': |
|
3019 assumes "th' \<noteq> th" |
|
3020 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3021 proof - |
|
3022 { fix cs' |
|
3023 assume "cs' \<in> ?L" |
|
3024 hence h_e: "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
3025 have "cs' \<noteq> cs" |
|
3026 proof |
|
3027 assume "cs' = cs" |
|
3028 from held_unique[OF h_e[unfolded this] holding_es_th_cs] |
|
3029 have "th' = th" . |
|
3030 with assms show False by simp |
|
3031 qed |
|
3032 from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]] |
|
3033 have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" . |
|
3034 hence "cs' \<in> ?R" |
|
3035 by (unfold holdents_def s_holding_def, fold wq_def, auto) |
|
3036 } moreover { |
|
3037 fix cs' |
|
3038 assume "cs' \<in> ?R" |
|
3039 hence "holding s th' cs'" by (auto simp:holdents_def) |
|
3040 from holding_kept[OF this] |
|
3041 have "holding (e # s) th' cs'" . |
|
3042 hence "cs' \<in> ?L" |
|
3043 by (unfold holdents_def, auto) |
|
3044 } ultimately show ?thesis by auto |
|
3045 qed |
|
3046 |
|
3047 lemma cntCS_es_th'[simp]: |
|
3048 assumes "th' \<noteq> th" |
|
3049 shows "cntCS (e#s) th' = cntCS s th'" |
|
3050 by (unfold cntCS_def holdents_es_th'[OF assms], simp) |
|
3051 |
|
3052 end |
|
3053 |
|
3054 context valid_trace_p |
|
3055 begin |
|
3056 |
|
3057 lemma readys_kept1: |
|
3058 assumes "th' \<noteq> th" |
|
3059 and "th' \<in> readys (e#s)" |
|
3060 shows "th' \<in> readys s" |
|
3061 proof - |
|
3062 { fix cs' |
|
3063 assume wait: "waiting s th' cs'" |
|
3064 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3065 using assms(2)[unfolded readys_def] by auto |
|
3066 have False |
|
3067 proof(cases "cs' = cs") |
|
3068 case False |
|
3069 with n_wait wait |
|
3070 show ?thesis |
|
3071 by (unfold s_waiting_def, fold wq_def, auto) |
|
3072 next |
|
3073 case True |
|
3074 show ?thesis |
|
3075 proof(cases "wq s cs = []") |
|
3076 case True |
|
3077 then interpret vt: valid_trace_p_h |
|
3078 by (unfold_locales, simp) |
|
3079 show ?thesis using n_wait wait waiting_kept by auto |
|
3080 next |
|
3081 case False |
|
3082 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
3083 show ?thesis using n_wait wait waiting_kept by blast |
|
3084 qed |
|
3085 qed |
|
3086 } with assms(2) show ?thesis |
|
3087 by (unfold readys_def, auto) |
|
3088 qed |
|
3089 |
|
3090 lemma readys_kept2: |
|
3091 assumes "th' \<noteq> th" |
|
3092 and "th' \<in> readys s" |
|
3093 shows "th' \<in> readys (e#s)" |
|
3094 proof - |
|
3095 { fix cs' |
|
3096 assume wait: "waiting (e#s) th' cs'" |
|
3097 have n_wait: "\<not> waiting s th' cs'" |
|
3098 using assms(2)[unfolded readys_def] by auto |
|
3099 have False |
|
3100 proof(cases "cs' = cs") |
|
3101 case False |
|
3102 with n_wait wait |
|
3103 show ?thesis |
|
3104 by (unfold s_waiting_def, fold wq_def, auto) |
|
3105 next |
|
3106 case True |
|
3107 show ?thesis |
|
3108 proof(cases "wq s cs = []") |
|
3109 case True |
|
3110 then interpret vt: valid_trace_p_h |
|
3111 by (unfold_locales, simp) |
|
3112 show ?thesis using n_wait vt.waiting_esE wait by blast |
|
3113 next |
|
3114 case False |
|
3115 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
3116 show ?thesis using assms(1) n_wait vt.waiting_esE wait by auto |
|
3117 qed |
|
3118 qed |
|
3119 } with assms(2) show ?thesis |
|
3120 by (unfold readys_def, auto) |
|
3121 qed |
|
3122 |
|
3123 lemma readys_simp [simp]: |
|
3124 assumes "th' \<noteq> th" |
|
3125 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3126 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3127 by metis |
|
3128 |
|
3129 lemma cnp_cnv_cncs_kept: (* ddd *) |
|
3130 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3131 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3132 proof(cases "th' = th") |
|
3133 case True |
|
3134 note eq_th' = this |
|
3135 show ?thesis |
|
3136 proof(cases "wq s cs = []") |
|
3137 case True |
|
3138 then interpret vt: valid_trace_p_h by (unfold_locales, simp) |
|
3139 show ?thesis |
|
3140 using assms eq_th' is_p ready_th_s vt.cntCS_es_th vt.ready_th_es pvD_def by auto |
|
3141 next |
|
3142 case False |
|
3143 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
3144 show ?thesis |
|
3145 using add.commute add.left_commute assms eq_th' is_p live_th_s |
|
3146 ready_th_s vt.th_not_ready_es pvD_def |
|
3147 apply (auto) |
|
3148 by (fold is_p, simp) |
|
3149 qed |
|
3150 next |
|
3151 case False |
|
3152 note h_False = False |
|
3153 thus ?thesis |
|
3154 proof(cases "wq s cs = []") |
|
3155 case True |
|
3156 then interpret vt: valid_trace_p_h by (unfold_locales, simp) |
|
3157 show ?thesis using assms |
|
3158 by (insert True h_False pvD_def, auto split:if_splits,unfold is_p, auto) |
|
3159 next |
|
3160 case False |
|
3161 then interpret vt: valid_trace_p_w by (unfold_locales, simp) |
|
3162 show ?thesis using assms |
|
3163 by (insert False h_False pvD_def, auto split:if_splits,unfold is_p, auto) |
|
3164 qed |
|
3165 qed |
|
3166 |
|
3167 end |
|
3168 |
|
3169 |
|
3170 context valid_trace_v |
|
3171 begin |
|
3172 |
|
3173 lemma holding_th_cs_s: |
|
3174 "holding s th cs" |
|
3175 by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) |
|
3176 |
|
3177 lemma th_ready_s [simp]: "th \<in> readys s" |
|
3178 using runing_th_s |
|
3179 by (unfold runing_def readys_def, auto) |
|
3180 |
|
3181 lemma th_live_s [simp]: "th \<in> threads s" |
|
3182 using th_ready_s by (unfold readys_def, auto) |
|
3183 |
|
3184 lemma th_ready_es [simp]: "th \<in> readys (e#s)" |
|
3185 using runing_th_s neq_t_th |
|
3186 by (unfold is_v runing_def readys_def, auto) |
|
3187 |
|
3188 lemma th_live_es [simp]: "th \<in> threads (e#s)" |
|
3189 using th_ready_es by (unfold readys_def, auto) |
|
3190 |
|
3191 lemma pvD_th_s[simp]: "pvD s th = 0" |
|
3192 by (unfold pvD_def, simp) |
|
3193 |
|
3194 lemma pvD_th_es[simp]: "pvD (e#s) th = 0" |
|
3195 by (unfold pvD_def, simp) |
|
3196 |
|
3197 lemma cntCS_s_th [simp]: "cntCS s th > 0" |
|
3198 proof - |
|
3199 have "cs \<in> holdents s th" using holding_th_cs_s |
|
3200 by (unfold holdents_def, simp) |
|
3201 moreover have "finite (holdents s th)" using finite_holdents |
|
3202 by simp |
|
3203 ultimately show ?thesis |
|
3204 by (unfold cntCS_def, |
|
3205 auto intro!:card_gt_0_iff[symmetric, THEN iffD1]) |
|
3206 qed |
|
3207 |
|
3208 end |
|
3209 |
|
3210 context valid_trace_v |
|
3211 begin |
|
3212 |
|
3213 lemma th_not_waiting: |
|
3214 "\<not> waiting s th c" |
|
3215 proof - |
|
3216 have "th \<in> readys s" |
|
3217 using runing_ready runing_th_s by blast |
|
3218 thus ?thesis |
|
3219 by (unfold readys_def, auto) |
|
3220 qed |
|
3221 |
|
3222 lemma waiting_neq_th: |
|
3223 assumes "waiting s t c" |
|
3224 shows "t \<noteq> th" |
|
3225 using assms using th_not_waiting by blast |
|
3226 |
|
3227 end |
|
3228 |
|
3229 context valid_trace_v_n |
|
3230 begin |
|
3231 |
|
3232 lemma not_ready_taker_s[simp]: |
|
3233 "taker \<notin> readys s" |
|
3234 using waiting_taker |
|
3235 by (unfold readys_def, auto) |
|
3236 |
|
3237 lemma taker_live_s [simp]: "taker \<in> threads s" |
|
3238 proof - |
|
3239 have "taker \<in> set wq'" by (simp add: eq_wq') |
|
3240 from th'_in_inv[OF this] |
|
3241 have "taker \<in> set rest" . |
|
3242 hence "taker \<in> set (wq s cs)" by (simp add: wq_s_cs) |
|
3243 thus ?thesis using wq_threads by auto |
|
3244 qed |
|
3245 |
|
3246 lemma taker_live_es [simp]: "taker \<in> threads (e#s)" |
|
3247 using taker_live_s threads_es by blast |
|
3248 |
|
3249 lemma taker_ready_es [simp]: |
|
3250 shows "taker \<in> readys (e#s)" |
|
3251 proof - |
|
3252 { fix cs' |
|
3253 assume "waiting (e#s) taker cs'" |
|
3254 hence False |
|
3255 proof(cases rule:waiting_esE) |
|
3256 case 1 |
|
3257 thus ?thesis using waiting_taker waiting_unique by auto |
|
3258 qed simp |
|
3259 } thus ?thesis by (unfold readys_def, auto) |
|
3260 qed |
|
3261 |
|
3262 lemma neq_taker_th: "taker \<noteq> th" |
|
3263 using th_not_waiting waiting_taker by blast |
|
3264 |
|
3265 lemma not_holding_taker_s_cs: |
|
3266 shows "\<not> holding s taker cs" |
|
3267 using holding_cs_eq_th neq_taker_th by auto |
|
3268 |
|
3269 lemma holdents_es_taker: |
|
3270 "holdents (e#s) taker = holdents s taker \<union> {cs}" (is "?L = ?R") |
|
3271 proof - |
|
3272 { fix cs' |
|
3273 assume "cs' \<in> ?L" |
|
3274 hence "holding (e#s) taker cs'" by (auto simp:holdents_def) |
|
3275 hence "cs' \<in> ?R" |
|
3276 proof(cases rule:holding_esE) |
|
3277 case 2 |
|
3278 thus ?thesis by (auto simp:holdents_def) |
|
3279 qed auto |
|
3280 } moreover { |
|
3281 fix cs' |
|
3282 assume "cs' \<in> ?R" |
|
3283 hence "holding s taker cs' \<or> cs' = cs" by (auto simp:holdents_def) |
|
3284 hence "cs' \<in> ?L" |
|
3285 proof |
|
3286 assume "holding s taker cs'" |
|
3287 hence "holding (e#s) taker cs'" |
|
3288 using holding_esI2 holding_taker by fastforce |
|
3289 thus ?thesis by (auto simp:holdents_def) |
|
3290 next |
|
3291 assume "cs' = cs" |
|
3292 with holding_taker |
|
3293 show ?thesis by (auto simp:holdents_def) |
|
3294 qed |
|
3295 } ultimately show ?thesis by auto |
|
3296 qed |
|
3297 |
|
3298 lemma cntCS_es_taker [simp]: "cntCS (e#s) taker = cntCS s taker + 1" |
|
3299 proof - |
|
3300 have "card (holdents s taker \<union> {cs}) = card (holdents s taker) + 1" |
|
3301 proof(subst card_Un_disjoint) |
|
3302 show "holdents s taker \<inter> {cs} = {}" |
|
3303 using not_holding_taker_s_cs by (auto simp:holdents_def) |
|
3304 qed (auto simp:finite_holdents) |
|
3305 thus ?thesis |
|
3306 by (unfold cntCS_def, insert holdents_es_taker, simp) |
|
3307 qed |
|
3308 |
|
3309 lemma pvD_taker_s[simp]: "pvD s taker = 1" |
|
3310 by (unfold pvD_def, simp) |
|
3311 |
|
3312 lemma pvD_taker_es[simp]: "pvD (e#s) taker = 0" |
|
3313 by (unfold pvD_def, simp) |
|
3314 |
|
3315 lemma pvD_th_s[simp]: "pvD s th = 0" |
|
3316 by (unfold pvD_def, simp) |
|
3317 |
|
3318 lemma pvD_th_es[simp]: "pvD (e#s) th = 0" |
|
3319 by (unfold pvD_def, simp) |
|
3320 |
|
3321 lemma holdents_es_th: |
|
3322 "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R") |
|
3323 proof - |
|
3324 { fix cs' |
|
3325 assume "cs' \<in> ?L" |
|
3326 hence "holding (e#s) th cs'" by (auto simp:holdents_def) |
|
3327 hence "cs' \<in> ?R" |
|
3328 proof(cases rule:holding_esE) |
|
3329 case 2 |
|
3330 thus ?thesis by (auto simp:holdents_def) |
|
3331 qed (insert neq_taker_th, auto) |
|
3332 } moreover { |
|
3333 fix cs' |
|
3334 assume "cs' \<in> ?R" |
|
3335 hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def) |
|
3336 from holding_esI2[OF this] |
|
3337 have "cs' \<in> ?L" by (auto simp:holdents_def) |
|
3338 } ultimately show ?thesis by auto |
|
3339 qed |
|
3340 |
|
3341 lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1" |
|
3342 proof - |
|
3343 have "card (holdents s th - {cs}) = card (holdents s th) - 1" |
|
3344 proof - |
|
3345 have "cs \<in> holdents s th" using holding_th_cs_s |
|
3346 by (auto simp:holdents_def) |
|
3347 moreover have "finite (holdents s th)" |
|
3348 by (simp add: finite_holdents) |
|
3349 ultimately show ?thesis by auto |
|
3350 qed |
|
3351 thus ?thesis by (unfold cntCS_def holdents_es_th) |
|
3352 qed |
|
3353 |
|
3354 lemma holdents_kept: |
|
3355 assumes "th' \<noteq> taker" |
|
3356 and "th' \<noteq> th" |
|
3357 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3358 proof - |
|
3359 { fix cs' |
|
3360 assume h: "cs' \<in> ?L" |
|
3361 have "cs' \<in> ?R" |
|
3362 proof(cases "cs' = cs") |
|
3363 case False |
|
3364 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3365 from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
3366 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3367 show ?thesis |
|
3368 by (unfold holdents_def s_holding_def, fold wq_def, auto) |
|
3369 next |
|
3370 case True |
|
3371 from h[unfolded this] |
|
3372 have "holding (e#s) th' cs" by (auto simp:holdents_def) |
|
3373 from held_unique[OF this holding_taker] |
|
3374 have "th' = taker" . |
|
3375 with assms show ?thesis by auto |
|
3376 qed |
|
3377 } moreover { |
|
3378 fix cs' |
|
3379 assume h: "cs' \<in> ?R" |
|
3380 have "cs' \<in> ?L" |
|
3381 proof(cases "cs' = cs") |
|
3382 case False |
|
3383 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3384 from h have "holding s th' cs'" by (auto simp:holdents_def) |
|
3385 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3386 show ?thesis |
|
3387 by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) |
|
3388 next |
|
3389 case True |
|
3390 from h[unfolded this] |
|
3391 have "holding s th' cs" by (auto simp:holdents_def) |
|
3392 from held_unique[OF this holding_th_cs_s] |
|
3393 have "th' = th" . |
|
3394 with assms show ?thesis by auto |
|
3395 qed |
|
3396 } ultimately show ?thesis by auto |
|
3397 qed |
|
3398 |
|
3399 lemma cntCS_kept [simp]: |
|
3400 assumes "th' \<noteq> taker" |
|
3401 and "th' \<noteq> th" |
|
3402 shows "cntCS (e#s) th' = cntCS s th'" |
|
3403 by (unfold cntCS_def holdents_kept[OF assms], simp) |
|
3404 |
|
3405 lemma readys_kept1: |
|
3406 assumes "th' \<noteq> taker" |
|
3407 and "th' \<in> readys (e#s)" |
|
3408 shows "th' \<in> readys s" |
|
3409 proof - |
|
3410 { fix cs' |
|
3411 assume wait: "waiting s th' cs'" |
|
3412 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3413 using assms(2)[unfolded readys_def] by auto |
|
3414 have False |
|
3415 proof(cases "cs' = cs") |
|
3416 case False |
|
3417 with n_wait wait |
|
3418 show ?thesis |
|
3419 by (unfold s_waiting_def, fold wq_def, auto) |
|
3420 next |
|
3421 case True |
|
3422 have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" |
|
3423 using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . |
|
3424 moreover have "\<not> (th' \<in> set rest \<and> th' \<noteq> hd (taker # rest'))" |
|
3425 using n_wait[unfolded True s_waiting_def, folded wq_def, |
|
3426 unfolded wq_es_cs set_wq', unfolded eq_wq'] . |
|
3427 ultimately have "th' = taker" by auto |
|
3428 with assms(1) |
|
3429 show ?thesis by simp |
|
3430 qed |
|
3431 } with assms(2) show ?thesis |
|
3432 by (unfold readys_def, auto) |
|
3433 qed |
|
3434 |
|
3435 lemma readys_kept2: |
|
3436 assumes "th' \<noteq> taker" |
|
3437 and "th' \<in> readys s" |
|
3438 shows "th' \<in> readys (e#s)" |
|
3439 proof - |
|
3440 { fix cs' |
|
3441 assume wait: "waiting (e#s) th' cs'" |
|
3442 have n_wait: "\<not> waiting s th' cs'" |
|
3443 using assms(2)[unfolded readys_def] by auto |
|
3444 have False |
|
3445 proof(cases "cs' = cs") |
|
3446 case False |
|
3447 with n_wait wait |
|
3448 show ?thesis |
|
3449 by (unfold s_waiting_def, fold wq_def, auto) |
|
3450 next |
|
3451 case True |
|
3452 have "th' \<in> set rest \<and> th' \<noteq> hd (taker # rest')" |
|
3453 using wait [unfolded True s_waiting_def, folded wq_def, |
|
3454 unfolded wq_es_cs set_wq', unfolded eq_wq'] . |
|
3455 moreover have "\<not> (th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest))" |
|
3456 using n_wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . |
|
3457 ultimately have "th' = taker" by auto |
|
3458 with assms(1) |
|
3459 show ?thesis by simp |
|
3460 qed |
|
3461 } with assms(2) show ?thesis |
|
3462 by (unfold readys_def, auto) |
|
3463 qed |
|
3464 |
|
3465 lemma readys_simp [simp]: |
|
3466 assumes "th' \<noteq> taker" |
|
3467 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3468 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3469 by metis |
|
3470 |
|
3471 lemma cnp_cnv_cncs_kept: |
|
3472 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3473 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3474 proof - |
|
3475 { assume eq_th': "th' = taker" |
|
3476 have ?thesis |
|
3477 apply (unfold eq_th' pvD_taker_es cntCS_es_taker) |
|
3478 by (insert neq_taker_th assms[unfolded eq_th'], unfold is_v, simp) |
|
3479 } moreover { |
|
3480 assume eq_th': "th' = th" |
|
3481 have ?thesis |
|
3482 apply (unfold eq_th' pvD_th_es cntCS_es_th) |
|
3483 by (insert assms[unfolded eq_th'], unfold is_v, simp) |
|
3484 } moreover { |
|
3485 assume h: "th' \<noteq> taker" "th' \<noteq> th" |
|
3486 have ?thesis using assms |
|
3487 apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp) |
|
3488 by (fold is_v, unfold pvD_def, simp) |
|
3489 } ultimately show ?thesis by metis |
|
3490 qed |
|
3491 |
|
3492 end |
|
3493 |
|
3494 context valid_trace_v_e |
|
3495 begin |
|
3496 |
|
3497 lemma holdents_es_th: |
|
3498 "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R") |
|
3499 proof - |
|
3500 { fix cs' |
|
3501 assume "cs' \<in> ?L" |
|
3502 hence "holding (e#s) th cs'" by (auto simp:holdents_def) |
|
3503 hence "cs' \<in> ?R" |
|
3504 proof(cases rule:holding_esE) |
|
3505 case 1 |
|
3506 thus ?thesis by (auto simp:holdents_def) |
|
3507 qed |
|
3508 } moreover { |
|
3509 fix cs' |
|
3510 assume "cs' \<in> ?R" |
|
3511 hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def) |
|
3512 from holding_esI2[OF this] |
|
3513 have "cs' \<in> ?L" by (auto simp:holdents_def) |
|
3514 } ultimately show ?thesis by auto |
|
3515 qed |
|
3516 |
|
3517 lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1" |
|
3518 proof - |
|
3519 have "card (holdents s th - {cs}) = card (holdents s th) - 1" |
|
3520 proof - |
|
3521 have "cs \<in> holdents s th" using holding_th_cs_s |
|
3522 by (auto simp:holdents_def) |
|
3523 moreover have "finite (holdents s th)" |
|
3524 by (simp add: finite_holdents) |
|
3525 ultimately show ?thesis by auto |
|
3526 qed |
|
3527 thus ?thesis by (unfold cntCS_def holdents_es_th) |
|
3528 qed |
|
3529 |
|
3530 lemma holdents_kept: |
|
3531 assumes "th' \<noteq> th" |
|
3532 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3533 proof - |
|
3534 { fix cs' |
|
3535 assume h: "cs' \<in> ?L" |
|
3536 have "cs' \<in> ?R" |
|
3537 proof(cases "cs' = cs") |
|
3538 case False |
|
3539 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3540 from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) |
|
3541 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3542 show ?thesis |
|
3543 by (unfold holdents_def s_holding_def, fold wq_def, auto) |
|
3544 next |
|
3545 case True |
|
3546 from h[unfolded this] |
|
3547 have "holding (e#s) th' cs" by (auto simp:holdents_def) |
|
3548 from this[unfolded s_holding_def, folded wq_def, |
|
3549 unfolded wq_es_cs nil_wq'] |
|
3550 show ?thesis by auto |
|
3551 qed |
|
3552 } moreover { |
|
3553 fix cs' |
|
3554 assume h: "cs' \<in> ?R" |
|
3555 have "cs' \<in> ?L" |
|
3556 proof(cases "cs' = cs") |
|
3557 case False |
|
3558 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp |
|
3559 from h have "holding s th' cs'" by (auto simp:holdents_def) |
|
3560 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] |
|
3561 show ?thesis |
|
3562 by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) |
|
3563 next |
|
3564 case True |
|
3565 from h[unfolded this] |
|
3566 have "holding s th' cs" by (auto simp:holdents_def) |
|
3567 from held_unique[OF this holding_th_cs_s] |
|
3568 have "th' = th" . |
|
3569 with assms show ?thesis by auto |
|
3570 qed |
|
3571 } ultimately show ?thesis by auto |
|
3572 qed |
|
3573 |
|
3574 lemma cntCS_kept [simp]: |
|
3575 assumes "th' \<noteq> th" |
|
3576 shows "cntCS (e#s) th' = cntCS s th'" |
|
3577 by (unfold cntCS_def holdents_kept[OF assms], simp) |
|
3578 |
|
3579 lemma readys_kept1: |
|
3580 assumes "th' \<in> readys (e#s)" |
|
3581 shows "th' \<in> readys s" |
|
3582 proof - |
|
3583 { fix cs' |
|
3584 assume wait: "waiting s th' cs'" |
|
3585 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3586 using assms(1)[unfolded readys_def] by auto |
|
3587 have False |
|
3588 proof(cases "cs' = cs") |
|
3589 case False |
|
3590 with n_wait wait |
|
3591 show ?thesis |
|
3592 by (unfold s_waiting_def, fold wq_def, auto) |
|
3593 next |
|
3594 case True |
|
3595 have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" |
|
3596 using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . |
|
3597 hence "th' \<in> set rest" by auto |
|
3598 with set_wq' have "th' \<in> set wq'" by metis |
|
3599 with nil_wq' show ?thesis by simp |
|
3600 qed |
|
3601 } thus ?thesis using assms |
|
3602 by (unfold readys_def, auto) |
|
3603 qed |
|
3604 |
|
3605 lemma readys_kept2: |
|
3606 assumes "th' \<in> readys s" |
|
3607 shows "th' \<in> readys (e#s)" |
|
3608 proof - |
|
3609 { fix cs' |
|
3610 assume wait: "waiting (e#s) th' cs'" |
|
3611 have n_wait: "\<not> waiting s th' cs'" |
|
3612 using assms[unfolded readys_def] by auto |
|
3613 have False |
|
3614 proof(cases "cs' = cs") |
|
3615 case False |
|
3616 with n_wait wait |
|
3617 show ?thesis |
|
3618 by (unfold s_waiting_def, fold wq_def, auto) |
|
3619 next |
|
3620 case True |
|
3621 have "th' \<in> set [] \<and> th' \<noteq> hd []" |
|
3622 using wait[unfolded True s_waiting_def, folded wq_def, |
|
3623 unfolded wq_es_cs nil_wq'] . |
|
3624 thus ?thesis by simp |
|
3625 qed |
|
3626 } with assms show ?thesis |
|
3627 by (unfold readys_def, auto) |
|
3628 qed |
|
3629 |
|
3630 lemma readys_simp [simp]: |
|
3631 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3632 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3633 by metis |
|
3634 |
|
3635 lemma cnp_cnv_cncs_kept: |
|
3636 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3637 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3638 proof - |
|
3639 { |
|
3640 assume eq_th': "th' = th" |
|
3641 have ?thesis |
|
3642 apply (unfold eq_th' pvD_th_es cntCS_es_th) |
|
3643 by (insert assms[unfolded eq_th'], unfold is_v, simp) |
|
3644 } moreover { |
|
3645 assume h: "th' \<noteq> th" |
|
3646 have ?thesis using assms |
|
3647 apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp) |
|
3648 by (fold is_v, unfold pvD_def, simp) |
|
3649 } ultimately show ?thesis by metis |
|
3650 qed |
|
3651 |
|
3652 end |
|
3653 |
|
3654 context valid_trace_v |
|
3655 begin |
|
3656 |
|
3657 lemma cnp_cnv_cncs_kept: |
|
3658 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3659 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3660 proof(cases "rest = []") |
|
3661 case True |
|
3662 then interpret vt: valid_trace_v_e by (unfold_locales, simp) |
|
3663 show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast |
|
3664 next |
|
3665 case False |
|
3666 then interpret vt: valid_trace_v_n by (unfold_locales, simp) |
|
3667 show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast |
|
3668 qed |
|
3669 |
|
3670 end |
|
3671 |
|
3672 context valid_trace_create |
|
3673 begin |
|
3674 |
|
3675 lemma th_not_live_s [simp]: "th \<notin> threads s" |
|
3676 proof - |
|
3677 from pip_e[unfolded is_create] |
|
3678 show ?thesis by (cases, simp) |
|
3679 qed |
|
3680 |
|
3681 lemma th_not_ready_s [simp]: "th \<notin> readys s" |
|
3682 using th_not_live_s by (unfold readys_def, simp) |
|
3683 |
|
3684 lemma th_live_es [simp]: "th \<in> threads (e#s)" |
|
3685 by (unfold is_create, simp) |
|
3686 |
|
3687 lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'" |
|
3688 proof |
|
3689 assume "waiting s th cs'" |
|
3690 from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3691 have "th \<in> set (wq s cs')" by auto |
|
3692 from wq_threads[OF this] have "th \<in> threads s" . |
|
3693 with th_not_live_s show False by simp |
|
3694 qed |
|
3695 |
|
3696 lemma not_holding_th_s [simp]: "\<not> holding s th cs'" |
|
3697 proof |
|
3698 assume "holding s th cs'" |
|
3699 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] |
|
3700 have "th \<in> set (wq s cs')" by auto |
|
3701 from wq_threads[OF this] have "th \<in> threads s" . |
|
3702 with th_not_live_s show False by simp |
|
3703 qed |
|
3704 |
|
3705 lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'" |
|
3706 proof |
|
3707 assume "waiting (e # s) th cs'" |
|
3708 from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3709 have "th \<in> set (wq s cs')" by auto |
|
3710 from wq_threads[OF this] have "th \<in> threads s" . |
|
3711 with th_not_live_s show False by simp |
|
3712 qed |
|
3713 |
|
3714 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'" |
|
3715 proof |
|
3716 assume "holding (e # s) th cs'" |
|
3717 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] |
|
3718 have "th \<in> set (wq s cs')" by auto |
|
3719 from wq_threads[OF this] have "th \<in> threads s" . |
|
3720 with th_not_live_s show False by simp |
|
3721 qed |
|
3722 |
|
3723 lemma ready_th_es [simp]: "th \<in> readys (e#s)" |
|
3724 by (simp add:readys_def) |
|
3725 |
|
3726 lemma holdents_th_s: "holdents s th = {}" |
|
3727 by (unfold holdents_def, auto) |
|
3728 |
|
3729 lemma holdents_th_es: "holdents (e#s) th = {}" |
|
3730 by (unfold holdents_def, auto) |
|
3731 |
|
3732 lemma cntCS_th_s [simp]: "cntCS s th = 0" |
|
3733 by (unfold cntCS_def, simp add:holdents_th_s) |
|
3734 |
|
3735 lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0" |
|
3736 by (unfold cntCS_def, simp add:holdents_th_es) |
|
3737 |
|
3738 lemma pvD_th_s [simp]: "pvD s th = 0" |
|
3739 by (unfold pvD_def, simp) |
|
3740 |
|
3741 lemma pvD_th_es [simp]: "pvD (e#s) th = 0" |
|
3742 by (unfold pvD_def, simp) |
|
3743 |
|
3744 lemma holdents_kept: |
|
3745 assumes "th' \<noteq> th" |
|
3746 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3747 proof - |
|
3748 { fix cs' |
|
3749 assume h: "cs' \<in> ?L" |
|
3750 hence "cs' \<in> ?R" |
|
3751 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3752 unfold wq_kept, auto) |
|
3753 } moreover { |
|
3754 fix cs' |
|
3755 assume h: "cs' \<in> ?R" |
|
3756 hence "cs' \<in> ?L" |
|
3757 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3758 unfold wq_kept, auto) |
|
3759 } ultimately show ?thesis by auto |
|
3760 qed |
|
3761 |
|
3762 lemma cntCS_kept [simp]: |
|
3763 assumes "th' \<noteq> th" |
|
3764 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R") |
|
3765 using holdents_kept[OF assms] |
|
3766 by (unfold cntCS_def, simp) |
|
3767 |
|
3768 lemma readys_kept1: |
|
3769 assumes "th' \<noteq> th" |
|
3770 and "th' \<in> readys (e#s)" |
|
3771 shows "th' \<in> readys s" |
|
3772 proof - |
|
3773 { fix cs' |
|
3774 assume wait: "waiting s th' cs'" |
|
3775 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3776 using assms by (auto simp:readys_def) |
|
3777 from wait[unfolded s_waiting_def, folded wq_def] |
|
3778 n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3779 have False by auto |
|
3780 } thus ?thesis using assms |
|
3781 by (unfold readys_def, auto) |
|
3782 qed |
|
3783 |
|
3784 lemma readys_kept2: |
|
3785 assumes "th' \<noteq> th" |
|
3786 and "th' \<in> readys s" |
|
3787 shows "th' \<in> readys (e#s)" |
|
3788 proof - |
|
3789 { fix cs' |
|
3790 assume wait: "waiting (e#s) th' cs'" |
|
3791 have n_wait: "\<not> waiting s th' cs'" |
|
3792 using assms(2) by (auto simp:readys_def) |
|
3793 from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3794 n_wait[unfolded s_waiting_def, folded wq_def] |
|
3795 have False by auto |
|
3796 } with assms show ?thesis |
|
3797 by (unfold readys_def, auto) |
|
3798 qed |
|
3799 |
|
3800 lemma readys_simp [simp]: |
|
3801 assumes "th' \<noteq> th" |
|
3802 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3803 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3804 by metis |
|
3805 |
|
3806 lemma pvD_kept [simp]: |
|
3807 assumes "th' \<noteq> th" |
|
3808 shows "pvD (e#s) th' = pvD s th'" |
|
3809 using assms |
|
3810 by (unfold pvD_def, simp) |
|
3811 |
|
3812 lemma cnp_cnv_cncs_kept: |
|
3813 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3814 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3815 proof - |
|
3816 { |
|
3817 assume eq_th': "th' = th" |
|
3818 have ?thesis using assms |
|
3819 by (unfold eq_th', simp, unfold is_create, simp) |
|
3820 } moreover { |
|
3821 assume h: "th' \<noteq> th" |
|
3822 hence ?thesis using assms |
|
3823 by (simp, simp add:is_create) |
|
3824 } ultimately show ?thesis by metis |
|
3825 qed |
|
3826 |
|
3827 end |
|
3828 |
|
3829 context valid_trace_exit |
|
3830 begin |
|
3831 |
|
3832 lemma th_live_s [simp]: "th \<in> threads s" |
|
3833 proof - |
|
3834 from pip_e[unfolded is_exit] |
|
3835 show ?thesis |
|
3836 by (cases, unfold runing_def readys_def, simp) |
|
3837 qed |
|
3838 |
|
3839 lemma th_ready_s [simp]: "th \<in> readys s" |
|
3840 proof - |
|
3841 from pip_e[unfolded is_exit] |
|
3842 show ?thesis |
|
3843 by (cases, unfold runing_def, simp) |
|
3844 qed |
|
3845 |
|
3846 lemma th_not_live_es [simp]: "th \<notin> threads (e#s)" |
|
3847 by (unfold is_exit, simp) |
|
3848 |
|
3849 lemma not_holding_th_s [simp]: "\<not> holding s th cs'" |
|
3850 proof - |
|
3851 from pip_e[unfolded is_exit] |
|
3852 show ?thesis |
|
3853 by (cases, unfold holdents_def, auto) |
|
3854 qed |
|
3855 |
|
3856 lemma cntCS_th_s [simp]: "cntCS s th = 0" |
|
3857 proof - |
|
3858 from pip_e[unfolded is_exit] |
|
3859 show ?thesis |
|
3860 by (cases, unfold cntCS_def, simp) |
|
3861 qed |
|
3862 |
|
3863 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'" |
|
3864 proof |
|
3865 assume "holding (e # s) th cs'" |
|
3866 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] |
|
3867 have "holding s th cs'" |
|
3868 by (unfold s_holding_def, fold wq_def, auto) |
|
3869 with not_holding_th_s |
|
3870 show False by simp |
|
3871 qed |
|
3872 |
|
3873 lemma ready_th_es [simp]: "th \<notin> readys (e#s)" |
|
3874 by (simp add:readys_def) |
|
3875 |
|
3876 lemma holdents_th_s: "holdents s th = {}" |
|
3877 by (unfold holdents_def, auto) |
|
3878 |
|
3879 lemma holdents_th_es: "holdents (e#s) th = {}" |
|
3880 by (unfold holdents_def, auto) |
|
3881 |
|
3882 lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0" |
|
3883 by (unfold cntCS_def, simp add:holdents_th_es) |
|
3884 |
|
3885 lemma pvD_th_s [simp]: "pvD s th = 0" |
|
3886 by (unfold pvD_def, simp) |
|
3887 |
|
3888 lemma pvD_th_es [simp]: "pvD (e#s) th = 0" |
|
3889 by (unfold pvD_def, simp) |
|
3890 |
|
3891 lemma holdents_kept: |
|
3892 assumes "th' \<noteq> th" |
|
3893 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3894 proof - |
|
3895 { fix cs' |
|
3896 assume h: "cs' \<in> ?L" |
|
3897 hence "cs' \<in> ?R" |
|
3898 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3899 unfold wq_kept, auto) |
|
3900 } moreover { |
|
3901 fix cs' |
|
3902 assume h: "cs' \<in> ?R" |
|
3903 hence "cs' \<in> ?L" |
|
3904 by (unfold holdents_def s_holding_def, fold wq_def, |
|
3905 unfold wq_kept, auto) |
|
3906 } ultimately show ?thesis by auto |
|
3907 qed |
|
3908 |
|
3909 lemma cntCS_kept [simp]: |
|
3910 assumes "th' \<noteq> th" |
|
3911 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R") |
|
3912 using holdents_kept[OF assms] |
|
3913 by (unfold cntCS_def, simp) |
|
3914 |
|
3915 lemma readys_kept1: |
|
3916 assumes "th' \<noteq> th" |
|
3917 and "th' \<in> readys (e#s)" |
|
3918 shows "th' \<in> readys s" |
|
3919 proof - |
|
3920 { fix cs' |
|
3921 assume wait: "waiting s th' cs'" |
|
3922 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
3923 using assms by (auto simp:readys_def) |
|
3924 from wait[unfolded s_waiting_def, folded wq_def] |
|
3925 n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3926 have False by auto |
|
3927 } thus ?thesis using assms |
|
3928 by (unfold readys_def, auto) |
|
3929 qed |
|
3930 |
|
3931 lemma readys_kept2: |
|
3932 assumes "th' \<noteq> th" |
|
3933 and "th' \<in> readys s" |
|
3934 shows "th' \<in> readys (e#s)" |
|
3935 proof - |
|
3936 { fix cs' |
|
3937 assume wait: "waiting (e#s) th' cs'" |
|
3938 have n_wait: "\<not> waiting s th' cs'" |
|
3939 using assms(2) by (auto simp:readys_def) |
|
3940 from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
3941 n_wait[unfolded s_waiting_def, folded wq_def] |
|
3942 have False by auto |
|
3943 } with assms show ?thesis |
|
3944 by (unfold readys_def, auto) |
|
3945 qed |
|
3946 |
|
3947 lemma readys_simp [simp]: |
|
3948 assumes "th' \<noteq> th" |
|
3949 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
3950 using readys_kept1[OF assms] readys_kept2[OF assms] |
|
3951 by metis |
|
3952 |
|
3953 lemma pvD_kept [simp]: |
|
3954 assumes "th' \<noteq> th" |
|
3955 shows "pvD (e#s) th' = pvD s th'" |
|
3956 using assms |
|
3957 by (unfold pvD_def, simp) |
|
3958 |
|
3959 lemma cnp_cnv_cncs_kept: |
|
3960 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
3961 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
3962 proof - |
|
3963 { |
|
3964 assume eq_th': "th' = th" |
|
3965 have ?thesis using assms |
|
3966 by (unfold eq_th', simp, unfold is_exit, simp) |
|
3967 } moreover { |
|
3968 assume h: "th' \<noteq> th" |
|
3969 hence ?thesis using assms |
|
3970 by (simp, simp add:is_exit) |
|
3971 } ultimately show ?thesis by metis |
|
3972 qed |
|
3973 |
|
3974 end |
|
3975 |
|
3976 context valid_trace_set |
|
3977 begin |
|
3978 |
|
3979 lemma th_live_s [simp]: "th \<in> threads s" |
|
3980 proof - |
|
3981 from pip_e[unfolded is_set] |
|
3982 show ?thesis |
|
3983 by (cases, unfold runing_def readys_def, simp) |
|
3984 qed |
|
3985 |
|
3986 lemma th_ready_s [simp]: "th \<in> readys s" |
|
3987 proof - |
|
3988 from pip_e[unfolded is_set] |
|
3989 show ?thesis |
|
3990 by (cases, unfold runing_def, simp) |
|
3991 qed |
|
3992 |
|
3993 lemma th_not_live_es [simp]: "th \<in> threads (e#s)" |
|
3994 by (unfold is_set, simp) |
|
3995 |
|
3996 |
|
3997 lemma holdents_kept: |
|
3998 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") |
|
3999 proof - |
|
4000 { fix cs' |
|
4001 assume h: "cs' \<in> ?L" |
|
4002 hence "cs' \<in> ?R" |
|
4003 by (unfold holdents_def s_holding_def, fold wq_def, |
|
4004 unfold wq_kept, auto) |
|
4005 } moreover { |
|
4006 fix cs' |
|
4007 assume h: "cs' \<in> ?R" |
|
4008 hence "cs' \<in> ?L" |
|
4009 by (unfold holdents_def s_holding_def, fold wq_def, |
|
4010 unfold wq_kept, auto) |
|
4011 } ultimately show ?thesis by auto |
|
4012 qed |
|
4013 |
|
4014 lemma cntCS_kept [simp]: |
|
4015 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R") |
|
4016 using holdents_kept |
|
4017 by (unfold cntCS_def, simp) |
|
4018 |
|
4019 lemma threads_kept[simp]: |
|
4020 "threads (e#s) = threads s" |
|
4021 by (unfold is_set, simp) |
|
4022 |
|
4023 lemma readys_kept1: |
|
4024 assumes "th' \<in> readys (e#s)" |
|
4025 shows "th' \<in> readys s" |
|
4026 proof - |
|
4027 { fix cs' |
|
4028 assume wait: "waiting s th' cs'" |
|
4029 have n_wait: "\<not> waiting (e#s) th' cs'" |
|
4030 using assms by (auto simp:readys_def) |
|
4031 from wait[unfolded s_waiting_def, folded wq_def] |
|
4032 n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
4033 have False by auto |
|
4034 } moreover have "th' \<in> threads s" |
|
4035 using assms[unfolded readys_def] by auto |
|
4036 ultimately show ?thesis |
|
4037 by (unfold readys_def, auto) |
|
4038 qed |
|
4039 |
|
4040 lemma readys_kept2: |
|
4041 assumes "th' \<in> readys s" |
|
4042 shows "th' \<in> readys (e#s)" |
|
4043 proof - |
|
4044 { fix cs' |
|
4045 assume wait: "waiting (e#s) th' cs'" |
|
4046 have n_wait: "\<not> waiting s th' cs'" |
|
4047 using assms by (auto simp:readys_def) |
|
4048 from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept] |
|
4049 n_wait[unfolded s_waiting_def, folded wq_def] |
|
4050 have False by auto |
|
4051 } with assms show ?thesis |
|
4052 by (unfold readys_def, auto) |
|
4053 qed |
|
4054 |
|
4055 lemma readys_simp [simp]: |
|
4056 shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)" |
|
4057 using readys_kept1 readys_kept2 |
|
4058 by metis |
|
4059 |
|
4060 lemma pvD_kept [simp]: |
|
4061 shows "pvD (e#s) th' = pvD s th'" |
|
4062 by (unfold pvD_def, simp) |
|
4063 |
|
4064 lemma cnp_cnv_cncs_kept: |
|
4065 assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
4066 shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" |
|
4067 using assms |
|
4068 by (unfold is_set, simp, fold is_set, simp) |
|
4069 |
|
4070 end |
|
4071 |
|
4072 context valid_trace |
|
4073 begin |
|
4074 |
|
4075 lemma cnp_cnv_cncs: "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" |
|
4076 proof(induct rule:ind) |
|
4077 case Nil |
|
4078 thus ?case |
|
4079 by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def |
|
4080 s_holding_def, simp) |
|
4081 next |
|
4082 case (Cons s e) |
|
4083 interpret vt_e: valid_trace_e s e using Cons by simp |
|
4084 show ?case |
|
4085 proof(cases e) |
|
4086 case (Create th prio) |
|
4087 interpret vt_create: valid_trace_create s e th prio |
|
4088 using Create by (unfold_locales, simp) |
|
4089 show ?thesis using Cons by (simp add: vt_create.cnp_cnv_cncs_kept) |
|
4090 next |
|
4091 case (Exit th) |
|
4092 interpret vt_exit: valid_trace_exit s e th |
|
4093 using Exit by (unfold_locales, simp) |
|
4094 show ?thesis using Cons by (simp add: vt_exit.cnp_cnv_cncs_kept) |
|
4095 next |
|
4096 case (P th cs) |
|
4097 interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp) |
|
4098 show ?thesis using Cons by (simp add: vt_p.cnp_cnv_cncs_kept) |
|
4099 next |
|
4100 case (V th cs) |
|
4101 interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp) |
|
4102 show ?thesis using Cons by (simp add: vt_v.cnp_cnv_cncs_kept) |
|
4103 next |
|
4104 case (Set th prio) |
|
4105 interpret vt_set: valid_trace_set s e th prio |
|
4106 using Set by (unfold_locales, simp) |
|
4107 show ?thesis using Cons by (simp add: vt_set.cnp_cnv_cncs_kept) |
|
4108 qed |
|
4109 qed |
|
4110 |
|
4111 end |
|
4112 |
|
4113 section {* Corollaries of @{thm valid_trace.cnp_cnv_cncs} *} |
|
4114 |
|
4115 context valid_trace |
|
4116 begin |
|
4117 |
|
4118 lemma not_thread_holdents: |
|
4119 assumes not_in: "th \<notin> threads s" |
|
4120 shows "holdents s th = {}" |
|
4121 proof - |
|
4122 { fix cs |
|
4123 assume "cs \<in> holdents s th" |
|
4124 hence "holding s th cs" by (auto simp:holdents_def) |
|
4125 from this[unfolded s_holding_def, folded wq_def] |
|
4126 have "th \<in> set (wq s cs)" by auto |
|
4127 with wq_threads have "th \<in> threads s" by auto |
|
4128 with assms |
|
4129 have False by simp |
|
4130 } thus ?thesis by auto |
|
4131 qed |
|
4132 |
|
4133 lemma not_thread_cncs: |
|
4134 assumes not_in: "th \<notin> threads s" |
|
4135 shows "cntCS s th = 0" |
|
4136 using not_thread_holdents[OF assms] |
|
4137 by (simp add:cntCS_def) |
|
4138 |
|
4139 lemma cnp_cnv_eq: |
|
4140 assumes "th \<notin> threads s" |
|
4141 shows "cntP s th = cntV s th" |
|
4142 using assms cnp_cnv_cncs not_thread_cncs pvD_def |
|
4143 by (auto) |
|
4144 |
|
4145 lemma eq_pv_children: |
|
4146 assumes eq_pv: "cntP s th = cntV s th" |
|
4147 shows "children (RAG s) (Th th) = {}" |
|
4148 proof - |
|
4149 from cnp_cnv_cncs and eq_pv |
|
4150 have "cntCS s th = 0" |
|
4151 by (auto split:if_splits) |
|
4152 from this[unfolded cntCS_def holdents_alt_def] |
|
4153 have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" . |
|
4154 have "finite (the_cs ` children (RAG s) (Th th))" |
|
4155 by (simp add: fsbtRAGs.finite_children) |
|
4156 from card_0[unfolded card_0_eq[OF this]] |
|
4157 show ?thesis by auto |
|
4158 qed |
|
4159 |
|
4160 lemma eq_pv_holdents: |
|
4161 assumes eq_pv: "cntP s th = cntV s th" |
|
4162 shows "holdents s th = {}" |
|
4163 by (unfold holdents_alt_def eq_pv_children[OF assms], simp) |
|
4164 |
|
4165 lemma eq_pv_subtree: |
|
4166 assumes eq_pv: "cntP s th = cntV s th" |
|
4167 shows "subtree (RAG s) (Th th) = {Th th}" |
|
4168 using eq_pv_children[OF assms] |
|
4169 by (unfold subtree_children, simp) |
|
4170 |
4150 lemma count_eq_RAG_plus: |
4171 lemma count_eq_RAG_plus: |
4151 assumes "cntP s th = cntV s th" |
4172 assumes "cntP s th = cntV s th" |
4152 shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
4173 shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}" |
4153 proof(rule ccontr) |
4174 proof(rule ccontr) |
4154 assume otherwise: "{th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} \<noteq> {}" |
4175 assume otherwise: "{th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} \<noteq> {}" |