author  nipkow 
Wed, 19 Oct 2011 16:32:12 +0200  
changeset 45200  1f1897ac7877 
parent 45134  9b02f6665fc8 
child 45212  e87feee00a4c 
permissions  rwrr 
44070  1 
header "Constant Folding" 
2 

3 
theory Fold imports Sem_Equiv begin 

4 

44850  5 
subsection "Simple folding of arithmetic expressions" 
44070  6 

45134  7 
type_synonym 
44070  8 
tab = "name \<Rightarrow> val option" 
9 

10 
(* maybe better as the composition of substitution and the existing simp_const(0) *) 

11 
fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where 

12 
"simp_const (N n) _ = N n"  

13 
"simp_const (V x) t = (case t x of None \<Rightarrow> V x  Some k \<Rightarrow> N k)"  

14 
"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of 

15 
(N n1, N n2) \<Rightarrow> N(n1+n2)  (e1',e2') \<Rightarrow> Plus e1' e2')" 

16 

17 
definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)" 

18 

19 
theorem aval_simp_const[simp]: 

20 
assumes "approx t s" 

21 
shows "aval (simp_const a t) s = aval a s" 

22 
using assms 

23 
by (induct a) (auto simp: approx_def split: aexp.split option.split) 

24 

25 
theorem aval_simp_const_N: 

26 
assumes "approx t s" 

27 
shows "simp_const a t = N n \<Longrightarrow> aval a s = n" 

28 
using assms 

29 
by (induct a arbitrary: n) 

30 
(auto simp: approx_def split: aexp.splits option.splits) 

31 

32 
definition 

33 
"merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)" 

34 

35 
primrec lnames :: "com \<Rightarrow> name set" where 

36 
"lnames SKIP = {}"  

37 
"lnames (x ::= a) = {x}"  

38 
"lnames (c1; c2) = lnames c1 \<union> lnames c2"  

39 
"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2"  

40 
"lnames (WHILE b DO c) = lnames c" 

41 

42 
primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where 

43 
"defs SKIP t = t"  

44 
"defs (x ::= a) t = 

45 
(case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k)  _ \<Rightarrow> t(x:=None))"  

46 
"defs (c1;c2) t = (defs c2 o defs c1) t"  

47 
"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)"  

48 
"defs (WHILE b DO c) t = t ` (lnames c)" 

49 

50 
primrec fold where 

51 
"fold SKIP _ = SKIP"  

52 
"fold (x ::= a) t = (x ::= (simp_const a t))"  

53 
"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))"  

54 
"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t"  

55 
"fold (WHILE b DO c) t = WHILE b DO fold c (t ` (lnames c))" 

56 

57 
lemma approx_merge: 

58 
"approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44850
diff
changeset

59 
by (fastforce simp: merge_def approx_def) 
44070  60 

61 
lemma approx_map_le: 

62 
"approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s" 

63 
by (clarsimp simp: approx_def map_le_def dom_def) 

64 

65 
lemma restrict_map_le [intro!, simp]: "t ` S \<subseteq>\<^sub>m t" 

66 
by (clarsimp simp: restrict_map_def map_le_def) 

67 

68 
lemma merge_restrict: 

69 
assumes "t1 ` S = t ` S" 

70 
assumes "t2 ` S = t ` S" 

71 
shows "merge t1 t2 ` S = t ` S" 

72 
proof  

73 
from assms 

74 
have "\<forall>x. (t1 ` S) x = (t ` S) x" 

75 
and "\<forall>x. (t2 ` S) x = (t ` S) x" by auto 

76 
thus ?thesis 

77 
by (auto simp: merge_def restrict_map_def 

78 
split: if_splits intro: ext) 

79 
qed 

80 

81 

82 
lemma defs_restrict: 

83 
"defs c t ` ( lnames c) = t ` ( lnames c)" 

45015  84 
proof (induction c arbitrary: t) 
44070  85 
case (Semi c1 c2) 
86 
hence "defs c1 t ` ( lnames c1) = t ` ( lnames c1)" 

87 
by simp 

88 
hence "defs c1 t ` ( lnames c1) ` (lnames c2) = 

89 
t ` ( lnames c1) ` (lnames c2)" by simp 

90 
moreover 

91 
from Semi 

92 
have "defs c2 (defs c1 t) ` ( lnames c2) = 

