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