equal
deleted
inserted
replaced
2267 qed |
2267 qed |
2268 qed |
2268 qed |
2269 qed |
2269 qed |
2270 |
2270 |
2271 |
2271 |
|
2272 lemma "vt s \<Longrightarrow> card (runing s) \<le> 1" |
|
2273 apply(subgoal_tac "finite (runing s)") |
|
2274 prefer 2 |
|
2275 apply (metis finite_nat_set_iff_bounded lessI runing_unique) |
|
2276 apply(case_tac "Suc (Suc 0) \<le> card (runing s)") |
|
2277 apply(subst (asm) card_le_Suc_iff) |
|
2278 apply(simp) |
|
2279 apply(auto)[1] |
|
2280 apply (metis insertCI runing_unique) |
|
2281 apply(auto) |
|
2282 done |
|
2283 |
|
2284 |
|
2285 |
2272 lemma create_pre: |
2286 lemma create_pre: |
2273 assumes stp: "step s e" |
2287 assumes stp: "step s e" |
2274 and not_in: "th \<notin> threads s" |
2288 and not_in: "th \<notin> threads s" |
2275 and is_in: "th \<in> threads (e#s)" |
2289 and is_in: "th \<in> threads (e#s)" |
2276 obtains prio where "e = Create th prio" |
2290 obtains prio where "e = Create th prio" |