1540 { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast |
1540 { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast |
1541 assume neq_th: "th \<noteq> thread" |
1541 assume neq_th: "th \<noteq> thread" |
1542 with eq_e |
1542 with eq_e |
1543 have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))" |
1543 have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))" |
1544 apply (simp add:readys_def s_waiting_def wq_def Let_def) |
1544 apply (simp add:readys_def s_waiting_def wq_def Let_def) |
1545 apply (rule_tac hh, clarify) |
1545 apply (rule_tac hh) |
1546 apply (intro iffI allI, clarify) |
1546 apply (intro iffI allI, clarify) |
1547 apply (erule_tac x = csa in allE, auto) |
1547 apply (erule_tac x = csa in allE, auto) |
1548 apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) |
1548 apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) |
1549 apply (erule_tac x = cs in allE, auto) |
1549 apply (erule_tac x = cs in allE, auto) |
1550 by (case_tac "(wq_fun (schs s) cs)", auto) |
1550 by (case_tac "(wq_fun (schs s) cs)", auto) |
1551 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
1551 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
2067 qed |
2067 qed |
2068 |
2068 |
2069 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" |
2069 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" |
2070 unfolding cp_def wq_def |
2070 unfolding cp_def wq_def |
2071 apply(induct s rule: schs.induct) |
2071 apply(induct s rule: schs.induct) |
|
2072 thm cpreced_initial |
2072 apply(simp add: Let_def cpreced_initial) |
2073 apply(simp add: Let_def cpreced_initial) |
2073 apply(simp add: Let_def) |
2074 apply(simp add: Let_def) |
2074 apply(simp add: Let_def) |
2075 apply(simp add: Let_def) |
2075 apply(simp add: Let_def) |
2076 apply(simp add: Let_def) |
2076 apply(subst (2) schs.simps) |
2077 apply(subst (2) schs.simps) |
2086 and runing_1: "th1 \<in> runing s" |
2087 and runing_1: "th1 \<in> runing s" |
2087 and runing_2: "th2 \<in> runing s" |
2088 and runing_2: "th2 \<in> runing s" |
2088 shows "th1 = th2" |
2089 shows "th1 = th2" |
2089 proof - |
2090 proof - |
2090 from runing_1 and runing_2 have "cp s th1 = cp s th2" |
2091 from runing_1 and runing_2 have "cp s th1 = cp s th2" |
2091 by (unfold runing_def, simp) |
2092 unfolding runing_def |
|
2093 apply(simp) |
|
2094 done |
2092 hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) = |
2095 hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) = |
2093 Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))" |
2096 Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))" |
2094 (is "Max (?f ` ?A) = Max (?f ` ?B)") |
2097 (is "Max (?f ` ?A) = Max (?f ` ?B)") |
2095 by (unfold cp_eq_cpreced cpreced_def) |
2098 thm cp_def image_Collect |
|
2099 unfolding cp_eq_cpreced |
|
2100 unfolding cpreced_def . |
2096 obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)" |
2101 obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)" |
|
2102 thm Max_in |
2097 proof - |
2103 proof - |
2098 have h1: "finite (?f ` ?A)" |
2104 have h1: "finite (?f ` ?A)" |
2099 proof - |
2105 proof - |
2100 have "finite ?A" |
2106 have "finite ?A" |
2101 proof - |
2107 proof - |
2126 moreover have h2: "(?f ` ?A) \<noteq> {}" |
2132 moreover have h2: "(?f ` ?A) \<noteq> {}" |
2127 proof - |
2133 proof - |
2128 have "?A \<noteq> {}" by simp |
2134 have "?A \<noteq> {}" by simp |
2129 thus ?thesis by simp |
2135 thus ?thesis by simp |
2130 qed |
2136 qed |
|
2137 thm Max_in |
2131 from Max_in [OF h1 h2] |
2138 from Max_in [OF h1 h2] |
2132 have "Max (?f ` ?A) \<in> (?f ` ?A)" . |
2139 have "Max (?f ` ?A) \<in> (?f ` ?A)" . |
2133 thus ?thesis by (auto intro:that) |
2140 thus ?thesis |
|
2141 thm cpreced_def |
|
2142 unfolding cpreced_def[symmetric] |
|
2143 unfolding cp_eq_cpreced[symmetric] |
|
2144 unfolding cpreced_def |
|
2145 using that[intro] by (auto) |
2134 qed |
2146 qed |
2135 obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)" |
2147 obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)" |
2136 proof - |
2148 proof - |
2137 have h1: "finite (?f ` ?B)" |
2149 have h1: "finite (?f ` ?B)" |
2138 proof - |
2150 proof - |
2271 |
2283 |
2272 lemma "vt s \<Longrightarrow> card (runing s) \<le> 1" |
2284 lemma "vt s \<Longrightarrow> card (runing s) \<le> 1" |
2273 apply(subgoal_tac "finite (runing s)") |
2285 apply(subgoal_tac "finite (runing s)") |
2274 prefer 2 |
2286 prefer 2 |
2275 apply (metis finite_nat_set_iff_bounded lessI runing_unique) |
2287 apply (metis finite_nat_set_iff_bounded lessI runing_unique) |
|
2288 apply(rule ccontr) |
|
2289 apply(simp) |
2276 apply(case_tac "Suc (Suc 0) \<le> card (runing s)") |
2290 apply(case_tac "Suc (Suc 0) \<le> card (runing s)") |
2277 apply(subst (asm) card_le_Suc_iff) |
2291 apply(subst (asm) card_le_Suc_iff) |
2278 apply(simp) |
2292 apply(simp) |
2279 apply(auto)[1] |
2293 apply(auto)[1] |
2280 apply (metis insertCI runing_unique) |
2294 apply (metis insertCI runing_unique) |