PIPBasics.thy
changeset 101 c7db2ccba18a
parent 100 3d2b59f15f26
child 102 3a801bbd2687
equal deleted inserted replaced
100:3d2b59f15f26 101:c7db2ccba18a
   169   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
   169   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
   170 
   170 
   171 lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
   171 lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
   172   by (unfold s_holding_def wq_def cs_holding_def, simp)
   172   by (unfold s_holding_def wq_def cs_holding_def, simp)
   173 
   173 
       
   174 lemma children_RAG_alt_def:
       
   175   "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
       
   176   by (unfold s_RAG_def, auto simp:children_def holding_eq)
       
   177 
       
   178 lemma holdents_alt_def:
       
   179   "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"
       
   180   by (unfold children_RAG_alt_def holdents_def, simp add: image_image)
       
   181 
       
   182 lemma cntCS_alt_def:
       
   183   "cntCS s th = card (children (RAG s) (Th th))"
       
   184   apply (unfold children_RAG_alt_def cntCS_def holdents_def)
       
   185   by (rule card_image[symmetric], auto simp:inj_on_def)
       
   186 
   174 lemma runing_ready: 
   187 lemma runing_ready: 
   175   shows "runing s \<subseteq> readys s"
   188   shows "runing s \<subseteq> readys s"
   176   unfolding runing_def readys_def
   189   unfolding runing_def readys_def
   177   by auto 
   190   by auto 
   178 
   191 
   270   assumes "(n1, n2) \<in> RAG (s::state)"
   283   assumes "(n1, n2) \<in> RAG (s::state)"
   271   obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
   284   obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
   272       | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
   285       | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
   273   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
   286   using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
   274   by auto
   287   by auto
       
   288 
       
   289 lemma count_rec1 [simp]: 
       
   290   assumes "Q e"
       
   291   shows "count Q (e#es) = Suc (count Q es)"
       
   292   using assms
       
   293   by (unfold count_def, auto)
       
   294 
       
   295 lemma count_rec2 [simp]: 
       
   296   assumes "\<not>Q e"
       
   297   shows "count Q (e#es) = (count Q es)"
       
   298   using assms
       
   299   by (unfold count_def, auto)
       
   300 
       
   301 lemma count_rec3 [simp]: 
       
   302   shows "count Q [] =  0"
       
   303   by (unfold count_def, auto)
       
   304 
       
   305 lemma cntP_simp1[simp]:
       
   306   "cntP (P th cs'#s) th = cntP s th + 1"
       
   307   by (unfold cntP_def, simp)
       
   308 
       
   309 lemma cntP_simp2[simp]:
       
   310   assumes "th' \<noteq> th"
       
   311   shows "cntP (P th cs'#s) th' = cntP s th'"
       
   312   using assms
       
   313   by (unfold cntP_def, simp)
       
   314 
       
   315 lemma cntP_simp3[simp]:
       
   316   assumes "\<not> isP e"
       
   317   shows "cntP (e#s) th' = cntP s th'"
       
   318   using assms
       
   319   by (unfold cntP_def, cases e, simp+)
       
   320 
       
   321 lemma cntV_simp1[simp]:
       
   322   "cntV (V th cs'#s) th = cntV s th + 1"
       
   323   by (unfold cntV_def, simp)
       
   324 
       
   325 lemma cntV_simp2[simp]:
       
   326   assumes "th' \<noteq> th"
       
   327   shows "cntV (V th cs'#s) th' = cntV s th'"
       
   328   using assms
       
   329   by (unfold cntV_def, simp)
       
   330 
       
   331 lemma cntV_simp3[simp]:
       
   332   assumes "\<not> isV e"
       
   333   shows "cntV (e#s) th' = cntV s th'"
       
   334   using assms
       
   335   by (unfold cntV_def, cases e, simp+)
       
   336 
       
   337 lemma cntP_diff_inv:
       
   338   assumes "cntP (e#s) th \<noteq> cntP s th"
       
   339   shows "isP e \<and> actor e = th"
       
   340 proof(cases e)
       
   341   case (P th' pty)
       
   342   show ?thesis
       
   343   by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", 
       
   344         insert assms P, auto simp:cntP_def)
       
   345 qed (insert assms, auto simp:cntP_def)
       
   346   
       
   347 lemma cntV_diff_inv:
       
   348   assumes "cntV (e#s) th \<noteq> cntV s th"
       
   349   shows "isV e \<and> actor e = th"
       
   350 proof(cases e)
       
   351   case (V th' pty)
       
   352   show ?thesis
       
   353   by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", 
       
   354         insert assms V, auto simp:cntV_def)
       
   355 qed (insert assms, auto simp:cntV_def)
       
   356 
       
   357 lemma eq_dependants: "dependants (wq s) = dependants s"
       
   358   by (simp add: s_dependants_abv wq_def)
       
   359 
       
   360 lemma inj_the_preced: 
       
   361   "inj_on (the_preced s) (threads s)"
       
   362   by (metis inj_onI preced_unique the_preced_def)
   275 
   363 
   276 (* ccc *)
   364 (* ccc *)
   277 
   365 
   278 section {* Locales used to investigate the execution of PIP *}
   366 section {* Locales used to investigate the execution of PIP *}
   279 
   367 
   703   using assms by simp
   791   using assms by simp
   704 end
   792 end
   705 
   793 
   706 context valid_trace
   794 context valid_trace
   707 begin
   795 begin
       
   796 
       
   797 lemma  finite_threads:
       
   798   shows "finite (threads s)"
       
   799   using vt by (induct) (auto elim: step.cases)
       
   800 
       
   801 lemma finite_readys [simp]: "finite (readys s)"
       
   802   using finite_threads readys_threads rev_finite_subset by blast
   708 
   803 
   709 lemma wq_distinct: "distinct (wq s cs)"
   804 lemma wq_distinct: "distinct (wq s cs)"
   710 proof(induct rule:ind)
   805 proof(induct rule:ind)
   711   case (Cons s e)
   806   case (Cons s e)
   712   interpret vt_e: valid_trace_e s e using Cons by simp
   807   interpret vt_e: valid_trace_e s e using Cons by simp
  2073       from tranclD[OF this]
  2168       from tranclD[OF this]
  2074       obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
  2169       obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
  2075         by (unfold s_RAG_def, auto)
  2170         by (unfold s_RAG_def, auto)
  2076       hence "waiting s th cs'" 
  2171       hence "waiting s th cs'" 
  2077         by (unfold s_RAG_def, fold waiting_eq, auto)
  2172         by (unfold s_RAG_def, fold waiting_eq, auto)
  2078       with th_not_waiting show False by auto (* ccc *)
  2173       with th_not_waiting show False by auto 
  2079     qed
  2174     qed
  2080     ultimately show ?thesis by auto
  2175     ultimately show ?thesis by auto
  2081   qed
  2176   qed
  2082   thus ?thesis by (unfold RAG_es, simp)
  2177   thus ?thesis by (unfold RAG_es, simp)
  2083 qed
  2178 qed
  2245       from wf_RAG show "wf (RAG s)" .
  2340       from wf_RAG show "wf (RAG s)" .
  2246     qed
  2341     qed
  2247   qed
  2342   qed
  2248 qed
  2343 qed
  2249 
  2344 
       
  2345 
  2250 section {* Derived properties for parts of RAG *}
  2346 section {* Derived properties for parts of RAG *}
  2251 
  2347 
  2252 context valid_trace
  2348 context valid_trace
  2253 begin
  2349 begin
  2254 
  2350 
  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> {}"
  4166 proof -
  4187 proof -
  4167   from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
  4188   from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
  4168   show ?thesis .
  4189   show ?thesis .
  4169 qed
  4190 qed
  4170 
  4191 
  4171 end
       
  4172 
       
  4173 lemma eq_dependants: "dependants (wq s) = dependants s"
       
  4174   by (simp add: s_dependants_abv wq_def)
       
  4175 
       
  4176 context valid_trace
       
  4177 begin
       
  4178 
       
  4179 lemma count_eq_tRAG_plus:
  4192 lemma count_eq_tRAG_plus:
  4180   assumes "cntP s th = cntV s th"
  4193   assumes "cntP s th = cntV s th"
  4181   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
  4194   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
  4182   using assms eq_pv_dependants dependants_alt_def eq_dependants by auto 
  4195   using assms eq_pv_dependants dependants_alt_def eq_dependants by auto 
  4183 
  4196 
  4188 
  4201 
  4189 lemma count_eq_tRAG_plus_Th:
  4202 lemma count_eq_tRAG_plus_Th:
  4190   assumes "cntP s th = cntV s th"
  4203   assumes "cntP s th = cntV s th"
  4191   shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
  4204   shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
  4192    using count_eq_tRAG_plus[OF assms] by auto
  4205    using count_eq_tRAG_plus[OF assms] by auto
  4193 end
  4206 
  4194 
  4207 end
  4195 lemma inj_the_preced: 
  4208 
  4196   "inj_on (the_preced s) (threads s)"
  4209 section {* hhh *}
  4197   by (metis inj_onI preced_unique the_preced_def)
       
  4198 
       
  4199 lemma tRAG_Field:
       
  4200   "Field (tRAG s) \<subseteq> Field (RAG s)"
       
  4201   by (unfold tRAG_alt_def Field_def, auto)
       
  4202 
       
  4203 lemma tRAG_ancestorsE:
       
  4204   assumes "x \<in> ancestors (tRAG s) u"
       
  4205   obtains th where "x = Th th"
       
  4206 proof -
       
  4207   from assms have "(u, x) \<in> (tRAG s)^+" 
       
  4208       by (unfold ancestors_def, auto)
       
  4209   from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
       
  4210   then obtain th where "x = Th th"
       
  4211     by (unfold tRAG_alt_def, auto)
       
  4212   from that[OF this] show ?thesis .
       
  4213 qed
       
  4214 
       
  4215 lemma tRAG_mono:
       
  4216   assumes "RAG s' \<subseteq> RAG s"
       
  4217   shows "tRAG s' \<subseteq> tRAG s"
       
  4218   using assms 
       
  4219   by (unfold tRAG_alt_def, auto)
       
  4220 
       
  4221 lemma holding_next_thI:
       
  4222   assumes "holding s th cs"
       
  4223   and "length (wq s cs) > 1"
       
  4224   obtains th' where "next_th s th cs th'"
       
  4225 proof -
       
  4226   from assms(1)[folded holding_eq, unfolded cs_holding_def]
       
  4227   have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 
       
  4228     by (unfold s_holding_def, fold wq_def, auto)
       
  4229   then obtain rest where h1: "wq s cs = th#rest" 
       
  4230     by (cases "wq s cs", auto)
       
  4231   with assms(2) have h2: "rest \<noteq> []" by auto
       
  4232   let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
       
  4233   have "next_th s th cs ?th'" using  h1(1) h2 
       
  4234     by (unfold next_th_def, auto)
       
  4235   from that[OF this] show ?thesis .
       
  4236 qed
       
  4237 
  4210 
  4238 lemma RAG_tRAG_transfer:
  4211 lemma RAG_tRAG_transfer:
  4239   assumes "vt s'"
  4212   assumes "vt s'"
  4240   assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
  4213   assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
  4241   and "(Cs cs, Th th'') \<in> RAG s'"
  4214   and "(Cs cs, Th th'') \<in> RAG s'"
  4298 
  4271 
  4299 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
  4272 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
  4300 
  4273 
  4301 end
  4274 end
  4302 
  4275 
  4303 lemma tRAG_subtree_eq: 
       
  4304    "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"
       
  4305    (is "?L = ?R")
       
  4306 proof -
       
  4307   { fix n 
       
  4308     assume h: "n \<in> ?L"
       
  4309     hence "n \<in> ?R"
       
  4310     by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 
       
  4311   } moreover {
       
  4312     fix n
       
  4313     assume "n \<in> ?R"
       
  4314     then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"
       
  4315       by (auto simp:subtree_def)
       
  4316     from rtranclD[OF this(2)]
       
  4317     have "n \<in> ?L"
       
  4318     proof
       
  4319       assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
       
  4320       with h have "n \<in> {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}" by auto
       
  4321       thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
       
  4322     qed (insert h, auto simp:subtree_def)
       
  4323   } ultimately show ?thesis by auto
       
  4324 qed
       
  4325 
       
  4326 lemma threads_set_eq: 
       
  4327    "the_thread ` (subtree (tRAG s) (Th th)) = 
       
  4328                   {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
       
  4329    by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
       
  4330 
       
  4331 lemma cp_alt_def1: 
  4276 lemma cp_alt_def1: 
  4332   "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
  4277   "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
  4333 proof -
  4278 proof -
  4334   have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
  4279   have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
  4335        ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
  4280        ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
  4658       show ?thesis .
  4603       show ?thesis .
  4659     qed
  4604     qed
  4660   } ultimately show ?thesis by auto
  4605   } ultimately show ?thesis by auto
  4661 qed
  4606 qed
  4662 
  4607 
  4663 lemma finite_readys [simp]: "finite (readys s)"
       
  4664   using finite_threads readys_threads rev_finite_subset by blast
       
  4665 
  4608 
  4666 text {* (* ccc *) \noindent
  4609 text {* (* ccc *) \noindent
  4667   Since the current precedence of the threads in ready queue will always be boosted,
  4610   Since the current precedence of the threads in ready queue will always be boosted,
  4668   there must be one inside it has the maximum precedence of the whole system. 
  4611   there must be one inside it has the maximum precedence of the whole system. 
  4669 *}
  4612 *}
  4700     thus ?thesis by simp
  4643     thus ?thesis by simp
  4701   qed
  4644   qed
  4702   finally show ?thesis by simp
  4645   finally show ?thesis by simp
  4703 qed (auto simp:threads_alt_def)
  4646 qed (auto simp:threads_alt_def)
  4704 
  4647 
  4705 end
  4648 lemma create_pre:
  4706 
  4649   assumes stp: "step s e"
  4707 end
  4650   and not_in: "th \<notin> threads s"
  4708 
  4651   and is_in: "th \<in> threads (e#s)"
       
  4652   obtains prio where "e = Create th prio"
       
  4653 proof -
       
  4654   from assms  
       
  4655   show ?thesis
       
  4656   proof(cases)
       
  4657     case (thread_create thread prio)
       
  4658     with is_in not_in have "e = Create th prio" by simp
       
  4659     from that[OF this] show ?thesis .
       
  4660   next
       
  4661     case (thread_exit thread)
       
  4662     with assms show ?thesis by (auto intro!:that)
       
  4663   next
       
  4664     case (thread_P thread)
       
  4665     with assms show ?thesis by (auto intro!:that)
       
  4666   next
       
  4667     case (thread_V thread)
       
  4668     with assms show ?thesis by (auto intro!:that)
       
  4669   next 
       
  4670     case (thread_set thread)
       
  4671     with assms show ?thesis by (auto intro!:that)
       
  4672   qed
       
  4673 qed
       
  4674 
       
  4675 end
       
  4676 
       
  4677 section {* Pending properties *}
       
  4678 
       
  4679 lemma holding_next_thI:
       
  4680   assumes "holding s th cs"
       
  4681   and "length (wq s cs) > 1"
       
  4682   obtains th' where "next_th s th cs th'"
       
  4683 proof -
       
  4684   from assms(1)[folded holding_eq, unfolded cs_holding_def]
       
  4685   have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 
       
  4686     by (unfold s_holding_def, fold wq_def, auto)
       
  4687   then obtain rest where h1: "wq s cs = th#rest" 
       
  4688     by (cases "wq s cs", auto)
       
  4689   with assms(2) have h2: "rest \<noteq> []" by auto
       
  4690   let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
       
  4691   have "next_th s th cs ?th'" using  h1(1) h2 
       
  4692     by (unfold next_th_def, auto)
       
  4693   from that[OF this] show ?thesis .
       
  4694 qed
       
  4695 
       
  4696 context valid_trace_e 
       
  4697 begin
       
  4698 
       
  4699 lemma actor_inv: 
       
  4700   assumes "\<not> isCreate e"
       
  4701   shows "actor e \<in> runing s"
       
  4702   using pip_e assms 
       
  4703   by (induct, auto)
       
  4704 
       
  4705 end
       
  4706 
       
  4707 end
       
  4708