src/HOL/Wellfounded.thy
 changeset 56166 9a241bc276cd parent 55932 68c5104d2204 child 56218 1c3f1f2431f9
equal inserted replaced
56165:dd89ce51d2c8 56166:9a241bc276cd
`   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 add: SUP_def)`
`   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.`
`   314      Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.`
`   314      Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.`