16 and h2: "distinct (wq s cs)" |
16 and h2: "distinct (wq s cs)" |
17 thus "distinct (wq (e # s) cs)" |
17 thus "distinct (wq (e # s) cs)" |
18 proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) |
18 proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) |
19 fix thread s |
19 fix thread s |
20 assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+" |
20 assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+" |
21 and h2: "thread \<in> set (waiting_queue (schs s) cs)" |
21 and h2: "thread \<in> set (wq_fun (schs s) cs)" |
22 and h3: "thread \<in> runing s" |
22 and h3: "thread \<in> runing s" |
23 show "False" |
23 show "False" |
24 proof - |
24 proof - |
25 from h3 have "\<And> cs. thread \<in> set (waiting_queue (schs s) cs) \<Longrightarrow> |
25 from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow> |
26 thread = hd ((waiting_queue (schs s) cs))" |
26 thread = hd ((wq_fun (schs s) cs))" |
27 by (simp add:runing_def readys_def s_waiting_def wq_def) |
27 by (simp add:runing_def readys_def s_waiting_def wq_def) |
28 from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" . |
28 from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" . |
29 with h2 |
29 with h2 |
30 have "(Cs cs, Th thread) \<in> (depend s)" |
30 have "(Cs cs, Th thread) \<in> (depend s)" |
31 by (simp add:s_depend_def s_holding_def wq_def cs_holding_def) |
31 by (simp add:s_depend_def s_holding_def wq_def cs_holding_def) |
32 with h1 show False by auto |
32 with h1 show False by auto |
33 qed |
33 qed |
79 case (V th cs) |
79 case (V th cs) |
80 with assms show ?thesis |
80 with assms show ?thesis |
81 apply (auto simp:wq_def Let_def split:if_splits) |
81 apply (auto simp:wq_def Let_def split:if_splits) |
82 proof - |
82 proof - |
83 fix q qs |
83 fix q qs |
84 assume h1: "thread \<notin> set (waiting_queue (schs s) cs)" |
84 assume h1: "thread \<notin> set (wq_fun (schs s) cs)" |
85 and h2: "q # qs = waiting_queue (schs s) cs" |
85 and h2: "q # qs = wq_fun (schs s) cs" |
86 and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" |
86 and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" |
87 and vt: "vt step (V th cs # s)" |
87 and vt: "vt step (V th cs # s)" |
88 from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp |
88 from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp |
89 moreover have "thread \<in> set qs" |
89 moreover have "thread \<in> set qs" |
90 proof - |
90 proof - |
141 apply (auto simp:wq_def simp:Let_def split:if_splits list.splits) |
141 apply (auto simp:wq_def simp:Let_def split:if_splits list.splits) |
142 proof - |
142 proof - |
143 fix th qs |
143 fix th qs |
144 assume vt: "vt step (V th cs # s)" |
144 assume vt: "vt step (V th cs # s)" |
145 and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" |
145 and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" |
146 and eq_wq: "waiting_queue (schs s) cs = thread # qs" |
146 and eq_wq: "wq_fun (schs s) cs = thread # qs" |
147 show "False" |
147 show "False" |
148 proof - |
148 proof - |
149 from wq_distinct[OF step_back_vt[OF vt], of cs] |
149 from wq_distinct[OF step_back_vt[OF vt], of cs] |
150 and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp |
150 and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp |
151 moreover have "thread \<in> set qs" |
151 moreover have "thread \<in> set qs" |
191 ultimately show ?thesis by auto |
191 ultimately show ?thesis by auto |
192 qed |
192 qed |
193 qed |
193 qed |
194 |
194 |
195 (* Wrong: |
195 (* Wrong: |
196 lemma \<lbrakk>thread \<in> set (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2" |
196 lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2" |
197 *) |
197 *) |
198 |
198 |
199 lemma waiting_unique_pre: |
199 lemma waiting_unique_pre: |
200 fixes cs1 cs2 s thread |
200 fixes cs1 cs2 s thread |
201 assumes vt: "vt step s" |
201 assumes vt: "vt step s" |
581 apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits) |
581 apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits) |
582 proof - |
582 proof - |
583 fix a list |
583 fix a list |
584 assume t_in: "t \<in> set list" |
584 assume t_in: "t \<in> set list" |
585 and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)" |
585 and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)" |
586 and eq_wq: "waiting_queue (schs s) cs = a # list" |
586 and eq_wq: "wq_fun (schs s) cs = a # list" |
587 have " set (SOME q. distinct q \<and> set q = set list) = set list" |
587 have " set (SOME q. distinct q \<and> set q = set list) = set list" |
588 proof(rule someI2) |
588 proof(rule someI2) |
589 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] |
589 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] |
590 show "distinct list \<and> set list = set list" by auto |
590 show "distinct list \<and> set list = set list" by auto |
591 next |
591 next |
595 with t_ni and t_in show "a = th" by auto |
595 with t_ni and t_in show "a = th" by auto |
596 next |
596 next |
597 fix a list |
597 fix a list |
598 assume t_in: "t \<in> set list" |
598 assume t_in: "t \<in> set list" |
599 and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)" |
599 and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)" |
600 and eq_wq: "waiting_queue (schs s) cs = a # list" |
600 and eq_wq: "wq_fun (schs s) cs = a # list" |
601 have " set (SOME q. distinct q \<and> set q = set list) = set list" |
601 have " set (SOME q. distinct q \<and> set q = set list) = set list" |
602 proof(rule someI2) |
602 proof(rule someI2) |
603 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] |
603 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def] |
604 show "distinct list \<and> set list = set list" by auto |
604 show "distinct list \<and> set list = set list" by auto |
605 next |
605 next |
607 by auto |
607 by auto |
608 qed |
608 qed |
609 with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto |
609 with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto |
610 next |
610 next |
611 fix a list |
611 fix a list |
612 assume eq_wq: "waiting_queue (schs s) cs = a # list" |
612 assume eq_wq: "wq_fun (schs s) cs = a # list" |
613 from step_back_step[OF vt] |
613 from step_back_step[OF vt] |
614 show "a = th" |
614 show "a = th" |
615 proof(cases) |
615 proof(cases) |
616 assume "holding s th cs" |
616 assume "holding s th cs" |
617 with eq_wq show ?thesis |
617 with eq_wq show ?thesis |
639 apply (unfold s_holding_def wq_def cs_holding_def) |
639 apply (unfold s_holding_def wq_def cs_holding_def) |
640 apply (auto simp:Let_def split:list.splits) |
640 apply (auto simp:Let_def split:list.splits) |
641 proof - |
641 proof - |
642 fix list |
642 fix list |
643 assume eq_wq[folded wq_def]: |
643 assume eq_wq[folded wq_def]: |
644 "waiting_queue (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list" |
644 "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list" |
645 and hd_in: "hd (SOME q. distinct q \<and> set q = set list) |
645 and hd_in: "hd (SOME q. distinct q \<and> set q = set list) |
646 \<in> set (SOME q. distinct q \<and> set q = set list)" |
646 \<in> set (SOME q. distinct q \<and> set q = set list)" |
647 have "set (SOME q. distinct q \<and> set q = set list) = set list" |
647 have "set (SOME q. distinct q \<and> set q = set list) = set list" |
648 proof(rule someI2) |
648 proof(rule someI2) |
649 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq |
649 from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq |
668 apply (unfold cs_holding_def next_th_def wq_def, |
668 apply (unfold cs_holding_def next_th_def wq_def, |
669 auto simp:Let_def) |
669 auto simp:Let_def) |
670 proof - |
670 proof - |
671 fix rest |
671 fix rest |
672 assume vt: "vt step (V th cs # s)" |
672 assume vt: "vt step (V th cs # s)" |
673 and eq_wq[folded wq_def]: " waiting_queue (schs s) cs = th # rest" |
673 and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest" |
674 and nrest: "rest \<noteq> []" |
674 and nrest: "rest \<noteq> []" |
675 and ni: "hd (SOME q. distinct q \<and> set q = set rest) |
675 and ni: "hd (SOME q. distinct q \<and> set q = set rest) |
676 \<notin> set (SOME q. distinct q \<and> set q = set rest)" |
676 \<notin> set (SOME q. distinct q \<and> set q = set rest)" |
677 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
677 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []" |
678 proof(rule someI2) |
678 proof(rule someI2) |
691 "\<And>c t. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> |
691 "\<And>c t. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> |
692 c = cs \<and> t = th" |
692 c = cs \<and> t = th" |
693 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) |
693 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) |
694 proof - |
694 proof - |
695 fix a list |
695 fix a list |
696 assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list" |
696 assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" |
697 from step_back_step [OF vt] show "a = th" |
697 from step_back_step [OF vt] show "a = th" |
698 proof(cases) |
698 proof(cases) |
699 assume "holding s th cs" with eq_wq |
699 assume "holding s th cs" with eq_wq |
700 show ?thesis |
700 show ?thesis |
701 by (unfold s_holding_def wq_def, auto) |
701 by (unfold s_holding_def wq_def, auto) |
702 qed |
702 qed |
703 next |
703 next |
704 fix a list |
704 fix a list |
705 assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list" |
705 assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" |
706 from step_back_step [OF vt] show "a = th" |
706 from step_back_step [OF vt] show "a = th" |
707 proof(cases) |
707 proof(cases) |
708 assume "holding s th cs" with eq_wq |
708 assume "holding s th cs" with eq_wq |
709 show ?thesis |
709 show ?thesis |
710 by (unfold s_holding_def wq_def, auto) |
710 by (unfold s_holding_def wq_def, auto) |
731 apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) |
731 apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) |
732 proof - |
732 proof - |
733 fix a list |
733 fix a list |
734 assume not_in: "t \<notin> set list" |
734 assume not_in: "t \<notin> set list" |
735 and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)" |
735 and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)" |
736 and eq_wq: "waiting_queue (schs s) cs = a # list" |
736 and eq_wq: "wq_fun (schs s) cs = a # list" |
737 have "set (SOME q. distinct q \<and> set q = set list) = set list" |
737 have "set (SOME q. distinct q \<and> set q = set list) = set list" |
738 proof(rule someI2) |
738 proof(rule someI2) |
739 from wq_distinct [OF step_back_vt[OF vt], of cs] |
739 from wq_distinct [OF step_back_vt[OF vt], of cs] |
740 and eq_wq[folded wq_def] |
740 and eq_wq[folded wq_def] |
741 show "distinct list \<and> set list = set list" by auto |
741 show "distinct list \<and> set list = set list" by auto |
745 qed |
745 qed |
746 with not_in is_in show "t = a" by auto |
746 with not_in is_in show "t = a" by auto |
747 next |
747 next |
748 fix list |
748 fix list |
749 assume is_waiting: "waiting (wq (V th cs # s)) t cs" |
749 assume is_waiting: "waiting (wq (V th cs # s)) t cs" |
750 and eq_wq: "waiting_queue (schs s) cs = t # list" |
750 and eq_wq: "wq_fun (schs s) cs = t # list" |
751 hence "t \<in> set list" |
751 hence "t \<in> set list" |
752 apply (unfold wq_def, auto simp:Let_def cs_waiting_def) |
752 apply (unfold wq_def, auto simp:Let_def cs_waiting_def) |
753 proof - |
753 proof - |
754 assume " t \<in> set (SOME q. distinct q \<and> set q = set list)" |
754 assume " t \<in> set (SOME q. distinct q \<and> set q = set list)" |
755 moreover have "\<dots> = set list" |
755 moreover have "\<dots> = set list" |
1123 next |
1123 next |
1124 case True |
1124 case True |
1125 from h |
1125 from h |
1126 show ?thesis |
1126 show ?thesis |
1127 proof(unfold V wq_def) |
1127 proof(unfold V wq_def) |
1128 assume th_in: "th \<in> set (waiting_queue (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l") |
1128 assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l") |
1129 show "th \<in> threads (V th' cs' # s)" |
1129 show "th \<in> threads (V th' cs' # s)" |
1130 proof(cases "cs = cs'") |
1130 proof(cases "cs = cs'") |
1131 case False |
1131 case False |
1132 hence "?l = waiting_queue (schs s) cs" by (simp add:Let_def) |
1132 hence "?l = wq_fun (schs s) cs" by (simp add:Let_def) |
1133 with th_in have " th \<in> set (wq s cs)" |
1133 with th_in have " th \<in> set (wq s cs)" |
1134 by (fold wq_def, simp) |
1134 by (fold wq_def, simp) |
1135 from ih [OF this] show ?thesis by simp |
1135 from ih [OF this] show ?thesis by simp |
1136 next |
1136 next |
1137 case True |
1137 case True |
1138 show ?thesis |
1138 show ?thesis |
1139 proof(cases "waiting_queue (schs s) cs'") |
1139 proof(cases "wq_fun (schs s) cs'") |
1140 case Nil |
1140 case Nil |
1141 with h V show ?thesis |
1141 with h V show ?thesis |
1142 apply (auto simp:wq_def Let_def split:if_splits) |
1142 apply (auto simp:wq_def Let_def split:if_splits) |
1143 by (fold wq_def, drule_tac ih, simp) |
1143 by (fold wq_def, drule_tac ih, simp) |
1144 next |
1144 next |
1145 case (Cons a rest) |
1145 case (Cons a rest) |
1146 assume eq_wq: "waiting_queue (schs s) cs' = a # rest" |
1146 assume eq_wq: "wq_fun (schs s) cs' = a # rest" |
1147 with h V show ?thesis |
1147 with h V show ?thesis |
1148 apply (auto simp:Let_def wq_def split:if_splits) |
1148 apply (auto simp:Let_def wq_def split:if_splits) |
1149 proof - |
1149 proof - |
1150 assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
1150 assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
1151 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
1151 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
1154 show "distinct rest \<and> set rest = set rest" by auto |
1154 show "distinct rest \<and> set rest = set rest" by auto |
1155 next |
1155 next |
1156 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" |
1156 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" |
1157 by auto |
1157 by auto |
1158 qed |
1158 qed |
1159 with eq_wq th_in have "th \<in> set (waiting_queue (schs s) cs')" by auto |
1159 with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto |
1160 from ih[OF this[folded wq_def]] show "th \<in> threads s" . |
1160 from ih[OF this[folded wq_def]] show "th \<in> threads s" . |
1161 next |
1161 next |
1162 assume th_in: "th \<in> set (waiting_queue (schs s) cs)" |
1162 assume th_in: "th \<in> set (wq_fun (schs s) cs)" |
1163 from ih[OF this[folded wq_def]] |
1163 from ih[OF this[folded wq_def]] |
1164 show "th \<in> threads s" . |
1164 show "th \<in> threads s" . |
1165 qed |
1165 qed |
1166 qed |
1166 qed |
1167 qed |
1167 qed |
1208 apply (erule_tac x = cs in allE) |
1208 apply (erule_tac x = cs in allE) |
1209 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
1209 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) |
1210 proof - |
1210 proof - |
1211 assume th_nin: "th \<notin> set rest" |
1211 assume th_nin: "th \<notin> set rest" |
1212 and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
1212 and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)" |
1213 and eq_wq: "waiting_queue (schs s) cs = thread # rest" |
1213 and eq_wq: "wq_fun (schs s) cs = thread # rest" |
1214 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
1214 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" |
1215 proof(rule someI2) |
1215 proof(rule someI2) |
1216 from wq_distinct[OF vt, of cs] and eq_wq[folded wq_def] |
1216 from wq_distinct[OF vt, of cs] and eq_wq[folded wq_def] |
1217 show "distinct rest \<and> set rest = set rest" by auto |
1217 show "distinct rest \<and> set rest = set rest" by auto |
1218 next |
1218 next |
1548 have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))" |
1548 have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))" |
1549 apply (simp add:readys_def s_waiting_def wq_def Let_def) |
1549 apply (simp add:readys_def s_waiting_def wq_def Let_def) |
1550 apply (rule_tac hh, clarify) |
1550 apply (rule_tac hh, clarify) |
1551 apply (intro iffI allI, clarify) |
1551 apply (intro iffI allI, clarify) |
1552 apply (erule_tac x = csa in allE, auto) |
1552 apply (erule_tac x = csa in allE, auto) |
1553 apply (subgoal_tac "waiting_queue (schs s) cs \<noteq> []", auto) |
1553 apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto) |
1554 apply (erule_tac x = cs in allE, auto) |
1554 apply (erule_tac x = cs in allE, auto) |
1555 by (case_tac "(waiting_queue (schs s) cs)", auto) |
1555 by (case_tac "(wq_fun (schs s) cs)", auto) |
1556 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
1556 moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" |
1557 apply (simp add:cntCS_def holdents_def) |
1557 apply (simp add:cntCS_def holdents_def) |
1558 by (unfold step_depend_p [OF vtp], auto) |
1558 by (unfold step_depend_p [OF vtp], auto) |
1559 moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" |
1559 moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" |
1560 by (simp add:cntP_def count_def) |
1560 by (simp add:cntP_def count_def) |
1805 from True eq_wq th_in neq_th |
1805 from True eq_wq th_in neq_th |
1806 have "th \<in> readys (e # s)" |
1806 have "th \<in> readys (e # s)" |
1807 apply (auto simp:eq_e readys_def s_waiting_def wq_def |
1807 apply (auto simp:eq_e readys_def s_waiting_def wq_def |
1808 Let_def next_th_def) |
1808 Let_def next_th_def) |
1809 proof - |
1809 proof - |
1810 assume eq_wq: "waiting_queue (schs s) cs = thread # rest" |
1810 assume eq_wq: "wq_fun (schs s) cs = thread # rest" |
1811 and t_in: "?t \<in> set rest" |
1811 and t_in: "?t \<in> set rest" |
1812 show "?t \<in> threads s" |
1812 show "?t \<in> threads s" |
1813 proof(rule wq_threads[OF step_back_vt[OF vtv]]) |
1813 proof(rule wq_threads[OF step_back_vt[OF vtv]]) |
1814 from eq_wq and t_in |
1814 from eq_wq and t_in |
1815 show "?t \<in> set (wq s cs)" by (auto simp:wq_def) |
1815 show "?t \<in> set (wq s cs)" by (auto simp:wq_def) |
1816 qed |
1816 qed |
1817 next |
1817 next |
1818 fix csa |
1818 fix csa |
1819 assume eq_wq: "waiting_queue (schs s) cs = thread # rest" |
1819 assume eq_wq: "wq_fun (schs s) cs = thread # rest" |
1820 and t_in: "?t \<in> set rest" |
1820 and t_in: "?t \<in> set rest" |
1821 and neq_cs: "csa \<noteq> cs" |
1821 and neq_cs: "csa \<noteq> cs" |
1822 and t_in': "?t \<in> set (waiting_queue (schs s) csa)" |
1822 and t_in': "?t \<in> set (wq_fun (schs s) csa)" |
1823 show "?t = hd (waiting_queue (schs s) csa)" |
1823 show "?t = hd (wq_fun (schs s) csa)" |
1824 proof - |
1824 proof - |
1825 { assume neq_hd': "?t \<noteq> hd (waiting_queue (schs s) csa)" |
1825 { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)" |
1826 from wq_distinct[OF step_back_vt[OF vtv], of cs] and |
1826 from wq_distinct[OF step_back_vt[OF vtv], of cs] and |
1827 eq_wq[folded wq_def] and t_in eq_wq |
1827 eq_wq[folded wq_def] and t_in eq_wq |
1828 have "?t \<noteq> thread" by auto |
1828 have "?t \<noteq> thread" by auto |
1829 with eq_wq and t_in |
1829 with eq_wq and t_in |
1830 have w1: "waiting s ?t cs" |
1830 have w1: "waiting s ?t cs" |