1.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Sun Oct 14 19:16:32 2012 +0200
     1.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Sun Oct 14 19:16:33 2012 +0200
     1.3 @@ -10,44 +10,39 @@
     1.4  begin
     1.5  
     1.6  lemma
     1.7 -  "finite {p. EX x. p = (x, x)}"
     1.8 -  apply simp
     1.9 -  oops
    1.10 +  "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
    1.11 +  by simp
    1.12  
    1.13  lemma
    1.14 -  "finite {f a b| a b. a : A \<and> b : B}"
    1.15 -  apply simp
    1.16 -  oops
    1.17 +  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"
    1.18 +  by simp
    1.19 +  
    1.20 +lemma
    1.21 +  "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
    1.22 +  by simp
    1.23  
    1.24  lemma
    1.25 -  "finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
    1.26 -  apply simp
    1.27 -  oops
    1.28 +  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
    1.29 +  by simp
    1.30  
    1.31  lemma
    1.32 -  "finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
    1.33 -  apply simp
    1.34 -  oops
    1.35 +  "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
    1.36 +  by simp
    1.37  
    1.38  lemma
    1.39 -  "finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
    1.40 -  apply simp
    1.41 -  oops
    1.42 +  "finite A ==> finite B ==> finite C ==> finite D ==>
    1.43 +     finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
    1.44 +  by simp
    1.45  
    1.46  lemma
    1.47 -  "finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
    1.48 -  apply simp
    1.49 -  oops
    1.50 -
    1.51 -lemma
    1.52 -  "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}"
    1.53 -  apply simp
    1.54 -  oops
    1.55 +  "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>
    1.56 +    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}"
    1.57 +  by simp
    1.58  
    1.59  lemma (* check arbitrary ordering *)
    1.60 -  "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'}"
    1.61 -  apply simp
    1.62 -  oops
    1.63 +  "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
    1.64 +    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'}"
    1.65 +  by simp
    1.66  
    1.67  lemma
    1.68    "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
    1.69 @@ -63,9 +58,35 @@
    1.70    "finite S ==> finite {s'. EX s:S. s' = f a e s}"
    1.71    by simp
    1.72  
    1.73 +lemma
    1.74 +  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"
    1.75 +  by simp
    1.76 +
    1.77 +lemma
    1.78 +  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"
    1.79 +by simp
    1.80 +
    1.81 +lemma
    1.82 +  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"
    1.83 +by simp
    1.84 +
    1.85 +lemma
    1.86 +  "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"
    1.87 +by simp
    1.88 +
    1.89 +lemma
    1.90 +  "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"
    1.91 +by simp
    1.92 +
    1.93 +lemma
    1.94 +  "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>
    1.95 +     finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"
    1.96 +apply simp
    1.97 +oops
    1.98 +
    1.99  schematic_lemma (* check interaction with schematics *)
   1.100    "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
   1.101 -   = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   1.102 +   = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   1.103    by simp
   1.104  
   1.105  lemma