renaming example invocations: tester predicate_compile is renamed to smart_exhaustive
authorbulwahn
Fri Nov 11 08:32:48 2011 +0100 (2011-11-11)
changeset 4545174515e8e6046
parent 45450 dc2236b19a3d
child 45452 414732ebf891
child 45462 aba629d6cee5
renaming example invocations: tester predicate_compile is renamed to smart_exhaustive
src/HOL/Predicate_Compile_Examples/IMP_1.thy
src/HOL/Predicate_Compile_Examples/IMP_2.thy
src/HOL/Predicate_Compile_Examples/IMP_3.thy
src/HOL/Predicate_Compile_Examples/IMP_4.thy
src/HOL/Predicate_Compile_Examples/List_Examples.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Nov 11 08:32:45 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Nov 11 08:32:48 2011 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  lemma
     1.6    "exec c s s' ==> exec (Seq c c) s s'"
     1.7 -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
     1.8 +quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
     1.9  oops
    1.10  
    1.11  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Nov 11 08:32:45 2011 +0100
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Nov 11 08:32:48 2011 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  lemma
     2.6    "exec c s s' ==> exec (Seq c c) s s'"
     2.7 -quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
     2.8 +quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
     2.9  oops
    2.10  
    2.11  
     3.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Nov 11 08:32:45 2011 +0100
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Nov 11 08:32:48 2011 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  lemma
     3.6    "exec c s s' ==> exec (Seq c c) s s'"
     3.7 -  quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=100, quiet = false, expect = counterexample]
     3.8 +  quickcheck[tester = smart_exhaustive, size=2, iterations=100, quiet = false, expect = counterexample]
     3.9  oops
    3.10  
    3.11  
     4.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Nov 11 08:32:45 2011 +0100
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Nov 11 08:32:48 2011 +0100
     4.3 @@ -30,7 +30,7 @@
     4.4  lemma
     4.5    "exec c s s' ==> exec (Seq c c) s s'"
     4.6    nitpick (* nitpick fails here! *)
     4.7 -  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=100, expect=counterexample]
     4.8 +  quickcheck[tester = smart_exhaustive, size=2, iterations=100, expect=counterexample]
     4.9  oops
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Nov 11 08:32:45 2011 +0100
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Nov 11 08:32:48 2011 +0100
     5.3 @@ -20,7 +20,7 @@
     5.4  
     5.5  lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
     5.6  quickcheck[tester = random, iterations = 10000]
     5.7 -quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
     5.8 +quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
     5.9  quickcheck[tester = prolog, expect = counterexample]
    5.10  oops
    5.11  
     6.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Nov 11 08:32:45 2011 +0100
     6.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Nov 11 08:32:48 2011 +0100
     6.3 @@ -93,8 +93,7 @@
     6.4  (*nitpick
     6.5  quickcheck[tester = random, iterations = 10000]
     6.6  quickcheck[tester = predicate_compile_wo_ff]
     6.7 -quickcheck[tester = predicate_compile_ff_fs]
     6.8 -oops*)
     6.9 +quickcheck[tester = predicate_compile_ff_fs]*)
    6.10  oops
    6.11  
    6.12  
    6.13 @@ -117,7 +116,8 @@
    6.14   prolog-style generation. *}
    6.15  
    6.16  lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
    6.17 -quickcheck[tester = random, iterations = 100000]
    6.18 +quickcheck[exhaustive]
    6.19 +quickcheck[tester = random, iterations = 1000]
    6.20  (*quickcheck[tester = predicate_compile_wo_ff]*)
    6.21  (*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
    6.22  (*quickcheck[tester = prolog, iterations = 1, size = 1]*)
    6.23 @@ -170,13 +170,13 @@
    6.24    assumes "q = Seq (Sym N0) (Sym N0)"
    6.25    assumes "s = [N0, N0]"
    6.26  shows "prop_regex (n, (k, (p, (q, s))))"
    6.27 -quickcheck[tester = predicate_compile_wo_ff]
    6.28 +quickcheck[tester = smart_exhaustive, depth = 30]
    6.29  quickcheck[tester = prolog]
    6.30  oops
    6.31  
    6.32  lemma "prop_regex a_sol"
    6.33  quickcheck[tester = random]
    6.34 -quickcheck[tester = predicate_compile_ff_fs]
    6.35 +quickcheck[tester = smart_exhaustive]
    6.36  oops
    6.37  
    6.38  value [code] "prop_regex a_sol"