summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/FSet.thy

changeset 56520 | 3373f5d1e074 |

parent 56519 | c1048f5bbb45 |

child 56524 | f4ba736040fa |

--- a/src/HOL/Library/FSet.thy Thu Apr 10 17:48:15 2014 +0200 +++ b/src/HOL/Library/FSet.thy Thu Apr 10 17:48:15 2014 +0200 @@ -810,15 +810,13 @@ apply (rule ext)+ by transfer (auto intro: finite_rel_set rel_set_OO[unfolded fun_eq_iff, rule_format, THEN iffD1]) -lemma Domainp_fset[relator_domain]: - assumes "Domainp T = P" - shows "Domainp (rel_fset T) = (\<lambda>A. fBall A P)" +lemma Domainp_fset[relator_domain]: "Domainp (rel_fset T) = (\<lambda>A. fBall A (Domainp T))" proof - - from assms obtain f where f: "\<forall>x\<in>Collect P. T x (f x)" + obtain f where f: "\<forall>x\<in>Collect (Domainp T). T x (f x)" unfolding Domainp_iff[abs_def] apply atomize_elim - by (subst bchoice_iff[symmetric]) auto - from assms f show ?thesis + by (subst bchoice_iff[symmetric]) (auto iff: bchoice_iff[symmetric]) + from f show ?thesis unfolding fun_eq_iff rel_fset_alt_def Domainp_iff apply clarify apply (rule iffI)