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.