# HG changeset patch
# User bulwahn
# Date 1350476037 -7200
# Node ID 1f0b7d5bea4e4e536b5bae5b8a2d84fd1aa2b97e
# Parent  dd2ae15ac74fa05dd249fd6b93d55f13f0ce3bfe
set_comprehension_pointfree simproc now handles the complicated test case; tuned

diff -r dd2ae15ac74f -r 1f0b7d5bea4e src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 17 14:13:57 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 17 14:13:57 2012 +0200
@@ -39,7 +39,7 @@
     finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
   by simp
 
-lemma (* check arbitrary ordering *)
+lemma
   "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
     finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
   by simp
@@ -104,21 +104,16 @@
     ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
   by (auto intro: finite_vimageI)
 
+lemma
+  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
+using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
+  (* injectivity to be automated with further rules and automation *)
 
 schematic_lemma (* check interaction with schematics *)
   "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
    = finite ((\<lambda>(b :: ?'B, a:: ?'A). 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
 
 section {* Testing simproc in code generation *}
 
@@ -132,6 +127,4 @@
 
 export_code union common_subsets in Haskell file -
 
-
-
 end