# [isabelle] Want a type of non-negatives for a field, to work like nat/int

Hi,

`I did some searching, but when I saw, starting at 'Ordered fields' of
``[Fields.thy,471] (link below), that the condition "0 < a" is having to
``be used a lot, I figured there doesn't exist the type that I describe
``below. (I did a search on positive in the HOL/HOL/document.pdf. I didn't
``find a type as I describe.)
`

`It'll probably be years before I get to work with rationals and reals,
``so if I ask for this now, it might be there when I want it, if it
``doesn't already exist.
`

`As a first choice, I show what I think I want, which is the typedef
``shown. It's the non-negative members, where the second choice of what I
``want is the type class. Further down, I show a more general version, but
``I don't think I want that.
`
typedef 'a lord_fieldNN = "{x::'a::linordered_field. x >= 0}"
by(auto)
class lord_fieldNN = linordered_field +
fixes NNeg :: "'a set"
assumes nonnegative: "NNeg = {x. x >= 0}"

`My request here is based on how easy `nat` works with `int`, that is, I
``can use `nat` where type `'a::linordered_idom` is specified, even though
```nat` doesn't meets the requirement of `linordered_idom`.
`
From here, I do more explaining, which may or may not be needed.

`I give a simple example. The scenario is where the main application is
``going to use `nat` exponents, but I go ahead and set things up to where
``I can use `int` exponents. This kind of scenario is very common. Your
``number system is the rational or real numbers, but you need to prove a
``lot of things about the non-negative rational or real numbers.
`

`This next source shows I can set up my function for types
```linordered_idom` and `int`, and then only have to use a type annotation
``of `nat` to prove things about non-negative values.
`
definition intPow :: "'a::linordered_idom => int => 'a * 'a" where
"intPow x z = (if (z < 0) then (1, x ^ nat(-z)) else (x ^ nat z, 1))"
theorem "intPow (x::nat) (z::nat) = (x ^ z, 1::nat)"
(*constants:
int :: nat => int
intPow :: int => int => int * int *)
by(unfold intPow_def, simp)

`That's the standard for how easy I want it to be, when working with
``non-negative rationals or reals, where the domain is the rational or reals.
`

`From reading and a little experience, I normally try to stay away from
```typedef`, but here it seems applicable. The main use of `typedef` seems
``to create big, important types, such as `prod` or `fset`. The type of
``non-negative members seems big enough to qualify.
`

`But, I don't know how much work it would take to get `lord_fieldNN` as a
```typedef` working right. Out of several other ways to work with the
``non-negative rational and reals, right now, I'm thinking that the
```lord_fieldNN` type class above would be the best alternative to using
```typedef`. However, anything less than a type is always going to require
``doing something like `x \<in> NNeg ==> Q`.
`

`In a typical real analysis book, such as [Bartle,pg.26], the author will
``define a subset P of R that's closed under addition and multiplication,
``and has the trichotomy property, and then use that to define the order
``relation. Doing it that way would allow defining the non-negative values
``for the type class `field`, but there probably wouldn't be any use in
``doing that, since it's just defining `P` to get `<`, rather than getting
```P` from defining `<`.
`
class lord_fieldNN_2 = field +
fixes NNeg :: "'a set"
assumes plusClosed: "x + y : NNeg"
assumes timesClosed: "x * y : NNeg"

` assumes trichotomy: "x = 0 | x : NNeg | -x : NNeg" (*Needs an
``exclusive or.*)
`

`If using a type class was somehow beneficial, I could go with everything
``like this, which might be overkill:
`
class lord_fieldALL = linordered_field +
fixes Pos :: "'a set"
fixes Neg :: "'a set"
fixes NNeg :: "'a set"
fixes NPos :: "'a set"
assumes Pos: "Pos = {x. x > 0}"
assumes Neg: "Neg = {x. x < 0}"
assumes NNeg: "NNeg = {x. x >= 0}"
assumes NPos: "NPos = {x. x <= 0}"
fixes is_Pos :: "'a => bool"
fixes is_Neg :: "'a => bool"
fixes is_NNeg :: "'a => bool"
fixes is_NPos :: "'a => bool"
assumes is_Pos: "is_Pos x = (x : Pos)"
assumes is_Neg: "is_Neg x = (x : Neg)"
assumes is_NNeg: "is_Neg x = (x : NNeg)"
assumes is_NPos: "is_Pos x = (x : NPos)"
Regards,
GB

`[Fields.thy,471]
``http://isabelle.in.tum.de/repos/isabelle/file/4dd08fe126ba/src/HOL/Fields.thy#l471
``[Bartle,pg.26]
``http://www.amazon.com/Introduction-Real-Analysis-3rd-Edition/dp/0471321486
`

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