equal
deleted
inserted
replaced
209 assumes "th \<in> runing s" |
209 assumes "th \<in> runing s" |
210 and "th \<in> set (wq s cs)" |
210 and "th \<in> set (wq s cs)" |
211 obtains rest where "wq s cs = th#rest" |
211 obtains rest where "wq s cs = th#rest" |
212 proof - |
212 proof - |
213 from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest" |
213 from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest" |
214 by (meson list.set_cases) |
214 by (metis empty_iff list.exhaust list.set(1)) |
215 have "th' = th" |
215 have "th' = th" |
216 proof(rule ccontr) |
216 proof(rule ccontr) |
217 assume "th' \<noteq> th" |
217 assume "th' \<noteq> th" |
218 hence "th \<noteq> hd (wq s cs)" using eq_wq by auto |
218 hence "th \<noteq> hd (wq s cs)" using eq_wq by auto |
219 with assms(2) |
219 with assms(2) |
1252 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto |
1252 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto |
1253 hence "t \<noteq> taker" by (simp add: taker_def) |
1253 hence "t \<noteq> taker" by (simp add: taker_def) |
1254 moreover hence "t \<noteq> th" using assms neq_t_th by blast |
1254 moreover hence "t \<noteq> th" using assms neq_t_th by blast |
1255 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) |
1255 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) |
1256 ultimately have "waiting s t cs" |
1256 ultimately have "waiting s t cs" |
1257 by (metis cs_waiting_def list.distinct(2) list.sel(1) |
1257 by (metis cs_waiting_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs) |
1258 list.set_sel(2) rest_def waiting_eq wq_s_cs) |
|
1259 show ?thesis using that(2) |
1258 show ?thesis using that(2) |
1260 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto |
1259 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto |
1261 qed |
1260 qed |
1262 |
1261 |
1263 lemma holding_esI1: |
1262 lemma holding_esI1: |
1592 |
1591 |
1593 lemma waiting_kept: |
1592 lemma waiting_kept: |
1594 assumes "waiting s th' cs'" |
1593 assumes "waiting s th' cs'" |
1595 shows "waiting (e#s) th' cs'" |
1594 shows "waiting (e#s) th' cs'" |
1596 using assms |
1595 using assms |
1597 by (metis cs_waiting_def hd_append2 list.sel(1) list.set_intros(2) |
1596 unfolding th_not_in_wq waiting_eq cs_waiting_def |
1598 rotate1.simps(2) self_append_conv2 set_rotate1 |
1597 by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD |
1599 th_not_in_wq waiting_eq wq_es_cs wq_neq_simp) |
1598 list.distinct(1) split_list wq_es_cs wq_neq_simp) |
1600 |
1599 |
1601 lemma holding_kept: |
1600 lemma holding_kept: |
1602 assumes "holding s th' cs'" |
1601 assumes "holding s th' cs'" |
1603 shows "holding (e#s) th' cs'" |
1602 shows "holding (e#s) th' cs'" |
1604 proof(cases "cs' = cs") |
1603 proof(cases "cs' = cs") |
1746 with assms show ?thesis |
1745 with assms show ?thesis |
1747 using cs_holding_def holding_eq that by auto |
1746 using cs_holding_def holding_eq that by auto |
1748 next |
1747 next |
1749 case True |
1748 case True |
1750 with assms show ?thesis |
1749 with assms show ?thesis |
1751 by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that |
1750 using event.inject(3) holder_def is_p s_holding_def s_waiting_def that |
1752 wq_es_cs' wq_s_cs) |
1751 waiting_es_th_cs wq_def wq_es_cs' wq_in_inv |
|
1752 by(force) |
1753 qed |
1753 qed |
1754 |
1754 |
1755 lemma waiting_esE: |
1755 lemma waiting_esE: |
1756 assumes "waiting (e#s) th' cs'" |
1756 assumes "waiting (e#s) th' cs'" |
1757 obtains "th' \<noteq> th" "waiting s th' cs'" |
1757 obtains "th' \<noteq> th" "waiting s th' cs'" |