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.