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


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}"

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)"
  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)"


[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.