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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
