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.