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.