author  haftmann 
Wed, 14 Jul 2010 17:15:58 +0200  
changeset 37831  fa3a2e35c4f1 
parent 37827  954c9ce1d333 
child 37842  27e7047d9ae6 
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 

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

13 
definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

15 

37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

16 
definition get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

18 

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

19 
definition set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

21 

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

22 
definition alloc :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

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

25 
r = Array l; 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

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

28 

37802  29 
definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

31 

37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

32 
definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

33 
"update a i x h = set a ((get h a)[i:=x]) h" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

34 

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

35 
definition noteq :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where 
37752  36 
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" 
37 

38 

39 
subsection {* Monad operations *} 

40 

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

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

42 
[code del]: "new n x = Heap_Monad.heap (alloc (replicate n x))" 
37752  43 

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

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

45 
[code del]: "of_list xs = Heap_Monad.heap (alloc xs)" 
37752  46 

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

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

48 
[code del]: "make n f = Heap_Monad.heap (alloc (map f [0 ..< n]))" 
37752  49 

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

37802  51 
[code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)" 
37752  52 

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

37802  54 
[code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a) 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

55 
(\<lambda>h. (get h a ! i, h))" 
37752  56 

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

37802  58 
[code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a) 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

59 
(\<lambda>h. (a, update a i x h))" 
37752  60 

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

37802  62 
[code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length h a) 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

63 
(\<lambda>h. (a, update a i (f (get h a ! i)) h))" 
37752  64 

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

37802  66 
[code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length h a) 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

67 
(\<lambda>h. (get h a ! i, update a i x h))" 
37752  68 

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

37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

70 
[code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get h a)" 
37752  71 

72 

73 
subsection {* Properties *} 

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

74 

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

75 
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

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

77 

37758  78 
text {* Primitives *} 
79 