93 
defs c1 t ` ( lnames c2)" 

94 
by simp 

95 
hence "defs c2 (defs c1 t) ` ( lnames c2) ` ( lnames c1) = 

96 
defs c1 t ` ( lnames c2) ` ( lnames c1)" 

97 
by simp 

98 
ultimately 

99 
show ?case by (clarsimp simp: Int_commute) 

100 
next 

101 
case (If b c1 c2) 

102 
hence "defs c1 t ` ( lnames c1) = t ` ( lnames c1)" by simp 

103 
hence "defs c1 t ` ( lnames c1) ` (lnames c2) = 

104 
t ` ( lnames c1) ` (lnames c2)" by simp 

105 
moreover 

106 
from If 

107 
have "defs c2 t ` ( lnames c2) = t ` ( lnames c2)" by simp 

108 
hence "defs c2 t ` ( lnames c2) ` (lnames c1) = 

109 
t ` ( lnames c2) ` (lnames c1)" by simp 

110 
ultimately 

111 
show ?case by (auto simp: Int_commute intro: merge_restrict) 

112 
qed (auto split: aexp.split) 

113 

114 

115 
lemma big_step_pres_approx: 

116 
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'" 

45015  117 
proof (induction arbitrary: t rule: big_step_induct) 
44070  118 
case Skip thus ?case by simp 
119 
next 

120 
case Assign 

121 
thus ?case 

122 
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) 

123 
next 

124 
case (Semi c1 s1 s2 c2 s3) 

45015  125 
have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems]) 
126 
hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2)) 

44070  127 
thus ?case by simp 
128 
next 

129 
case (IfTrue b s c1 s') 

130 
hence "approx (defs c1 t) s'" by simp 

131 
thus ?case by (simp add: approx_merge) 

132 
next 

133 
case (IfFalse b s c2 s') 

134 
hence "approx (defs c2 t) s'" by simp 

135 
thus ?case by (simp add: approx_merge) 

136 
next 

137 
case WhileFalse 

138 
thus ?case by (simp add: approx_def restrict_map_def) 

139 
next 

140 
case (WhileTrue b s1 c s2 s3) 

141 
hence "approx (defs c t) s2" by simp 

142 
with WhileTrue 

143 
have "approx (defs c t ` (lnames c)) s3" by simp 

144 
thus ?case by (simp add: defs_restrict) 

145 
qed 

146 

147 
corollary approx_defs_inv [simp]: 

148 
"\<Turnstile> {approx t} c {approx (defs c t)}" 

149 
by (simp add: hoare_valid_def big_step_pres_approx) 

150 

151 

152 
lemma big_step_pres_approx_restrict: 

153 
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t ` (lnames c)) s \<Longrightarrow> approx (t ` (lnames c)) s'" 

45015  154 
proof (induction arbitrary: t rule: big_step_induct) 
44070  155 
case Assign 
156 
thus ?case by (clarsimp simp: approx_def) 

157 
next 

158 
case (Semi c1 s1 s2 c2 s3) 

159 
hence "approx (t ` (lnames c2) ` (lnames c1)) s1" 

160 
by (simp add: Int_commute) 

161 
hence "approx (t ` (lnames c2) ` (lnames c1)) s2" 

162 
by (rule Semi) 

163 
hence "approx (t ` (lnames c1) ` (lnames c2)) s2" 

164 
by (simp add: Int_commute) 

165 
hence "approx (t ` (lnames c1) ` (lnames c2)) s3" 

166 
by (rule Semi) 

167 
thus ?case by simp 

168 
next 

