equal
deleted
inserted
replaced
788 instance word :: (len0) comm_ring .. |
788 instance word :: (len0) comm_ring .. |
789 |
789 |
790 instance word :: (len) comm_semiring_1 |
790 instance word :: (len) comm_semiring_1 |
791 by (intro_classes) (simp add: lenw1_zero_neq_one) |
791 by (intro_classes) (simp add: lenw1_zero_neq_one) |
792 |
792 |
|
793 instance word :: (len) recpower .. |
|
794 |
793 instance word :: (len) comm_ring_1 .. |
795 instance word :: (len) comm_ring_1 .. |
794 |
796 |
795 instance word :: (len0) comm_semiring_0 .. |
797 instance word :: (len0) comm_semiring_0 .. |
796 |
798 |
797 instance word :: (len0) order .. |
799 instance word :: (len0) order .. |
798 |
|
799 instance word :: (len) recpower |
|
800 by (intro_classes) simp_all |
|
801 |
800 |
802 (* note that iszero_def is only for class comm_semiring_1_cancel, |
801 (* note that iszero_def is only for class comm_semiring_1_cancel, |
803 which requires word length >= 1, ie 'a :: len word *) |
802 which requires word length >= 1, ie 'a :: len word *) |
804 lemma zero_bintrunc: |
803 lemma zero_bintrunc: |
805 "iszero (number_of x :: 'a :: len word) = |
804 "iszero (number_of x :: 'a :: len word) = |