author  haftmann 
Wed, 17 Feb 2010 11:21:47 +0100  
changeset 35164  8e3b8b5f1e96 
parent 35160  6eb2b6c1d2d5 
child 36109  1028cf8c0d1b 
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 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

6 
imports Main AssocList 
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 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

29 
then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def) 
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; 

61 
first, we formally insert the constructor @{term AList} and split the one equation into two, 

62 
where the second one provides the necessary context: 

63 
*} 

64 

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

65 
lemma valuesum_rec_AList: 
35164  66 
shows [code]: "valuesum (AList []) = 0" 
67 
and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in 

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

68 
the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

69 
by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList) 
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]: 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

79 
"valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

80 
the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))" 
35164  81 
proof  
82 
let ?M = "AList (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_AList) 

86 
moreover have "?l1 \<in> Mapping.keys ?M" 

87 
by (rule someI) (auto simp add: keys_AList) 

88 
moreover have "?l2 \<in> Mapping.keys ?M" 

89 
by (simp add: keys_AList) 

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

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 

35164  100 
value "valuesum (AList [(''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 