169 
case (IfTrue b s c1 s' c2) 

170 
hence "approx (t ` (lnames c2) ` (lnames c1)) s" 

171 
by (simp add: Int_commute) 

172 
hence "approx (t ` (lnames c2) ` (lnames c1)) s'" 

173 
by (rule IfTrue) 

174 
thus ?case by (simp add: Int_commute) 

175 
next 

176 
case (IfFalse b s c2 s' c1) 

177 
hence "approx (t ` (lnames c1) ` (lnames c2)) s" 

178 
by simp 

179 
hence "approx (t ` (lnames c1) ` (lnames c2)) s'" 

180 
by (rule IfFalse) 

181 
thus ?case by simp 

182 
qed auto 

183 

184 

185 
lemma approx_restrict_inv: 

186 
"\<Turnstile> {approx (t ` (lnames c))} c {approx (t ` (lnames c))}" 

187 
by (simp add: hoare_valid_def big_step_pres_approx_restrict) 

188 

189 
declare assign_simp [simp] 

190 

191 
lemma approx_eq: 

192 
"approx t \<Turnstile> c \<sim> fold c t" 

45015  193 
proof (induction c arbitrary: t) 
44070  194 
case SKIP show ?case by simp 
195 
next 

196 
case Assign 

197 
show ?case by (simp add: equiv_up_to_def) 

198 
next 

199 
case Semi 

200 
thus ?case by (auto intro!: equiv_up_to_semi) 

201 
next 

202 
case If 

203 
thus ?case by (auto intro!: equiv_up_to_if_weak) 

204 
next 

205 
case (While b c) 

206 
hence "approx (t ` ( lnames c)) \<Turnstile> 

207 
WHILE b DO c \<sim> WHILE b DO fold c (t ` ( lnames c))" 

208 
by (auto intro: equiv_up_to_while_weak approx_restrict_inv) 

209 
thus ?case 

210 
by (auto intro: equiv_up_to_weaken approx_map_le) 

211 
qed 

212 

213 

214 
lemma approx_empty [simp]: 

215 
"approx empty = (\<lambda>_. True)" 

216 
by (auto intro!: ext simp: approx_def) 

217 

218 
lemma equiv_sym: 

219 
"c \<sim> c' \<longleftrightarrow> c' \<sim> c" 

220 
by (auto simp add: equiv_def) 

221 

222 
theorem constant_folding_equiv: 

223 
"fold c empty \<sim> c" 

224 
using approx_eq [of empty c] 

225 
by (simp add: equiv_up_to_True equiv_sym) 

226 

227 

228 

44850  229 
subsection {* More ambitious folding including boolean expressions *} 
44070  230 

231 

232 
fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where 

233 
"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)"  

234 
"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)"  

235 
"bsimp_const (Not b) t = not(bsimp_const b t)"  

45200  236 
"bsimp_const (Bc bc) _ = Bc bc" 
44070  237 

238 
theorem bvalsimp_const [simp]: 

239 
assumes "approx t s" 

240 
shows "bval (bsimp_const b t) s = bval b s" 

241 
using assms by (induct b) auto 

242 

45200  243 
lemma not_Bc [simp]: "not (Bc v) = Bc (\<not>v)" 
44070  244 
by (cases v) auto 
245 

45200  246 
lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))" 
44070  247 
by (cases b) auto 
248 

45200  249 
lemma and_Bc_eq: 
250 
"(and a b = Bc v) = 

251 
(a = Bc False \<and> \<not>v \<or> b = Bc False \<and> \<not>v \<or> 

252 
(\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))" 

44070  253 
by (rule and.induct) auto 
254 

45200  255 
lemma less_Bc_eq [simp]: 
256 
"(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))" 

44070  257 
by (rule less.induct) auto 
258 

45200  259 
theorem bvalsimp_const_Bc: 
44070  260 
assumes "approx t s" 
45200  261 
shows "bsimp_const b t = Bc v \<Longrightarrow> bval b s = v" 
44070  262 
using assms 
263 
by (induct b arbitrary: v) 

45200  264 
(auto simp: approx_def and_Bc_eq aval_simp_const_N 
44070  265 
split: bexp.splits bool.splits) 
266 

267 

268 
primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where 

269 
"bdefs SKIP t = t"  

270 
"bdefs (x ::= a) t = 

271 
(case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k)  _ \<Rightarrow> t(x:=None))"  

272 
"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t"  

273 
"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of 

45200  274 
Bc True \<Rightarrow> bdefs c1 t 
275 
 Bc False \<Rightarrow> bdefs c2 t 

44070  276 
 _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))"  
277 
"bdefs (WHILE b DO c) t = t ` (lnames c)" 

278 

279 

280 
primrec bfold where 

281 
"bfold SKIP _ = SKIP"  

282 
"bfold (x ::= a) t = (x ::= (simp_const a t))"  

283 
"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))"  

284 
"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of 

45200  285 
Bc True \<Rightarrow> bfold c1 t 
286 
 Bc False \<Rightarrow> bfold c2 t 

44070  287 
 _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)"  
288 
"bfold (WHILE b DO c) t = (case bsimp_const b t of 

45200  289 
Bc False \<Rightarrow> SKIP 
44070  290 
 _ \<Rightarrow> WHILE bsimp_const b (t ` (lnames c)) DO bfold c (t ` (lnames c)))" 
291 

292 

293 
lemma bdefs_restrict: 

294 
"bdefs c t ` ( lnames c) = t ` ( lnames c)" 

45015  295 
proof (induction c arbitrary: t) 
44070  296 
case (Semi c1 c2) 
297 
hence "bdefs c1 t ` ( lnames c1) = t ` ( lnames c1)" 

298 
by simp 

299 
hence "bdefs c1 t ` ( lnames c1) ` (lnames c2) = 

300 
t ` ( lnames c1) ` (lnames c2)" by simp 

301 
moreover 

302 
from Semi 

303 
have "bdefs c2 (bdefs c1 t) ` ( lnames c2) = 

304 
bdefs c1 t ` ( lnames c2)" 

305 
by simp 

306 
hence "bdefs c2 (bdefs c1 t) ` ( lnames c2) ` ( lnames c1) = 

307 
bdefs c1 t ` ( lnames c2) ` ( lnames c1)" 

308 
by simp 

309 
ultimately 

310 
show ?case by (clarsimp simp: Int_commute) 

311 
next 

312 
case (If b c1 c2) 

313 
hence "bdefs c1 t ` ( lnames c1) = t ` ( lnames c1)" by simp 

314 
hence "bdefs c1 t ` ( lnames c1) ` (lnames c2) = 

315 
t ` ( lnames c1) ` (lnames c2)" by simp 

316 
moreover 

317 
from If 

318 
have "bdefs c2 t ` ( lnames c2) = t ` ( lnames c2)" by simp 

319 
hence "bdefs c2 t ` ( lnames c2) ` (lnames c1) = 

320 
t ` ( lnames c2) ` (lnames c1)" by simp 

321 
ultimately 

322 
show ?case 

323 
by (auto simp: Int_commute intro: merge_restrict 

324 
split: bexp.splits bool.splits) 

325 
qed (auto split: aexp.split bexp.split bool.split) 

326 

327 

328 
lemma big_step_pres_approx_b: 

329 
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 

45015  330 
proof (induction arbitrary: t rule: big_step_induct) 
44070  331 
case Skip thus ?case by simp 
332 
next 

333 
case Assign 

334 
thus ?case 

335 
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) 

336 
next 

337 
case (Semi c1 s1 s2 c2 s3) 

45015  338 
have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems]) 
339 
hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2)) 

44070  340 
thus ?case by simp 
341 
next 

342 
case (IfTrue b s c1 s') 

343 
hence "approx (bdefs c1 t) s'" by simp 

344 
thus ?case using `bval b s` `approx t s` 

45200  345 
by (clarsimp simp: approx_merge bvalsimp_const_Bc 
44070  346 
split: bexp.splits bool.splits) 
347 
next 

348 
case (IfFalse b s c2 s') 

349 
hence "approx (bdefs c2 t) s'" by simp 

350 
thus ?case using `\<not>bval b s` `approx t s` 

45200  351 
by (clarsimp simp: approx_merge bvalsimp_const_Bc 
44070  352 
split: bexp.splits bool.splits) 
353 
next 

354 
case WhileFalse 

355 
thus ?case 

45200  356 
by (clarsimp simp: bvalsimp_const_Bc approx_def restrict_map_def 
44070  357 
split: bexp.splits bool.splits) 
358 
next 

359 
case (WhileTrue b s1 c s2 s3) 

360 
hence "approx (bdefs c t) s2" by simp 

361 
with WhileTrue 

362 
have "approx (bdefs c t ` ( lnames c)) s3" 

