Email Gateway (Aug 22 2022 at 14:38): Email Gateway (Aug 22 2022 at 14:38):From: Giuliano Losa <giuliano@losa.fr>
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
signature.asc
Email Gateway (Aug 22 2022 at 14:38):From: Peter Lammich <lammich@in.tum.de>
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
Last updated: Apr 25 2024 at 08:20 UTC