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