author  blanchet 
Wed, 03 Sep 2014 00:06:24 +0200  
changeset 58152  6fe60a9a5bad 
parent 57992  2371bff894f9 
child 58310  91ea607a34d8 
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 

57242  11 
imports Record 
55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55415
diff
changeset

12 
keywords 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55415
diff
changeset

13 
"nitpick" :: diag and 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
55415
diff
changeset

14 
"nitpick_params" :: thy_decl 
33192  15 
begin 
16 

58152  17 
datatype_new (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b" 
18 
datatype_new (dead 'a, dead 'b) pair_box = PairBox 'a 'b 

19 
datatype_new (dead 'a) word = Word "'a set" 

33192  20 

57992  21 
typedecl bisim_iterator 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
33747
diff
changeset

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

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

24 

57992  25 
consts 
26 
unknown :: 'a 

27 
is_unknown :: "'a \<Rightarrow> bool" 

28 
bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 

29 
bisim_iterator_max :: bisim_iterator 

30 
Quot :: "'a \<Rightarrow> 'b" 

31 
safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" 

33192  32 

33 
text {* 

34 
Alternative definitions. 

35 
*} 

36 

57992  37 
lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}" 
38 
apply (rule eq_reflection) 

39 
apply (simp add: Ex1_def set_eq_iff) 

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) 

47 
by auto 

33192  48 

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

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

33192  54 

57992  55 
lemma tranclp_unfold[nitpick_unfold]: 
56 
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" 

57 
by (simp add: trancl_def) 

33192  58 

54148  59 
lemma [nitpick_simp]: 
57992  60 
"of_nat n = (if n = 0 then 0 else 1 + of_nat (n  1))" 
61 
by (cases n) auto 

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

62 

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

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

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

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

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

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

72 
definition card' :: "'a set \<Rightarrow> nat" where 
57992  73 
"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0" 
33192  74 

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

75 
definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where 
57992  76 
"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0" 
33192  77 

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

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

33192  81 

82 
text {* 

83 
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

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

57992  87 
lemma The_psimp[nitpick_psimp]: "P = (op =) x \<Longrightarrow> The P = x" 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45140
diff
changeset

88 
by auto 
33192  89 

57992  90 
lemma Eps_psimp[nitpick_psimp]: 
91 
"\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x" 

92 
apply (cases "P (Eps P)") 

93 
apply auto 

94 
apply (erule contrapos_np) 

95 
by (rule someI) 

33192  96 

57992  97 
lemma case_unit_unfold[nitpick_unfold]: 
98 
"case_unit x u \<equiv> x" 

99 
apply (subgoal_tac "u = ()") 

100 
apply (simp only: unit.case) 

101 
by simp 

33192  102 

57992  103 
declare unit.case[nitpick_simp del] 
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

104 

57992  105 
lemma case_nat_unfold[nitpick_unfold]: 
106 
"case_nat x f n \<equiv> if n = 0 then x else f (n  1)" 

107 
apply (rule eq_reflection) 

108 
by (cases n) auto 

33192  109 

57992  110 
declare nat.case[nitpick_simp del] 
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

111 

57992  112 
lemma size_list_simp[nitpick_simp]: 
113 
"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))" 

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

115 
by (cases xs) auto 

33192  116 

117 
text {* 

118 
Auxiliary definitions used to provide an alternative representation for 

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

120 
*} 

121 

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

57992  123 
"nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" 
124 
by auto 

125 
termination 

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

127 
apply auto 

128 
apply (metis mod_less_divisor xt1(9)) 

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

130 

131 
declare nat_gcd.simps[simp del] 

33192  132 

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

57992  134 
"nat_lcm x y = x * y div (nat_gcd x y)" 
33192  135 

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

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

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

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

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

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

57992  145 
consts 
146 
Abs_Frac :: "int \<times> int \<Rightarrow> 'a" 

56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
55642
diff
changeset

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

149 
definition zero_frac :: 'a where 

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

152 
definition one_frac :: 'a where 

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

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

57992  156 
"num \<equiv> fst o Rep_Frac" 
33192  157 

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

57992  159 
"denom \<equiv> snd o Rep_Frac" 
33192  160 

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

57992  162 
"norm_frac a b = 
163 
(if b < 0 then norm_frac ( a) ( b) 

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

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

166 
by pat_completeness auto 

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

168 

169 
declare norm_frac.simps[simp del] 

33192  170 

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

57992  172 
"frac a b \<equiv> Abs_Frac (norm_frac a b)" 
33192  173 

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

57992  175 
[nitpick_simp]: "plus_frac q r = (let d = int_lcm (denom q) (denom r) in 
176 
frac (num q * (d div denom q) + num r * (d div denom r)) d)" 

33192  177 

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

57992  179 
[nitpick_simp]: "times_frac q r = frac (num q * num r) (denom q * denom r)" 
33192  180 

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

57992  182 
"uminus_frac q \<equiv> Abs_Frac ( num q, denom q)" 
33192  183 

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

57992  185 
"number_of_frac n \<equiv> Abs_Frac (n, 1)" 
33192  186 

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

57992  188 
"inverse_frac q \<equiv> frac (denom q) (num q)" 
33192  189 

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

190 
definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 
57992  191 
[nitpick_simp]: "less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0" 
37397
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 
57992  194 
[nitpick_simp]: "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0" 
33192  195 

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

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

55017  199 
axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 
200 

201 
definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 

57992  202 
[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" 
55017  203 

204 
definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 

57992  205 
"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x else THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y" 
55017  206 

48891  207 
ML_file "Tools/Nitpick/kodkod.ML" 
208 
ML_file "Tools/Nitpick/kodkod_sat.ML" 

209 
ML_file "Tools/Nitpick/nitpick_util.ML" 

210 
ML_file "Tools/Nitpick/nitpick_hol.ML" 

211 
ML_file "Tools/Nitpick/nitpick_mono.ML" 

212 
ML_file "Tools/Nitpick/nitpick_preproc.ML" 

213 
ML_file "Tools/Nitpick/nitpick_scope.ML" 

214 
ML_file "Tools/Nitpick/nitpick_peephole.ML" 

215 
ML_file "Tools/Nitpick/nitpick_rep.ML" 

216 
ML_file "Tools/Nitpick/nitpick_nut.ML" 

217 
ML_file "Tools/Nitpick/nitpick_kodkod.ML" 

218 
ML_file "Tools/Nitpick/nitpick_model.ML" 

219 
ML_file "Tools/Nitpick/nitpick.ML" 

55199  220 
ML_file "Tools/Nitpick/nitpick_commands.ML" 
48891  221 
ML_file "Tools/Nitpick/nitpick_tests.ML" 
33192  222 

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

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

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

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

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

227 
(@{const_name fold_graph}, @{const_name fold_graph'}), 
55017  228 
(@{const_name wf}, @{const_name wf'}), 
229 
(@{const_name wf_wfrec}, @{const_name wf_wfrec'}), 

230 
(@{const_name wfrec}, @{const_name wfrec'})] 

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

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

232 

57992  233 
hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod 
234 
refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac 

235 
zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac 

236 
inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec' 

237 

46324  238 
hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word 
57992  239 

240 
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def 

241 
card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold 

242 
size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def 

243 
num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def 

244 
number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def 

245 
wfrec'_def 

33192  246 

247 
end 