a draft for an example how to turn specifications involving choice executable

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Execute_Choice.thy	Wed Feb 17 09:48:53 2010 +0100
@@ -0,0 +1,64 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A simple cookbook example how to eliminate choice in programs. *}
+
+theory Execute_Choice
+imports Main AssocList
+begin
+
+definition valuesum :: "('a, 'b :: comm_monoid_add) mapping \<Rightarrow> 'b" where
+  "valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
+
+lemma valuesum_rec:
+  assumes fin: "finite (dom (Mapping.lookup m))"
+  shows "valuesum m = (if Mapping.is_empty m then 0 else
+    let l = (SOME l. l \<in> Mapping.keys m) in the (Mapping.lookup m l) + valuesum (Mapping.delete l m))"
+proof (cases "Mapping.is_empty m")
+  case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
+next
+  case False
+  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def)
+  then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
+     the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
+       (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
+  proof (rule someI2_ex)
+    fix l
+    note fin
+    moreover assume "l \<in> dom (Mapping.lookup m)"
+    moreover obtain A where "A = dom (Mapping.lookup m) - {l}" by simp
+    ultimately have "dom (Mapping.lookup m) = insert l A" and "finite A" and "l \<notin> A" by auto
+    then show "(let l = l
+        in the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
+        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
+      by simp
+   qed
+  then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
+qed
+
+lemma valuesum_rec_AList:
+  "valuesum (AList []) = 0"
+  "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
+    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
+  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
+
+axioms
+  FIXME: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> C x = C y"
+
+lemma aux: "(SOME l. l \<in> Mapping.keys (AList (x # xs))) = fst (hd (x # xs))"
+proof (rule FIXME)
+  show "fst (hd (x # xs)) \<in> Mapping.keys (AList (x # xs))"
+    by (simp add: keys_AList)
+  show "(SOME l. l \<in> Mapping.keys (AList (x # xs))) \<in> Mapping.keys (AList (x # xs))"
+    apply (rule someI) apply (simp add: keys_AList) apply auto
+    done
+qed
+
+lemma valuesum_rec_exec [code]:
+  "valuesum (AList []) = 0"
+  "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
+    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
+  by (simp_all add: valuesum_rec_AList aux)
+
+value "valuesum (AList [(''abc'', (42::nat)), (''def'', 1705)])"
+
+end

--- a/src/HOL/ex/ROOT.ML	Wed Feb 17 09:48:53 2010 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Feb 17 09:48:53 2010 +0100
@@ -65,7 +65,8 @@
   "HarmonicSeries",
   "Refute_Examples",
   "Quickcheck_Examples",
-  "Landau"
+  "Landau",
+  "Execute_Choice"
 ];
 
 HTML.with_charset "utf-8" (no_document use_thys)