1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* A simple cookbook example how to eliminate choice in programs. *}
13 definition valuesum :: "('a, 'b :: ab_group_add) mapping \<Rightarrow> 'b" where
14 "valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
17 Not that instead of defining @{term valuesum} with choice, we define it
18 directly and derive a description involving choice afterwards:
22 assumes fin: "finite (dom (Mapping.lookup m))"
23 shows "valuesum m = (if Mapping.is_empty m then 0 else
24 let l = (SOME l. l \<in> Mapping.keys m) in the (Mapping.lookup m l) + valuesum (Mapping.delete l m))"
25 proof (cases "Mapping.is_empty m")
26 case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
29 then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def)
30 then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
31 the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
32 (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
33 proof (rule someI2_ex)
36 moreover assume "l \<in> dom (Mapping.lookup m)"
37 moreover obtain A where "A = dom (Mapping.lookup m) - {l}" by simp
38 ultimately have "dom (Mapping.lookup m) = insert l A" and "finite A" and "l \<notin> A" by auto
40 in the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
41 (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
44 then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
48 In the context of the else-branch we can show that the exact choice is
49 irrelvant; in practice, finding this point where choice becomes irrelevant is the
53 lemma valuesum_choice:
54 "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow>
55 the (Mapping.lookup M x) + valuesum (Mapping.delete x M) =
56 the (Mapping.lookup M y) + valuesum (Mapping.delete y M)"
57 by (simp add: valuesum_def keys_def setsum_diff)
60 Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
61 first, we formally insert the constructor @{term AList} and split the one equation into two,
62 where the second one provides the necessary context:
65 lemma valuesum_rec_AList:
66 shows [code]: "valuesum (AList []) = 0"
67 and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
68 the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
69 by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
72 As a side effect the precondition disappears (but note this has nothing to do with choice!).
73 The first equation deals with the uncritical empty case and can already be used for code generation.
75 Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
78 lemma valuesum_rec_exec [code]:
79 "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
80 the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
82 let ?M = "AList (x # xs)"
83 let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)"
84 let ?l2 = "fst (hd (x # xs))"
85 have "finite (Mapping.keys ?M)" by (simp add: keys_AList)
86 moreover have "?l1 \<in> Mapping.keys ?M"
87 by (rule someI) (auto simp add: keys_AList)
88 moreover have "?l2 \<in> Mapping.keys ?M"
89 by (simp add: keys_AList)
90 ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) =
91 the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)"
92 by (rule valuesum_choice)
93 then show ?thesis by (simp add: valuesum_rec_AList)
100 value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])"