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



On 2/13/2014 9:14 AM, Ondřej Kunčar wrote:
Just a side note: I am not sure if linordered_idom is the best choice because I fear you cannot prove that your type 'a loidN is again in linordered_idom (usual problems with minus). Which I believe, you would like to do.

Ondrej,

Thanks a lot. I'll have to wait for summertime. Fortunately, it took you, like, two days, instead of one. Otherwise, I might not have learned about Lifting_Option.thy, and using it as a template for the lifting setup I did.

I can get confused by the complexities of type classes, coercion, and the many algebra type classes, but the context is a generalization of this:

(1) one function,
(2) the type variable sort must have the properties of int (linordered_idom), (3) but the function must work with nat, even though nat does not have the required properties of linordered_idom.

The short story, according to what I currently understand, is that coercion is the magic for there to be that one function, and auto coercion is the magic to make it notationally convenient.

There's more I don't know than do know, but I worked up the example below to show what I think I know, about what I think I want. Thanks again for the magic. --GB.

(******************************************************************************)
(* id_loid: It must work with nat and int, and generalizations of nat and int.*)
(******************************************************************************)

definition id_loid :: "'a::linordered_idom => 'a" where
  "id_loid x = x"

(******************************************************************************)
(* Works with nat, int, and linordered_idom, but not with linordered_semidom.*)
(******************************************************************************)

value "id_loid (x::int)" (*x::int*)
value "id_loid (x::nat)" (*coerced to int*)
value "id_loid (x::'a::linordered_idom)" (*x::'a::linordered_idom*)
term "id_loid (x::'a::linordered_semidom)"
(*
ERROR: Type unification failed: Variable 'a::linordered_semidom not of sort
linordered_idom
*)

(******************************************************************************) (* As nat is to int, loidNNeg is to linordered_idom. Coercion is the magic.*)
(******************************************************************************)

typedef 'a loidNNeg = "{x::'a::linordered_idom. x >= 0}"
  by(auto)

term "id_loid (Rep_loidNNeg(x::'a::linordered_idom loidNNeg))"
value "id_loid (Rep_loidNNeg(x::'a::linordered_idom loidNNeg))"

(******************************************************************************)
(*My subtype is supposed to model the natural numbers, so I try to narrow down the sort of the type class variable to linordered_semidom, and then use it
 in the function id_loid, but it doesn't work.*)
(******************************************************************************)

typedef 'a losdNNeg = "{x::'a::linordered_semidom. x >= 0}"
  by(auto)

term "id_loid (Rep_losdNNeg(x::'a::linordered_semidom losdNNeg))"
(*
ERROR: Type unification failed: Variable 'a::linordered_semidom not of sort
linordered_idom
*)

(******************************************************************************)
(*It didn't work, so whatever I'm confused about, it's not that. I want to check
that linordered_semidom accomodates nat. I can't depend on a type error
to know when I've exceed the properties of nat, because it will get coerced to int when I do. I have to look at the output panel to see if it got coerced with
value.

It looks like linordered_semidom may be the maximum properties.*)
(******************************************************************************)

definition id_losr :: "'a::linordered_semidom => 'a" where
  "id_losr x = x"

term "id_losr (x::nat)" (*x::nat*)
value "id_losr (x::nat)" (*x::nat*)

(******************************************************************************)
(*Well, okay, I don't let the lack of knowledge keep me from blindly trying to
do things, because the magic kicks in many times. Am I making things too
complex? I don't know. If I start with linordered_semidom, there has to be some kind of coercion function, but I can't use the same x on both sides, as below.*)
(******************************************************************************)

definition losd_to_loid :: "'a::linordered_semidom => 'b::linordered_idom option" where
  "losd_to_loid x = Some x"

(******************************************************************************)
(*
The thing for me to pursue is whether I can define any of these typedefs in the
context of the type class linordered_idom.

Thanks to explanations by Andreas Lochbihler about locales, I was sorting out
the difference between global and locale polymorhpic functions, and how the
inference engine will interpret the sort of any type variable as broadly as
possible. That can result in a 'b variable appearing in a type class context,
when a global function is used.

Yes, there are many thing to confuse a Pure novice, and a HOL novice, too. But
error messages can be educational, such as that a type class variable name
must be 'a, which is related to the fact that type classes can only have one
type variable, and related to what I said in the last paragraph.

class tester =
  fixes tester :: 'b
Error: No type variable other than 'a allowed in class specification
*)
(******************************************************************************)
(*
Now, I try to define the typedef in a linordered_idom context.
*)
context linordered_idom
begin
typedef 'a loidNNeg = "{x::'a::linordered_idom. x >= 0}"
end
(*
ERROR: Sort constraint linordered_idom inconsistent with default type for type
variable "'a". The error(s) above occurred in typedef "loidNNeg"
*)
(*
The Wizard is talking to me. What is the Wizard saying? I suppose he's saying something similar to what Andreas Lochbihler was trying to tell me months ago.
That the linordered_idom type variable sort has been specified broadly, as
'a::type, and here I am trying to put restrictions on it.

There is value in being able to experiment with software, except when the
software is running on the primary server of a large, worldwide corporation.
*)





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