*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Maps*From*: Andrzej Mazurkiewicz <andrzej at mazurkiewicz.org>*Date*: Sat, 21 Feb 2009 16:33:25 +0100*User-agent*: KMail/1.10.3 (Linux/2.6.27.7-9-default; KDE/4.1.3; x86_64; ; )

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

**Follow-Ups**:**Re: [isabelle] Maps***From:*Tobias Nipkow

**Re: [isabelle] Maps***From:*Brian Huffman

- Previous by Date: Re: [isabelle] reasoning about classes of many-sorted structures
- Next by Date: Re: [isabelle] Isabelle and Computer Algebra (revisted) / Large Proof Goals
- Previous by Thread: Re: [isabelle] Some comments on CONST/\<^const> mechanism in 2008
- Next by Thread: Re: [isabelle] Maps
- Cl-isabelle-users February 2009 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