author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 49989  34d0ac1bdac6 
permissions  rwrr 
33192  1 
(* Title: HOL/Nitpick.thy 
2 
Author: Jasmin Blanchette, TU Muenchen 

35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35699
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Nitpick: Yet another counterexample generator for Isabelle/HOL. 

6 
*) 

7 

8 
header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} 

9 

10 
theory Nitpick 

38393  11 
imports Map Quotient SAT Record 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46324
diff
changeset

12 
keywords "nitpick" :: diag and "nitpick_params" :: thy_decl 
33192  13 
begin 
14 

15 
typedecl bisim_iterator 

16 

17 
axiomatization unknown :: 'a 

34938  18 
and is_unknown :: "'a \<Rightarrow> bool" 
33192  19 
and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
20 
and bisim_iterator_max :: bisim_iterator 

34938  21 
and Quot :: "'a \<Rightarrow> 'b" 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

22 
and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" 
33192  23 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35311
diff
changeset

24 
datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)" 
33192  25 
datatype ('a, 'b) pair_box = PairBox 'a 'b 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33747
diff
changeset

26 

c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33747
diff
changeset

27 
typedecl unsigned_bit 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33747
diff
changeset

28 
typedecl signed_bit 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33747
diff
changeset

29 

c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33747
diff
changeset

30 
datatype 'a word = Word "('a set)" 
33192  31 

32 
text {* 

33 
Alternative definitions. 

34 
*} 

35 

41797  36 
lemma Ex1_unfold [nitpick_unfold, no_atp]: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

37 
"Ex1 P \<equiv> \<exists>x. {x. P x} = {x}" 
33192  38 
apply (rule eq_reflection) 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39223
diff
changeset

39 
apply (simp add: Ex1_def set_eq_iff) 
33192  40 
apply (rule iffI) 
41 
apply (erule exE) 

42 
apply (erule conjE) 

43 
apply (rule_tac x = x in exI) 

44 
apply (rule allI) 

45 
apply (rename_tac y) 

46 
apply (erule_tac x = y in allE) 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

47 
by auto 
33192  48 

41797  49 
lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>=" 
45140  50 
by (simp only: rtrancl_trancl_reflcl) 
33192  51 

41797  52 
lemma rtranclp_unfold [nitpick_unfold, no_atp]: 
33192  53 
"rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)" 
54 
by (rule eq_reflection) (auto dest: rtranclpD) 

55 

41797  56 
lemma tranclp_unfold [nitpick_unfold, no_atp]: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

57 
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

58 
by (simp add: trancl_def) 
33192  59 

47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
46950
diff
changeset

60 
lemma [nitpick_simp, no_atp]: 
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
46950
diff
changeset

61 
"of_nat n = (if n = 0 then 0 else 1 + of_nat (n  1))" 
47988  62 
by (cases n) auto 
47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
46950
diff
changeset

63 

41046  64 
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where 
65 
"prod A B = {(a, b). a \<in> A \<and> b \<in> B}" 

66 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44016
diff
changeset

67 
definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where 
33192  68 
"refl' r \<equiv> \<forall>x. (x, x) \<in> r" 
69 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44016
diff
changeset

70 
definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where 
33192  71 
"wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)" 
72 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44016
diff
changeset

73 
definition card' :: "'a set \<Rightarrow> nat" where 
39365
9cab71c20613
remove more clutter related to old "fast_descrs" optimization
blanchet
parents:
39302
diff
changeset

74 
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0" 
33192  75 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44016
diff
changeset

76 
definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where 
39365
9cab71c20613
remove more clutter related to old "fast_descrs" optimization
blanchet
parents:
39302
diff
changeset

77 
"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0" 
33192  78 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44016
diff
changeset

79 
inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where 
33192  80 
"fold_graph' f z {} z"  
81 
"\<lbrakk>x \<in> A; fold_graph' f z (A  {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)" 

82 

