# Re: [isabelle] Field lemmas in theory Int

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.
- Brian
On Wed, Oct 1, 2014 at 4:47 PM, W. Douglas Maurer <maurer at gwu.edu> wrote:
> 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.
> --
> Prof. W. Douglas Maurer Washington, DC 20052, USA
> Department of Computer Science Tel. (1-202)994-5921
> The George Washington University Fax (1-202)994-4875
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*