author  wenzelm 
Tue, 06 Oct 2015 17:47:28 +0200  
changeset 61343  5b5656a63bd6 
parent 58889  5b7a9633cfa8 
child 61933  cf58b5b794b2 
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 

61343  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  9 
text \<open> 
35164  10 
A trivial example: 
61343  11 
\<close> 
35164  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 

61343  16 
text \<open> 
35164  17 
Not that instead of defining @{term valuesum} with choice, we define it 
18 
directly and derive a description involving choice afterwards: 

61343  19 
\<close> 
35164  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  47 
text \<open> 
35164  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! 

61343  51 
\<close> 
35164  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)" 

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  58 

61343  59 
text \<open> 
35164  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: 
61343  63 
\<close> 
35164  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 

61343  71 
text \<open> 
35164  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}: 
61343  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  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 

61343  96 
text \<open> 
35164  97 
See how it works: 
61343  98 
\<close> 
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 