83 
text {* 

84 
The following lemmas are not strictly necessary but they help the 

47909
5f1afeebafbc
fixed "real" after they were redefined as a 'quotient_type'
blanchet
parents:
46950
diff
changeset

85 
\textit{specialize} optimization. 
33192  86 
*} 
87 

36918  88 
lemma The_psimp [nitpick_psimp, no_atp]: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

89 
"P = (op =) x \<Longrightarrow> The P = x" 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

90 
by auto 
33192  91 

36918  92 
lemma Eps_psimp [nitpick_psimp, no_atp]: 
33192  93 
"\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x" 
47988  94 
apply (cases "P (Eps P)") 
33192  95 
apply auto 
96 
apply (erule contrapos_np) 

97 
by (rule someI) 

98 

41797  99 
lemma unit_case_unfold [nitpick_unfold, no_atp]: 
33192  100 
"unit_case x u \<equiv> x" 
101 
apply (subgoal_tac "u = ()") 

102 
apply (simp only: unit.cases) 

103 
by simp 

104 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33192
diff
changeset

105 
declare unit.cases [nitpick_simp del] 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33192
diff
changeset

106 

41797  107 
lemma nat_case_unfold [nitpick_unfold, no_atp]: 
33192  108 
"nat_case x f n \<equiv> if n = 0 then x else f (n  1)" 
109 
apply (rule eq_reflection) 

47988  110 
by (cases n) auto 
33192  111 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33192
diff
changeset

112 
declare nat.cases [nitpick_simp del] 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33192
diff
changeset

113 

36918  114 
lemma list_size_simp [nitpick_simp, no_atp]: 
33192  115 
"list_size f xs = (if xs = [] then 0 
116 
else Suc (f (hd xs) + list_size f (tl xs)))" 

117 
"size xs = (if xs = [] then 0 else Suc (size (tl xs)))" 

47988  118 
by (cases xs) auto 
33192  119 

120 
text {* 

121 
Auxiliary definitions used to provide an alternative representation for 

122 
@{text rat} and @{text real}. 

123 
*} 

124 

125 
function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where 

126 
[simp del]: "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" 

127 
by auto 

128 
termination 

129 
apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))") 

130 
apply auto 

131 
apply (metis mod_less_divisor xt1(9)) 

132 
by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10)) 

133 

134 
definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where 

135 
"nat_lcm x y = x * y div (nat_gcd x y)" 

136 

137 
definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where 

138 
"int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))" 

139 

140 
definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where 

141 
"int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))" 

142 

143 
definition Frac :: "int \<times> int \<Rightarrow> bool" where 

144 
"Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1" 

145 

146 
axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a" 

147 
and Rep_Frac :: "'a \<Rightarrow> int \<times> int" 

148 

149 
definition zero_frac :: 'a where 

150 
"zero_frac \<equiv> Abs_Frac (0, 1)" 

151 

152 
definition one_frac :: 'a where 

153 
"one_frac \<equiv> Abs_Frac (1, 1)" 

154 

155 
definition num :: "'a \<Rightarrow> int" where 

156 
"num \<equiv> fst o Rep_Frac" 

157 

158 
definition denom :: "'a \<Rightarrow> int" where 

159 
"denom \<equiv> snd o Rep_Frac" 

160 

161 
function norm_frac :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where 

162 
[simp del]: "norm_frac a b = (if b < 0 then norm_frac ( a) ( b) 

163 
else if a = 0 \<or> b = 0 then (0, 1) 

164 
else let c = int_gcd a b in (a div c, b div c))" 

165 
by pat_completeness auto 

166 
termination by (relation "measure (\<lambda>(_, b). if b < 0 then 1 else 0)") auto 

167 

168 
definition frac :: "int \<Rightarrow> int \<Rightarrow> 'a" where 

169 
"frac a b \<equiv> Abs_Frac (norm_frac a b)" 

170 

171 
definition plus_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

172 
[nitpick_simp]: 

173 
"plus_frac q r = (let d = int_lcm (denom q) (denom r) in 

