33197
|
1 |
(* Title: HOL/Nitpick_Examples/Pattern_Nits.thy
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Copyright 2009
|
|
4 |
|
|
5 |
Examples featuring Nitpick's "destroy_constrs" optimization.
|
|
6 |
*)
|
|
7 |
|
|
8 |
header {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}
|
|
9 |
|
|
10 |
theory Pattern_Nits
|
|
11 |
imports Main
|
|
12 |
begin
|
|
13 |
|
|
14 |
nitpick_params [card = 14]
|
|
15 |
|
|
16 |
lemma "x = (case u of () \<Rightarrow> y)"
|
|
17 |
nitpick [expect = genuine]
|
|
18 |
oops
|
|
19 |
|
|
20 |
lemma "x = (case b of True \<Rightarrow> x | False \<Rightarrow> y)"
|
|
21 |
nitpick [expect = genuine]
|
|
22 |
oops
|
|
23 |
|
|
24 |
lemma "x = (case p of (x, y) \<Rightarrow> y)"
|
|
25 |
nitpick [expect = genuine]
|
|
26 |
oops
|
|
27 |
|
|
28 |
lemma "x = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> n)"
|
|
29 |
nitpick [expect = genuine]
|
|
30 |
oops
|
|
31 |
|
|
32 |
lemma "x = (case opt of None \<Rightarrow> x | Some y \<Rightarrow> y)"
|
|
33 |
nitpick [expect = genuine]
|
|
34 |
oops
|
|
35 |
|
|
36 |
lemma "x = (case xs of [] \<Rightarrow> x | y # ys \<Rightarrow> y)"
|
|
37 |
nitpick [expect = genuine]
|
|
38 |
oops
|
|
39 |
|
|
40 |
lemma "x = (case xs of
|
|
41 |
[] \<Rightarrow> x
|
|
42 |
| y # ys \<Rightarrow>
|
|
43 |
(case ys of
|
|
44 |
[] \<Rightarrow> x
|
|
45 |
| z # zs \<Rightarrow>
|
|
46 |
(case z of
|
|
47 |
None \<Rightarrow> x
|
|
48 |
| Some p \<Rightarrow>
|
|
49 |
(case p of
|
|
50 |
(a, b) \<Rightarrow> b))))"
|
|
51 |
nitpick [expect = genuine]
|
|
52 |
oops
|
|
53 |
|
|
54 |
fun f1 where
|
|
55 |
"f1 x () = x"
|
|
56 |
|
|
57 |
lemma "x = f1 y u"
|
|
58 |
nitpick [expect = genuine]
|
|
59 |
oops
|
|
60 |
|
|
61 |
fun f2 where
|
|
62 |
"f2 x _ True = x" |
|
|
63 |
"f2 _ y False = y"
|
|
64 |
|
|
65 |
lemma "x = f2 x y b"
|
|
66 |
nitpick [expect = genuine]
|
|
67 |
oops
|
|
68 |
|
|
69 |
fun f3 where
|
|
70 |
"f3 (_, y) = y"
|
|
71 |
|
|
72 |
lemma "x = f3 p"
|
|
73 |
nitpick [expect = genuine]
|
|
74 |
oops
|
|
75 |
|
|
76 |
fun f4 where
|
|
77 |
"f4 x 0 = x" |
|
|
78 |
"f4 _ (Suc n) = n"
|
|
79 |
|
|
80 |
lemma "x = f4 x n"
|
|
81 |
nitpick [expect = genuine]
|
|
82 |
oops
|
|
83 |
|
|
84 |
fun f5 where
|
|
85 |
"f5 x None = x" |
|
|
86 |
"f5 _ (Some y) = y"
|
|
87 |
|
|
88 |
lemma "x = f5 x opt"
|
|
89 |
nitpick [expect = genuine]
|
|
90 |
oops
|
|
91 |
|
|
92 |
fun f6 where
|
|
93 |
"f6 x [] = x" |
|
|
94 |
"f6 _ (y # ys) = y"
|
|
95 |
|
|
96 |
lemma "x = f6 x xs"
|
|
97 |
nitpick [expect = genuine]
|
|
98 |
oops
|
|
99 |
|
|
100 |
fun f7 where
|
|
101 |
"f7 _ (y # Some (a, b) # zs) = b" |
|
|
102 |
"f7 x (y # None # zs) = x" |
|
|
103 |
"f7 x [y] = x" |
|
|
104 |
"f7 x [] = x"
|
|
105 |
|
|
106 |
lemma "x = f7 x xs"
|
|
107 |
nitpick [expect = genuine]
|
|
108 |
oops
|
|
109 |
|
|
110 |
lemma "u = ()"
|
|
111 |
nitpick [expect = none]
|
|
112 |
sorry
|
|
113 |
|
|
114 |
lemma "\<exists>y. (b::bool) = y"
|
|
115 |
nitpick [expect = none]
|
|
116 |
sorry
|
|
117 |
|
|
118 |
lemma "\<exists>x y. p = (x, y)"
|
|
119 |
nitpick [expect = none]
|
|
120 |
sorry
|
|
121 |
|
|
122 |
lemma "\<exists>x. n = Suc x"
|
|
123 |
nitpick [expect = genuine]
|
|
124 |
oops
|
|
125 |
|
|
126 |
lemma "\<exists>y. x = Some y"
|
|
127 |
nitpick [expect = genuine]
|
|
128 |
oops
|
|
129 |
|
|
130 |
lemma "\<exists>y ys. xs = y # ys"
|
|
131 |
nitpick [expect = genuine]
|
|
132 |
oops
|
|
133 |
|
|
134 |
lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)"
|
|
135 |
nitpick [expect = genuine]
|
|
136 |
oops
|
|
137 |
|
|
138 |
end
|