author | blanchet |
Wed, 24 Sep 2014 15:45:55 +0200 | |
changeset 58425 | 246985c6b20b |
parent 52666 | 391913d17d15 |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
1 |
theory List_Examples |
41956 | 2 |
imports |
3 |
Main |
|
4 |
"~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
|
5 |
"~~/src/HOL/Library/Code_Prolog" |
|
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
6 |
begin |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
7 |
|
52666 | 8 |
setup {* |
9 |
Context.theory_map |
|
10 |
(Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) |
|
11 |
*} |
|
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
12 |
|
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
13 |
setup {* Code_Prolog.map_code_options (K |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
14 |
{ensure_groundness = true, |
39800 | 15 |
limit_globally = NONE, |
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
16 |
limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)], |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
17 |
limited_predicates = [(["appendP"], 4), (["revP"], 4)], |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
18 |
replacing = |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
19 |
[(("appendP", "limited_appendP"), "quickcheck"), |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
20 |
(("revP", "limited_revP"), "quickcheck"), |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
21 |
(("appendP", "limited_appendP"), "lim_revP")], |
39463 | 22 |
manual_reorder = []}) *} |
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
23 |
|
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
24 |
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs" |
40924 | 25 |
quickcheck[tester = random, iterations = 10000] |
45451
74515e8e6046
renaming example invocations: tester predicate_compile is renamed to smart_exhaustive
bulwahn
parents:
43937
diff
changeset
|
26 |
quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample] |
40924 | 27 |
quickcheck[tester = prolog, expect = counterexample] |
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
28 |
oops |
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
29 |
|
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
diff
changeset
|
30 |
end |