204 lemma "nat (of_nat n) = n" |
204 lemma "nat (of_nat n) = n" |
205 nitpick [unary_ints, expect = none] |
205 nitpick [unary_ints, expect = none] |
206 nitpick [binary_ints, expect = none] |
206 nitpick [binary_ints, expect = none] |
207 sorry |
207 sorry |
208 |
208 |
|
209 datatype tree = Null | Node nat tree tree |
|
210 |
|
211 primrec labels where |
|
212 "labels Null = {}" | |
|
213 "labels (Node x t u) = {x} \<union> labels t \<union> labels u" |
|
214 |
|
215 lemma "labels (Node x t u) \<noteq> labels (Node y v w)" |
|
216 nitpick [expect = genuine] |
|
217 nitpick [dont_finitize, expect = potential] |
|
218 oops |
|
219 |
|
220 lemma "labels (Node x t u) \<noteq> {}" |
|
221 nitpick [expect = none] |
|
222 oops |
|
223 |
|
224 lemma "card (labels t) > 0" |
|
225 nitpick [expect = genuine] |
|
226 nitpick [dont_finitize, expect = potential] |
|
227 oops |
|
228 |
|
229 lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2" |
|
230 nitpick [expect = genuine] |
|
231 nitpick [dont_finitize, expect = potential] |
|
232 oops |
|
233 |
|
234 lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2" |
|
235 nitpick [expect = none] |
|
236 nitpick [dont_finitize, expect = none] |
|
237 sorry |
|
238 |
|
239 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)" |
|
240 nitpick [expect = genuine] |
|
241 nitpick [dont_finitize, expect = none] |
|
242 oops |
|
243 |
209 end |
244 end |