renaming example invocations: tester predicate_compile is renamed to smart_exhaustive
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Nov 11 08:32:48 2011 +0100
@@ -26,7 +26,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
+quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Nov 11 08:32:48 2011 +0100
@@ -29,7 +29,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
+quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Nov 11 08:32:48 2011 +0100
@@ -29,7 +29,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
- quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=100, quiet = false, expect = counterexample]
+ quickcheck[tester = smart_exhaustive, size=2, iterations=100, quiet = false, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Fri Nov 11 08:32:48 2011 +0100
@@ -30,7 +30,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
nitpick (* nitpick fails here! *)
- quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=100, expect=counterexample]
+ quickcheck[tester = smart_exhaustive, size=2, iterations=100, expect=counterexample]
oops
end
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Nov 11 08:32:48 2011 +0100
@@ -20,7 +20,7 @@
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
quickcheck[tester = random, iterations = 10000]
-quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
quickcheck[tester = prolog, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Nov 11 08:32:48 2011 +0100
@@ -93,8 +93,7 @@
(*nitpick
quickcheck[tester = random, iterations = 10000]
quickcheck[tester = predicate_compile_wo_ff]
-quickcheck[tester = predicate_compile_ff_fs]
-oops*)
+quickcheck[tester = predicate_compile_ff_fs]*)
oops
@@ -117,7 +116,8 @@
prolog-style generation. *}
lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[tester = random, iterations = 100000]
+quickcheck[exhaustive]
+quickcheck[tester = random, iterations = 1000]
(*quickcheck[tester = predicate_compile_wo_ff]*)
(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
@@ -170,13 +170,13 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = smart_exhaustive, depth = 30]
quickcheck[tester = prolog]
oops
lemma "prop_regex a_sol"
quickcheck[tester = random]
-quickcheck[tester = predicate_compile_ff_fs]
+quickcheck[tester = smart_exhaustive]
oops
value [code] "prop_regex a_sol"