Email Gateway (Aug 18 2022 at 13:02): Email Gateway (Aug 18 2022 at 13:02):From: Andrzej Mazurkiewicz <andrzej@mazurkiewicz.org>
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
primrec
"RangeSum (empty::(nat ~=> preal)) = 0"
That has returned
*** Primrec definition error:
*** ill-formed constructor
*** in
*** "RangeSum empty = (0::real)"
*** At command "primrec".
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
Email Gateway (Aug 18 2022 at 13:02):From: Tobias Nipkow <nipkow@in.tum.de>
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:
Email Gateway (Aug 18 2022 at 13:02):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Andrzej Mazurkiewicz <andrzej@mazurkiewicz.org>:
As Tobias pointed out, you can't use primrec on type "'a ~=> 'b"
because it is not a datatype. If you want to calculate the sum of the
values in a map, here's an approach that works: First convert the map
to a set; then use "setsum" (which uses the "SUM _ : _. _" syntax) to
compute the sum.
definition assocs :: "('a ~=> 'b) => ('a * 'b) set"
where "assocs m = {(x, y). m x = Some y}"
definition "RangeSum m = (SUM (x,y) : assocs m. y)"
lemma assocs_empty: "assocs empty = {}"
unfolding assocs_def by simp
lemma assocs_upd: "assocs (m(a |-> b)) = insert (a, b) {x : assocs m.
fst x ~= a}"
unfolding assocs_def by (auto split: if_splits)
lemma "RangeSum (map_of [(x, 1)]) = 1"
unfolding RangeSum_def by (simp add: assocs_upd assocs_empty)
Hope this helps,
Last updated: May 03 2024 at 12:27 UTC