equal
deleted
inserted
replaced
523 |
523 |
524 lemma "P ()" |
524 lemma "P ()" |
525 refute [expect = genuine] |
525 refute [expect = genuine] |
526 oops |
526 oops |
527 |
527 |
528 lemma "unit_rec u x = u" |
|
529 refute [expect = none] |
|
530 by simp |
|
531 |
|
532 lemma "P (unit_rec u x)" |
|
533 refute [expect = genuine] |
|
534 oops |
|
535 |
|
536 lemma "P (case x of () \<Rightarrow> u)" |
528 lemma "P (case x of () \<Rightarrow> u)" |
537 refute [expect = genuine] |
529 refute [expect = genuine] |
538 oops |
530 oops |
539 |
531 |
540 text {* option *} |
532 text {* option *} |
595 |
587 |
596 lemma "P Pair" |
588 lemma "P Pair" |
597 refute [expect = genuine] |
589 refute [expect = genuine] |
598 oops |
590 oops |
599 |
591 |
600 lemma "prod_rec p (a, b) = p a b" |
|
601 refute [maxsize = 2, expect = none] |
|
602 by simp |
|
603 |
|
604 lemma "P (prod_rec p x)" |
|
605 refute [expect = genuine] |
|
606 oops |
|
607 |
|
608 lemma "P (case x of Pair a b \<Rightarrow> p a b)" |
592 lemma "P (case x of Pair a b \<Rightarrow> p a b)" |
609 refute [expect = genuine] |
593 refute [expect = genuine] |
610 oops |
594 oops |
611 |
595 |
612 text {* + *} |
596 text {* + *} |
626 lemma "P (Inr x)" |
610 lemma "P (Inr x)" |
627 refute [expect = genuine] |
611 refute [expect = genuine] |
628 oops |
612 oops |
629 |
613 |
630 lemma "P Inl" |
614 lemma "P Inl" |
631 refute [expect = genuine] |
|
632 oops |
|
633 |
|
634 lemma "sum_rec l r (Inl x) = l x" |
|
635 refute [maxsize = 3, expect = none] |
|
636 by simp |
|
637 |
|
638 lemma "sum_rec l r (Inr x) = r x" |
|
639 refute [maxsize = 3, expect = none] |
|
640 by simp |
|
641 |
|
642 lemma "P (sum_rec l r x)" |
|
643 refute [expect = genuine] |
615 refute [expect = genuine] |
644 oops |
616 oops |
645 |
617 |
646 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)" |
618 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)" |
647 refute [expect = genuine] |
619 refute [expect = genuine] |