src/HOL/Wellfounded.thy
changeset 32263 8bc0fd4a23a0
parent 32244 a99723d77ae0
child 32461 eee4fa79398f
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Jul 28 08:49:03 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Jul 28 13:37:08 2009 +0200
     1.3 @@ -283,8 +283,10 @@
     1.4  apply (blast elim!: allE)  
     1.5  done
     1.6  
     1.7 -lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
     1.8 -  to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
     1.9 +lemma wfP_SUP:
    1.10 +  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
    1.11 +  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq])
    1.12 +    (simp_all add: bot_fun_eq bot_bool_eq)
    1.13  
    1.14  lemma wf_Union: 
    1.15   "[| ALL r:R. wf r;