author  haftmann 
Mon, 12 Jul 2010 16:05:08 +0200  
changeset 37771  1bec64044b5e 
parent 37758  bf86a65403a8 
child 37772  026ed2fc15d4 
permissions  rwrr 
26170  1 
(* Title: HOL/Library/Heap_Monad.thy 
2 
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen 

3 
*) 

4 

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

5 
header {* A monad with a polymorphic heap and primitive reasoning infrastructure *} 
26170  6 

7 
theory Heap_Monad 

8 
imports Heap 

9 
begin 

10 

11 
subsection {* The monad *} 

12 

37758  13 
subsubsection {* Monad construction *} 
26170  14 

15 
text {* Monadic heap actions either produce values 

16 
and transform the heap, or fail *} 

37709  17 
datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option" 
26170  18 

37709  19 
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where 
20 
[code del]: "execute (Heap f) = f" 

26170  21 

37758  22 
lemma Heap_cases [case_names succeed fail]: 
23 
fixes f and h 

24 
assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P" 

25 
assumes fail: "execute f h = None \<Longrightarrow> P" 

26 
shows P 

27 
using assms by (cases "execute f h") auto 

28 

26170  29 
lemma Heap_execute [simp]: 
30 
"Heap (execute f) = f" by (cases f) simp_all 

31 

32 
lemma Heap_eqI: 

33 
"(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g" 

34 
by (cases f, cases g) (auto simp: expand_fun_eq) 

35 

37758  36 
ML {* structure Execute_Simps = Named_Thms( 
37 
val name = "execute_simps" 

38 
val description = "simplification rules for execute" 

39 
) *} 

40 

41 
setup Execute_Simps.setup 

42 

43 
lemma execute_Let [simp, execute_simps]: 

44 
"execute (let x = t in f x) = (let x = t in execute (f x))" 

45 
by (simp add: Let_def) 

46 

47 

48 
subsubsection {* Specialised lifters *} 

49 

50 
definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where 

51 
[code del]: "tap f = Heap (\<lambda>h. Some (f h, h))" 

52 

53 
lemma execute_tap [simp, execute_simps]: 

54 
"execute (tap f) h = Some (f h, h)" 

55 
by (simp add: tap_def) 

26170  56 

37709  57 
definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where 
58 
[code del]: "heap f = Heap (Some \<circ> f)" 

26170  59 

37758  60 
lemma execute_heap [simp, execute_simps]: 
37709  61 
"execute (heap f) = Some \<circ> f" 
26170  62 
by (simp add: heap_def) 
63 

37754  64 
definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where 
65 
[code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)" 

66 

37758  67 
lemma execute_guard [execute_simps]: 
37754  68 
"\<not> P h \<Longrightarrow> execute (guard P f) h = None" 
69 
"P h \<Longrightarrow> execute (guard P f) h = Some (f h)" 

70 
by (simp_all add: guard_def) 

71 

37758  72 

73 
subsubsection {* Predicate classifying successful computations *} 

74 

75 
definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where 

76 
"success f h \<longleftrightarrow> execute f h \<noteq> None" 

77 

78 
lemma successI: 

79 
"execute f h \<noteq> None \<Longrightarrow> success f h" 

80 
by (simp add: success_def) 

81 

82 
lemma successE: 

83 
assumes "success f h" 

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

84 
obtains r h' where "r = fst (the (execute c h))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

85 
and "h' = snd (the (execute c h))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

86 
and "execute f h \<noteq> None" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

87 
using assms by (simp add: success_def) 
37758  88 

89 
ML {* structure Success_Intros = Named_Thms( 

90 
val name = "success_intros" 

91 
val description = "introduction rules for success" 

92 
) *} 

93 

94 
setup Success_Intros.setup 

95 

96 
lemma success_tapI [iff, success_intros]: 

97 
"success (tap f) h" 

98 
by (rule successI) simp 

99 

100 
lemma success_heapI [iff, success_intros]: 

101 
"success (heap f) h" 

102 
by (rule successI) simp 

103 

104 
lemma success_guardI [success_intros]: 

105 
"P h \<Longrightarrow> success (guard P f) h" 

