equal
deleted
inserted
replaced
181 lemma lam_FiniteFun: "A: Fin(X) ==> (\<lambda>x\<in>A. b(x)) \<in> A -||> {b(x). x:A}" |
181 lemma lam_FiniteFun: "A: Fin(X) ==> (\<lambda>x\<in>A. b(x)) \<in> A -||> {b(x). x:A}" |
182 by (blast intro: fun_FiniteFunI lam_funtype) |
182 by (blast intro: fun_FiniteFunI lam_funtype) |
183 |
183 |
184 lemma FiniteFun_Collect_iff: |
184 lemma FiniteFun_Collect_iff: |
185 "f \<in> FiniteFun(A, {y:B. P(y)}) |
185 "f \<in> FiniteFun(A, {y:B. P(y)}) |
186 <-> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))" |
186 \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))" |
187 apply auto |
187 apply auto |
188 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD]) |
188 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD]) |
189 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun) |
189 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun) |
190 apply (rule_tac A1="domain(f)" in |
190 apply (rule_tac A1="domain(f)" in |
191 subset_refl [THEN [2] FiniteFun_mono, THEN subsetD]) |
191 subset_refl [THEN [2] FiniteFun_mono, THEN subsetD]) |