author  haftmann 
Wed, 17 Feb 2010 09:48:53 +0100  
changeset 35160  6eb2b6c1d2d5 
child 35164  8e3b8b5f1e96 
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 

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

9 
definition valuesum :: "('a, 'b :: comm_monoid_add) mapping \<Rightarrow> 'b" where 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

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

11 

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

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

13 
assumes fin: "finite (dom (Mapping.lookup m))" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

14 
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

15 
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

16 
proof (cases "Mapping.is_empty m") 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

17 
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

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

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

20 
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

21 
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

22 
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

23 
(\<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

24 
proof (rule someI2_ex) 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

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

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

27 
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

28 
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

29 
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

30 
then show "(let l = l 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

31 
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

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

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

35 
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

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

37 

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

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

39 
"valuesum (AList []) = 0" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

40 
"valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

41 
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

42 
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

43 

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

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

45 
FIXME: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> C x = C y" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

46 

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

47 
lemma aux: "(SOME l. l \<in> Mapping.keys (AList (x # xs))) = fst (hd (x # xs))" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

48 
proof (rule FIXME) 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

49 
show "fst (hd (x # xs)) \<in> Mapping.keys (AList (x # xs))" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

50 
by (simp add: keys_AList) 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

51 
show "(SOME l. l \<in> Mapping.keys (AList (x # xs))) \<in> Mapping.keys (AList (x # xs))" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

52 
apply (rule someI) apply (simp add: keys_AList) apply auto 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

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

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

55 

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

56 
lemma valuesum_rec_exec [code]: 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

57 
"valuesum (AList []) = 0" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

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

59 
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

60 
by (simp_all add: valuesum_rec_AList aux) 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

61 

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

62 
value "valuesum (AList [(''abc'', (42::nat)), (''def'', 1705)])" 
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
diff
changeset

63 

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

64 
end 