Re: [isabelle] Maps



Primrec only works for types defined via *datatype*, eg lists. But not
maps. And just like in functional programming, pattern matching in
primrec expects datatype constructors, not arbitrary functions like map_of.

Be warned against using preal - it is an auxiliary type for internal
purposes and you cannot do much with it. Use real.

Tobias

Andrzej Mazurkiewicz schrieb:
> Hello everybody.
> 
> I am a beginner in Isabelle/HOL and I have the following problems.
> 
> The final goal is the following.
> I would like to define a subtype of a "nat ~=> preal" map, with constraints 
> that sum of all preal values should be equal 1.
> 
> Since Isabelle/HOL has brutally simplified my complex plan I have decided to 
> start with something simpler, i. e. with a function RangeSum that would 
> provide a sum of the preal values of the map.
> 
> ========= the file ==============
> theory FarmUserModel
> imports Main PReal RealDef Map
> begin
> 
> consts RangeSum :: "(nat ~=> preal)  => real"
> 
> term "empty::(nat ~=> preal)"
> 
> term   "map_of [(a::nat,b::preal)]"
> 
> =============================
> 
> term "empty::(nat ~=> preal)"
> returns
> "empty"
>   :: "nat ~=> preal"
> 
> ------------
> 
> term   "map_of [(a::nat,b::preal)]"
> returns
> "map_of [(a::nat, b::preal)]"
>   :: "nat ~=> preal"
> 
> ==============================
> I have tried to begin with primrec in two variants
> 
> 1. Defining that RangeSum of an empty map equals zero.
> ---------------------------------
> primrec
>    "RangeSum (empty::(nat ~=> preal)) = 0"
> ---------------------------------
> That has returned
> *** Primrec definition error:
> *** ill-formed constructor
> *** in
> *** "RangeSum empty = (0::real)"
> *** At command "primrec".
> 
> 2. Defining that RangeSum of the map consisting of a single element, for 
> example (3 -> 0.5) returns 0.5
> ---------------------------------
> primrec
>   "RangeSum (map_of [(a::nat,b::preal)]) = real b"
> ---------------------------------
> That has returned
> *** Primrec definition error:
> *** illegal argument in pattern
> *** in
> *** "RangeSum (map_of [(a::nat, b::preal)]) = real b"
> *** At command "primrec".
> ---------------------------------
> I do not know why the above errors has been generated although arguments seem 
> to be OK (for me at least).
> 
> I need some help I am afraid.
> 
> Thanks in advance.
> Regards
> Andrzej Mazurkiewicz





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