# Re: [isabelle] Question about autoref

```Hi Giuliano,

you can iterate over the set of key-value pairs of a map, using
map_to_set. Find your modified example below.

Best,
Â Peter

definition test_spec :: "(nat â nat) â nat nres"
Â where "test_spec m â SPEC (Î n . n = (â x â (dom m) . the (m x)))"

definition test :: "(nat â nat) â nat nres"
Â where "test m â FOREACH (map_to_set m) (Î (k,v) r . RETURN (v+r)) 0"

lemma test_correct:
Â assumes "finite (dom m)" shows "test m â test_spec m"
Â using assms unfolding test_def test_spec_def
Â apply -
Â apply (refine_vcg FOREACH_rule[whereÂ
ÂÂÂÂÂÂÂÂÂÂI="Îit r . r = (â (k,v) â (map_to_set m - it) . v)"])
Â apply (auto simp add:it_step_insert_iff finite_map_to_set)
Â apply (rule sum.reindex_cong[where l="Îk. (k,the (m k))"])
Â apply (auto simp: map_to_set_def)
Â done

schematic_goal test_impl:
Â assumes [autoref_rules]: "(r,m)âânat_rel,nat_relâdflt_rm_rel"
Â shows "(RETURN ?c, test m) â ânat_relânres_rel"
Â unfolding test_def
Â (*supply [[autoref_trace_failed_id]] Â(*enable id-op tracing*) *)
Â apply (autoref_monadic(trace)) (* phase id_op fails *)
Â done
end

On Fr, 2016-11-11 at 19:10 -0500, Giuliano Losa wrote:
> Hello,
> I would like to use AFP/Collections, monadic refinement, and autoref
> to
> generate code that computes the sum of all values in a map, as
> follows:
>
> theory Scratch
> Â imports Main "\$AFP/Collections/Refine_Dflt"
> begin
>
> definition test_spec :: "(nat â nat) â nat nres"
> Â where "test_spec m â SPEC (Î n . n = (â x â (dom m) . the (m x)))"
>
> definition test :: "(nat â nat) â nat nres"
> Â where "test m â FOREACH (dom m) (Î x r . RETURN (the (m x)+r)) 0"
>
> lemma test_correct:
> Â assumes "finite (dom m)" shows "test m â test_spec m"
> Â using assms unfolding test_def test_spec_def
> Â apply -
> Â apply (refine_vcg FOREACH_rule[where I="Îit r . r = (â x â (dom m -
> it) . the (m x))"])
> Â done
>
> schematic_goal test_impl:
> Â assumes [autoref_rules]: "(r,m)âânat_rel,nat_relâdflt_rm_rel"
> Â shows "(RETURN ?c, test m) â ânat_relânres_rel"
> Â unfolding test_def
> Â apply (autoref_monadic(trace)) (* phase id_op fails *)
> Â oops
> end
>
> I did not find any map-interface operation that corresponds to dom,
> which probably explains why id_op fails. But, I do not see how to
> make
> it work otherwise. Can anybody suggest how I could do this (I am
> using
> Isabelle2016-1-RC2 and afp-devel)? Is iterating over a map with
> FOREACH
> not supported by autoref?
>
> Thanks,
> Giuliano
>

```

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