author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45606  b1e1508643b1 
child 48564  eaa36c0d620a 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/ex/Hoare.thy 
1479  2 
Author: Franz Regensburger 
244  3 

12036  4 
Theory for an example by C.A.R. Hoare 
244  5 

17291  6 
p x = if b1 x 
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset

7 
then p (g x) 
244  8 
else x fi 
9 

17291  10 
q x = if b1 x orelse b2 x 
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset

11 
then q (g x) 
244  12 
else x fi 
13 

17291  14 
Prove: for all b1 b2 g . 
15 
q o p = q 

244  16 

17 
In order to get a nice notation we fix the functions b1,b2 and g in the 

18 
signature of this example 

19 

20 
*) 

21 

17291  22 
theory Hoare 
23 
imports HOLCF 

24 
begin 

244  25 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset

26 
axiomatization 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset

27 
b1 :: "'a > tr" and 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset

28 
b2 :: "'a > tr" and 
17291  29 
g :: "'a > 'a" 
244  30 

19763  31 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

32 
p :: "'a > 'a" where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40028
diff
changeset

33 
"p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x)" 
244  34 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

35 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

36 
q :: "'a > 'a" where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40028
diff
changeset

37 
"q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x)" 
244  38 

19742  39 

40 
(*  pure HOLCF logic, some little lemmas  *) 

41 

42 
lemma hoare_lemma2: "b~=TT ==> b=FF  b=UU" 

43 
apply (rule Exh_tr [THEN disjE]) 

44 
apply blast+ 

45 
done 

46 

47 
lemma hoare_lemma3: " (ALL k. b1$(iterate k$g$x) = TT)  (EX k. b1$(iterate k$g$x)~=TT)" 

48 
apply blast 

49 
done 

50 

51 
lemma hoare_lemma4: "(EX k. b1$(iterate k$g$x) ~= TT) ==> 

52 
EX k. b1$(iterate k$g$x) = FF  b1$(iterate k$g$x) = UU" 

53 
apply (erule exE) 

54 
apply (rule exI) 

55 
apply (rule hoare_lemma2) 

56 
apply assumption 

57 
done 

58 

59 
lemma hoare_lemma5: "[(EX k. b1$(iterate k$g$x) ~= TT); 

60 
k=Least(%n. b1$(iterate n$g$x) ~= TT)] ==> 

61 
b1$(iterate k$g$x)=FF  b1$(iterate k$g$x)=UU" 

62 
apply hypsubst 

63 
apply (rule hoare_lemma2) 

64 
apply (erule exE) 

65 
apply (erule LeastI) 

66 
done 

67 

68 
lemma hoare_lemma6: "b=UU ==> b~=TT" 

69 
apply hypsubst 

70 
apply (rule dist_eq_tr) 

71 
done 

72 

73 
lemma hoare_lemma7: "b=FF ==> b~=TT" 

74 
apply hypsubst 

75 
apply (rule dist_eq_tr) 

76 
done 

77 

78 
lemma hoare_lemma8: "[(EX k. b1$(iterate k$g$x) ~= TT); 

79 
k=Least(%n. b1$(iterate n$g$x) ~= TT)] ==> 

80 
ALL m. m < k > b1$(iterate m$g$x)=TT" 

81 
apply hypsubst 

82 
apply (erule exE) 

83 
apply (intro strip) 

84 
apply (rule_tac p = "b1$ (iterate m$g$x) " in trE) 

85 
prefer 2 apply (assumption) 

26334  86 
apply (rule le_less_trans [THEN less_irrefl [THEN notE]]) 
19742  87 
prefer 2 apply (assumption) 
88 
apply (rule Least_le) 

89 
apply (erule hoare_lemma6) 

26334  90 
apply (rule le_less_trans [THEN less_irrefl [THEN notE]]) 
19742  91 
prefer 2 apply (assumption) 
92 
apply (rule Least_le) 

93 
apply (erule hoare_lemma7) 

94 
done 

95 

96 

97 
lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU" 

40429  98 
by (rule strictI) 
19742  99 

100 

101 
(*  access to definitions  *) 

102 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40028
diff
changeset

103 
lemma p_def3: "p$x = If b1$x then p$(g$x) else x" 
19742  104 
apply (rule trans) 
19763  105 
apply (rule p_def [THEN eq_reflection, THEN fix_eq3]) 
19742  106 
apply simp 
107 
done 

