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'