# Re: [isabelle] Maps

Quoting Andrzej Mazurkiewicz <andrzej at 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.

`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,
- Brian

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