Add some simple test for bitArithLib and document in next-release.md

doc/next-release.md

@@ -63,6 +63,15 @@ New theories:
 New tools:
 ----------
 
+- **improvements of multiplications of large numbers**:
+
+    In `src/real` there is a new library `bitArithLib.sml` which improves the
+    performance of large multiplications for the types `:num` and `:real`.
+    The library uses arithmetic of bitstrings in combination with the Karatsuba
+    multiplication algorithm.
+    To use the library, it has to be loaded before the functions that should be
+    evaluated are **defined**.
+
 New examples:
 -------------
 

src/real/selftest.sml

@@ -1,6 +1,6 @@
 open HolKernel Parse bossLib boolLib;
 
-open simpLib realSimps isqrtLib RealArith RealField;
+open simpLib realSimps isqrtLib RealArith RealField bitArithLib;
 
 open testutils;
 
@@ -380,4 +380,26 @@ val _ = require_msg (check_result (aconv expected2)) term_to_string
                     (quietly Parse.Term) ‘0 < x’
 val _ = temp_set_grammars grammars
 
+(* tests for bitArithLib *)
+val _ = convtest("Testing karatsuba_conv on ``1 * 2``",
+                  karatsuba_conv,
+                 ``1 * (2:num)``,
+                 ``2:num``)
+
+val _ = convtest("Testing karatsuba_conv on ``64 * 128``",
+                  karatsuba_conv,
+                 ``64 * (128:num)``,
+                 ``8192:num``)
+
+val _ = convtest("Testing karatsuba_conv on ``1 * 2``",
+                  real_mul_conv,
+                 ``1 * (2:real)``,
+                 ``2:real``)
+
+val _ = convtest("Testing real_mul_conv on ``64 * 128``",
+                  real_mul_conv,
+                 ``64 * (128:real)``,
+                 ``8192:real``)
+
+
 val _ = Process.exit Process.success