author  bulwahn 
Thu, 09 Jun 2011 10:19:51 +0200  
changeset 43318  825f4f0dcf71 
parent 43239  42f82fda796b 
child 43356  2dee03f192b7 
permissions  rwrr 
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 narrowingbased 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 *} 
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
42020
diff
changeset

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 
42021
52551c0a3374
extending code_int type more; adding narrowing instance for type int; added test case for int instance
bulwahn
parents:
42020
diff
changeset

18 
*) 
41907  19 
(* 
42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

20 
lemma 
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

21 
"x = y" 
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

22 
quickcheck[tester = narrowing, finite_types = true, expect = counterexample] 
41907  23 
oops 
24 
*) 

25 

43239  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 copynpaste 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 

42020
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

67 
subsection {* Simple list examples *} 
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

68 

2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

69 
lemma "rev xs = xs" 
43239  70 
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

71 
oops 
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

72 

43239  73 
(* 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

74 
lemma "rev xs = xs" 
43239  75 
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

76 
oops 
42184
1d4fae76ba5e
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents:
42024
diff
changeset

77 
(* 
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 
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

79 
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

80 
oops 
42184
1d4fae76ba5e
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
bulwahn
parents:
42024
diff
changeset

81 
*) 
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

82 
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

83 

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 
lemma "map f xs = map g xs" 
43239  85 
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

86 
oops 
2da02764d523
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
bulwahn
parents:
41963
diff
changeset

87 

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

88 
lemma "map f xs = map f ys ==> xs = ys" 
43239  89 
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

90 
oops 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

91 

51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

92 
lemma 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

93 
"list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)" 
43239  94 
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

95 
oops 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

96 

51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

97 
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

98 
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

99 
oops 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

100 

43239  101 
lemma "map f xs = F f xs" 
102 
quickcheck[tester = narrowing, finite_types = false, expect = counterexample] 

103 
oops 

104 

105 
(* requires some work...*) 

106 
(* 

42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

107 
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

108 
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

109 
oops 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

110 
*) 
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset

111 

41907  112 
subsection {* AVL Trees *} 
113 

114 
datatype 'a tree = ET  MKT 'a "'a tree" "'a tree" nat 

115 

116 
primrec set_of :: "'a tree \<Rightarrow> 'a set" 

117 
where 

118 
"set_of ET = {}"  

119 
"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)" 

120 

121 
primrec height :: "'a tree \<Rightarrow> nat" 

122 
where 

123 
"height ET = 0"  

124 
"height (MKT x l r h) = max (height l) (height r) + 1" 

125 

126 
primrec avl :: "'a tree \<Rightarrow> bool" 

127 
where 

128 
"avl ET = True"  

129 
"avl (MKT x l r h) = 

130 
((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and> 

131 
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" 

132 

133 
primrec is_ord :: "('a::order) tree \<Rightarrow> bool" 

134 
where 

135 
"is_ord ET = True"  

136 
"is_ord (MKT n l r h) = 

137 
((\<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)" 

138 

139 
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool" 

140 
where 

141 
"is_in k ET = False"  

142 
"is_in k (MKT n l r h) = (if k = n then True else 

143 
if k < n then (is_in k l) 

144 
else (is_in k r))" 

145 

146 
primrec ht :: "'a tree \<Rightarrow> nat" 

147 
where 

148 
"ht ET = 0"  

149 
"ht (MKT x l r h) = h" 

150 

151 
definition 

152 
mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where 

153 
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)" 

154 

155 
(* replaced MKT lrn lrl lrr by MKT lrr lrl *) 

156 
fun l_bal where 

157 
"l_bal(n, MKT ln ll lr h, r) = 

158 
(if ht ll < ht lr 

159 
then case lr of ET \<Rightarrow> ET (* impossible *) 

160 
 MKT lrn lrr lrl lrh \<Rightarrow> 

161 
mkt lrn (mkt ln ll lrl) (mkt n lrr r) 

162 
else mkt ln ll (mkt n lr r))" 

163 

164 
fun r_bal where 

165 
"r_bal(n, l, MKT rn rl rr h) = 

166 
(if ht rl > ht rr 

167 
then case rl of ET \<Rightarrow> ET (* impossible *) 

168 
 MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr) 

169 
else mkt rn (mkt n l rl) rr)" 

170 

171 
primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 

172 
where 

173 
"insrt x ET = MKT x ET ET 1"  

174 
"insrt x (MKT n l r h) = 

175 
(if x=n 

176 
then MKT n l r h 

177 
else if x<n 

178 
then let l' = insrt x l; hl' = ht l'; hr = ht r 

179 
in if hl' = 2+hr then l_bal(n,l',r) 

180 
else MKT n l' r (1 + max hl' hr) 

181 
else let r' = insrt x r; hl = ht l; hr' = ht r' 

182 
in if hr' = 2+hl then r_bal(n,l,r') 

183 
else MKT n l r' (1 + max hl hr'))" 

184 

185 

186 
subsubsection {* Necessary setup for code generation *} 

187 

188 
primrec set_of' 

189 
where 

190 
"set_of' ET = []" 

191 
 "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)" 

192 

193 
lemma set_of': 

194 
"set (set_of' t) = set_of t" 

195 
by (induct t) auto 

196 

197 
lemma is_ord_mkt: 

198 
"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)" 

199 
by (simp add: set_of') 

200 

201 
declare is_ord.simps(1)[code] is_ord_mkt[code] 

202 

203 
subsubsection {* Invalid Lemma due to typo in lbal *} 

204 

205 
lemma is_ord_l_bal: 

206 
"\<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

207 
quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 1000, expect = counterexample] 
41907  208 
oops 
209 

210 

211 
end 