a draft for an example how to turn specifications involving choice executable
authorhaftmann
Wed Feb 17 09:48:53 2010 +0100 (2010-02-17)
changeset 351606eb2b6c1d2d5
parent 35159 df38e92af926
child 35161 be96405ccaf3
a draft for an example how to turn specifications involving choice executable
src/HOL/ex/Execute_Choice.thy
src/HOL/ex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Execute_Choice.thy	Wed Feb 17 09:48:53 2010 +0100
     1.3 @@ -0,0 +1,64 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* A simple cookbook example how to eliminate choice in programs. *}
     1.7 +
     1.8 +theory Execute_Choice
     1.9 +imports Main AssocList
    1.10 +begin
    1.11 +
    1.12 +definition valuesum :: "('a, 'b :: comm_monoid_add) mapping \<Rightarrow> 'b" where
    1.13 +  "valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
    1.14 +
    1.15 +lemma valuesum_rec:
    1.16 +  assumes fin: "finite (dom (Mapping.lookup m))"
    1.17 +  shows "valuesum m = (if Mapping.is_empty m then 0 else
    1.18 +    let l = (SOME l. l \<in> Mapping.keys m) in the (Mapping.lookup m l) + valuesum (Mapping.delete l m))"
    1.19 +proof (cases "Mapping.is_empty m")
    1.20 +  case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
    1.21 +next
    1.22 +  case False
    1.23 +  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def)
    1.24 +  then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
    1.25 +     the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
    1.26 +       (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
    1.27 +  proof (rule someI2_ex)
    1.28 +    fix l
    1.29 +    note fin
    1.30 +    moreover assume "l \<in> dom (Mapping.lookup m)"
    1.31 +    moreover obtain A where "A = dom (Mapping.lookup m) - {l}" by simp
    1.32 +    ultimately have "dom (Mapping.lookup m) = insert l A" and "finite A" and "l \<notin> A" by auto
    1.33 +    then show "(let l = l
    1.34 +        in the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
    1.35 +        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
    1.36 +      by simp
    1.37 +   qed
    1.38 +  then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
    1.39 +qed
    1.40 +
    1.41 +lemma valuesum_rec_AList:
    1.42 +  "valuesum (AList []) = 0"
    1.43 +  "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
    1.44 +    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
    1.45 +  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
    1.46 +
    1.47 +axioms
    1.48 +  FIXME: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> C x = C y"
    1.49 +
    1.50 +lemma aux: "(SOME l. l \<in> Mapping.keys (AList (x # xs))) = fst (hd (x # xs))"
    1.51 +proof (rule FIXME)
    1.52 +  show "fst (hd (x # xs)) \<in> Mapping.keys (AList (x # xs))"
    1.53 +    by (simp add: keys_AList)
    1.54 +  show "(SOME l. l \<in> Mapping.keys (AList (x # xs))) \<in> Mapping.keys (AList (x # xs))"
    1.55 +    apply (rule someI) apply (simp add: keys_AList) apply auto
    1.56 +    done
    1.57 +qed
    1.58 +
    1.59 +lemma valuesum_rec_exec [code]:
    1.60 +  "valuesum (AList []) = 0"
    1.61 +  "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
    1.62 +    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
    1.63 +  by (simp_all add: valuesum_rec_AList aux)
    1.64 +
    1.65 +value "valuesum (AList [(''abc'', (42::nat)), (''def'', 1705)])"
    1.66 +
    1.67 +end
     2.1 --- a/src/HOL/ex/ROOT.ML	Wed Feb 17 09:48:53 2010 +0100
     2.2 +++ b/src/HOL/ex/ROOT.ML	Wed Feb 17 09:48:53 2010 +0100
     2.3 @@ -65,7 +65,8 @@
     2.4    "HarmonicSeries",
     2.5    "Refute_Examples",
     2.6    "Quickcheck_Examples",
     2.7 -  "Landau"
     2.8 +  "Landau",
     2.9 +  "Execute_Choice"
    2.10  ];
    2.11  
    2.12  HTML.with_charset "utf-8" (no_document use_thys)