[isabelle] Question about autoref



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
Description: OpenPGP digital signature



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