equal
deleted
inserted
replaced
19 proof(cases) |
19 proof(cases) |
20 case (thread_create thread prio) |
20 case (thread_create thread prio) |
21 assume eq_e: "e = Create thread prio" |
21 assume eq_e: "e = Create thread prio" |
22 and not_in': "thread \<notin> threads s" |
22 and not_in': "thread \<notin> threads s" |
23 have "holdents (e # s) th = holdents s th" |
23 have "holdents (e # s) th = holdents s th" |
24 apply (unfold eq_e holdents_def) |
24 apply (unfold eq_e holdents_test) |
25 by (simp add:depend_create_unchanged) |
25 by (simp add:depend_create_unchanged) |
26 moreover have "th \<notin> threads s" |
26 moreover have "th \<notin> threads s" |
27 proof - |
27 proof - |
28 from not_in eq_e show ?thesis by simp |
28 from not_in eq_e show ?thesis by simp |
29 qed |
29 qed |
35 show ?thesis |
35 show ?thesis |
36 proof(cases "th = thread") |
36 proof(cases "th = thread") |
37 case True |
37 case True |
38 with nh eq_e |
38 with nh eq_e |
39 show ?thesis |
39 show ?thesis |
40 by (auto simp:holdents_def depend_exit_unchanged) |
40 by (auto simp:holdents_test depend_exit_unchanged) |
41 next |
41 next |
42 case False |
42 case False |
43 with not_in and eq_e |
43 with not_in and eq_e |
44 have "th \<notin> threads s" by simp |
44 have "th \<notin> threads s" by simp |
45 from ih[OF this] False eq_e show ?thesis |
45 from ih[OF this] False eq_e show ?thesis |
46 by (auto simp:holdents_def depend_exit_unchanged) |
46 by (auto simp:holdents_test depend_exit_unchanged) |
47 qed |
47 qed |
48 next |
48 next |
49 case (thread_P thread cs) |
49 case (thread_P thread cs) |
50 assume eq_e: "e = P thread cs" |
50 assume eq_e: "e = P thread cs" |
51 and is_runing: "thread \<in> runing s" |
51 and is_runing: "thread \<in> runing s" |
56 moreover from is_runing have "thread \<in> threads s" |
56 moreover from is_runing have "thread \<in> threads s" |
57 by (simp add:runing_def readys_def) |
57 by (simp add:runing_def readys_def) |
58 ultimately show ?thesis by auto |
58 ultimately show ?thesis by auto |
59 qed |
59 qed |
60 hence "holdents (e # s) th = holdents s th " |
60 hence "holdents (e # s) th = holdents s th " |
61 apply (unfold cntCS_def holdents_def eq_e) |
61 apply (unfold cntCS_def holdents_test eq_e) |
62 by (unfold step_depend_p[OF vtp], auto) |
62 by (unfold step_depend_p[OF vtp], auto) |
63 moreover have "holdents s th = {}" |
63 moreover have "holdents s th = {}" |
64 proof(rule ih) |
64 proof(rule ih) |
65 from not_in eq_e show "th \<notin> threads s" by simp |
65 from not_in eq_e show "th \<notin> threads s" by simp |
66 qed |
66 qed |
99 from wq_threads[OF step_back_vt[OF vtv], OF this] and ni |
99 from wq_threads[OF step_back_vt[OF vtv], OF this] and ni |
100 show False by auto |
100 show False by auto |
101 qed |
101 qed |
102 moreover note neq_th eq_wq |
102 moreover note neq_th eq_wq |
103 ultimately have "holdents (e # s) th = holdents s th" |
103 ultimately have "holdents (e # s) th = holdents s th" |
104 by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) |
104 by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) |
105 moreover have "holdents s th = {}" |
105 moreover have "holdents s th = {}" |
106 proof(rule ih) |
106 proof(rule ih) |
107 from not_in eq_e show "th \<notin> threads s" by simp |
107 from not_in eq_e show "th \<notin> threads s" by simp |
108 qed |
108 qed |
109 ultimately show ?thesis by simp |
109 ultimately show ?thesis by simp |
113 assume eq_e: "e = Set thread prio" |
113 assume eq_e: "e = Set thread prio" |
114 and is_runing: "thread \<in> runing s" |
114 and is_runing: "thread \<in> runing s" |
115 from not_in and eq_e have "th \<notin> threads s" by auto |
115 from not_in and eq_e have "th \<notin> threads s" by auto |
116 from ih [OF this] and eq_e |
116 from ih [OF this] and eq_e |
117 show ?thesis |
117 show ?thesis |
118 apply (unfold eq_e cntCS_def holdents_def) |
118 apply (unfold eq_e cntCS_def holdents_test) |
119 by (simp add:depend_set_unchanged) |
119 by (simp add:depend_set_unchanged) |
120 qed |
120 qed |
121 next |
121 next |
122 case vt_nil |
122 case vt_nil |
123 show ?case |
123 show ?case |
124 by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) |
124 by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) |
125 qed |
125 qed |
126 qed |
126 qed |
127 |
127 |
128 |
128 |
129 |
129 |
1917 then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+" |
1917 then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+" |
1918 by (auto simp:s_dependents_def eq_depend) |
1918 by (auto simp:s_dependents_def eq_depend) |
1919 from tranclE[OF this] obtain cs' where |
1919 from tranclE[OF this] obtain cs' where |
1920 "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def) |
1920 "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def) |
1921 with hdn |
1921 with hdn |
1922 have False by (auto simp:holdents_def) |
1922 have False by (auto simp:holdents_test) |
1923 } thus ?thesis by auto |
1923 } thus ?thesis by auto |
1924 qed |
1924 qed |
1925 thus ?thesis |
1925 thus ?thesis |
1926 by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp) |
1926 by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp) |
1927 qed |
1927 qed |