equal
deleted
inserted
replaced
230 unfolding cpreced_def image_def |
230 unfolding cpreced_def image_def |
231 apply(rule eq_reflection) |
231 apply(rule eq_reflection) |
232 apply(rule_tac f="Max" in arg_cong) |
232 apply(rule_tac f="Max" in arg_cong) |
233 by (auto) |
233 by (auto) |
234 |
234 |
|
235 lemma cpreced_def3: |
|
236 "cpreced wq s th \<equiv> Max (preceds ({th} \<union> dependants_raw wq th) s)" |
|
237 unfolding cpreced_def2 image_def |
|
238 apply(rule eq_reflection) |
|
239 apply(rule_tac f="Max" in arg_cong) |
|
240 by (auto) |
|
241 |
235 definition |
242 definition |
236 cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set" |
243 cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set" |
237 where |
244 where |
238 "cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}" |
245 "cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}" |
239 |
246 |