author  haftmann 
Tue, 13 Jul 2010 12:05:20 +0200  
changeset 37797  96551d6b1414 
parent 37792  ba0bc31b90d7 
parent 37796  08bd610b2583 
child 37798  0b0570445a2a 
permissions  rwrr 
31870  1 
(* Title: HOL/Imperative_HOL/Array.thy 
26170  2 
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen 
3 
*) 

4 

5 
header {* Monadic arrays *} 

6 

7 
theory Array 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
29822
diff
changeset

8 
imports Heap_Monad 
26170  9 
begin 
10 

37752  11 
subsection {* Primitives *} 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

12 

37752  13 
definition (*FIXME present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where*) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

14 
array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

15 
"array_present a h \<longleftrightarrow> addr_of_array a < lim h" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

16 

37752  17 
definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

18 
get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

19 
"get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

20 

37752  21 
definition (*FIXME set*) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

22 
set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

23 
"set_array a x = 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

24 
arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

25 

37752  26 
definition (*FIXME alloc*) 
27 
array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

28 
"array xs h = (let 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

29 
l = lim h; 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

30 
r = Array l; 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

31 
h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

32 
in (r, h''))" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

33 

37752  34 
definition (*FIXME length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where*) 
35 
length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

36 
"length a h = List.length (get_array a h)" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

37 

37752  38 
definition (*FIXME update*) 
39 
change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

40 
"change a i x h = set_array a ((get_array a h)[i:=x]) h" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

41 

37752  42 
definition (*FIXME noteq*) 
43 
noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where 

44 
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" 

45 

46 

47 
subsection {* Monad operations *} 

48 

49 
definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where 

50 
[code del]: "new n x = Heap_Monad.heap (array (replicate n x))" 

51 

52 
definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where 

53 
[code del]: "of_list xs = Heap_Monad.heap (array xs)" 

54 

55 
definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where 

56 
[code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))" 

57 

58 
definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where 

37758  59 
[code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)" 
37752  60 

61 
definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where 

62 
[code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h) 

63 
(\<lambda>h. (get_array a h ! i, h))" 

64 

65 
definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where 

66 
[code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h) 

67 
(\<lambda>h. (a, change a i x h))" 

68 

69 
definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where 

70 
[code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h) 

71 
(\<lambda>h. (a, change a i (f (get_array a h ! i)) h))" 

72 

73 
definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where 

74 
[code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h) 

75 
(\<lambda>h. (get_array a h ! i, change a i x h))" 

76 

77 
definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where 

37758  78 
[code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)" 
37752  79 

80 

81 
subsection {* Properties *} 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

82 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

83 
text {* FIXME: Does there exist a "canonical" array axiomatisation in 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

84 
the literature? *} 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

85 

37758  86 
text {* Primitives *} 
87 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

88 
lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

89 
and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

90 
unfolding noteq_arrs_def by auto 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

91 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

92 
lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

93 
unfolding noteq_arrs_def by auto 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

94 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

95 
lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

