# HG changeset patch # User bulwahn # Date 1350234993 -7200 # Node ID 4d33963962fa86de2fc048b3002e5620d069f6f5 # Parent 873fa7156468c37a41adf0e3ecd9f1e0a1adf1c9 adding further test cases to check new functionality of the simproc; strengthened test cases to check the success of the simproc more faithfully diff -r 873fa7156468 -r 4d33963962fa src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Oct 14 19:16:32 2012 +0200 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Oct 14 19:16:33 2012 +0200 @@ -10,44 +10,39 @@ begin lemma - "finite {p. EX x. p = (x, x)}" - apply simp - oops + "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}" + by simp lemma - "finite {f a b| a b. a : A \ b : B}" - apply simp - oops + "finite A ==> finite B ==> finite {f a b| a b. a : A \ b : B}" + by simp + +lemma + "finite B ==> finite A' ==> finite {f a b| a b. a : A \ a : A' \ b : B}" + by simp lemma - "finite {f a b| a b. a : A \ a : A' \ b : B}" - apply simp - oops + "finite A ==> finite B ==> finite {f a b| a b. a : A \ b : B \ b : B'}" + by simp lemma - "finite {f a b| a b. a : A \ b : B \ b : B'}" - apply simp - oops + "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \ b : B \ c : C}" + by simp lemma - "finite {f a b c| a b c. a : A \ b : B \ c : C}" - apply simp - oops + "finite A ==> finite B ==> finite C ==> finite D ==> + finite {f a b c d| a b c d. a : A \ b : B \ c : C \ d : D}" + by simp lemma - "finite {f a b c d| a b c d. a : A \ b : B \ c : C \ d : D}" - apply simp - oops - -lemma - "finite {f a b c d e | a b c d e. a : A \ b : B \ c : C \ d : D \ e : E}" - apply simp - oops + "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==> + finite {f a b c d e | a b c d e. a : A \ b : B \ c : C \ d : D \ e : E}" + by simp lemma (* check arbitrary ordering *) - "finite {f a d c b e | e b c d a. b : B \ a : A \ e : E' \ c : C \ d : D \ e : E \ b : B'}" - apply simp - oops + "finite A ==> finite B ==> finite C ==> finite D ==> finite E \ + finite {f a d c b e | e b c d a. b : B \ a : A \ e : E' \ c : C \ d : D \ e : E \ b : B'}" + by simp lemma "\ finite A ; finite B ; finite C ; finite D \ @@ -63,9 +58,35 @@ "finite S ==> finite {s'. EX s:S. s' = f a e s}" by simp +lemma + "finite A ==> finite B ==> finite {f a b| a b. a : A \ b : B \ a \ Z}" + by simp + +lemma + "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \ b : B \ (x,y) \ R}" +by simp + +lemma + "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \ (x,y) \ R \ b : B}" +by simp + +lemma + "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \ (x,y) \ R \ b : B}" +by simp + +lemma + "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \ a : AA) \ b : B \ a \ Z}" +by simp + +lemma + "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==> + finite {f a b c | a b c. ((a : A1 \ a : A2) \ (a : A3 \ (a : A4 \ a : A5))) \ b : B \ a \ Z}" +apply simp +oops + schematic_lemma (* check interaction with schematics *) "finite {x :: ?'A \ ?'B \ bool. \a b. x = Pair_Rep a b} - = finite ((\(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \ UNIV))" + = finite ((\(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \ UNIV))" by simp lemma