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

`I'm no expert on algebra, and the number of classes in Groups and Rings
``is dizzying, but I guess I would try to put these typedef
``positive/non-negative types lower down. I don't know any of the
``ramifications of these types, other than the operations need to be closed.
`

`typedef 'a ordered_ab_group_add_NN = "{x::'a::ordered_ab_group_add. x >=
``0}"
` by(auto)
typedef 'a ordered_ring_NN = "{x::'a::ordered_ring. x >= 0}"
by(auto)
typedef 'a linordered_idom_Pos = "{x::'a::linordered_idom. x > 0}"
proof-
have "1 : {x::'a. 0 < x}" by(auto) thus ?thesis by(blast) qed

`So I wanted to do a little test to see if `-(-1)` would be of these
``types, because experimenting with that might tell me if this is a loser
``idea. I couldn't do that without doing the required lifting.
`

`That's why I don't try to implement any this by myself right now. It's
``because when I look at something like `fset`, I see that a lot of work
``went into making it work.
`

`Also, if I was proving theorems about `x::nat` when it gets coerced to
```int`, I don't know if that's the same thing as proving theorems about
```(x::int) >= 0`. I would want to know if I was getting locked into
``something.
`

`But, a type for the positive and non-negative members of a group or ring
``could also be used in datatypes.
`
Regards,
GB

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