src/HOL/ex/Execute_Choice.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 44174 d1d79f0e1ea6 child 44899 95a53c01ed61 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 header {* A simple cookbook example how to eliminate choice in programs. *}
```
```     4
```
```     5 theory Execute_Choice
```
```     6 imports Main "~~/src/HOL/Library/AssocList"
```
```     7 begin
```
```     8
```
```     9 text {*
```
```    10   A trivial example:
```
```    11 *}
```
```    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 {*
```
```    17   Not that instead of defining @{term valuesum} with choice, we define it
```
```    18   directly and derive a description involving choice afterwards:
```
```    19 *}
```
```    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)" by (auto simp add: is_empty_def keys_def)
```
```    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 by (simp add: keys_def valuesum_def is_empty_def)
```
```    45 qed
```
```    46
```
```    47 text {*
```
```    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 *}
```
```    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   by (simp add: valuesum_def keys_def setsum_diff)
```
```    58
```
```    59 text {*
```
```    60   Given @{text valuesum_rec} 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 *}
```
```    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 {*
```
```    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 @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
```
```    76 *}
```
```    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 {*
```
```    97   See how it works:
```
```    98 *}
```
```    99
```
```   100 value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])"
```
```   101
```
```   102 end
```