author | wenzelm |
Sat, 09 Jul 2011 21:53:27 +0200 | |
changeset 43721 | fad8634cee62 |
parent 43356 | 2dee03f192b7 |
child 45082 | 54c4e12bb5e0 |
permissions | -rw-r--r-- |
41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41931
diff
changeset
|
1 |
(* Title: HOL/ex/Quickcheck_Narrowing_Examples.thy |
41907 | 2 |
Author: Lukas Bulwahn |
3 |
Copyright 2011 TU Muenchen |
|
4 |
*) |
|
5 |
||
41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41931
diff
changeset
|
6 |
header {* Examples for narrowing-based testing *} |
41907 | 7 |
|
41932
e8f113ce8a94
adapting Quickcheck_Narrowing and example file to new names
bulwahn
parents:
41931
diff
changeset
|
8 |
theory Quickcheck_Narrowing_Examples |
43318 | 9 |
imports Main |
41907 | 10 |
begin |
11 |
||
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
12 |
subsection {* Minimalistic examples *} |
43356 | 13 |
|
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
14 |
lemma |
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
15 |
"x = y" |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
42020
diff
changeset
|
16 |
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample] |
41907 | 17 |
oops |
43356 | 18 |
|
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
19 |
lemma |
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
20 |
"x = y" |
43356 | 21 |
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
41907 | 22 |
oops |
23 |
||
43239 | 24 |
subsection {* Simple examples with existentials *} |
25 |
||
26 |
lemma |
|
27 |
"\<exists> y :: nat. \<forall> x. x = y" |
|
28 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
|
29 |
oops |
|
43356 | 30 |
(* |
31 |
lemma |
|
32 |
"\<exists> y :: int. \<forall> x. x = y" |
|
33 |
quickcheck[tester = narrowing, size = 2] |
|
34 |
oops |
|
35 |
*) |
|
43239 | 36 |
lemma |
37 |
"x > 1 --> (\<exists>y :: nat. x < y & y <= 1)" |
|
38 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
|
39 |
oops |
|
40 |
||
41 |
lemma |
|
42 |
"x > 2 --> (\<exists>y :: nat. x < y & y <= 2)" |
|
43 |
quickcheck[tester = narrowing, finite_types = false, size = 10] |
|
44 |
oops |
|
45 |
||
46 |
lemma |
|
47 |
"\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)" |
|
48 |
quickcheck[tester = narrowing, finite_types = false, size = 7] |
|
49 |
oops |
|
50 |
||
51 |
text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *} |
|
52 |
lemma |
|
53 |
"~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]" |
|
54 |
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
|
55 |
oops |
|
56 |
||
57 |
text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *} |
|
58 |
lemma |
|
59 |
"x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys" |
|
60 |
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
|
61 |
oops |
|
62 |
||
63 |
text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *} |
|
64 |
lemma |
|
65 |
"(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)" |
|
66 |
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
|
67 |
oops |
|
68 |
||
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
69 |
subsection {* Simple list examples *} |
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
70 |
|
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
71 |
lemma "rev xs = xs" |
43239 | 72 |
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] |
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
73 |
oops |
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
74 |
|
43239 | 75 |
(* FIXME: integer has strange representation! *) |
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
76 |
lemma "rev xs = xs" |
43239 | 77 |
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample] |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
42020
diff
changeset
|
78 |
oops |
42184
1d4fae76ba5e
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents:
42024
diff
changeset
|
79 |
(* |
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
42020
diff
changeset
|
80 |
lemma "rev xs = xs" |
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
81 |
quickcheck[tester = narrowing, finite_types = true, expect = counterexample] |
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
82 |
oops |
42184
1d4fae76ba5e
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents:
42024
diff
changeset
|
83 |
*) |
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
84 |
subsection {* Simple examples with functions *} |
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
85 |
|
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
86 |
lemma "map f xs = map g xs" |
43239 | 87 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
88 |
oops |
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset
|
89 |
|
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42021
diff
changeset
|
90 |
lemma "map f xs = map f ys ==> xs = ys" |
43239 | 91 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
92 |
oops |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
93 |
|
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
94 |
lemma |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
95 |
"list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)" |
43239 | 96 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
97 |
oops |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
98 |
|
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
99 |
lemma "map f xs = F f xs" |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
100 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
101 |
oops |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
102 |
|
43239 | 103 |
lemma "map f xs = F f xs" |
104 |
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] |
|
105 |
oops |
|
106 |
||
107 |
(* requires some work...*) |
|
108 |
(* |
|
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
109 |
lemma "R O S = S O R" |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
110 |
quickcheck[tester = narrowing, size = 2] |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
111 |
oops |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
112 |
*) |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
113 |
|
41907 | 114 |
subsection {* AVL Trees *} |
115 |
||
116 |
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat |
|
117 |
||
118 |
primrec set_of :: "'a tree \<Rightarrow> 'a set" |
|
119 |
where |
|
120 |
"set_of ET = {}" | |
|
121 |
"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)" |
|
122 |
||
123 |
primrec height :: "'a tree \<Rightarrow> nat" |
|
124 |
where |
|
125 |
"height ET = 0" | |
|
126 |
"height (MKT x l r h) = max (height l) (height r) + 1" |
|
127 |
||
128 |
primrec avl :: "'a tree \<Rightarrow> bool" |
|
129 |
where |
|
130 |
"avl ET = True" | |
|
131 |
"avl (MKT x l r h) = |
|
132 |
((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and> |
|
133 |
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
|
134 |
||
135 |
primrec is_ord :: "('a::order) tree \<Rightarrow> bool" |
|
136 |
where |
|
137 |
"is_ord ET = True" | |
|
138 |
"is_ord (MKT n l r h) = |
|
139 |
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)" |
|
140 |
||
141 |
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool" |
|
142 |
where |
|
143 |
"is_in k ET = False" | |
|
144 |
"is_in k (MKT n l r h) = (if k = n then True else |
|
145 |
if k < n then (is_in k l) |
|
146 |
else (is_in k r))" |
|
147 |
||
148 |
primrec ht :: "'a tree \<Rightarrow> nat" |
|
149 |
where |
|
150 |
"ht ET = 0" | |
|
151 |
"ht (MKT x l r h) = h" |
|
152 |
||
153 |
definition |
|
154 |
mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
155 |
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)" |
|
156 |
||
157 |
(* replaced MKT lrn lrl lrr by MKT lrr lrl *) |
|
158 |
fun l_bal where |
|
159 |
"l_bal(n, MKT ln ll lr h, r) = |
|
160 |
(if ht ll < ht lr |
|
161 |
then case lr of ET \<Rightarrow> ET (* impossible *) |
|
162 |
| MKT lrn lrr lrl lrh \<Rightarrow> |
|
163 |
mkt lrn (mkt ln ll lrl) (mkt n lrr r) |
|
164 |
else mkt ln ll (mkt n lr r))" |
|
165 |
||
166 |
fun r_bal where |
|
167 |
"r_bal(n, l, MKT rn rl rr h) = |
|
168 |
(if ht rl > ht rr |
|
169 |
then case rl of ET \<Rightarrow> ET (* impossible *) |
|
170 |
| MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr) |
|
171 |
else mkt rn (mkt n l rl) rr)" |
|
172 |
||
173 |
primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree" |
|
174 |
where |
|
175 |
"insrt x ET = MKT x ET ET 1" | |
|
176 |
"insrt x (MKT n l r h) = |
|
177 |
(if x=n |
|
178 |
then MKT n l r h |
|
179 |
else if x<n |
|
180 |
then let l' = insrt x l; hl' = ht l'; hr = ht r |
|
181 |
in if hl' = 2+hr then l_bal(n,l',r) |
|
182 |
else MKT n l' r (1 + max hl' hr) |
|
183 |
else let r' = insrt x r; hl = ht l; hr' = ht r' |
|
184 |
in if hr' = 2+hl then r_bal(n,l,r') |
|
185 |
else MKT n l r' (1 + max hl hr'))" |
|
186 |
||
187 |
||
188 |
subsubsection {* Necessary setup for code generation *} |
|
189 |
||
190 |
primrec set_of' |
|
191 |
where |
|
192 |
"set_of' ET = []" |
|
193 |
| "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)" |
|
194 |
||
195 |
lemma set_of': |
|
196 |
"set (set_of' t) = set_of t" |
|
197 |
by (induct t) auto |
|
198 |
||
199 |
lemma is_ord_mkt: |
|
200 |
"is_ord (MKT n l r h) = ((ALL n': set (set_of' l). n' < n) & (ALL n': set (set_of' r). n < n') & is_ord l & is_ord r)" |
|
201 |
by (simp add: set_of') |
|
202 |
||
203 |
declare is_ord.simps(1)[code] is_ord_mkt[code] |
|
204 |
||
205 |
subsubsection {* Invalid Lemma due to typo in lbal *} |
|
206 |
||
207 |
lemma is_ord_l_bal: |
|
208 |
"\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
|
42184
1d4fae76ba5e
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents:
42024
diff
changeset
|
209 |
quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 1000, expect = counterexample] |
41907 | 210 |
oops |
211 |
||
212 |
||
213 |
end |