Email Gateway (Aug 19 2022 at 16:17): Email Gateway (Aug 19 2022 at 16:17):From: "W. Douglas Maurer" <maurer@gwu.edu>
Why are the divide_minus1, minus1_divide, and divide_Numeral1 lemmas
in theory Int? These apply only to x in a field; but the integers are
not a field.
Email Gateway (Aug 19 2022 at 16:18):From: Brian Huffman <huffman.brian.c@gmail.com>
They are there for historical reasons: Previously numeral notation
like "-1" was defined in terms of operations on type "int", so Int.thy
was the earliest place where those lemmas could even be stated. In the
bootstrapping order, the general theory of fields in Fields.thy occurs
before the development of types like "nat" and "int".
Since the most recent renovation of numeral notation, "-1" is just
"uminus" applied to "1", so it should be possible to move those
theorems to Fields.thy.
Last updated: Apr 20 2024 at 01:05 UTC