src/HOL/Library/FSet.thy
changeset 56520 3373f5d1e074
parent 56519 c1048f5bbb45
child 56524 f4ba736040fa
equal deleted inserted replaced
56519:c1048f5bbb45 56520:3373f5d1e074
   808 
   808 
   809 lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
   809 lemma rel_fset_OO[relator_distr]: "rel_fset R OO rel_fset S = rel_fset (R OO S)"
   810 apply (rule ext)+
   810 apply (rule ext)+
   811 by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
   811 by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1])
   812 
   812 
   813 lemma Domainp_fset[relator_domain]:
   813 lemma Domainp_fset[relator_domain]: "Domainp (rel_fset T) = (\<lambda>A. fBall A (Domainp T))"
   814   assumes "Domainp T = P"
       
   815   shows "Domainp (rel_fset T) = (\<lambda>A. fBall A P)"
       
   816 proof -
   814 proof -
   817   from assms obtain f where f: "\<forall>x\<in>Collect P. T x (f x)"
   815   obtain f where f: "\<forall>x\<in>Collect (Domainp T). T x (f x)"
   818     unfolding Domainp_iff[abs_def]
   816     unfolding Domainp_iff[abs_def]
   819     apply atomize_elim
   817     apply atomize_elim
   820     by (subst bchoice_iff[symmetric]) auto
   818     by (subst bchoice_iff[symmetric]) (auto iff: bchoice_iff[symmetric])
   821   from assms f show ?thesis
   819   from f show ?thesis
   822     unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
   820     unfolding fun_eq_iff rel_fset_alt_def Domainp_iff
   823     apply clarify
   821     apply clarify
   824     apply (rule iffI)
   822     apply (rule iffI)
   825       apply blast
   823       apply blast
   826     by (rename_tac A, rule_tac x="f |`| A" in exI, blast)
   824     by (rename_tac A, rule_tac x="f |`| A" in exI, blast)