src/HOL/ex/Execute_Choice.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39302 d7728f65b353
child 44174 d1d79f0e1ea6
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
haftmann@35160
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@35160
     2
haftmann@35160
     3
header {* A simple cookbook example how to eliminate choice in programs. *}
haftmann@35160
     4
haftmann@35160
     5
theory Execute_Choice
wenzelm@41413
     6
imports Main "~~/src/HOL/Library/AssocList"
haftmann@35160
     7
begin
haftmann@35160
     8
haftmann@35164
     9
text {*
haftmann@35164
    10
  A trivial example:
haftmann@35164
    11
*}
haftmann@35164
    12
haftmann@35164
    13
definition valuesum :: "('a, 'b :: ab_group_add) mapping \<Rightarrow> 'b" where
haftmann@35160
    14
  "valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
haftmann@35160
    15
haftmann@35164
    16
text {*
haftmann@35164
    17
  Not that instead of defining @{term valuesum} with choice, we define it
haftmann@35164
    18
  directly and derive a description involving choice afterwards:
haftmann@35164
    19
*}
haftmann@35164
    20
haftmann@35160
    21
lemma valuesum_rec:
haftmann@35160
    22
  assumes fin: "finite (dom (Mapping.lookup m))"
haftmann@35160
    23
  shows "valuesum m = (if Mapping.is_empty m then 0 else
haftmann@35160
    24
    let l = (SOME l. l \<in> Mapping.keys m) in the (Mapping.lookup m l) + valuesum (Mapping.delete l m))"
haftmann@35160
    25
proof (cases "Mapping.is_empty m")
haftmann@35160
    26
  case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
haftmann@35160
    27
next
haftmann@35160
    28
  case False
nipkow@39302
    29
  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def fun_eq_iff mem_def keys_def)
haftmann@35160
    30
  then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
haftmann@35160
    31
     the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
haftmann@35160
    32
       (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
haftmann@35160
    33
  proof (rule someI2_ex)
haftmann@35160
    34
    fix l
haftmann@35160
    35
    note fin
haftmann@35160
    36
    moreover assume "l \<in> dom (Mapping.lookup m)"
haftmann@35160
    37
    moreover obtain A where "A = dom (Mapping.lookup m) - {l}" by simp
haftmann@35160
    38
    ultimately have "dom (Mapping.lookup m) = insert l A" and "finite A" and "l \<notin> A" by auto
haftmann@35160
    39
    then show "(let l = l
haftmann@35160
    40
        in the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
haftmann@35160
    41
        (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
haftmann@35160
    42
      by simp
haftmann@35160
    43
   qed
haftmann@35160
    44
  then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
haftmann@35160
    45
qed
haftmann@35160
    46
haftmann@35164
    47
text {*
haftmann@35164
    48
  In the context of the else-branch we can show that the exact choice is
haftmann@35164
    49
  irrelvant; in practice, finding this point where choice becomes irrelevant is the
haftmann@35164
    50
  most difficult thing!
haftmann@35164
    51
*}
haftmann@35164
    52
haftmann@35164
    53
lemma valuesum_choice:
haftmann@35164
    54
  "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow>
haftmann@35164
    55
    the (Mapping.lookup M x) + valuesum (Mapping.delete x M) =
haftmann@35164
    56
    the (Mapping.lookup M y) + valuesum (Mapping.delete y M)"
haftmann@35164
    57
  by (simp add: valuesum_def keys_def setsum_diff)
haftmann@35164
    58
haftmann@35164
    59
text {*
haftmann@35164
    60
  Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
haftmann@36109
    61
  first, we formally insert the constructor @{term Mapping} and split the one equation into two,
haftmann@35164
    62
  where the second one provides the necessary context:
haftmann@35164
    63
*}
haftmann@35164
    64
haftmann@36109
    65
lemma valuesum_rec_Mapping:
haftmann@36109
    66
  shows [code]: "valuesum (Mapping []) = 0"
haftmann@36109
    67
  and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
haftmann@36109
    68
    the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
haftmann@37595
    69
  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping null_def)
haftmann@35160
    70
haftmann@35164
    71
text {*
haftmann@35164
    72
  As a side effect the precondition disappears (but note this has nothing to do with choice!).
haftmann@35164
    73
  The first equation deals with the uncritical empty case and can already be used for code generation.
haftmann@35160
    74
haftmann@35164
    75
  Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
haftmann@35164
    76
*}
haftmann@35160
    77
haftmann@35160
    78
lemma valuesum_rec_exec [code]:
haftmann@36109
    79
  "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in
haftmann@36109
    80
    the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
haftmann@35164
    81
proof -
haftmann@36109
    82
  let ?M = "Mapping (x # xs)"
haftmann@35164
    83
  let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)"
haftmann@35164
    84
  let ?l2 = "fst (hd (x # xs))"
haftmann@36109
    85
  have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping)
haftmann@35164
    86
  moreover have "?l1 \<in> Mapping.keys ?M"
haftmann@36109
    87
    by (rule someI) (auto simp add: keys_Mapping)
haftmann@35164
    88
  moreover have "?l2 \<in> Mapping.keys ?M"
haftmann@36109
    89
    by (simp add: keys_Mapping)
haftmann@35164
    90
  ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) =
haftmann@35164
    91
    the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)"
haftmann@35164
    92
    by (rule valuesum_choice)
haftmann@36109
    93
  then show ?thesis by (simp add: valuesum_rec_Mapping)
haftmann@35164
    94
qed
haftmann@35164
    95
  
haftmann@35164
    96
text {*
haftmann@35164
    97
  See how it works:
haftmann@35164
    98
*}
haftmann@35160
    99
haftmann@36109
   100
value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])"
haftmann@35160
   101
haftmann@35160
   102
end