21 "x = y" |
21 "x = y" |
22 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
22 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
23 oops |
23 oops |
24 *) |
24 *) |
25 |
25 |
|
26 (*declare [[quickcheck_narrowing_overlord]]*) |
|
27 subsection {* Simple examples with existentials *} |
|
28 |
|
29 lemma |
|
30 "\<exists> y :: nat. \<forall> x. x = y" |
|
31 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
|
32 oops |
|
33 |
|
34 lemma |
|
35 "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)" |
|
36 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
|
37 oops |
|
38 |
|
39 lemma |
|
40 "x > 2 --> (\<exists>y :: nat. x < y & y <= 2)" |
|
41 quickcheck[tester = narrowing, finite_types = false, size = 10] |
|
42 oops |
|
43 |
|
44 lemma |
|
45 "\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)" |
|
46 quickcheck[tester = narrowing, finite_types = false, size = 7] |
|
47 oops |
|
48 |
|
49 text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *} |
|
50 lemma |
|
51 "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]" |
|
52 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
|
53 oops |
|
54 |
|
55 text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *} |
|
56 lemma |
|
57 "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys" |
|
58 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
|
59 oops |
|
60 |
|
61 text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *} |
|
62 lemma |
|
63 "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)" |
|
64 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
|
65 oops |
|
66 |
26 subsection {* Simple list examples *} |
67 subsection {* Simple list examples *} |
27 |
68 |
28 lemma "rev xs = xs" |
69 lemma "rev xs = xs" |
29 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
70 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
30 oops |
71 oops |
31 |
72 |
|
73 (* FIXME: integer has strange representation! *) |
32 lemma "rev xs = xs" |
74 lemma "rev xs = xs" |
33 quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample] |
75 quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample] |
34 oops |
76 oops |
35 (* |
77 (* |
36 lemma "rev xs = xs" |
78 lemma "rev xs = xs" |
37 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
79 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
38 oops |
80 oops |
39 *) |
81 *) |
40 subsection {* Simple examples with functions *} |
82 subsection {* Simple examples with functions *} |
41 |
83 |
42 declare [[quickcheck_finite_functions]] |
|
43 (* |
|
44 lemma "map f xs = map g xs" |
84 lemma "map f xs = map g xs" |
45 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
85 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
46 oops |
86 oops |
47 |
87 |
48 lemma "map f xs = map f ys ==> xs = ys" |
88 lemma "map f xs = map f ys ==> xs = ys" |
49 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
89 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
50 oops |
90 oops |
51 |
91 |
52 lemma |
92 lemma |
53 "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)" |
93 "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)" |
54 quickcheck[tester = narrowing, expect = counterexample] |
94 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
55 oops |
95 oops |
56 |
96 |
57 lemma "map f xs = F f xs" |
97 lemma "map f xs = F f xs" |
58 quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
98 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
59 oops |
99 oops |
60 *) |
100 |
61 lemma "map f xs = F f xs" |
101 lemma "map f xs = F f xs" |
62 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
102 quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
63 oops |
103 oops |
64 |
104 |
65 (* requires some work... |
105 (* requires some work...*) |
|
106 (* |
66 lemma "R O S = S O R" |
107 lemma "R O S = S O R" |
67 quickcheck[tester = narrowing, size = 2] |
108 quickcheck[tester = narrowing, size = 2] |
68 oops |
109 oops |
69 *) |
110 *) |
70 |
111 |