[isabelle-dev] proposal for new numeral representation
makarius at sketis.net
Fri Nov 25 16:56:14 CET 2011
On Thu, 24 Nov 2011, Brian Huffman wrote:
> 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 ; a patched version of
> the Isabelle hg repo is also available .
>  https://isabelle.in.tum.de/isanotes/index.php/Numerals
>  http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals
This looks generally quite good to me. The big initial change is not so
complicated for such a substantial reform after so many years. (In 1999
I've assisted Larry in doing the original version of numerals, but of
course I cannot claim any special expertise on the subject anymore.)
> 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"
Is there a conceptual point for neg_numeral, beyond concrete syntax
One could just use regular uminus, but then there will be an accidental
change in concrete syntax: -42 and - 42 would be the same, both with the
weaker priority of unary minus.
Some notes also about the wiki material:
> Named "bin" after the old binary type Int.bin, which merged with type
> "int" a few years ago. Other sensible choices for the type name would be
> "num" (as used in ex/Numeral.thy) or "pos" for "positive" numbers (as
> used in the Coq standard libraries). Perhaps "pos" would make the most
> sense if we decide to support this as a user-visible abstract semiring
> type. The type name "num" has an unfortunate clash with the global
> grammar terminal of the same name, which causes the type name "num" to
> be always printed with a qualifier.
I was at first confused about "pos", since it is a concrete datatype.
But here it really seems to be an isomorphic copy of positive natural
numbers, without the former redundancy of leading 0s.
You can also have "num", since the one in Pure is hardly ever used as
such, only the derived form "num_const". We already have "float_token"
vs. "fload_const", so it would make sense to rename Pure "num" to
"num_token" to get it out of the way.
BTW, there are some other "num" types defined in some user theories, but
that should not be a decisive point.
> The numeral "2" always means "1 + 1", "3" always means "1 + 1 + 1", etc.
> Because there is a single, fixed definition for the meaning of numerals,
> we can now prove theorems like "1 + 2 = 3" without needing any
> additional type annotations.
Great! No longer this odd problem that the system cannot even prove
"1 + 1 = 2" due to unexpectedly general types.
> Broken proof methods
> some uses in Library/Sum_of_Squares.thy
BTW the regular "sos" method with the server communication is broken for
some months already. It would be nice if someone could volunteer to
recover this nice student project of Philipp Meyer.
More information about the isabelle-dev