--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Mon Jul 02 10:50:17 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Mon Jul 02 11:39:24 2012 +0200
@@ -64,4 +64,14 @@
= finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"
by simp
+lemma
+ assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
+proof -
+ have eq: "{(a,b,c,d). ([a, b], [c, d]) : S} = ((%(a, b, c, d). ([a, b], [c, d])) -` S)"
+ unfolding vimage_def by (auto split: prod.split) (* to be proved with the simproc *)
+ from `finite S` show ?thesis
+ unfolding eq by (auto intro!: finite_vimageI simp add: inj_on_def)
+ (* to be automated with further rules and automation *)
+qed
+
end