Hi all, I have been working on a new numeral representation for Isabelle recently, and I would like to share it with everyone. An overview of the design is now available on the Isanotes wiki [1]; a patched version of the Isabelle hg repo is also available [2].
[1] https://isabelle.in.tum.de/isanotes/index.php/Numerals [2] http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals The design is based on the one in HOL/ex/Numeral.thy by Florian Haftmann. The main definitions are as follows: datatype bin = One | Bit0 bin | Bit1 bin class numeral = semigroup_add + one primrec (in numeral) numeral :: "bin => 'a" where "numeral One = 1" | "numeral (Bit0 k) = numeral k + numeral k" | "numeral (Bit1 k) = numeral k + numeral k + 1" class neg_numeral = group_add + one definition (in neg_numeral) neg_numeral :: "bin => 'a" where "neg_numeral k = - numeral k" Some of the advantages of the design: * No more number_ring class; numerals are available on any ring type. * Nonsense like "10^-3" is not allowed; using negative numerals on type nat causes a type error. * Arithmetic simp rules on type nat are *much* simpler. * Arithmetic rules are easier to configure for other semirings, like extended nat. * It is no longer ever necessary to use "1+1" in place of "2". Adapting theories to work with the new numerals is usually not a problem: Of all the AFP entries I tested, all but three worked without modification. Two required small one-line changes; only RSAPSS (which has several theorems that explicitly depend on the numeral representation) will need deeper changes. I would welcome any suggestions, criticism, or other feedback. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