37807  80 
lemma noteq_sym: "a =!!= b \<Longrightarrow> b =!!= a" 
81 
and unequal [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" 

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

83 

37807  84 
lemma noteq_irrefl: "r =!!= r \<Longrightarrow> False" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

86 

37807  87 
lemma present_alloc_noteq: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

88 
by (simp add: present_def noteq_def alloc_def Let_def) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

89 

37807  90 
lemma get_set_eq [simp]: "get (set r x h) r = x" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

91 
by (simp add: get_def set_def o_def) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

92 

37807  93 
lemma get_set_neq [simp]: "r =!!= s \<Longrightarrow> get (set s x h) r = get h r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

94 
by (simp add: noteq_def get_def set_def) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

95 

37807  96 
lemma set_same [simp]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

97 
"set r x (set r y h) = set r x h" 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

99 

37807  100 
lemma set_set_swap: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

101 
"r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)" 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

102 
by (simp add: Let_def expand_fun_eq noteq_def set_def) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

103 

37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

104 
lemma get_update_eq [simp]: 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

105 
"get (update a i v h) a = (get h a) [i := v]" 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

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

107 

37807  108 
lemma nth_update_neq [simp]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

109 
"a =!!= b \<Longrightarrow> get (update b j v h) a ! i = get h a ! i" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

111 

37807  112 
lemma get_update_elem_neqIndex [simp]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

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

115 

37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

116 
lemma length_update [simp]: 
37802  117 
"length (update b i v h) = length h" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

118 
by (simp add: update_def length_def set_def get_def expand_fun_eq) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

119 

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

121 
"a =!!= a' \<Longrightarrow> 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

122 
update a i v (update a' i' v' h) 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

123 
= update a' i' v' (update a i v h)" 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

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

125 
apply simp 
37807  126 
apply (subst set_set_swap, assumption) 
127 
apply (subst get_set_neq) 

128 
apply (erule noteq_sym) 

129 
apply simp 

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

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

131 

37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

132 
lemma update_swap_neqIndex: 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

133 
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)" 
37807  134 
by (auto simp add: update_def set_set_swap list_update_swap) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

135 

37807  136 
lemma get_alloc: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

137 
"get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

139 

37807  140 
lemma set: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

141 
"set (fst (alloc ls h)) 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

142 
new_ls (snd (alloc ls h)) 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

143 
= snd (alloc new_ls h)" 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

145 

37807  146 
lemma present_update [simp]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

147 
"present (update b i v h) = present h" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

148 
by (simp add: update_def present_def set_def get_def expand_fun_eq) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

149 

37807  150 
lemma present_alloc [simp]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

151 
"present (snd (alloc xs h)) (fst (alloc xs h))" 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

152 
by (simp add: present_def alloc_def set_def Let_def) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

153 

37807  154 
lemma not_present_alloc [simp]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

155 
"\<not> present h (fst (alloc xs h))" 
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

156 
by (simp add: present_def alloc_def Let_def) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

157 

37758  158 

159 
text {* Monad operations *} 

160 

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

161 
lemma execute_new [execute_simps]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

162 
"execute (new n x) h = Some (alloc (replicate n x) h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

163 
by (simp add: new_def execute_simps) 
37758  164 

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

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

167 
by (auto intro: success_intros simp add: new_def) 
26170  168 

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

169 
lemma crel_newI [crel_intros]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

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

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

173 

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

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

175 
assumes "crel (new n x) h h' r" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

176 
obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

177 
"get h' r = replicate n x" "present h' r" "\<not> present h r" 
37807  178 
using assms by (rule crelE) (simp add: get_alloc execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

179 

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

180 
lemma execute_of_list [execute_simps]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

181 
"execute (of_list xs) h = Some (alloc xs h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

182 
by (simp add: of_list_def execute_simps) 
37758  183 

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

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

186 
by (auto intro: success_intros simp add: of_list_def) 
26170  187 

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

188 
lemma crel_of_listI [crel_intros]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

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

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

192 

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

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

194 
assumes "crel (of_list xs) h h' r" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

195 
obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

196 
"get h' r = xs" "present h' r" "\<not> present h r" 
37807  197 
using assms by (rule crelE) (simp add: get_alloc execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

198 

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

199 
lemma execute_make [execute_simps]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

200 
"execute (make n f) h = Some (alloc (map f [0 ..< n]) h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

201 
by (simp add: make_def execute_simps) 
26170  202 

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

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

205 
by (auto intro: success_intros simp add: make_def) 
37758  206 

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

207 
lemma crel_makeI [crel_intros]: 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

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

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

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

211 

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

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

213 
assumes "crel (make n f) h h' r" 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

214 
obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

215 
"get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r" 
37807  216 
using assms by (rule crelE) (simp add: get_alloc execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

217 

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

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

220 
by (simp add: len_def execute_simps) 
37758  221 

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

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

224 
by (auto intro: success_intros simp add: len_def) 
37752  225 

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

226 
lemma crel_lengthI [crel_intros]: 
37802  227 
assumes "h' = h" "r = length h a" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

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

230 

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

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

232 
assumes "crel (len a) h h' r" 
37802  233 
obtains "r = length h' a" "h' = h" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

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

235 

37758  236 
lemma execute_nth [execute_simps]: 
37802  237 
"i < length h a \<Longrightarrow> 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

238 
execute (nth a i) h = Some (get h a ! i, h)" 
37802  239 
"i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None" 
37758  240 
by (simp_all add: nth_def execute_simps) 
241 

242 
lemma success_nthI [success_intros]: 

37802  243 
"i < length h a \<Longrightarrow> success (nth a i) h" 
37758  244 
by (auto intro: success_intros simp add: nth_def) 
26170  245 

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

246 
lemma crel_nthI [crel_intros]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

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

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

250 

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

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

252 
assumes "crel (nth a i) h h' r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

254 
using assms by (rule crelE) 
37802  255 
(erule successE, cases "i < length h a", simp_all add: execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

256 

37758  257 
lemma execute_upd [execute_simps]: 
37802  258 
"i < length h a \<Longrightarrow> 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

259 
execute (upd i x a) h = Some (a, update a i x h)" 
37802  260 
"i \<ge> length h a \<Longrightarrow> execute (upd i x a) h = None" 
37758  261 
by (simp_all add: upd_def execute_simps) 
26170  262 

37758  263 
lemma success_updI [success_intros]: 
37802  264 
"i < length h a \<Longrightarrow> success (upd i x a) h" 
37758  265 
by (auto intro: success_intros simp add: upd_def) 
266 

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

267 
lemma crel_updI [crel_intros]: 
37802  268 
assumes "i < length h a" "h' = update a i v h" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

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

271 

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

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

273 
assumes "crel (upd i v a) h h' r" 
37802  274 
obtains "r = a" "h' = update a i v h" "i < length h a" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

275 
using assms by (rule crelE) 
37802  276 
(erule successE, cases "i < length h a", simp_all add: execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

277 

37758  278 
lemma execute_map_entry [execute_simps]: 
37802  279 
"i < length h a \<Longrightarrow> 
37758  280 
execute (map_entry i f a) h = 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

281 
Some (a, update a i (f (get h a ! i)) h)" 
37802  282 
"i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None" 
37758  283 
by (simp_all add: map_entry_def execute_simps) 
37752  284 

37758  285 
lemma success_map_entryI [success_intros]: 
37802  286 
"i < length h a \<Longrightarrow> success (map_entry i f a) h" 
37758  287 
by (auto intro: success_intros simp add: map_entry_def) 
288 

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

289 
lemma crel_map_entryI [crel_intros]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

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

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

293 

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

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

295 
assumes "crel (map_entry i f a) h h' r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

297 
using assms by (rule crelE) 
37802  298 
(erule successE, cases "i < length h a", simp_all add: execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

299 

37758  300 
lemma execute_swap [execute_simps]: 
37802  301 
"i < length h a \<Longrightarrow> 
37758  302 
execute (swap i x a) h = 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

303 
Some (get h a ! i, update a i x h)" 
37802  304 
"i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None" 
37758  305 
by (simp_all add: swap_def execute_simps) 
306 

307 
lemma success_swapI [success_intros]: 

37802  308 
"i < length h a \<Longrightarrow> success (swap i x a) h" 
37758  309 
by (auto intro: success_intros simp add: swap_def) 
37752  310 

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

311 
lemma crel_swapI [crel_intros]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

312 
assumes "i < length h a" "h' = update a i x h" "r = get h a ! i" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

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

315 

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

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

317 
assumes "crel (swap i x a) h h' r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

318 
obtains "r = get h a ! i" "h' = update a i x h" "i < length h a" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

319 
using assms by (rule crelE) 
37802  320 
(erule successE, cases "i < length h a", simp_all add: execute_simps) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

321 

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

322 
lemma execute_freeze [execute_simps]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

323 
"execute (freeze a) h = Some (get h a, h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

324 
by (simp add: freeze_def execute_simps) 
37758  325 

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

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

328 
by (auto intro: success_intros simp add: freeze_def) 
26170  329 

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

330 
lemma crel_freezeI [crel_intros]: 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

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

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

334 

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

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

336 
assumes "crel (freeze a) h h' r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

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

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

339 

26170  340 
lemma upd_return: 
341 
"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

342 
by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps) 
26170  343 

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

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

346 
by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps) 
26170  347 

37752  348 
lemma array_of_list_make: 
349 
"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

350 
by (rule Heap_eqI) (simp add: map_nth execute_simps) 
26170  351 

37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

352 
hide_const (open) present get set alloc length update noteq new of_list make len nth upd map_entry swap freeze 
26170  353 

26182  354 

355 
subsection {* Code generator setup *} 

356 

357 
subsubsection {* Logical intermediate layer *} 

358 

359 
definition new' where 

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

360 
[code del]: "new' = Array.new o Code_Numeral.nat_of" 
37752  361 

28562  362 
lemma [code]: 
37752  363 
"Array.new = new' o Code_Numeral.of_nat" 
26182  364 
by (simp add: new'_def o_def) 
365 

366 
definition make' where 

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

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

28562  369 
lemma [code]: 
37752  370 
"Array.make n f = make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" 
26182  371 
by (simp add: make'_def o_def) 
372 

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

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

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

28562  376 
lemma [code]: 
37752  377 
"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

378 
by (simp add: len'_def) 
26182  379 

380 
definition nth' where 

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

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

28562  383 
lemma [code]: 
37752  384 
"Array.nth a n = nth' a (Code_Numeral.of_nat n)" 
26182  385 
by (simp add: nth'_def) 
386 

387 
definition upd' where 

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

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

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

37752  394 
lemma [code]: 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

395 
"Array.map_entry i f a = do { 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

396 
x \<leftarrow> Array.nth a i; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

397 
Array.upd i (f x) a 
37792  398 
}" 
37758  399 
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps) 
26182  400 

37752  401 
lemma [code]: 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

402 
"Array.swap i x a = do { 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

403 
y \<leftarrow> Array.nth a i; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

404 
Array.upd i x a; 
37752  405 
return y 
37792  406 
}" 
37758  407 
by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps) 
37752  408 

409 
lemma [code]: 

37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

410 
"Array.freeze a = do { 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

411 
n \<leftarrow> Array.len a; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

412 
Heap_Monad.fold_map (\<lambda>i. Array.nth a i) [0..<n] 
37792  413 
}" 
37752  414 
proof (rule Heap_eqI) 
415 
fix h 

416 
have *: "List.map 

37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

417 
(\<lambda>x. fst (the (if x < Array.length h a 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

418 
then Some (Array.get h a ! x, h) else None))) 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

419 
[0..<Array.length h a] = 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

420 
List.map (List.nth (Array.get h a)) [0..<Array.length h a]" 
37752  421 
by simp 
37804
0145e59c1f6c
qualified names for (almost) all array operations
haftmann
parents:
37803
diff
changeset

422 
have "execute (Heap_Monad.fold_map (Array.nth a) [0..<Array.length h a]) h = 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

423 
Some (Array.get h a, 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

424 
apply (subst execute_fold_map_unchanged_heap) 
37752  425 
apply (simp_all add: nth_def guard_def *) 
426 
apply (simp add: length_def map_nth) 

427 
done 

37792  428 
then have "execute (do { 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

429 
n \<leftarrow> Array.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

430 
Heap_Monad.fold_map (Array.nth a) [0..<n] 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

431 
}) h = Some (Array.get h a, h)" 
37787
30dc3abf4a58
theorem collections do not contain default rules any longer
haftmann
parents:
37771
diff
changeset

432 
by (auto intro: execute_bind_eq_SomeI simp add: execute_simps) 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

433 
then show "execute (Array.freeze a) h = execute (do { 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

434 
n \<leftarrow> Array.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

435 
Heap_Monad.fold_map (Array.nth a) [0..<n] 
37792  436 
}) h" by (simp add: execute_simps) 
37752  437 
qed 
438 

37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

439 
hide_const (open) new' make' len' nth' upd' 
37752  440 

441 

442 
text {* SML *} 

26182  443 

444 
code_type array (SML "_/ array") 

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

26752  446 
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") 
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

447 
code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)") 
26752  448 
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

