727 |
727 |
728 subsection {* Integer numeral div/mod simprocs *} |
728 subsection {* Integer numeral div/mod simprocs *} |
729 |
729 |
730 notepad begin |
730 notepad begin |
731 have "(10::int) div 3 = 3" |
731 have "(10::int) div 3 = 3" |
732 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
732 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
733 have "(10::int) mod 3 = 1" |
733 have "(10::int) mod 3 = 1" |
734 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
734 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
735 have "(10::int) div -3 = -4" |
735 have "(10::int) div -3 = -4" |
736 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
736 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
737 have "(10::int) mod -3 = -2" |
737 have "(10::int) mod -3 = -2" |
738 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
738 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
739 have "(-10::int) div 3 = -4" |
739 have "(-10::int) div 3 = -4" |
740 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
740 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
741 have "(-10::int) mod 3 = 2" |
741 have "(-10::int) mod 3 = 2" |
742 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
742 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
743 have "(-10::int) div -3 = 3" |
743 have "(-10::int) div -3 = 3" |
744 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
744 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
745 have "(-10::int) mod -3 = -1" |
745 have "(-10::int) mod -3 = -1" |
746 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
746 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
747 have "(8452::int) mod 3 = 1" |
747 have "(8452::int) mod 3 = 1" |
748 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
748 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
749 have "(59485::int) div 434 = 137" |
749 have "(59485::int) div 434 = 137" |
750 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
750 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
751 have "(1000006::int) mod 10 = 6" |
751 have "(1000006::int) mod 10 = 6" |
752 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
752 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
753 have "10000000 div 2 = (5000000::int)" |
753 have "10000000 div 2 = (5000000::int)" |
754 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
754 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
755 have "10000001 mod 2 = (1::int)" |
755 have "10000001 mod 2 = (1::int)" |
756 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
756 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
757 have "10000055 div 32 = (312501::int)" |
757 have "10000055 div 32 = (312501::int)" |
758 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
758 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
759 have "10000055 mod 32 = (23::int)" |
759 have "10000055 mod 32 = (23::int)" |
760 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
760 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
761 have "100094 div 144 = (695::int)" |
761 have "100094 div 144 = (695::int)" |
762 by (tactic {* test @{context} [@{simproc binary_int_div}] *}) |
762 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
763 have "100094 mod 144 = (14::int)" |
763 have "100094 mod 144 = (14::int)" |
764 by (tactic {* test @{context} [@{simproc binary_int_mod}] *}) |
764 by (tactic {* test @{context} [@{simproc numeral_divmod}] *}) |
765 end |
765 end |
766 |
766 |
767 end |
767 end |