*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Question about autoref*From*: Giuliano Losa <giuliano at losa.fr>*Date*: Fri, 11 Nov 2016 19:10:30 -0500*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Icedove/45.4.0

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

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Question about autoref***From:*Peter Lammich

- Previous by Date: Re: [isabelle] AFP submission + Jenkins maintenance
- Next by Date: Re: [isabelle] Question about autoref
- Previous by Thread: [isabelle] New in the AFP: Deep Learning
- Next by Thread: Re: [isabelle] Question about autoref
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list