equal
deleted
inserted
replaced
2069 hence "th \<in> set (wq s cs)" |
2069 hence "th \<in> set (wq s cs)" |
2070 by (unfold s_depend_def, auto simp:cs_waiting_def) |
2070 by (unfold s_depend_def, auto simp:cs_waiting_def) |
2071 from wq_threads [OF vt this] show ?thesis . |
2071 from wq_threads [OF vt this] show ?thesis . |
2072 qed |
2072 qed |
2073 |
2073 |
2074 lemma cp_eq_cpreced: "cp s th = cpreced s (wq s) th" |
2074 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" |
2075 proof(unfold cp_def wq_def, induct s) |
2075 proof(unfold cp_def wq_def, induct s) |
2076 case (Cons e s') |
2076 case (Cons e s') |
2077 show ?case |
2077 show ?case |
2078 by (auto simp:Let_def) |
2078 by (auto simp:Let_def) |
2079 next |
2079 next |