equal
deleted
inserted
replaced
303 done |
303 done |
304 |
304 |
305 lemma wf_Union: |
305 lemma wf_Union: |
306 "[| ALL r:R. wf r; |
306 "[| ALL r:R. wf r; |
307 ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} |
307 ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} |
308 |] ==> wf(Union R)" |
308 |] ==> wf (\<Union> R)" |
309 using wf_UN[of R "\<lambda>i. i"] by simp |
309 using wf_UN[of R "\<lambda>i. i"] by simp |
310 |
310 |
311 (*Intuition: we find an (R u S)-min element of a nonempty subset A |
311 (*Intuition: we find an (R u S)-min element of a nonempty subset A |
312 by case distinction. |
312 by case distinction. |
313 1. There is a step a -R-> b with a,b : A. |
313 1. There is a step a -R-> b with a,b : A. |