summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Simproc_Tests.thy

changeset 45530 | 0c4853bb77bf |

parent 45464 | 5a5a6e6c6789 |

child 46240 | 933f35c4e126 |

--- a/src/HOL/ex/Simproc_Tests.thy Wed Nov 16 13:58:31 2011 +0100 +++ b/src/HOL/ex/Simproc_Tests.thy Wed Nov 16 15:20:27 2011 +0100 @@ -420,9 +420,11 @@ assume "4*k = u" have "k + 3*k = u" by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact next + (* FIXME "Suc (i + 3) \<equiv> i + 4" *) assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact next + (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *) assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact next @@ -712,4 +714,43 @@ } end +subsection {* Integer numeral div/mod simprocs *} + +notepad begin + have "(10::int) div 3 = 3" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(10::int) mod 3 = 1" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(10::int) div -3 = -4" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(10::int) mod -3 = -2" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(-10::int) div 3 = -4" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(-10::int) mod 3 = 2" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(-10::int) div -3 = 3" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(-10::int) mod -3 = -1" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(8452::int) mod 3 = 1" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(59485::int) div 434 = 137" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(1000006::int) mod 10 = 6" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "10000000 div 2 = (5000000::int)" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "10000001 mod 2 = (1::int)" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "10000055 div 32 = (312501::int)" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "10000055 mod 32 = (23::int)" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "100094 div 144 = (695::int)" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "100094 mod 144 = (14::int)" + by (tactic {* test [@{simproc binary_int_mod}] *}) end + +end