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

`(*NOTE: The "exception TYPE raised" error shown below might be of
``interest to someone.)
`

`The value of trying to get fancy can be the tangents. The
```setup_lifting` command works if `typedef` uses type `rat`, but not if
```typedef` uses `'a::linordered_idom`. It has nothing specifically to do
``with `linordered_idom`. A test case I made using `'a::finite` does the
``same thing.
`
So with a typedef based on `rat`, I can start down the lifting road:
typedef ratN = "{x::rat. x >= 0}"
by(auto)
declare [[coercion Rep_ratN]]
setup_lifting type_definition_ratN
instantiation ratN :: zero
begin
lift_definition zero_ratN :: ratN is "0::rat" ..
instance ..
end
theorem "(0::ratN) + x = (x::rat)"
by(transfer, simp)

`But, if I want to use `'a::linordered_idom`, I have to do it the
``non-lifting, definitional way, because of the "exception TYPE raised"
``error shown below:
`
typedef 'a loidN = "{x::('a::linordered_idom). x >= 0}"
by(auto)
declare Abs_loidN_inverse [simp add]
setup_lifting type_definition_loidN
(*
exception TYPE raised (line 246 of "term.ML"):
dest_Type
'f::linordered_idom
*)
instantiation loidN :: (linordered_idom) zero
begin
definition zero_loidN :: "'a loidN" where
"0 = Abs_loidN 0"
declare zero_loidN_def [simp add]
instance ..
end
theorem "Rep_loidN(0::'a loidN) + x = (x::'a::linordered_idom)"
by(simp)
Regards,
GB

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