96 
by (simp add: array_present_def noteq_arrs_def array_def Let_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

97 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

98 
lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

99 
by (simp add: get_array_def set_array_def o_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

100 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

101 
lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

102 
by (simp add: noteq_arrs_def get_array_def set_array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

103 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

104 
lemma set_array_same [simp]: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

105 
"set_array r x (set_array r y h) = set_array r x h" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

106 
by (simp add: set_array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

107 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

108 
lemma array_set_set_swap: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

109 
"r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

110 
by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

111 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

112 
lemma get_array_change_eq [simp]: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

113 
"get_array a (change a i v h) = (get_array a h) [i := v]" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

114 
by (simp add: change_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

115 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

116 
lemma nth_change_array_neq_array [simp]: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

117 
"a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

118 
by (simp add: change_def noteq_arrs_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

119 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

120 
lemma get_arry_array_change_elem_neqIndex [simp]: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

121 
"i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

122 
by simp 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

123 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

124 
lemma length_change [simp]: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

125 
"length a (change b i v h) = length a h" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

126 
by (simp add: change_def length_def set_array_def get_array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

127 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

128 
lemma change_swap_neqArray: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

129 
"a =!!= a' \<Longrightarrow> 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

130 
change a i v (change a' i' v' h) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

131 
= change a' i' v' (change a i v h)" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

132 
apply (unfold change_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

133 
apply simp 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

134 
apply (subst array_set_set_swap, assumption) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

135 
apply (subst array_get_set_neq) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

136 
apply (erule noteq_arrs_sym) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

137 
apply (simp) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

138 
done 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

139 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

140 
lemma change_swap_neqIndex: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

141 
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

142 
by (auto simp add: change_def array_set_set_swap list_update_swap) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

143 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

144 
lemma get_array_init_array_list: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

145 
"get_array (fst (array ls h)) (snd (array ls' h)) = ls'" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

146 
by (simp add: Let_def split_def array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

147 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

148 
lemma set_array: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

149 
"set_array (fst (array ls h)) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

150 
new_ls (snd (array ls h)) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

151 
= snd (array new_ls h)" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

152 
by (simp add: Let_def split_def array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

153 

271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

154 
lemma array_present_change [simp]: 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

155 
"array_present a (change b i v h) = array_present a h" 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

156 
by (simp add: change_def array_present_def set_array_def get_array_def) 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

157 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

158 
lemma array_present_array [simp]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

159 
"array_present (fst (array xs h)) (snd (array xs h))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

160 
by (simp add: array_present_def array_def set_array_def Let_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

161 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

162 
lemma not_array_present_array [simp]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

163 
"\<not> array_present (fst (array xs h)) h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

164 
by (simp add: array_present_def array_def Let_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

165 

37758  166 

167 
text {* Monad operations *} 

168 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

169 
lemma execute_new [execute_simps]: 
37758  170 
"execute (new n x) h = Some (array (replicate n x) h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

171 
by (simp add: new_def execute_simps) 
37758  172 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

173 
lemma success_newI [success_intros]: 
37758  174 
"success (new n x) h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

175 
by (auto intro: success_intros simp add: new_def) 
26170  176 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

177 
lemma crel_newI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

178 
assumes "(a, h') = array (replicate n x) h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

179 
shows "crel (new n x) h h' a" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

180 
by (rule crelI) (simp add: assms execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

181 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

182 
lemma crel_newE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

183 
assumes "crel (new n x) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

184 
obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

185 
"get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

186 
using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

187 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

188 
lemma execute_of_list [execute_simps]: 
37758  189 
"execute (of_list xs) h = Some (array xs h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

190 
by (simp add: of_list_def execute_simps) 
37758  191 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

192 
lemma success_of_listI [success_intros]: 
37758  193 
"success (of_list xs) h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

194 
by (auto intro: success_intros simp add: of_list_def) 
26170  195 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

196 
lemma crel_of_listI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

197 
assumes "(a, h') = array xs h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

198 
shows "crel (of_list xs) h h' a" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

199 
by (rule crelI) (simp add: assms execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

200 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

201 
lemma crel_of_listE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

202 
assumes "crel (of_list xs) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

203 
obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

204 
"get_array r h' = xs" "array_present r h'" "\<not> array_present r h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

205 
using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

206 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

207 
lemma execute_make [execute_simps]: 
37758  208 
"execute (make n f) h = Some (array (map f [0 ..< n]) h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

209 
by (simp add: make_def execute_simps) 
26170  210 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

211 
lemma success_makeI [success_intros]: 
37758  212 
"success (make n f) h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

213 
by (auto intro: success_intros simp add: make_def) 
37758  214 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

215 
lemma crel_makeI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

216 
assumes "(a, h') = array (map f [0 ..< n]) h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

217 
shows "crel (make n f) h h' a" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

218 
by (rule crelI) (simp add: assms execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

219 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

220 
lemma crel_makeE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

221 
assumes "crel (make n f) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

222 
obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

223 
"get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

224 
using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

225 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

226 
lemma execute_len [execute_simps]: 
37758  227 
"execute (len a) h = Some (length a h, h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

228 
by (simp add: len_def execute_simps) 
37758  229 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

230 
lemma success_lenI [success_intros]: 
37758  231 
"success (len a) h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

232 
by (auto intro: success_intros simp add: len_def) 
37752  233 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

234 
lemma crel_lengthI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

235 
assumes "h' = h" "r = length a h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

236 
shows "crel (len a) h h' r" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

237 
by (rule crelI) (simp add: assms execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

238 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

239 
lemma crel_lengthE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

240 
assumes "crel (len a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

241 
obtains "r = length a h'" "h' = h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

242 
using assms by (rule crelE) (simp add: execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

243 

37758  244 
lemma execute_nth [execute_simps]: 
37752  245 
"i < length a h \<Longrightarrow> 
37758  246 
execute (nth a i) h = Some (get_array a h ! i, h)" 
247 
"i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None" 

248 
by (simp_all add: nth_def execute_simps) 

249 

250 
lemma success_nthI [success_intros]: 

251 
"i < length a h \<Longrightarrow> success (nth a i) h" 

252 
by (auto intro: success_intros simp add: nth_def) 

26170  253 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

254 
lemma crel_nthI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

255 
assumes "i < length a h" "h' = h" "r = get_array a h ! i" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

256 
shows "crel (nth a i) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

257 
by (rule crelI) (insert assms, simp add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

258 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

259 
lemma crel_nthE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

260 
assumes "crel (nth a i) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

261 
obtains "i < length a h" "r = get_array a h ! i" "h' = h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

262 
using assms by (rule crelE) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

263 
(erule successE, cases "i < length a h", simp_all add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

264 

37758  265 
lemma execute_upd [execute_simps]: 
37752  266 
"i < length a h \<Longrightarrow> 
37758  267 
execute (upd i x a) h = Some (a, change a i x h)" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

268 
"i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None" 
37758  269 
by (simp_all add: upd_def execute_simps) 
26170  270 

37758  271 
lemma success_updI [success_intros]: 
272 
"i < length a h \<Longrightarrow> success (upd i x a) h" 

273 
by (auto intro: success_intros simp add: upd_def) 

274 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

275 
lemma crel_updI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

276 
assumes "i < length a h" "h' = change a i v h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

277 
shows "crel (upd i v a) h h' a" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

278 
by (rule crelI) (insert assms, simp add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

279 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

280 
lemma crel_updE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

281 
assumes "crel (upd i v a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

282 
obtains "r = a" "h' = change a i v h" "i < length a h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

283 
using assms by (rule crelE) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

284 
(erule successE, cases "i < length a h", simp_all add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

285 

37758  286 
lemma execute_map_entry [execute_simps]: 
37752  287 
"i < length a h \<Longrightarrow> 
37758  288 
execute (map_entry i f a) h = 
37752  289 
Some (a, change a i (f (get_array a h ! i)) h)" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

290 
"i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None" 
37758  291 
by (simp_all add: map_entry_def execute_simps) 
37752  292 

37758  293 
lemma success_map_entryI [success_intros]: 
294 
"i < length a h \<Longrightarrow> success (map_entry i f a) h" 

295 
by (auto intro: success_intros simp add: map_entry_def) 

296 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

297 
lemma crel_map_entryI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

298 
assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

299 
shows "crel (map_entry i f a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

300 
by (rule crelI) (insert assms, simp add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

301 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

302 
lemma crel_map_entryE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

303 
assumes "crel (map_entry i f a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

304 
obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

305 
using assms by (rule crelE) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

306 
(erule successE, cases "i < length a h", simp_all add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

307 

37758  308 
lemma execute_swap [execute_simps]: 
37752  309 
"i < length a h \<Longrightarrow> 
37758  310 
execute (swap i x a) h = 
37752  311 
Some (get_array a h ! i, change a i x h)" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

312 
"i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None" 
37758  313 
by (simp_all add: swap_def execute_simps) 
314 

315 
lemma success_swapI [success_intros]: 

316 
"i < length a h \<Longrightarrow> success (swap i x a) h" 

317 
by (auto intro: success_intros simp add: swap_def) 

37752  318 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

319 
lemma crel_swapI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

320 
assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

321 
shows "crel (swap i x a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

322 
by (rule crelI) (insert assms, simp add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

323 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

324 
lemma crel_swapE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

325 
assumes "crel (swap i x a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

326 
obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

327 
using assms by (rule crelE) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

328 
(erule successE, cases "i < length a h", simp_all add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

329 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

330 
lemma execute_freeze [execute_simps]: 
37758  331 
"execute (freeze a) h = Some (get_array a h, h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

332 
by (simp add: freeze_def execute_simps) 
37758  333 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

334 
lemma success_freezeI [success_intros]: 
37758  335 
"success (freeze a) h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

336 
by (auto intro: success_intros simp add: freeze_def) 
26170  337 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

338 
lemma crel_freezeI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

339 
assumes "h' = h" "r = get_array a h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

340 
shows "crel (freeze a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

341 
by (rule crelI) (insert assms, simp add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

342 

1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

343 
lemma crel_freezeE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

344 
assumes "crel (freeze a) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

345 
obtains "h' = h" "r = get_array a h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

346 
using assms by (rule crelE) (simp add: execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

347 

26170  348 
lemma upd_return: 
349 
"upd i x a \<guillemotright> return a = upd i x a" 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

350 
by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps) 
26170  351 

37752  352 
lemma array_make: 
353 
"new n x = make n (\<lambda>_. x)" 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

354 
by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps) 
26170  355 

37752  356 
lemma array_of_list_make: 
357 
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" 

37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

358 
by (rule Heap_eqI) (simp add: map_nth execute_simps) 
26170  359 

37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

360 
hide_const (open) new 
26170  361 

26182  362 

363 
subsection {* Code generator setup *} 

364 

365 
subsubsection {* Logical intermediate layer *} 

366 

367 
definition new' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

368 
[code del]: "new' = Array.new o Code_Numeral.nat_of" 
37752  369 

28562  370 
lemma [code]: 
37752  371 
"Array.new = new' o Code_Numeral.of_nat" 
26182  372 
by (simp add: new'_def o_def) 
373 

374 
definition of_list' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

375 
[code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" 
37752  376 

28562  377 
lemma [code]: 
37752  378 
"Array.of_list xs = of_list' (Code_Numeral.of_nat (List.length xs)) xs" 
26182  379 
by (simp add: of_list'_def) 
380 

381 
definition make' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

382 
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" 
37752  383 

28562  384 
lemma [code]: 
37752  385 
"Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" 
26182  386 
by (simp add: make'_def o_def) 
387 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

388 
definition len' where 
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

389 
[code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))" 
37752  390 

28562  391 
lemma [code]: 
37752  392 
"Array.len a = len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

393 
by (simp add: len'_def) 
26182  394 

395 
definition nth' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

396 
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" 
37752  397 

28562  398 
lemma [code]: 
37752  399 
"Array.nth a n = nth' a (Code_Numeral.of_nat n)" 
26182  400 
by (simp add: nth'_def) 
401 

402 
definition upd' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

403 
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()" 
37752  404 

28562  405 
lemma [code]: 
37752  406 
"Array.upd i x a = upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a" 
37709  407 
by (simp add: upd'_def upd_return) 
26182  408 

37752  409 
lemma [code]: 
37792  410 
"map_entry i f a = do { 
37752  411 
x \<leftarrow> nth a i; 
412 
upd i (f x) a 

37792  413 
}" 
37758  414 
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) 
26182  415 

37752  416 
lemma [code]: 
37792  417 
"swap i x a = do { 
37752  418 
y \<leftarrow> nth a i; 
419 
upd i x a; 

420 
return y 

37792  421 
}" 
37758  422 
by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) 
37752  423 

424 
lemma [code]: 

37792  425 
"freeze a = do { 
37752  426 
n \<leftarrow> len a; 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset

427 
Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n] 
37792  428 
}" 
37752  429 
proof (rule Heap_eqI) 
430 
fix h 

431 
have *: "List.map 

432 
(\<lambda>x. fst (the (if x < length a h 

433 
then Some (get_array a h ! x, h) else None))) 

434 
[0..<length a h] = 

435 
List.map (List.nth (get_array a h)) [0..<length a h]" 

436 
by simp 

37758  437 
have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h = 
37752  438 
Some (get_array a h, h)" 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset

439 
apply (subst execute_fold_map_unchanged_heap) 
37752  440 
apply (simp_all add: nth_def guard_def *) 
441 
apply (simp add: length_def map_nth) 

442 
done 

37792  443 
then have "execute (do { 
37752  444 
n \<leftarrow> len a; 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset

445 
Heap_Monad.fold_map (Array.nth a) [0..<n] 
37792  446 
}) h = Some (get_array a h, h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

447 
by (auto intro: execute_bind_eq_SomeI simp add: execute_simps) 
37792  448 
then show "execute (freeze a) h = execute (do { 
37752  449 
n \<leftarrow> len a; 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37752
diff
changeset

450 
Heap_Monad.fold_map (Array.nth a) [0..<n] 
37792  451 
}) h" by (simp add: execute_simps) 
37752  452 
qed 
453 

454 
hide_const (open) new' of_list' make' len' nth' upd' 

455 

456 

457 
text {* SML *} 

26182  458 

459 
code_type array (SML "_/ array") 

460 
code_const Array (SML "raise/ (Fail/ \"bare Array\")") 

26752  461 
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") 
35846  462 
code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)") 
26752  463 
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

464 
code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") 
26752  465 
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") 
466 
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") 

26182  467 

468 
code_reserved SML Array 

469 

470 

37752  471 
text {* OCaml *} 
26182  472 

473 
code_type array (OCaml "_/ array") 

474 
code_const Array (OCaml "failwith/ \"bare Array\"") 

32580  475 
code_const Array.new' (OCaml "(fun/ ()/ >/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)") 
35846  476 
code_const Array.of_list' (OCaml "(fun/ ()/ >/ Array.of'_list/ _)") 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

477 
code_const Array.len' (OCaml "(fun/ ()/ >/ Big'_int.big'_int'_of'_int/ (Array.length/ _))") 
32580  478 
code_const Array.nth' (OCaml "(fun/ ()/ >/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))") 
479 
code_const Array.upd' (OCaml "(fun/ ()/ >/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)") 

26182  480 

481 
code_reserved OCaml Array 

482 

483 

37752  484 
text {* Haskell *} 
26182  485 

29793  486 
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") 
26182  487 
code_const Array (Haskell "error/ \"bare Array\"") 
29793  488 
code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)") 
489 
code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)") 

37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

490 
code_const Array.len' (Haskell "Heap.lengthArray") 
29793  491 
code_const Array.nth' (Haskell "Heap.readArray") 
492 
code_const Array.upd' (Haskell "Heap.writeArray") 

26182  493 

26170  494 
end 