108 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40028
diff
changeset

109 
lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x" 
19742  110 
apply (rule trans) 
19763  111 
apply (rule q_def [THEN eq_reflection, THEN fix_eq3]) 
19742  112 
apply simp 
113 
done 

114 

115 
(**  proofs about iterations of p and q  **) 

116 

117 
lemma hoare_lemma9: "(ALL m. m< Suc k > b1$(iterate m$g$x)=TT) > 

118 
p$(iterate k$g$x)=p$x" 

119 
apply (induct_tac k) 

120 
apply (simp (no_asm)) 

121 
apply (simp (no_asm)) 

122 
apply (intro strip) 

123 
apply (rule_tac s = "p$ (iterate n$g$x) " in trans) 

124 
apply (rule trans) 

125 
apply (rule_tac [2] p_def3 [symmetric]) 

126 
apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst) 

127 
apply (rule mp) 

128 
apply (erule spec) 

129 
apply (simp (no_asm) add: less_Suc_eq) 

130 
apply simp 

131 
apply (erule mp) 

132 
apply (intro strip) 

133 
apply (rule mp) 

134 
apply (erule spec) 

135 
apply (erule less_trans) 

136 
apply simp 

137 
done 

138 

139 
lemma hoare_lemma24: "(ALL m. m< Suc k > b1$(iterate m$g$x)=TT) > 

140 
q$(iterate k$g$x)=q$x" 

141 
apply (induct_tac k) 

142 
apply (simp (no_asm)) 

143 
apply (simp (no_asm) add: less_Suc_eq) 

144 
apply (intro strip) 

145 
apply (rule_tac s = "q$ (iterate n$g$x) " in trans) 

146 
apply (rule trans) 

147 
apply (rule_tac [2] q_def3 [symmetric]) 

148 
apply (rule_tac s = "TT" and t = "b1$ (iterate n$g$x) " in ssubst) 

149 
apply blast 

150 
apply simp 

151 
apply (erule mp) 

152 
apply (intro strip) 

153 
apply (fast dest!: less_Suc_eq [THEN iffD1]) 

154 
done 

155 

156 
(*  results about p for case (EX k. b1$(iterate k$g$x)~=TT)  *) 

157 

158 
lemma hoare_lemma10: 

159 
"EX k. b1$(iterate k$g$x) ~= TT 

160 
==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> p$(iterate k$g$x) = p$x" 

161 
by (rule hoare_lemma8 [THEN hoare_lemma9 [THEN mp]]) 

162 

163 
lemma hoare_lemma11: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 

164 
k=(LEAST n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x)=FF 

165 
> p$x = iterate k$g$x" 

166 
apply (case_tac "k") 

167 
apply hypsubst 

168 
apply (simp (no_asm)) 

169 
apply (intro strip) 

170 
apply (erule conjE) 

171 
apply (rule trans) 

172 
apply (rule p_def3) 

173 
apply simp 

174 
apply hypsubst 

175 
apply (intro strip) 

176 
apply (erule conjE) 

177 
apply (rule trans) 

178 
apply (erule hoare_lemma10 [symmetric]) 

179 
apply assumption 

180 
apply (rule trans) 

181 
apply (rule p_def3) 

182 
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) 

183 
apply (rule hoare_lemma8 [THEN spec, THEN mp]) 

184 
apply assumption 

185 
apply assumption 

186 
apply (simp (no_asm)) 

40028  187 
apply (simp (no_asm)) 
19742  188 
apply (rule trans) 
189 
apply (rule p_def3) 

190 
apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric]) 

191 
apply (erule_tac s = "FF" in ssubst) 

192 
apply simp 

193 
done 

194 

195 
lemma hoare_lemma12: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 

196 
k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU 

197 
> p$x = UU" 

198 
apply (case_tac "k") 

199 
apply hypsubst 

200 
apply (simp (no_asm)) 

201 
apply (intro strip) 

202 
apply (erule conjE) 

203 
apply (rule trans) 

204 
apply (rule p_def3) 

205 
apply simp 

206 
apply hypsubst 

207 
apply (simp (no_asm)) 

208 
apply (intro strip) 

209 
apply (erule conjE) 

210 
apply (rule trans) 

211 
apply (rule hoare_lemma10 [symmetric]) 

212 
apply assumption 