363 
by simp 

364 
thus ?case 

365 
by (simp add: bdefs_restrict) 

366 
qed 

367 

368 
corollary approx_bdefs_inv [simp]: 

369 
"\<Turnstile> {approx t} c {approx (bdefs c t)}" 

370 
by (simp add: hoare_valid_def big_step_pres_approx_b) 

371 

372 
lemma bfold_equiv: 

373 
"approx t \<Turnstile> c \<sim> bfold c t" 

45015  374 
proof (induction c arbitrary: t) 
44070  375 
case SKIP show ?case by simp 
376 
next 

377 
case Assign 

378 
thus ?case by (simp add: equiv_up_to_def) 

379 
next 

380 
case Semi 

381 
thus ?case by (auto intro!: equiv_up_to_semi) 

382 
next 

383 
case (If b c1 c2) 

384 
hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 

385 
IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t" 

386 
by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 

387 
thus ?case using If 

45200  388 
by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits 
44070  389 
intro: equiv_up_to_trans) 
390 
next 

391 
case (While b c) 

392 
hence "approx (t ` ( lnames c)) \<Turnstile> 

393 
WHILE b DO c \<sim> 

394 
WHILE bsimp_const b (t ` ( lnames c)) 

395 
DO bfold c (t ` ( lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'") 

396 
by (auto intro: equiv_up_to_while_weak approx_restrict_inv 

397 
simp: bequiv_up_to_def) 

398 
hence "approx t \<Turnstile> ?W \<sim> ?W'" 

399 
by (auto intro: equiv_up_to_weaken approx_map_le) 

400 
thus ?case 

401 
by (auto split: bexp.splits bool.splits 

402 
intro: equiv_up_to_while_False 

45200  403 
simp: bvalsimp_const_Bc) 
44070  404 
qed 
405 

406 

407 
theorem constant_bfolding_equiv: 

408 
"bfold c empty \<sim> c" 

409 
using bfold_equiv [of empty c] 

410 
by (simp add: equiv_up_to_True equiv_sym) 

411 

412 

413 
end 