Re: [isabelle] Maps -Tanks for help



Many thanks to Tobias  Nipkow and Brian Huffman for help.
Regards
Andrzej Mazurkiewicz

Sunday 22 of February 2009 17:27:30 Brian Huffman napisał(a):
> 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.