[isabelle-dev] proposal for new numeral representation

[Makarius]

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 [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

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 
issues?

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
>
> sos_cert
>   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.


 	Makarius