3 Main |
3 Main |
4 "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
4 "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
5 "~~/src/HOL/Library/Code_Prolog" |
5 "~~/src/HOL/Library/Code_Prolog" |
6 begin |
6 begin |
7 |
7 |
8 setup {* |
8 setup \<open> |
9 Context.theory_map |
9 Context.theory_map |
10 (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) |
10 (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) |
11 *} |
11 \<close> |
12 |
12 |
13 setup {* Code_Prolog.map_code_options (K |
13 setup \<open>Code_Prolog.map_code_options (K |
14 {ensure_groundness = true, |
14 {ensure_groundness = true, |
15 limit_globally = NONE, |
15 limit_globally = NONE, |
16 limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)], |
16 limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)], |
17 limited_predicates = [(["appendP"], 4), (["revP"], 4)], |
17 limited_predicates = [(["appendP"], 4), (["revP"], 4)], |
18 replacing = |
18 replacing = |
19 [(("appendP", "limited_appendP"), "quickcheck"), |
19 [(("appendP", "limited_appendP"), "quickcheck"), |
20 (("revP", "limited_revP"), "quickcheck"), |
20 (("revP", "limited_revP"), "quickcheck"), |
21 (("appendP", "limited_appendP"), "lim_revP")], |
21 (("appendP", "limited_appendP"), "lim_revP")], |
22 manual_reorder = []}) *} |
22 manual_reorder = []})\<close> |
23 |
23 |
24 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs" |
24 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs" |
25 quickcheck[tester = random, iterations = 10000] |
25 quickcheck[tester = random, iterations = 10000] |
26 quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample] |
26 quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample] |
27 quickcheck[tester = prolog, expect = counterexample] |
27 quickcheck[tester = prolog, expect = counterexample] |