author  bulwahn 
Mon, 12 Sep 2011 12:33:37 +0200  
changeset 44899  95a53c01ed61 
parent 44174  d1d79f0e1ea6 
child 49929  70300f1b6835 
permissions  rwrr 
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 

6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

3 
header {* A simple cookbook example how to eliminate choice in programs. *} 
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 

35164  9 
text {* 
10 
A trivial example: 

11 
*} 

12 

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 

35164  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 

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 
44174
d1d79f0e1ea6
make more HOL theories work with separate set type
huffman
parents:
41413
diff
changeset

29 
then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def keys_def) 
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 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

44 
then show ?thesis by (simp add: keys_def valuesum_def is_empty_def) 
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 

35164  47 
text {* 
48 
In the context of the elsebranch 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; 

36109  61 
first, we formally insert the constructor @{term Mapping} and split the one equation into two, 
35164  62 
where the second one provides the necessary context: 
63 
*} 

64 

36109  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))))" 

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 

35164  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. 

35160
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

74 

35164  75 
Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}: 
76 
*} 

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  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))))" 

35164  81 
proof  
36109  82 
let ?M = "Mapping (x # xs)" 
35164  83 
let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)" 
84 
let ?l2 = "fst (hd (x # xs))" 

36109  85 
have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping) 
35164  86 
moreover have "?l1 \<in> Mapping.keys ?M" 
36109  87 
by (rule someI) (auto simp add: keys_Mapping) 
35164  88 
moreover have "?l2 \<in> Mapping.keys ?M" 
36109  89 
by (simp add: keys_Mapping) 
35164  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) 

36109  93 
then show ?thesis by (simp add: valuesum_rec_Mapping) 
35164  94 
qed 
95 

96 
text {* 

97 
See how it works: 

98 
*} 

35160
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

99 

36109  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 