author | bulwahn |
Sat, 21 Jul 2012 10:55:42 +0200 | |
changeset 48415 | b42067a3188f |
parent 48046 | 359bec38a4ee |
child 48812 | 9509fc5485b2 |
permissions | -rw-r--r-- |
34126 | 1 |
(* Title: HOL/Nitpick_Examples/Integer_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
45035 | 3 |
Copyright 2009-2011 |
34126 | 4 |
|
5 |
Examples featuring Nitpick applied to natural numbers and integers. |
|
6 |
*) |
|
7 |
||
46090 | 8 |
header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} |
34126 | 9 |
|
10 |
theory Integer_Nits |
|
46090 | 11 |
imports Main |
34126 | 12 |
begin |
13 |
||
42959 | 14 |
nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6, |
42208
02513eb26eb7
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
krauss
parents:
41278
diff
changeset
|
15 |
sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
34126 | 16 |
|
17 |
lemma "Suc x = x + 1" |
|
18 |
nitpick [unary_ints, expect = none] |
|
19 |
nitpick [binary_ints, expect = none] |
|
20 |
sorry |
|
21 |
||
22 |
lemma "x < Suc x" |
|
23 |
nitpick [unary_ints, expect = none] |
|
24 |
nitpick [binary_ints, expect = none] |
|
25 |
sorry |
|
26 |
||
27 |
lemma "x + y \<ge> (x::nat)" |
|
28 |
nitpick [unary_ints, expect = none] |
|
29 |
nitpick [binary_ints, expect = none] |
|
30 |
sorry |
|
31 |
||
32 |
lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::nat)" |
|
33 |
nitpick [unary_ints, expect = none] |
|
34 |
nitpick [binary_ints, expect = none] |
|
35 |
sorry |
|
36 |
||
37 |
lemma "x + y = y + (x::nat)" |
|
38 |
nitpick [unary_ints, expect = none] |
|
39 |
nitpick [binary_ints, expect = none] |
|
40 |
sorry |
|
41 |
||
42 |
lemma "x > y \<Longrightarrow> x - y \<noteq> (0::nat)" |
|
43 |
nitpick [unary_ints, expect = none] |
|
44 |
nitpick [binary_ints, expect = none] |
|
45 |
sorry |
|
46 |
||
47 |
lemma "x \<le> y \<Longrightarrow> x - y = (0::nat)" |
|
48 |
nitpick [unary_ints, expect = none] |
|
49 |
nitpick [binary_ints, expect = none] |
|
50 |
sorry |
|
51 |
||
52 |
lemma "x - (0::nat) = x" |
|
53 |
nitpick [unary_ints, expect = none] |
|
54 |
nitpick [binary_ints, expect = none] |
|
55 |
sorry |
|
56 |
||
57 |
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::nat)" |
|
58 |
nitpick [unary_ints, expect = none] |
|
59 |
nitpick [binary_ints, expect = none] |
|
60 |
sorry |
|
61 |
||
62 |
lemma "0 * y = (0::nat)" |
|
63 |
nitpick [unary_ints, expect = none] |
|
64 |
nitpick [binary_ints, expect = none] |
|
65 |
sorry |
|
66 |
||
67 |
lemma "y * 0 = (0::nat)" |
|
68 |
nitpick [unary_ints, expect = none] |
|
69 |
nitpick [binary_ints, expect = none] |
|
70 |
sorry |
|
71 |
||
72 |
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::nat)" |
|
73 |
nitpick [unary_ints, expect = none] |
|
74 |
nitpick [binary_ints, expect = none] |
|
75 |
sorry |
|
76 |
||
77 |
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::nat)" |
|
78 |
nitpick [unary_ints, expect = none] |
|
79 |
nitpick [binary_ints, expect = none] |
|
80 |
sorry |
|
81 |
||
82 |
lemma "x * y div y = (x::nat)" |
|
83 |
nitpick [unary_ints, expect = genuine] |
|
84 |
nitpick [binary_ints, expect = genuine] |
|
85 |
oops |
|
86 |
||
87 |
lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::nat)" |
|
88 |
nitpick [unary_ints, expect = none] |
|
89 |
nitpick [binary_ints, expect = none] |
|
90 |
sorry |
|
91 |
||
92 |
lemma "5 * 55 < (260::nat)" |
|
93 |
nitpick [unary_ints, expect = none] |
|
94 |
nitpick [binary_ints, expect = none] |
|
95 |
nitpick [binary_ints, bits = 9, expect = genuine] |
|
96 |
oops |
|
97 |
||
48046
359bec38a4ee
temporarily comment out nitpick examples broken by changes to Int.thy
huffman
parents:
47109
diff
changeset
|
98 |
(* FIXME |
359bec38a4ee
temporarily comment out nitpick examples broken by changes to Int.thy
huffman
parents:
47109
diff
changeset
|
99 |
*** Invalid intermediate term ("Nitpick_Nut.the_name"): (ConstName Nitpick.sel0$Nitpick.Quot int \<Rightarrow> nat X). |
359bec38a4ee
temporarily comment out nitpick examples broken by changes to Int.thy
huffman
parents:
47109
diff
changeset
|
100 |
|
34126 | 101 |
lemma "nat (of_nat n) = n" |
102 |
nitpick [unary_ints, expect = none] |
|
103 |
nitpick [binary_ints, expect = none] |
|
104 |
sorry |
|
105 |
||
106 |
lemma "x + y \<ge> (x::int)" |
|
107 |
nitpick [unary_ints, expect = genuine] |
|
108 |
nitpick [binary_ints, expect = genuine] |
|
109 |
oops |
|
110 |
||
111 |
lemma "\<lbrakk>x \<ge> 0; y \<ge> 0\<rbrakk> \<Longrightarrow> x + y \<ge> (0::int)" |
|
112 |
nitpick [unary_ints, expect = none] |
|
113 |
nitpick [binary_ints, expect = none] |
|
114 |
sorry |
|
115 |
||
116 |
lemma "y \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)" |
|
117 |
nitpick [unary_ints, expect = none] |
|
118 |
nitpick [binary_ints, expect = none] |
|
119 |
sorry |
|
120 |
||
121 |
lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (y::int)" |
|
122 |
nitpick [unary_ints, expect = none] |
|
123 |
nitpick [binary_ints, expect = none] |
|
124 |
sorry |
|
125 |
||
126 |
lemma "x \<ge> 0 \<Longrightarrow> x + y \<ge> (x::int)" |
|
127 |
nitpick [unary_ints, expect = genuine] |
|
128 |
nitpick [binary_ints, expect = genuine] |
|
129 |
oops |
|
130 |
||
131 |
lemma "\<lbrakk>x \<le> 0; y \<le> 0\<rbrakk> \<Longrightarrow> x + y \<le> (0::int)" |
|
132 |
nitpick [unary_ints, expect = none] |
|
133 |
nitpick [binary_ints, expect = none] |
|
134 |
sorry |
|
135 |
||
136 |
lemma "y \<noteq> 0 \<Longrightarrow> x + y > (x::int)" |
|
137 |
nitpick [unary_ints, expect = genuine] |
|
138 |
nitpick [binary_ints, expect = genuine] |
|
139 |
oops |
|
140 |
||
141 |
lemma "x + y = y + (x::int)" |
|
142 |
nitpick [unary_ints, expect = none] |
|
143 |
nitpick [binary_ints, expect = none] |
|
144 |
sorry |
|
145 |
||
146 |
lemma "x > y \<Longrightarrow> x - y \<noteq> (0::int)" |
|
147 |
nitpick [unary_ints, expect = none] |
|
148 |
nitpick [binary_ints, expect = none] |
|
149 |
sorry |
|
150 |
||
151 |
lemma "x \<le> y \<Longrightarrow> x - y = (0::int)" |
|
152 |
nitpick [unary_ints, expect = genuine] |
|
153 |
nitpick [binary_ints, expect = genuine] |
|
154 |
oops |
|
155 |
||
156 |
lemma "x - (0::int) = x" |
|
157 |
nitpick [unary_ints, expect = none] |
|
158 |
nitpick [binary_ints, expect = none] |
|
159 |
sorry |
|
160 |
||
161 |
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<noteq> (0::int)" |
|
162 |
nitpick [unary_ints, expect = none] |
|
163 |
nitpick [binary_ints, expect = none] |
|
164 |
sorry |
|
165 |
||
166 |
lemma "0 * y = (0::int)" |
|
167 |
nitpick [unary_ints, expect = none] |
|
168 |
nitpick [binary_ints, expect = none] |
|
169 |
sorry |
|
170 |
||
171 |
lemma "y * 0 = (0::int)" |
|
172 |
nitpick [unary_ints, expect = none] |
|
173 |
nitpick [binary_ints, expect = none] |
|
174 |
sorry |
|
175 |
||
176 |
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (x::int)" |
|
177 |
nitpick [unary_ints, expect = genuine] |
|
178 |
nitpick [binary_ints, expect = genuine] |
|
179 |
oops |
|
180 |
||
181 |
lemma "\<lbrakk>x \<noteq> 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> x * y \<ge> (y::int)" |
|
182 |
nitpick [unary_ints, expect = genuine] |
|
183 |
nitpick [binary_ints, expect = genuine] |
|
184 |
oops |
|
185 |
||
186 |
lemma "x * y div y = (x::int)" |
|
187 |
nitpick [unary_ints, expect = genuine] |
|
188 |
nitpick [binary_ints, expect = genuine] |
|
189 |
oops |
|
190 |
||
191 |
lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)" |
|
192 |
nitpick [unary_ints, expect = none] |
|
42959 | 193 |
nitpick [binary_ints, card = 1\<emdash>4, bits = 1\<emdash>4, expect = none] |
34126 | 194 |
sorry |
195 |
||
196 |
lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))" |
|
197 |
nitpick [unary_ints, expect = none] |
|
198 |
nitpick [binary_ints, expect = none] |
|
199 |
sorry |
|
200 |
||
201 |
lemma "-5 * 55 > (-260::int)" |
|
202 |
nitpick [unary_ints, expect = none] |
|
203 |
nitpick [binary_ints, expect = none] |
|
204 |
nitpick [binary_ints, bits = 9, expect = genuine] |
|
205 |
oops |
|
206 |
||
207 |
lemma "nat (of_nat n) = n" |
|
208 |
nitpick [unary_ints, expect = none] |
|
209 |
nitpick [binary_ints, expect = none] |
|
210 |
sorry |
|
48046
359bec38a4ee
temporarily comment out nitpick examples broken by changes to Int.thy
huffman
parents:
47109
diff
changeset
|
211 |
*) |
34126 | 212 |
|
35695 | 213 |
datatype tree = Null | Node nat tree tree |
214 |
||
215 |
primrec labels where |
|
216 |
"labels Null = {}" | |
|
217 |
"labels (Node x t u) = {x} \<union> labels t \<union> labels u" |
|
218 |
||
219 |
lemma "labels (Node x t u) \<noteq> labels (Node y v w)" |
|
37477
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
35695
diff
changeset
|
220 |
nitpick [expect = potential] (* unfortunate *) |
35695 | 221 |
nitpick [dont_finitize, expect = potential] |
222 |
oops |
|
223 |
||
224 |
lemma "labels (Node x t u) \<noteq> {}" |
|
225 |
nitpick [expect = none] |
|
226 |
oops |
|
227 |
||
228 |
lemma "card (labels t) > 0" |
|
37477
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
35695
diff
changeset
|
229 |
nitpick [expect = potential] (* unfortunate *) |
35695 | 230 |
nitpick [dont_finitize, expect = potential] |
231 |
oops |
|
232 |
||
233 |
lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2" |
|
37477
e482320bcbfe
adjusted Nitpick examples to latest changes + make them slightly faster
blanchet
parents:
35695
diff
changeset
|
234 |
nitpick [expect = potential] (* unfortunate *) |
35695 | 235 |
nitpick [dont_finitize, expect = potential] |
236 |
oops |
|
237 |
||
238 |
lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2" |
|
39362
ee65900bfced
adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents:
38185
diff
changeset
|
239 |
nitpick [expect = potential] (* unfortunate *) |
ee65900bfced
adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents:
38185
diff
changeset
|
240 |
nitpick [dont_finitize, expect = potential] |
35695 | 241 |
sorry |
242 |
||
243 |
lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)" |
|
39362
ee65900bfced
adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents:
38185
diff
changeset
|
244 |
nitpick [expect = potential] (* unfortunate *) |
ee65900bfced
adapt examples to latest Nitpick changes + speed them up a little bit
blanchet
parents:
38185
diff
changeset
|
245 |
nitpick [dont_finitize, expect = potential] |
35695 | 246 |
oops |
247 |
||
34126 | 248 |
end |