449 
code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") 
26752  450 
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") 
451 
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") 

26182  452 

453 
code_reserved SML Array 

454 

455 

37752  456 
text {* OCaml *} 
26182  457 

458 
code_type array (OCaml "_/ array") 

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

32580  460 
code_const Array.new' (OCaml "(fun/ ()/ >/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)") 
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

461 
code_const Array.of_list (OCaml "(fun/ ()/ >/ Array.of'_list/ _)") 
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

462 
code_const Array.make' (OCaml "(fun/ ()/ >/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ 
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

463 
(fun k'_ >/ _/ (Big'_int.big'_int'_of'_int/ k'_)))") 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

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

26182  467 

468 
code_reserved OCaml Array 

469 

470 

37752  471 
text {* Haskell *} 
26182  472 

29793  473 
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") 
26182  474 
code_const Array (Haskell "error/ \"bare Array\"") 
37831
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

475 
code_const Array.new' (Haskell "Heap.newArray") 
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

476 
code_const Array.of_list (Haskell "Heap.newListArray") 
fa3a2e35c4f1
repaired some implementations of imperative operations
haftmann
parents:
37827
diff
changeset

477 
code_const Array.make' (Haskell "Heap.newFunArray") 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37716
diff
changeset

478 
code_const Array.len' (Haskell "Heap.lengthArray") 
29793  479 
code_const Array.nth' (Haskell "Heap.readArray") 
480 
code_const Array.upd' (Haskell "Heap.writeArray") 

26182  481 

26170  482 
end 