213 
apply assumption 

214 
apply (rule trans) 

215 
apply (rule p_def3) 

216 
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) 

217 
apply (rule hoare_lemma8 [THEN spec, THEN mp]) 

218 
apply assumption 

219 
apply assumption 

220 
apply (simp (no_asm)) 

40028  221 
apply (simp) 
19742  222 
apply (rule trans) 
223 
apply (rule p_def3) 

224 
apply simp 

225 
done 

226 

227 
(*  results about p for case (ALL k. b1$(iterate k$g$x)=TT)  *) 

228 

229 
lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU" 

19763  230 
apply (rule p_def [THEN eq_reflection, THEN def_fix_ind]) 
35948  231 
apply simp 
232 
apply simp 

19742  233 
apply (simp (no_asm)) 
234 
apply (rule allI) 

235 
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst) 

236 
apply (erule spec) 

40028  237 
apply (simp) 
19742  238 
apply (rule iterate_Suc [THEN subst]) 
239 
apply (erule spec) 

240 
done 

241 

242 
lemma hoare_lemma16: "(ALL k. b1$(iterate k$g$x)=TT) ==> p$x = UU" 

243 
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst]) 

244 
apply (erule fernpass_lemma [THEN spec]) 

245 
done 

246 

247 
(*  results about q for case (ALL k. b1$(iterate k$g$x)=TT)  *) 

248 

249 
lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU" 

19763  250 
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind]) 
35948  251 
apply simp 
252 
apply simp 

19742  253 
apply (rule allI) 
254 
apply (simp (no_asm)) 

255 
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst) 

256 
apply (erule spec) 

40028  257 
apply (simp) 
19742  258 
apply (rule iterate_Suc [THEN subst]) 
259 
apply (erule spec) 

260 
done 

261 

262 
lemma hoare_lemma18: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$x = UU" 

263 
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst]) 

264 
apply (erule hoare_lemma17 [THEN spec]) 

265 
done 

266 

267 
lemma hoare_lemma19: 

268 
"(ALL k. (b1::'a>tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU  (ALL y. b1$(y::'a)=TT)" 

269 
apply (rule flat_codom) 

270 
apply (rule_tac t = "x1" in iterate_0 [THEN subst]) 

271 
apply (erule spec) 

272 
done 

273 

274 
lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU" 

19763  275 
apply (rule q_def [THEN eq_reflection, THEN def_fix_ind]) 
35948  276 
apply simp 
277 
apply simp 

19742  278 
apply (rule allI) 
279 
apply (simp (no_asm)) 

280 
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst) 

281 
apply (erule spec) 

40028  282 
apply (simp) 
19742  283 
apply (rule iterate_Suc [THEN subst]) 
284 
apply (erule spec) 

285 
done 

286 

287 
lemma hoare_lemma21: "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU" 

288 
apply (rule_tac F1 = "g" and t = "x" in iterate_0 [THEN subst]) 

289 
apply (erule hoare_lemma20 [THEN spec]) 

290 
done 

291 

292 
lemma hoare_lemma22: "b1$(UU::'a)=UU ==> q$(UU::'a) = UU" 

293 
apply (subst q_def3) 

294 
apply simp 

295 
done 

296 

297 
(*  results about q for case (EX k. b1$(iterate k$g$x) ~= TT)  *) 

298 

299 
lemma hoare_lemma25: "EX k. b1$(iterate k$g$x) ~= TT 

300 
==> Suc k = (LEAST n. b1$(iterate n$g$x) ~= TT) ==> q$(iterate k$g$x) = q$x" 

301 
by (rule hoare_lemma8 [THEN hoare_lemma24 [THEN mp]]) 

302 

303 
lemma hoare_lemma26: "(EX n. b1$(iterate n$g$x)~=TT) ==> 

304 
k=Least(%n. b1$(iterate n$g$x) ~= TT) & b1$(iterate k$g$x) =FF 

305 
> q$x = q$(iterate k$g$x)" 

306 
apply (case_tac "k") 

307 
apply hypsubst 

308 
apply (intro strip) 

309 
apply (simp (no_asm)) 

310 
apply hypsubst 

311 
apply (intro strip) 

312 
apply (erule conjE) 

313 
apply (rule trans) 

314 
apply (rule hoare_lemma25 [symmetric]) 

315 
apply assumption 

