equal
deleted
inserted
replaced
274 show "th1 = th2" by simp |
274 show "th1 = th2" by simp |
275 qed |
275 qed |
276 qed |
276 qed |
277 |
277 |
278 |
278 |
279 lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)" |
279 lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s" |
280 proof - |
280 proof - |
281 from fun_eq_iff |
281 from fun_eq_iff |
282 have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto |
282 have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto |
283 show ?thesis |
283 show ?thesis |
284 proof(rule h) |
284 proof(rule h) |
285 from cp_eq_cpreced show "\<forall>x. cp s x = cpreced s (wq s) x" by auto |
285 from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto |
286 qed |
286 qed |
287 qed |
287 qed |
288 |
288 |
289 lemma depend_children: |
289 lemma depend_children: |
290 assumes h: "(Th th1, Th th2) \<in> (depend s)^+" |
290 assumes h: "(Th th1, Th th2) \<in> (depend s)^+" |