src/HOL/Wellfounded.thy
changeset 56166 9a241bc276cd
parent 55932 68c5104d2204
child 56218 1c3f1f2431f9
equal deleted 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}.