316 
apply assumption 

317 
apply (rule trans) 

318 
apply (rule q_def3) 

319 
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) 

320 
apply (rule hoare_lemma8 [THEN spec, THEN mp]) 

321 
apply assumption 

322 
apply assumption 

323 
apply (simp (no_asm)) 

324 
apply (simp (no_asm)) 

325 
done 

326 

327 

328 
lemma hoare_lemma27: "(EX n. b1$(iterate n$g$x) ~= TT) ==> 

329 
k=Least(%n. b1$(iterate n$g$x)~=TT) & b1$(iterate k$g$x)=UU 

330 
> q$x = UU" 

331 
apply (case_tac "k") 

332 
apply hypsubst 

333 
apply (simp (no_asm)) 

334 
apply (intro strip) 

335 
apply (erule conjE) 

336 
apply (subst q_def3) 

40028  337 
apply (simp) 
19742  338 
apply hypsubst 
339 
apply (simp (no_asm)) 

340 
apply (intro strip) 

341 
apply (erule conjE) 

342 
apply (rule trans) 

343 
apply (rule hoare_lemma25 [symmetric]) 

344 
apply assumption 

345 
apply assumption 

346 
apply (rule trans) 

347 
apply (rule q_def3) 

348 
apply (rule_tac s = "TT" and t = "b1$ (iterate nat$g$x) " in ssubst) 

349 
apply (rule hoare_lemma8 [THEN spec, THEN mp]) 

350 
apply assumption 

351 
apply assumption 

352 
apply (simp (no_asm)) 

40028  353 
apply (simp) 
19742  354 
apply (rule trans) 
355 
apply (rule q_def3) 

40028  356 
apply (simp) 
19742  357 
done 
358 

359 
(*  (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q  *) 

360 

361 
lemma hoare_lemma23: "(ALL k. b1$(iterate k$g$x)=TT) ==> q$(p$x) = q$x" 

362 
apply (subst hoare_lemma16) 

363 
apply assumption 

364 
apply (rule hoare_lemma19 [THEN disjE]) 

365 
apply assumption 

366 
apply (simplesubst hoare_lemma18) 

367 
apply assumption 

368 
apply (simplesubst hoare_lemma22) 

369 
apply assumption 

370 
apply (rule refl) 

371 
apply (simplesubst hoare_lemma21) 

372 
apply assumption 

373 
apply (simplesubst hoare_lemma21) 

374 
apply assumption 

375 
apply (rule refl) 

376 
done 

377 

378 
(*  EX k. b1~(iterate k$g$x) ~= TT ==> q o p = q  *) 

379 

380 
lemma hoare_lemma29: "EX k. b1$(iterate k$g$x) ~= TT ==> q$(p$x) = q$x" 

381 
apply (rule hoare_lemma5 [THEN disjE]) 

382 
apply assumption 

383 
apply (rule refl) 

384 
apply (subst hoare_lemma11 [THEN mp]) 

385 
apply assumption 

386 
apply (rule conjI) 

387 
apply (rule refl) 

388 
apply assumption 

389 
apply (rule hoare_lemma26 [THEN mp, THEN subst]) 

390 
apply assumption 

391 
apply (rule conjI) 

392 
apply (rule refl) 

393 
apply assumption 

394 
apply (rule refl) 

395 
apply (subst hoare_lemma12 [THEN mp]) 

396 
apply assumption 

397 
apply (rule conjI) 

398 
apply (rule refl) 

399 
apply assumption 

400 
apply (subst hoare_lemma22) 

401 
apply (subst hoare_lemma28) 

402 
apply assumption 

403 
apply (rule refl) 

404 
apply (rule sym) 

405 
apply (subst hoare_lemma27 [THEN mp]) 

406 
apply assumption 

407 
apply (rule conjI) 

408 
apply (rule refl) 

409 
apply assumption 

410 
apply (rule refl) 

411 
done 

412 

413 
(*  the main proof q o p = q  *) 

414 

415 
theorem hoare_main: "q oo p = q" 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
35948
diff
changeset

416 
apply (rule cfun_eqI) 
19742  417 
apply (subst cfcomp2) 
418 
apply (rule hoare_lemma3 [THEN disjE]) 

419 
apply (erule hoare_lemma23) 

420 
apply (erule hoare_lemma29) 

421 
done 

17291  422 

244  423 
end 