1.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Oct 14 19:16:35 2012 +0200
1.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Oct 14 19:16:39 2012 +0200
1.3 @@ -84,6 +84,13 @@
1.4 apply simp
1.5 oops
1.6
1.7 +lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
1.8 +by simp
1.9 +
1.10 +lemma
1.11 + "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
1.12 +by simp
1.13 +
1.14 schematic_lemma (* check interaction with schematics *)
1.15 "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
1.16 = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"