268 |
268 |
269 |
269 |
270 subsection {* Examples with relations *} |
270 subsection {* Examples with relations *} |
271 |
271 |
272 lemma |
272 lemma |
273 "acyclic R ==> acyclic S ==> acyclic (R Un S)" |
273 "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)" |
274 (* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *) |
274 quickcheck[exhaustive, expect = counterexample] |
275 oops |
275 oops |
276 |
276 |
|
277 lemma |
|
278 "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)" |
|
279 quickcheck[exhaustive, expect = counterexample] |
|
280 oops |
|
281 |
|
282 (* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *) |
277 lemma |
283 lemma |
278 "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S" |
284 "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S" |
279 (* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *) |
285 (*quickcheck[exhaustive, expect = counterexample]*) |
280 oops |
286 oops |
|
287 |
|
288 lemma |
|
289 "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)" |
|
290 quickcheck[exhaustive, expect = counterexample] |
|
291 oops |
|
292 |
|
293 lemma |
|
294 "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)" |
|
295 quickcheck[exhaustive, expect = counterexample] |
|
296 oops |
|
297 |
|
298 lemma |
|
299 "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)" |
|
300 quickcheck[exhaustive, expect = counterexample] |
|
301 oops |
|
302 |
281 |
303 |
282 subsection {* Examples with the descriptive operator *} |
304 subsection {* Examples with the descriptive operator *} |
283 |
305 |
284 lemma |
306 lemma |
285 "(THE x. x = a) = b" |
307 "(THE x. x = a) = b" |