src/HOL/Wellfounded.thy
changeset 46177 adac34829e10
parent 45970 b6d0cff57d96
child 46333 46c2c96f5d92
equal deleted inserted replaced
46176:1898e61e89c4 46177:adac34829e10
   296 apply (blast elim!: allE)  
   296 apply (blast elim!: allE)  
   297 done
   297 done
   298 
   298 
   299 lemma wfP_SUP:
   299 lemma wfP_SUP:
   300   "\<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)"
   300   "\<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)"
   301   apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
   301   apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
   302   apply (simp_all add: inf_set_def)
   302   apply (simp_all add: inf_set_def)
   303   apply auto
   303   apply auto
   304   done
   304   done
   305 
   305 
   306 lemma wf_Union: 
   306 lemma wf_Union: 
   609 
   609 
   610 lemmas acc_wfD = accp_wfPD [to_set]
   610 lemmas acc_wfD = accp_wfPD [to_set]
   611 
   611 
   612 lemmas wf_acc_iff = wfP_accp_iff [to_set]
   612 lemmas wf_acc_iff = wfP_accp_iff [to_set]
   613 
   613 
   614 lemmas acc_subset = accp_subset [to_set pred_subset_eq]
   614 lemmas acc_subset = accp_subset [to_set]
   615 
   615 
   616 lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq]
   616 lemmas acc_subset_induct = accp_subset_induct [to_set]
   617 
   617 
   618 
   618 
   619 subsection {* Tools for building wellfounded relations *}
   619 subsection {* Tools for building wellfounded relations *}
   620 
   620 
   621 text {* Inverse Image *}
   621 text {* Inverse Image *}