[isabelle] Maps



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.