src/HOL/ex/Execute_Choice.thy

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

(* 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