equal
deleted
inserted
replaced
561 quickcheck[exhaustive, expect = no_counterexample] |
561 quickcheck[exhaustive, expect = no_counterexample] |
562 oops |
562 oops |
563 |
563 |
564 declare [[quickcheck_full_support = true]] |
564 declare [[quickcheck_full_support = true]] |
565 |
565 |
|
566 |
|
567 subsection {* Equality Optimisation *} |
|
568 |
|
569 lemma |
|
570 "f x = y ==> y = (0 :: nat)" |
|
571 quickcheck |
|
572 oops |
|
573 |
|
574 lemma |
|
575 "y = f x ==> y = (0 :: nat)" |
|
576 quickcheck |
|
577 oops |
|
578 |
|
579 lemma |
|
580 "f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []" |
|
581 quickcheck |
|
582 oops |
|
583 |
|
584 lemma |
|
585 "f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []" |
|
586 quickcheck |
|
587 oops |
|
588 |
|
589 lemma |
|
590 "x = f x \<Longrightarrow> x = (0 :: nat)" |
|
591 quickcheck |
|
592 oops |
|
593 |
|
594 lemma |
|
595 "f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []" |
|
596 quickcheck |
|
597 oops |
|
598 |
|
599 lemma |
|
600 "m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v" |
|
601 quickcheck |
|
602 oops |
|
603 |
|
604 |
566 end |
605 end |