Re: [isabelle] Modular arithmetic theory?





On Thu, 10 Nov 2005 nipkow at in.tum.de wrote:

Presburger arithmetic (which is also
tried) deals with "mod n" where n is a numeral - but it appears far too slow
on these problems.

The presburger method is not even tried on this goal (at least on my computer). Before the core procedure (written purely for integers) is called, rewriting rules (or conversions) are applied in order to transform Problems on nat into problems on int. Afterwards several conversions have to be performed to get rid of mod and div (the procedure deals with dvd over integers) and max min etc... This rewriting step gets stuck because the terms are too large. Every mod or div results into 4 universal quantifiers (nested into the formula). To get an intuition how big the terms are i apapended the result of the first rewriting step that gets rid of mod and div. The other 3 rwriting steps does not even succed to take place (on my machine). PolyML crashes. I even added a simplification rule to make this theorem smaller. The approach of dealing with linear arithmetic on nat using the one written for int shows his disadvantages at this example very demonstratively.

Cheers,
Amine.



val tmp_thm =
   "ALL m.
         4294967296 = 0 &
         (ALL n.
             4294967296 = 0 &
             (4294967296 = 0 &
              (4294967296 = 0 & n - 0 + (m - 0) - 0 = m + n - 0 |
               (EX q.
(4294967296 * q <= m + n & m + n < 4294967296 * (q + 1)) &
                   n - 0 + (m - 0) - 0 = m + n - q * 4294967296)) |
              (EX q.
                  (4294967296 * q <= n - 0 + (m - 0) &
                   n - 0 + (m - 0) < 4294967296 * (q + 1)) &
                  (4294967296 = 0 &
                   n - 0 + (m - 0) - q * 4294967296 = m + n - 0 |
                   (EX qa.
                       (4294967296 * qa <= m + n &
                        m + n < 4294967296 * (qa + 1)) &
                       n - 0 + (m - 0) - q * 4294967296 =
                       m + n - qa * 4294967296)))) |
             (EX q.
                 (4294967296 * q <= n & n < 4294967296 * (q + 1)) &
                 (4294967296 = 0 &
                  (4294967296 = 0 &
                   n - q * 4294967296 + (m - 0) - 0 = m + n - 0 |
                   (EX qa.
                       (4294967296 * qa <= m + n &
                        m + n < 4294967296 * (qa + 1)) &
                       n - q * 4294967296 + (m - 0) - 0 =
                       m + n - qa * 4294967296)) |
                  (EX qa.
                      (4294967296 * qa <= n - q * 4294967296 + (m - 0) &
                       n - q * 4294967296 + (m - 0)
                       < 4294967296 * (qa + 1)) &
                      (4294967296 = 0 &
                       n - q * 4294967296 + (m - 0) - qa * 4294967296 =
                       m + n - 0 |
                       (EX qb.
                           (4294967296 * qb <= m + n &
                            m + n < 4294967296 * (qb + 1)) &
n - q * 4294967296 + (m - 0) - qa * 4294967296 =
                           m + n - qb * 4294967296)))))) |
         (EX q.
             (4294967296 * q <= m & m < 4294967296 * (q + 1)) &
             (ALL n.
                 4294967296 = 0 &
                 (4294967296 = 0 &
                  (4294967296 = 0 &
                   n - 0 + (m - q * 4294967296) - 0 = m + n - 0 |
                   (EX qa.
                       (4294967296 * qa <= m + n &
                        m + n < 4294967296 * (qa + 1)) &
                       n - 0 + (m - q * 4294967296) - 0 =
                       m + n - qa * 4294967296)) |
                  (EX qa.
                      (4294967296 * qa <= n - 0 + (m - q * 4294967296) &
                       n - 0 + (m - q * 4294967296)
                       < 4294967296 * (qa + 1)) &
                      (4294967296 = 0 &
                       n - 0 + (m - q * 4294967296) - qa * 4294967296 =
                       m + n - 0 |
                       (EX qb.
                           (4294967296 * qb <= m + n &
                            m + n < 4294967296 * (qb + 1)) &
n - 0 + (m - q * 4294967296) - qa * 4294967296 =
                           m + n - qb * 4294967296)))) |
                 (EX qa.
                     (4294967296 * qa <= n & n < 4294967296 * (qa + 1)) &
                     (4294967296 = 0 &
                      (4294967296 = 0 &
                       n - qa * 4294967296 + (m - q * 4294967296) - 0 =
                       m + n - 0 |
                       (EX qb.
                           (4294967296 * qb <= m + n &
                            m + n < 4294967296 * (qb + 1)) &
n - qa * 4294967296 + (m - q * 4294967296) - 0 =
                           m + n - qb * 4294967296)) |
                      (EX qb.
                          (4294967296 * qb
                           <= n - qa * 4294967296 + (m - q * 4294967296) &
                           n - qa * 4294967296 + (m - q * 4294967296)
                           < 4294967296 * (qb + 1)) &
                          (4294967296 = 0 &
                           n - qa * 4294967296 + (m - q * 4294967296) -
                           qb * 4294967296 = m + n - 0 |
                           (EX qc.
                               (4294967296 * qc <= m + n &
                                m + n < 4294967296 * (qc + 1)) &
n - qa * 4294967296 + (m - q * 4294967296) -
                               qb * 4294967296 =
                               m + n - qc * 4294967296)))))))
      ==> ALL m n.
         (n mod 4294967296 + m mod 4294967296) mod 4294967296 =
         (m + n) mod 4294967296" : Thm.thm





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.