*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int*From*: Gottfried Barrow <igbi at gmx.com>*Date*: Thu, 13 Feb 2014 13:49:55 -0600*In-reply-to*: <52FCE141.9020005@in.tum.de>*References*: <52F68FD1.3060307@gmx.com> <52F695E2.7080602@gmx.com> <52F6CB1A.7060500@gmx.com> <52F7ACAC.6040100@gmx.com> <52F803E9.2010005@in.tum.de> <52FCE141.9020005@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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 choicebecause I fear you cannot prove that your type 'a loidN is again inlinordered_idom (usual problems with minus). Which I believe, youwould like to do.

Ondrej,

(1) one function,

(******************************************************************************)

(******************************************************************************) definition id_loid :: "'a::linordered_idom => 'a" where "id_loid x = x" (******************************************************************************)

(******************************************************************************) 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 *)

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

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 *) (******************************************************************************)

that linordered_semidom accomodates nat. I can't depend on a type error

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*) (******************************************************************************)

do things, because the magic kicks in many times. Am I making things too

(******************************************************************************)

"losd_to_loid x = Some x" (******************************************************************************) (*

context of the type class linordered_idom.

the difference between global and locale polymorhpic functions, and how the inference engine will interpret the sort of any type variable as broadly as

when a global function is used.

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 (*

variable "'a". The error(s) above occurred in typedef "loidNNeg" *) (*

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

*)

**References**:**[isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Gottfried Barrow

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

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

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

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Ondřej Kunčar

**Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int***From:*Ondřej Kunčar

- Previous by Date: Re: [isabelle] Bijection f: nat --> nat x nat
- Next by Date: Re: [isabelle] Name clashes in theory names
- Previous by Thread: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Next by Thread: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list