--- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Nov 06 08:11:58 2009 +0100
@@ -9,7 +9,9 @@
quickcheck[generator=predicate_compile]
oops
+(* TODO: some error with doubled negation *)
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
+(*quickcheck[generator=predicate_compile]*)
oops
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
@@ -23,12 +25,17 @@
section {* Numerals *}
lemma
- "x \<in> {1, 2, (3::nat)} ==> x < 3"
+ "x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {1, 2, (3::nat)} ==> x < 3"
(*quickcheck[generator=predicate_compile]*)
oops
+
lemma
- "x \<in> {1, 2} \<union> {3, 4} ==> x > 4"
-(*quickcheck[generator=predicate_compile]*)
+ "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)"
+quickcheck[generator=predicate_compile]
oops
section {* Context Free Grammar *}