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))"])
> ÂÂÂÂapply (auto simp add:it_step_insert_iff)
> Â 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.