equal
deleted
inserted
replaced
391 quickcheck[exhaustive, expect = counterexample] |
391 quickcheck[exhaustive, expect = counterexample] |
392 oops |
392 oops |
393 |
393 |
394 subsubsection {* floor and ceiling functions *} |
394 subsubsection {* floor and ceiling functions *} |
395 |
395 |
396 lemma |
396 lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: rat\<rfloor>" |
397 "floor x + floor y = floor (x + y :: rat)" |
|
398 quickcheck[expect = counterexample] |
397 quickcheck[expect = counterexample] |
399 oops |
398 oops |
400 |
399 |
401 lemma |
400 lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: real\<rfloor>" |
402 "floor x + floor y = floor (x + y :: real)" |
|
403 quickcheck[expect = counterexample] |
401 quickcheck[expect = counterexample] |
404 oops |
402 oops |
405 |
403 |
406 lemma |
404 lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: rat\<rceil>" |
407 "ceiling x + ceiling y = ceiling (x + y :: rat)" |
|
408 quickcheck[expect = counterexample] |
405 quickcheck[expect = counterexample] |
409 oops |
406 oops |
410 |
407 |
411 lemma |
408 lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: real\<rceil>" |
412 "ceiling x + ceiling y = ceiling (x + y :: real)" |
|
413 quickcheck[expect = counterexample] |
409 quickcheck[expect = counterexample] |
414 oops |
410 oops |
415 |
411 |
416 subsection {* Examples with abstract types *} |
412 subsection {* Examples with abstract types *} |
417 |
413 |