src/HOL/ex/Execute_Choice.thy
author nipkow
Mon Oct 17 11:46:22 2016 +0200 (2016-10-17)
changeset 64267 b9a1486e79be
parent 61933 cf58b5b794b2
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
setsum -> sum
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 section \<open>A simple cookbook example how to eliminate choice in programs.\<close>
     4 
     5 theory Execute_Choice
     6 imports Main "~~/src/HOL/Library/AList_Mapping"
     7 begin
     8 
     9 text \<open>
    10   A trivial example:
    11 \<close>
    12 
    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))"
    15 
    16 text \<open>
    17   Not that instead of defining @{term valuesum} with choice, we define it
    18   directly and derive a description involving choice afterwards:
    19 \<close>
    20 
    21 lemma valuesum_rec:
    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)
    27 next
    28   case False
    29   then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" unfolding is_empty_def by transfer auto
    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)
    34     fix l
    35     note fin
    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
    39     then show "(let l = l
    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))"
    42       by simp
    43    qed
    44   then show ?thesis unfolding is_empty_def valuesum_def by transfer simp
    45 qed
    46 
    47 text \<open>
    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
    50   most difficult thing!
    51 \<close>
    52 
    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   unfolding valuesum_def  by transfer (simp add: sum_diff)
    58 
    59 text \<open>
    60   Given \<open>valuesum_rec\<close> as initial description, we stepwise refine it to something executable;
    61   first, we formally insert the constructor @{term Mapping} and split the one equation into two,
    62   where the second one provides the necessary context:
    63 \<close>
    64 
    65 lemma valuesum_rec_Mapping:
    66   shows [code]: "valuesum (Mapping []) = 0"
    67   and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
    68     the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
    69   by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
    70 
    71 text \<open>
    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.
    74 
    75   Using \<open>valuesum_choice\<close>, we are able to prove an executable version of @{term valuesum}:
    76 \<close>
    77 
    78 lemma valuesum_rec_exec [code]:
    79   "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in
    80     the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
    81 proof -
    82   let ?M = "Mapping (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_Mapping)
    86   moreover have "?l1 \<in> Mapping.keys ?M"
    87     by (rule someI) (auto simp add: keys_Mapping)
    88   moreover have "?l2 \<in> Mapping.keys ?M"
    89     by (simp add: keys_Mapping)
    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_Mapping)
    94 qed
    95   
    96 text \<open>
    97   See how it works:
    98 \<close>
    99 
   100 value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])"
   101 
   102 end