171 ultimately show ?thesis by auto |
171 ultimately show ?thesis by auto |
172 qed |
172 qed |
173 qed |
173 qed |
174 qed |
174 qed |
175 |
175 |
176 lemma vt_moment: "\<And> t. \<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)" |
176 lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)" |
177 proof(induct s, simp) |
177 proof(induct s, simp) |
178 fix a s t |
178 fix a s t |
179 assume h: "\<And>t.\<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)" |
179 assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)" |
180 and vt_a: "vt (a # s)" |
180 and vt_a: "vt (a # s)" |
181 and le_t: "t \<le> length (a # s)" |
|
182 show "vt (moment t (a # s))" |
181 show "vt (moment t (a # s))" |
183 proof(cases "t = length (a#s)") |
182 proof(cases "t \<ge> length (a#s)") |
184 case True |
183 case True |
185 from True have "moment t (a#s) = a#s" by simp |
184 from True have "moment t (a#s) = a#s" by simp |
186 with vt_a show ?thesis by simp |
185 with vt_a show ?thesis by simp |
187 next |
186 next |
188 case False |
187 case False |
189 with le_t have le_t1: "t \<le> length s" by simp |
188 hence le_t1: "t \<le> length s" by simp |
190 from vt_a have "vt s" |
189 from vt_a have "vt s" |
191 by (erule_tac evt_cons, simp) |
190 by (erule_tac evt_cons, simp) |
192 from h [OF this le_t1] have "vt (moment t s)" . |
191 from h [OF this] have "vt (moment t s)" . |
193 moreover have "moment t (a#s) = moment t s" |
192 moreover have "moment t (a#s) = moment t s" |
194 proof - |
193 proof - |
195 from moment_app [OF le_t1, of "[a]"] |
194 from moment_app [OF le_t1, of "[a]"] |
196 show ?thesis by simp |
195 show ?thesis by simp |
197 qed |
196 qed |
242 from nn2 [rule_format, OF this] and eq_m |
241 from nn2 [rule_format, OF this] and eq_m |
243 have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and |
242 have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and |
244 h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto |
243 h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto |
245 have vt_e: "vt (e#moment t2 s)" |
244 have vt_e: "vt (e#moment t2 s)" |
246 proof - |
245 proof - |
247 from vt_moment [OF vt le_t3] |
246 from vt_moment [OF vt] |
248 have "vt (moment ?t3 s)" . |
247 have "vt (moment ?t3 s)" . |
249 with eq_m show ?thesis by simp |
248 with eq_m show ?thesis by simp |
250 qed |
249 qed |
251 have ?thesis |
250 have ?thesis |
252 proof(cases "thread \<in> set (wq (moment t2 s) cs2)") |
251 proof(cases "thread \<in> set (wq (moment t2 s) cs2)") |
275 from nn1 [rule_format, OF this] and eq_m |
274 from nn1 [rule_format, OF this] and eq_m |
276 have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and |
275 have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and |
277 h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto |
276 h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto |
278 have vt_e: "vt (e#moment t1 s)" |
277 have vt_e: "vt (e#moment t1 s)" |
279 proof - |
278 proof - |
280 from vt_moment [OF vt le_t3] |
279 from vt_moment [OF vt] |
281 have "vt (moment ?t3 s)" . |
280 have "vt (moment ?t3 s)" . |
282 with eq_m show ?thesis by simp |
281 with eq_m show ?thesis by simp |
283 qed |
282 qed |
284 have ?thesis |
283 have ?thesis |
285 proof(cases "thread \<in> set (wq (moment t1 s) cs1)") |
284 proof(cases "thread \<in> set (wq (moment t1 s) cs1)") |
308 from nn1 [rule_format, OF this] and eq_m |
307 from nn1 [rule_format, OF this] and eq_m |
309 have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and |
308 have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and |
310 h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto |
309 h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto |
311 have vt_e: "vt (e#moment t1 s)" |
310 have vt_e: "vt (e#moment t1 s)" |
312 proof - |
311 proof - |
313 from vt_moment [OF vt le_t3] |
312 from vt_moment [OF vt] |
314 have "vt (moment ?t3 s)" . |
313 have "vt (moment ?t3 s)" . |
315 with eq_m show ?thesis by simp |
314 with eq_m show ?thesis by simp |
316 qed |
315 qed |
317 have ?thesis |
316 have ?thesis |
318 proof(cases "thread \<in> set (wq (moment t1 s) cs1)") |
317 proof(cases "thread \<in> set (wq (moment t1 s) cs1)") |
340 show ?thesis . |
339 show ?thesis . |
341 next |
340 next |
342 case False |
341 case False |
343 have vt_e: "vt (e#moment t2 s)" |
342 have vt_e: "vt (e#moment t2 s)" |
344 proof - |
343 proof - |
345 from vt_moment [OF vt le_t3] eqt12 |
344 from vt_moment [OF vt] eqt12 |
346 have "vt (moment (Suc t2) s)" by auto |
345 have "vt (moment (Suc t2) s)" by auto |
347 with eq_m eqt12 show ?thesis by simp |
346 with eq_m eqt12 show ?thesis by simp |
348 qed |
347 qed |
349 from block_pre [OF vt_e False h1] |
348 from block_pre [OF vt_e False h1] |
350 have "e = P thread cs2" . |
349 have "e = P thread cs2" . |
2769 proof |
2768 proof |
2770 show "f ` A \<subseteq> g ` A" |
2769 show "f ` A \<subseteq> g ` A" |
2771 by(rule image_subsetI, auto intro:h) |
2770 by(rule image_subsetI, auto intro:h) |
2772 next |
2771 next |
2773 show "g ` A \<subseteq> f ` A" |
2772 show "g ` A \<subseteq> f ` A" |
2774 by(rule image_subsetI, auto intro:h[symmetric]) |
2773 by (rule image_subsetI, auto intro:h[symmetric]) |
2775 qed |
2774 qed |
|
2775 |
|
2776 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
|
2777 where "detached s th \<equiv> (Th th \<notin> Field (depend s))" |
|
2778 |
|
2779 lemma detached_intro: |
|
2780 fixes s th |
|
2781 assumes vt: "vt s" |
|
2782 and eq_pv: "cntP s th = cntV s th" |
|
2783 shows "detached s th" |
|
2784 proof - |
|
2785 from cnp_cnv_cncs[OF vt] |
|
2786 have eq_cnt: "cntP s th = |
|
2787 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . |
|
2788 hence cncs_zero: "cntCS s th = 0" |
|
2789 by (auto simp:eq_pv split:if_splits) |
|
2790 with eq_cnt |
|
2791 have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:eq_pv) |
|
2792 thus ?thesis |
|
2793 proof |
|
2794 assume "th \<notin> threads s" |
|
2795 with range_in[OF vt] dm_depend_threads[OF vt] |
|
2796 show ?thesis |
|
2797 by (auto simp:detached_def Field_def Domain_def Range_def) |
|
2798 next |
|
2799 assume "th \<in> readys s" |
|
2800 moreover have "Th th \<notin> Range (depend s)" |
|
2801 proof - |
|
2802 from card_0_eq [OF finite_holding [OF vt]] and cncs_zero |
|
2803 have "holdents s th = {}" |
|
2804 by (simp add:cntCS_def) |
|
2805 thus ?thesis |
|
2806 by (auto simp:holdents_def, case_tac x, |
|
2807 auto simp:holdents_def s_depend_def) |
|
2808 qed |
|
2809 ultimately show ?thesis |
|
2810 apply (auto simp:detached_def Field_def Domain_def readys_def) |
|
2811 apply (case_tac y, auto simp:s_depend_def) |
|
2812 by (erule_tac x = "nat" in allE, simp add: eq_waiting) |
|
2813 qed |
|
2814 qed |
|
2815 |
|
2816 lemma detached_elim: |
|
2817 fixes s th |
|
2818 assumes vt: "vt s" |
|
2819 and dtc: "detached s th" |
|
2820 shows "cntP s th = cntV s th" |
|
2821 proof - |
|
2822 from cnp_cnv_cncs[OF vt] |
|
2823 have eq_pv: " cntP s th = |
|
2824 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" . |
|
2825 have cncs_z: "cntCS s th = 0" |
|
2826 proof - |
|
2827 from dtc have "holdents s th = {}" |
|
2828 by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def) |
|
2829 thus ?thesis by (auto simp:cntCS_def) |
|
2830 qed |
|
2831 show ?thesis |
|
2832 proof(cases "th \<in> threads s") |
|
2833 case True |
|
2834 with dtc |
|
2835 have "th \<in> readys s" |
|
2836 by (unfold readys_def detached_def Field_def Domain_def Range_def, |
|
2837 auto simp:eq_waiting s_depend_def) |
|
2838 with cncs_z and eq_pv show ?thesis by simp |
|
2839 next |
|
2840 case False |
|
2841 with cncs_z and eq_pv show ?thesis by simp |
|
2842 qed |
|
2843 qed |
|
2844 |
|
2845 lemma detached_eq: |
|
2846 fixes s th |
|
2847 assumes vt: "vt s" |
|
2848 shows "(detached s th) = (cntP s th = cntV s th)" |
|
2849 by (insert vt, auto intro:detached_intro detached_elim) |
2776 |
2850 |
2777 end |
2851 end |