174 
frac (num q * (d div denom q) + num r * (d div denom r)) d)" 

175 

176 
definition times_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

177 
[nitpick_simp]: 

178 
"times_frac q r = frac (num q * num r) (denom q * denom r)" 

179 

180 
definition uminus_frac :: "'a \<Rightarrow> 'a" where 

181 
"uminus_frac q \<equiv> Abs_Frac ( num q, denom q)" 

182 

183 
definition number_of_frac :: "int \<Rightarrow> 'a" where 

184 
"number_of_frac n \<equiv> Abs_Frac (n, 1)" 

185 

186 
definition inverse_frac :: "'a \<Rightarrow> 'a" where 

187 
"inverse_frac q \<equiv> frac (denom q) (num q)" 

188 

37397
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37213
diff
changeset

189 
definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37213
diff
changeset

190 
[nitpick_simp]: 
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37213
diff
changeset

191 
"less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0" 
18000f9d783e
adjust Nitpick's handling of "<" on "rat"s and "reals"
blanchet
parents:
37213
diff
changeset

192 

33192  193 
definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 
194 
[nitpick_simp]: 

195 
"less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0" 

196 

197 
definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where 

198 
"of_frac q \<equiv> of_int (num q) / of_int (denom q)" 

199 

48891  200 
ML_file "Tools/Nitpick/kodkod.ML" 
201 
ML_file "Tools/Nitpick/kodkod_sat.ML" 

202 
ML_file "Tools/Nitpick/nitpick_util.ML" 

203 
ML_file "Tools/Nitpick/nitpick_hol.ML" 

204 
ML_file "Tools/Nitpick/nitpick_mono.ML" 

205 
ML_file "Tools/Nitpick/nitpick_preproc.ML" 

206 
ML_file "Tools/Nitpick/nitpick_scope.ML" 

207 
ML_file "Tools/Nitpick/nitpick_peephole.ML" 

208 
ML_file "Tools/Nitpick/nitpick_rep.ML" 

209 
ML_file "Tools/Nitpick/nitpick_nut.ML" 

210 
ML_file "Tools/Nitpick/nitpick_kodkod.ML" 

211 
ML_file "Tools/Nitpick/nitpick_model.ML" 

212 
ML_file "Tools/Nitpick/nitpick.ML" 

213 
ML_file "Tools/Nitpick/nitpick_isar.ML" 

214 
ML_file "Tools/Nitpick/nitpick_tests.ML" 

33192  215 

44016
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

216 
setup {* 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

217 
Nitpick_Isar.setup #> 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

218 
Nitpick_HOL.register_ersatz_global 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

219 
[(@{const_name card}, @{const_name card'}), 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

220 
(@{const_name setsum}, @{const_name setsum'}), 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

221 
(@{const_name fold_graph}, @{const_name fold_graph'}), 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

222 
(@{const_name wf}, @{const_name wf'})] 
51184010c609
replaced Nitpick's hardwired basic_ersatz_table by context data
krauss
parents:
44013
diff
changeset

223 
*} 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33556
diff
changeset

224 

39365
9cab71c20613
remove more clutter related to old "fast_descrs" optimization
blanchet
parents:
39302
diff
changeset

225 
hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
42064
diff
changeset

226 
FunBox PairBox Word prod refl' wf' card' setsum' 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41046
diff
changeset

227 
fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac 
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41046
diff
changeset

228 
one_frac num denom norm_frac frac plus_frac times_frac uminus_frac 
39365
9cab71c20613
remove more clutter related to old "fast_descrs" optimization
blanchet
parents:
39302
diff
changeset

229 
number_of_frac inverse_frac less_frac less_eq_frac of_frac 
46324  230 
hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word 
41797  231 
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
42064
diff
changeset

232 
prod_def refl'_def wf'_def card'_def setsum'_def 
41797  233 
fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold 
41046  234 
list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def 
235 
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def 

236 
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def 

237 
inverse_frac_def less_frac_def less_eq_frac_def of_frac_def 

33192  238 

239 
end 