added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
1 (* Title: HOL/Nitpick_Examples/Manual_Nits.thy
2 Author: Jasmin Blanchette, TU Muenchen
5 Examples from the Nitpick manual.
8 header {* Examples from the Nitpick Manual *}
11 imports Main Coinductive_List RealDef
14 chapter {* 3. First Steps *}
16 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
18 subsection {* 3.1. Propositional Logic *}
20 lemma "P \<longleftrightarrow> Q"
27 subsection {* 3.2. Type Variables *}
29 lemma "P x \<Longrightarrow> P (THE y. P y)"
33 subsection {* 3.3. Constants *}
35 lemma "P x \<Longrightarrow> P (THE y. P y)"
37 nitpick [full_descrs, show_consts]
38 nitpick [dont_specialize, full_descrs, show_consts]
41 lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
43 nitpick [card 'a = 1-50]
45 apply (metis the_equality)
48 subsection {* 3.4. Skolemization *}
50 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
54 lemma "\<exists>x. \<forall>f. f x = x"
58 lemma "refl r \<Longrightarrow> sym r"
62 subsection {* 3.5. Natural Numbers and Integers *}
64 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
68 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
69 nitpick [card nat = 100, check_potential]
76 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
77 nitpick [card nat = 1]
78 nitpick [card nat = 2]
81 subsection {* 3.6. Inductive Datatypes *}
83 lemma "hd (xs @ [y, y]) = hd xs"
85 nitpick [show_consts, show_datatypes]
88 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
89 nitpick [show_datatypes]
92 subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
94 typedef three = "{0\<Colon>nat, 1, 2}"
97 definition A :: three where "A \<equiv> Abs_three 0"
98 definition B :: three where "B \<equiv> Abs_three 1"
99 definition C :: three where "C \<equiv> Abs_three 2"
101 lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
102 nitpick [show_datatypes]
109 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
110 nitpick [show_datatypes]
113 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
114 nitpick [show_datatypes]
117 subsection {* 3.8. Inductive and Coinductive Predicates *}
121 "even n \<Longrightarrow> even (Suc (Suc n))"
123 lemma "\<exists>n. even n \<and> even (Suc n)"
124 nitpick [card nat = 100, unary_ints, verbose]
127 lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
128 nitpick [card nat = 100, unary_ints, verbose]
131 inductive even' where
132 "even' (0\<Colon>nat)" |
134 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
136 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
137 nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
140 lemma "even' (n - 2) \<Longrightarrow> even' n"
141 nitpick [card nat = 10, show_consts]
144 coinductive nats where
145 "nats (x\<Colon>nat) \<Longrightarrow> nats x"
147 lemma "nats = {0, 1, 2, 3, 4}"
148 nitpick [card nat = 10, show_consts]
153 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
155 lemma "odd n \<Longrightarrow> odd (n - 2)"
156 nitpick [card nat = 10, show_consts]
159 subsection {* 3.9. Coinductive Datatypes *}
161 lemma "xs \<noteq> LCons a xs"
165 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
167 nitpick [bisim_depth = -1, verbose]
170 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
171 nitpick [bisim_depth = -1, show_datatypes]
175 subsection {* 3.10. Boxing *}
177 datatype tm = Var nat | Lam tm | App tm tm
180 "lift (Var j) k = Var (if j < k then j else j + 1)" |
181 "lift (Lam t) k = Lam (lift t (k + 1))" |
182 "lift (App t u) k = App (lift t k) (lift u k)"
185 "loose (Var j) k = (j \<ge> k)" |
186 "loose (Lam t) k = loose t (Suc k)" |
187 "loose (App t u) k = (loose t k \<or> loose u k)"
189 primrec subst\<^isub>1 where
190 "subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
191 "subst\<^isub>1 \<sigma> (Lam t) =
192 Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
193 "subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
195 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
197 nitpick [eval = "subst\<^isub>1 \<sigma> t"]
201 primrec subst\<^isub>2 where
202 "subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
203 "subst\<^isub>2 \<sigma> (Lam t) =
204 Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
205 "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
207 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
211 subsection {* 3.11. Scope Monotonicity *}
213 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
215 nitpick [card = 8, verbose]
218 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
223 subsection {* 3.12. Inductive Properties *}
225 inductive_set reach where
226 "(4\<Colon>nat) \<in> reach" |
227 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
228 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
230 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
232 apply (induct set: reach)
235 apply (thin_tac "n \<in> reach")
239 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
241 apply (induct set: reach)
244 apply (thin_tac "n \<in> reach")
248 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
249 by (induct set: reach) arith+
251 datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
254 "labels (Leaf a) = {a}" |
255 "labels (Branch t u) = labels t \<union> labels u"
259 (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
260 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
262 lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
265 case Leaf thus ?case by simp
267 case (Branch t u) thus ?case
269 nitpick [non_std, show_all]
272 lemma "labels (swap t a b) =
273 (if a \<in> labels t then
274 if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
276 if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
279 case Leaf thus ?case by simp
281 case (Branch t u) thus ?case
282 nitpick [non_std "'a bin_tree", show_consts]
286 section {* 4. Case Studies *}
288 nitpick_params [max_potential = 0, max_threads = 2]
290 subsection {* 4.1. A Context-Free Grammar *}
292 datatype alphabet = a | b
294 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
295 "[] \<in> S\<^isub>1"
296 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
297 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
298 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
299 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
300 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
302 theorem S\<^isub>1_sound:
303 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
307 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
308 "[] \<in> S\<^isub>2"
309 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
310 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
311 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
312 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
313 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
315 theorem S\<^isub>2_sound:
316 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
320 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
321 "[] \<in> S\<^isub>3"
322 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
323 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
324 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
325 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
326 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
328 theorem S\<^isub>3_sound:
329 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
333 theorem S\<^isub>3_complete:
334 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
338 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
339 "[] \<in> S\<^isub>4"
340 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
341 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
342 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
343 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
344 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
345 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
347 theorem S\<^isub>4_sound:
348 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
352 theorem S\<^isub>4_complete:
353 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
357 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
358 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
359 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
360 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
364 subsection {* 4.2. AA Trees *}
366 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
369 "data \<Lambda> = undefined" |
370 "data (N x _ _ _) = x"
372 primrec dataset where
373 "dataset \<Lambda> = {}" |
374 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
377 "level \<Lambda> = 0" |
378 "level (N _ k _ _) = k"
381 "left \<Lambda> = \<Lambda>" |
382 "left (N _ _ t\<^isub>1 _) = t\<^isub>1"
385 "right \<Lambda> = \<Lambda>" |
386 "right (N _ _ _ t\<^isub>2) = t\<^isub>2"
389 "wf \<Lambda> = True" |
391 (if t = \<Lambda> then
392 k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
394 wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
397 "skew \<Lambda> = \<Lambda>" |
399 (if t \<noteq> \<Lambda> \<and> k = level t then
400 N (data t) k (left t) (N x k (right t) u)
405 "split \<Lambda> = \<Lambda>" |
407 (if u \<noteq> \<Lambda> \<and> k = level (right u) then
408 N (data u) (Suc k) (N x k t (left u)) (right u)
412 theorem dataset_skew_split:
413 "dataset (skew t) = dataset t"
414 "dataset (split t) = dataset t"
418 theorem wf_skew_split:
419 "wf t \<Longrightarrow> skew t = t"
420 "wf t \<Longrightarrow> split t = t"
424 primrec insort\<^isub>1 where
425 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
426 "insort\<^isub>1 (N y k t u) x =
427 (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
428 (if x > y then insort\<^isub>1 u x else u))"
430 theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
434 theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
435 nitpick [eval = "insort\<^isub>1 t x"]
438 primrec insort\<^isub>2 where
439 "insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
440 "insort\<^isub>2 (N y k t u) x =
441 (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
442 (if x > y then insort\<^isub>2 u x else u))"
444 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
448 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"