106 
by (rule successI) (simp add: execute_guard) 

107 

108 
lemma success_LetI [success_intros]: 

109 
"x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h" 

110 
by (simp add: Let_def) 

111 

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

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

113 
"(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow> 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

114 
success (if c then t else e) h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

115 
by (simp add: success_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

116 

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

117 

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

118 
subsubsection {* Predicate for a simple relational calculus *} 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

119 

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

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

121 
The @{text crel} predicate states that when a computation @{text c} 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

122 
runs with the heap @{text h} will result in return value @{text r} 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

123 
and a heap @{text "h'"}, i.e.~no exception occurs. 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

125 

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

126 
definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

127 
crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

128 

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

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

130 
"Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

131 
by (simp add: crel_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

132 

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

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

134 
assumes "crel c h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

135 
obtains "r = fst (the (execute c h))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

136 
and "h' = snd (the (execute c h))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

137 
and "success c h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

138 
proof (rule that) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

139 
from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

140 
then show "success c h" by (simp add: success_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

141 
from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

143 
then show "r = fst (the (execute c h))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

144 
and "h' = snd (the (execute c h))" by simp_all 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

146 

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

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

148 
"crel c h h' r \<Longrightarrow> success c h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

149 
by (simp add: crel_def success_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

150 

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

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

152 
assumes "success c h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

153 
obtains r h' where "crel c h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

154 
using assms by (auto simp add: crel_def success_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

155 

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

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

157 
assumes "crel f h h' a" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

158 
and "crel f h h'' b" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

159 
shows "a = b" and "h' = h''" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

160 
using assms unfolding crel_def by auto 
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 
ML {* structure Crel_Intros = Named_Thms( 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

163 
val name = "crel_intros" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

164 
val description = "introduction rules for crel" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

166 

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

167 
ML {* structure Crel_Elims = Named_Thms( 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

168 
val name = "crel_elims" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

169 
val description = "elimination rules for crel" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

171 

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

172 
setup "Crel_Intros.setup #> Crel_Elims.setup" 
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_LetI [crel_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

175 
assumes "x = t" "crel (f x) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

176 
shows "crel (let x = t in f x) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

177 
using assms by simp 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

178 

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

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

180 
assumes "crel (let x = t in f x) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

181 
obtains "crel (f t) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

182 
using assms by simp 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

183 

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

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

185 
assumes "c \<Longrightarrow> crel t h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

186 
and "\<not> c \<Longrightarrow> crel e h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

187 
shows "crel (if c then t else e) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

188 
by (cases c) (simp_all add: assms) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

189 

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

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

191 
assumes "crel (if c then t else e) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

192 
obtains "c" "crel t h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

193 
 "\<not> c" "crel e h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

194 
using assms by (cases c) simp_all 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

195 

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

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

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

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

199 
by (rule crelI) (simp add: assms) 
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_tapE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

203 
obtains "h' = h" and "r = f h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

205 

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

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

207 
assumes "h' = snd (f h)" "r = fst (f h)" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

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

210 

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

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

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

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

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

215 

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

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

217 
assumes "P h" "h' = snd (f h)" "r = fst (f h)" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

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

220 

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

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

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

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

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

225 
(auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

226 

37758  227 

228 
subsubsection {* Monad combinators *} 

26170  229 

37709  230 
definition return :: "'a \<Rightarrow> 'a Heap" where 
26170  231 
[code del]: "return x = heap (Pair x)" 
232 

37758  233 
lemma execute_return [simp, execute_simps]: 
37709  234 
"execute (return x) = Some \<circ> Pair x" 
26170  235 
by (simp add: return_def) 
236 

37758  237 
lemma success_returnI [iff, success_intros]: 
238 
"success (return x) h" 

239 
by (rule successI) simp 

240 

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

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

242 
"h = h' \<Longrightarrow> crel (return x) h h' x" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

243 
by (rule crelI) simp 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

244 

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

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

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

247 
obtains "r = x" "h' = h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

249 

37709  250 
definition raise :: "string \<Rightarrow> 'a Heap" where  {* the string is just decoration *} 
251 
[code del]: "raise s = Heap (\<lambda>_. None)" 

26170  252 

37758  253 
lemma execute_raise [simp, execute_simps]: 
37709  254 
"execute (raise s) = (\<lambda>_. None)" 
26170  255 
by (simp add: raise_def) 
256 

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

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

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

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

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

261 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

262 
definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where 
37709  263 
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of 
264 
Some (x, h') \<Rightarrow> execute (g x) h' 

265 
 None \<Rightarrow> None)" 

266 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

267 
notation bind (infixl "\<guillemotright>=" 54) 
37709  268 

37758  269 
lemma execute_bind [execute_simps]: 
37709  270 
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'" 
271 
"execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None" 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

272 
by (simp_all add: bind_def) 
37709  273 

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

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

275 
"success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

276 
by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

277 

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

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

279 
"execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h" 
37758  280 
by (auto intro!: successI elim!: successE simp add: bind_def) 
281 

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

282 
lemma success_bind_crelI [success_intros]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

283 
"crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

284 
by (auto simp add: crel_def success_def bind_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

285 

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

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

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

288 
shows "crel (f \<guillemotright>= g) h h'' r'" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

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

290 
apply (auto intro!: crelI elim!: crelE successE) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

291 
apply (subst execute_bind, simp_all) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

292 
done 
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_bindE [crel_elims]: 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

295 
assumes "crel (f \<guillemotright>= g) h h'' r'" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

296 
obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

297 
using assms by (auto simp add: crel_def bind_def split: option.split_asm) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

298 

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

299 
lemma execute_bind_eq_SomeI: 
37754  300 
assumes "Heap_Monad.execute f h = Some (x, h')" 
301 
and "Heap_Monad.execute (g x) h' = Some (y, h'')" 

302 
shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')" 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

303 
using assms by (simp add: bind_def) 
37754  304 

37709  305 
lemma return_bind [simp]: "return x \<guillemotright>= f = f x" 
37758  306 
by (rule Heap_eqI) (simp add: execute_bind) 
37709  307 

308 
lemma bind_return [simp]: "f \<guillemotright>= return = f" 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

309 
by (rule Heap_eqI) (simp add: bind_def split: option.splits) 
37709  310 

311 
lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)" 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

312 
by (rule Heap_eqI) (simp add: bind_def split: option.splits) 
37709  313 

314 
lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e" 

37758  315 
by (rule Heap_eqI) (simp add: execute_bind) 
37709  316 

37754  317 
abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where 
37709  318 
"f >> g \<equiv> f >>= (\<lambda>_. g)" 
319 

37754  320 
notation chain (infixl "\<guillemotright>" 54) 
37709  321 

26170  322 

323 
subsubsection {* dosyntax *} 

324 

325 
text {* 

326 
We provide a convenient donotation for monadic expressions 

327 
wellknown from Haskell. @{const Let} is printed 

328 
specially in doexpressions. 

329 
*} 

330 

331 
nonterminals do_expr 

332 

333 
syntax 

334 
"_do" :: "do_expr \<Rightarrow> 'a" 

335 
("(do (_)//done)" [12] 100) 

37754  336 
"_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 
26170  337 
("_ < _;//_" [1000, 13, 12] 12) 
37754  338 
"_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 
26170  339 
("_;//_" [13, 12] 12) 
340 
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

341 
("let _ = _;//_" [1000, 13, 12] 12) 

342 
"_nil" :: "'a \<Rightarrow> do_expr" 

343 
("_" [12] 12) 

344 

345 
syntax (xsymbols) 

37754  346 
"_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 
26170  347 
("_ \<leftarrow> _;//_" [1000, 13, 12] 12) 
348 

349 
translations 

28145  350 
"_do f" => "f" 
37754  351 
"_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)" 
352 
"_chain f g" => "f \<guillemotright> g" 

26170  353 
"_let x t f" => "CONST Let t (\<lambda>x. f)" 
354 
"_nil f" => "f" 

355 

356 
print_translation {* 

357 
let 

358 
fun dest_abs_eta (Abs (abs as (_, ty, _))) = 

359 
let 

360 
val (v, t) = Syntax.variant_abs abs; 

28145  361 
in (Free (v, ty), t) end 
26170  362 
 dest_abs_eta t = 
363 
let 

364 
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0); 

28145  365 
in (Free (v, dummyT), t) end; 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

366 
fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) = 
26170  367 
let 
28145  368 
val (v, g') = dest_abs_eta g; 
369 
val vs = fold_aterms (fn Free (v, _) => insert (op =) v  _ => I) v []; 

26170  370 
val v_used = fold_aterms 
28145  371 
(fn Free (w, _) => (fn s => s orelse member (op =) vs w)  _ => I) g' false; 
26170  372 
in if v_used then 
37754  373 
Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g' 
26170  374 
else 
37754  375 
Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g' 
26170  376 
end 
37754  377 
 unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) = 
378 
Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g 

26170  379 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = 
380 
let 

28145  381 
val (v, g') = dest_abs_eta g; 
35113  382 
in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end 
26170  383 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) = 
28145  384 
Const (@{const_syntax return}, dummyT) $ f 
26170  385 
 unfold_monad f = f; 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

386 
fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true 
37754  387 
 contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = 
388 
contains_bind t; 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

389 
fun bind_monad_tr' (f::g::ts) = list_comb 
35113  390 
(Const (@{syntax_const "_do"}, dummyT) $ 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

391 
unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts); 
35113  392 
fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = 
37754  393 
if contains_bind g' then list_comb 
35113  394 
(Const (@{syntax_const "_do"}, dummyT) $ 
395 
unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts) 

28145  396 
else raise Match; 
35113  397 
in 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

398 
[(@{const_syntax bind}, bind_monad_tr'), 
35113  399 
(@{const_syntax Let}, Let_monad_tr')] 
400 
end; 

26170  401 
*} 
402 

403 

37758  404 
subsection {* Generic combinators *} 
26170  405 

37758  406 
subsubsection {* Assertions *} 
26170  407 

37709  408 
definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where 
409 
"assert P x = (if P x then return x else raise ''assert'')" 

28742  410 

37758  411 
lemma execute_assert [execute_simps]: 
37754  412 
"P x \<Longrightarrow> execute (assert P x) h = Some (x, h)" 
413 
"\<not> P x \<Longrightarrow> execute (assert P x) h = None" 

414 
by (simp_all add: assert_def) 

415 

37758  416 
lemma success_assertI [success_intros]: 
417 
"P x \<Longrightarrow> success (assert P x) h" 

418 
by (rule successI) (simp add: execute_assert) 

419 

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

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

421 
"P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

422 
by (rule crelI) (simp add: execute_assert) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

423 

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

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

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

426 
obtains "P x" "r = x" "h' = h" 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

427 
using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def) 
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37758
diff
changeset

428 

28742  429 
lemma assert_cong [fundef_cong]: 
430 
assumes "P = P'" 

431 
assumes "\<And>x. P' x \<Longrightarrow> f x = f' x" 

432 
shows "(assert P x >>= f) = (assert P' x >>= f')" 

37754  433 
by (rule Heap_eqI) (insert assms, simp add: assert_def) 
28742  434 

37758  435 

436 
subsubsection {* Plain lifting *} 

437 

37754  438 
definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where 
439 
"lift f = return o f" 

37709  440 

37754  441 
lemma lift_collapse [simp]: 
442 
"lift f x = return (f x)" 

443 
by (simp add: lift_def) 

37709  444 

37754  445 
lemma bind_lift: 
446 
"(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))" 

447 
by (simp add: lift_def comp_def) 

37709  448 

37758  449 

450 
subsubsection {* Iteration  warning: this is rarely useful! *} 

451 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

452 
primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where 
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

453 
"fold_map f [] = return []" 
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

454 
 "fold_map f (x # xs) = do 
37709  455 
y \<leftarrow> f x; 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

456 
ys \<leftarrow> fold_map f xs; 
37709  457 
return (y # ys) 
458 
done" 

459 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

460 
lemma fold_map_append: 
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

461 
"fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))" 
37754  462 
by (induct xs) simp_all 
463 

37758  464 
lemma execute_fold_map_unchanged_heap [execute_simps]: 
37754  465 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)" 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

466 
shows "execute (fold_map f xs) h = 
37754  467 
Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" 
468 
using assms proof (induct xs) 

469 
case Nil show ?case by simp 

470 
next 

471 
case (Cons x xs) 

472 
from Cons.prems obtain y 

473 
where y: "execute (f x) h = Some (y, h)" by auto 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

474 
moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h = 
37754  475 
Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto 
476 
ultimately show ?case by (simp, simp only: execute_bind(1), simp) 

477 
qed 

478 

37709  479 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

480 
subsubsection {* A monadic combinator for simple recursive functions *} 
36057  481 

482 
text {* Using a locale to fix arguments f and g of MREC *} 

483 

484 
locale mrec = 

37709  485 
fixes f :: "'a \<Rightarrow> ('b + 'a) Heap" 
486 
and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap" 

36057  487 
begin 
488 

37709  489 
function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where 
490 
"mrec x h = (case execute (f x) h of 

491 
Some (Inl r, h') \<Rightarrow> Some (r, h') 

492 
 Some (Inr s, h') \<Rightarrow> (case mrec s h' of 

493 
Some (z, h'') \<Rightarrow> execute (g x s z) h'' 

494 
 None \<Rightarrow> None) 

495 
 None \<Rightarrow> None)" 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

496 
by auto 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

497 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

498 
lemma graph_implies_dom: 
35423  499 
"mrec_graph x y \<Longrightarrow> mrec_dom x" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

500 
apply (induct rule:mrec_graph.induct) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

501 
apply (rule accpI) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

502 
apply (erule mrec_rel.cases) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

503 
by simp 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

504 

37709  505 
lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None" 
35423  506 
unfolding mrec_def 
36057  507 
by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified]) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

508 

36057  509 
lemma mrec_di_reverse: 
510 
assumes "\<not> mrec_dom (x, h)" 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

511 
shows " 
37709  512 
(case execute (f x) h of 
513 
Some (Inl r, h') \<Rightarrow> False 

514 
 Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h') 

515 
 None \<Rightarrow> False 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

516 
)" 
37709  517 
using assms apply (auto split: option.split sum.split) 
518 
apply (rule ccontr) 

519 
apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+ 

520 
done 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

521 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

522 
lemma mrec_rule: 
36057  523 
"mrec x h = 
37709  524 
(case execute (f x) h of 
525 
Some (Inl r, h') \<Rightarrow> Some (r, h') 

526 
 Some (Inr s, h') \<Rightarrow> 

36057  527 
(case mrec s h' of 
37709  528 
Some (z, h'') \<Rightarrow> execute (g x s z) h'' 
529 
 None \<Rightarrow> None) 

530 
 None \<Rightarrow> None 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

531 
)" 
36057  532 
apply (cases "mrec_dom (x,h)", simp) 
533 
apply (frule mrec_default) 

534 
apply (frule mrec_di_reverse, simp) 

37709  535 
by (auto split: sum.split option.split simp: mrec_default) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

536 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

537 
definition 
36057  538 
"MREC x = Heap (mrec x)" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

539 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

540 
lemma MREC_rule: 
36057  541 
"MREC x = 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

542 
(do y \<leftarrow> f x; 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

543 
(case y of 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

544 
Inl r \<Rightarrow> return r 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

545 
 Inr s \<Rightarrow> 
36057  546 
do z \<leftarrow> MREC s ; 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

547 
g x s z 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

548 
done) done)" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

549 
unfolding MREC_def 
37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

550 
unfolding bind_def return_def 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

551 
apply simp 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

552 
apply (rule ext) 
36057  553 
apply (unfold mrec_rule[of x]) 
37709  554 
by (auto split: option.splits prod.splits sum.splits) 
36057  555 

556 
lemma MREC_pinduct: 

37709  557 
assumes "execute (MREC x) h = Some (r, h')" 
558 
assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r" 

559 
assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z 

560 
\<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r" 

36057  561 
shows "P x h h' r" 
562 
proof  

37709  563 
from assms(1) have mrec: "mrec x h = Some (r, h')" 
36057  564 
unfolding MREC_def execute.simps . 
565 
from mrec have dom: "mrec_dom (x, h)" 

566 
apply  

567 
apply (rule ccontr) 

568 
apply (drule mrec_default) by auto 

37709  569 
from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))" 
36057  570 
by auto 
37709  571 
from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))" 
36057  572 
proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom]) 
573 
case (1 x h) 

37709  574 
obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp 
36057  575 
show ?case 
37709  576 
proof (cases "execute (f x) h") 
577 
case (Some result) 

578 
then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp 

36057  579 
note Inl' = this 
580 
show ?thesis 

581 
proof (cases a) 

582 
case (Inl aa) 

583 
from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis 

584 
by auto 

585 
next 

586 
case (Inr b) 

587 
note Inr' = this 

37709  588 
show ?thesis 
589 
proof (cases "mrec b h1") 

590 
case (Some result) 

591 
then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp 

592 
moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" 

593 
apply (intro 1(2)) 

594 
apply (auto simp add: Inr Inl') 

595 
done 

596 
moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3) 

597 
ultimately show ?thesis 

598 
apply auto 

599 
apply (rule rec_case) 

600 
apply auto 

601 
unfolding MREC_def by auto 

36057  602 
next 
37709  603 
case None 
604 
from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto 

36057  605 
qed 
606 
qed 

607 
next 

37709  608 
case None 
609 
from this 1(1) mrec 1(3) show ?thesis by simp 

36057  610 
qed 
611 
qed 

612 
from this h'_r show ?thesis by simp 

613 
qed 

614 

615 
end 

616 

617 
text {* Providing global versions of the constant and the theorems *} 

618 

619 
abbreviation "MREC == mrec.MREC" 

620 
lemmas MREC_rule = mrec.MREC_rule 

621 
lemmas MREC_pinduct = mrec.MREC_pinduct 

622 

26182  623 

624 
subsection {* Code generator setup *} 

625 

626 
subsubsection {* Logical intermediate layer *} 

627 

37709  628 
primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where 
629 
[code del, code_post]: "raise' (STR s) = raise s" 

26182  630 

37709  631 
lemma raise_raise' [code_inline]: 
632 
"raise s = raise' (STR s)" 

633 
by simp 

26182  634 

37709  635 
code_datatype raise'  {* avoid @{const "Heap"} formally *} 
26182  636 

637 

27707  638 
subsubsection {* SML and OCaml *} 
26182  639 

26752  640 
code_type Heap (SML "unit/ >/ _") 
27826  641 
code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())") 
27707  642 
code_const return (SML "!(fn/ ()/ =>/ _)") 
37709  643 
code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)") 
26182  644 

37754  645 
code_type Heap (OCaml "unit/ >/ _") 
27826  646 
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ >/ f'_/ (_/ ())/ ())") 
27707  647 
code_const return (OCaml "!(fun/ ()/ >/ _)") 
37709  648 
code_const Heap_Monad.raise' (OCaml "failwith/ _") 
27707  649 

31871  650 
setup {* 
651 

652 
let 

27707  653 

31871  654 
open Code_Thingol; 
655 

656 
fun imp_program naming = 

27707  657 

31871  658 
let 
659 
fun is_const c = case lookup_const naming c 

660 
of SOME c' => (fn c'' => c' = c'') 

661 
 NONE => K false; 

37756
59caa6180fff
avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
haftmann
parents:
37754
diff
changeset

662 
val is_bind = is_const @{const_name bind}; 
31871  663 
val is_return = is_const @{const_name return}; 
31893  664 
val dummy_name = ""; 
31871  665 
val dummy_type = ITyVar dummy_name; 
31893  666 
val dummy_case_term = IVar NONE; 
31871  667 
(*assumption: dummy values are not relevant for serialization*) 
668 
val unitt = case lookup_const naming @{const_name Unity} 

669 
of SOME unit' => IConst (unit', (([], []), [])) 

670 
 NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants."); 

671 
fun dest_abs ((v, ty) `=> t, _) = ((v, ty), t) 

672 
 dest_abs (t, ty) = 

673 
let 

674 
val vs = fold_varnames cons t []; 

675 
val v = Name.variant vs "x"; 

676 
val ty' = (hd o fst o unfold_fun) ty; 

31893  677 
in ((SOME v, ty'), t `$ IVar (SOME v)) end; 
31871  678 
fun force (t as IConst (c, _) `$ t') = if is_return c 
679 
then t' else t `$ unitt 

680 
 force t = t `$ unitt; 

681 
fun tr_bind' [(t1, _), (t2, ty2)] = 

682 
let 

683 
val ((v, ty), t) = dest_abs (t2, ty2); 

684 
in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end 

685 
and tr_bind'' t = case unfold_app t 

37754  686 
of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c 
31871  687 
then tr_bind' [(x1, ty1), (x2, ty2)] 
688 
else force t 

689 
 _ => force t; 

31893  690 
fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `=> ICase (((IVar (SOME dummy_name), dummy_type), 
31871  691 
[(unitt, tr_bind' ts)]), dummy_case_term) 
37754  692 
and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys) 
31871  693 
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] 
694 
 ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 

695 
 (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) 

696 
else IConst const `$$ map imp_monad_bind ts 

697 
and imp_monad_bind (IConst const) = imp_monad_bind' const [] 

698 
 imp_monad_bind (t as IVar _) = t 

699 
 imp_monad_bind (t as _ `$ _) = (case unfold_app t 

700 
of (IConst const, ts) => imp_monad_bind' const ts 

701 
 (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts) 

702 
 imp_monad_bind (v_ty `=> t) = v_ty `=> imp_monad_bind t 

703 
 imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase 

704 
(((imp_monad_bind t, ty), 

705 
(map o pairself) imp_monad_bind pats), 

706 
imp_monad_bind t0); 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28562
diff
changeset

707 

31871  708 
in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; 
27707  709 

710 
in 

711 

31871  712 
Code_Target.extend_target ("SML_imp", ("SML", imp_program)) 
713 
#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) 

27707  714 

715 
end 

31871  716 

27707  717 
*} 
718 

26182  719 

720 
subsubsection {* Haskell *} 

721 

722 
text {* Adaption layer *} 

723 

29793  724 
code_include Haskell "Heap" 
26182  725 
{*import qualified Control.Monad; 
726 
import qualified Control.Monad.ST; 

727 
import qualified Data.STRef; 

728 
import qualified Data.Array.ST; 

729 

27695  730 
type RealWorld = Control.Monad.ST.RealWorld; 
26182  731 
type ST s a = Control.Monad.ST.ST s a; 
732 
type STRef s a = Data.STRef.STRef s a; 

27673  733 
type STArray s a = Data.Array.ST.STArray s Int a; 
26182  734 

735 
newSTRef = Data.STRef.newSTRef; 

736 
readSTRef = Data.STRef.readSTRef; 

737 
writeSTRef = Data.STRef.writeSTRef; 

738 

27673  739 
newArray :: (Int, Int) > a > ST s (STArray s a); 
26182  740 
newArray = Data.Array.ST.newArray; 
741 

27673  742 
newListArray :: (Int, Int) > [a] > ST s (STArray s a); 
26182  743 
newListArray = Data.Array.ST.newListArray; 
744 

27673  745 
lengthArray :: STArray s a > ST s Int; 
746 
lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a); 

26182  747 

27673  748 
readArray :: STArray s a > Int > ST s a; 
26182  749 
readArray = Data.Array.ST.readArray; 
750 

27673  751 
writeArray :: STArray s a > Int > a > ST s (); 
26182  752 
writeArray = Data.Array.ST.writeArray;*} 
753 

29793  754 
code_reserved Haskell Heap 
26182  755 

756 
text {* Monad *} 

757 

29793  758 
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") 
28145  759 
code_monad "op \<guillemotright>=" Haskell 
26182  760 
code_const return (Haskell "return") 
37709  761 
code_const Heap_Monad.raise' (Haskell "error/ _") 
26182  762 

37758  763 
hide_const (open) Heap heap guard raise' fold_map 
37724  764 

26170  765 
end 