# HG changeset patch
# User bulwahn
# Date 1350388628 -7200
# Node ID 8cbd8340a21ef0b36cdc5b9476c035ff642b773e
# Parent  0adcb5cd4eba59c8bb5d5a9d790d186c99272e54
adding test cases for f x y : S patterns in set_comprehension_pointfree simproc

diff -r 0adcb5cd4eba -r 8cbd8340a21e src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Tue Oct 16 13:18:13 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Tue Oct 16 13:57:08 2012 +0200
@@ -91,6 +91,20 @@
   "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
 by simp
 
+lemma
+  "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
+  by (auto intro: finite_vimageI)
+
+lemma
+  "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
+  by (auto intro: finite_vimageI)
+
+lemma
+  "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
+    ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
+  by (auto intro: finite_vimageI)
+
+
 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))"
@@ -106,4 +120,18 @@
     (* to be automated with further rules and automation *)
 qed
 
+section {* Testing simproc in code generation *}
+
+definition union :: "nat set => nat set => nat set"
+where
+  "union A B = {x. x : A \<or> x : B}"
+
+definition common_subsets :: "nat set => nat set => nat set set"
+where
+  "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
+
+export_code union common_subsets in Haskell file -
+
+
+
 end