author  huffman 
Fri, 04 Mar 2005 23:23:47 +0100  
changeset 15577  e16da3068ad6 
parent 15576  efb95d0d01f7 
child 15588  14e3228f18cc 
permissions  rwrr 
1479  1 
(* Title: HOLCF/cont.thy 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1479  3 
Author: Franz Regensburger 
15565  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

5 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

6 
Results about continuity and monotonicity 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

7 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

8 

15577  9 
header {* Continuity and monotonicity *} 
10 

11 
theory Cont 

12 
imports FunCpo 

13 
begin 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

14 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

15 
(* 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

16 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

17 
Now we change the default class! Form now on all untyped typevariables are 
3323
194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents:
2838
diff
changeset

18 
of default class po 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

19 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

20 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

21 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

22 

15565  23 
defaultsort po 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

24 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

25 
consts 
2838
2e908f29bc3d
changed continuous functions from pcpo to cpo (including instances)
slotosch
parents:
1479
diff
changeset

26 
monofun :: "('a => 'b) => bool" (* monotonicity *) 
2e908f29bc3d
changed continuous functions from pcpo to cpo (including instances)
slotosch
parents:
1479
diff
changeset

27 
contlub :: "('a::cpo => 'b::cpo) => bool" (* first cont. def *) 
2e908f29bc3d
changed continuous functions from pcpo to cpo (including instances)
slotosch
parents:
1479
diff
changeset

28 
cont :: "('a::cpo => 'b::cpo) => bool" (* secnd cont. def *) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

29 

1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1150
diff
changeset

30 
defs 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

31 

15565  32 
monofun: "monofun(f) == ! x y. x << y > f(x) << f(y)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

33 

15565  34 
contlub: "contlub(f) == ! Y. chain(Y) > 
3842  35 
f(lub(range(Y))) = lub(range(% i. f(Y(i))))" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

36 

15565  37 
cont: "cont(f) == ! Y. chain(Y) > 
3842  38 
range(% i. f(Y(i))) << f(lub(range(Y)))" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

39 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

40 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

41 
(* the main purpose of cont.thy is to show: *) 
1274  42 
(* monofun(f) & contlub(f) <==> cont(f) *) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

43 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

44 

15565  45 
(* Title: HOLCF/Cont.ML 
46 
ID: $Id$ 

47 
Author: Franz Regensburger 

48 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

49 

50 
Results about continuity and monotonicity 

51 
*) 

52 

53 
(*  *) 

54 
(* access to definition *) 

55 
(*  *) 

56 

57 
lemma contlubI: 

58 
"! Y. chain(Y) > f(lub(range(Y))) = lub(range(%i. f(Y(i))))==> 

59 
contlub(f)" 

60 
apply (unfold contlub) 

61 
apply assumption 

62 
done 

63 

64 
lemma contlubE: 

65 
" contlub(f)==> 

66 
! Y. chain(Y) > f(lub(range(Y))) = lub(range(%i. f(Y(i))))" 

67 
apply (unfold contlub) 

68 
apply assumption 

69 
done 

70 

71 

72 
lemma contI: 

73 
"! Y. chain(Y) > range(% i. f(Y(i))) << f(lub(range(Y))) ==> cont(f)" 

74 

75 
apply (unfold cont) 

76 
apply assumption 

77 
done 

78 

79 
lemma contE: 

80 
"cont(f) ==> ! Y. chain(Y) > range(% i. f(Y(i))) << f(lub(range(Y)))" 

81 
apply (unfold cont) 

82 
apply assumption 

83 
done 

84 

85 

86 
lemma monofunI: 

87 
"! x y. x << y > f(x) << f(y) ==> monofun(f)" 

88 
apply (unfold monofun) 

89 
apply assumption 

90 
done 

91 

92 
lemma monofunE: 

93 
"monofun(f) ==> ! x y. x << y > f(x) << f(y)" 

94 
apply (unfold monofun) 

95 
apply assumption 

96 
done 

97 

98 
(*  *) 

99 
(* the main purpose of cont.thy is to show: *) 

100 
(* monofun(f) & contlub(f) <==> cont(f) *) 

101 
(*  *) 

102 

103 
(*  *) 

104 
(* monotone functions map chains to chains *) 

105 
(*  *) 

106 

107 
lemma ch2ch_monofun: 

108 
"[ monofun(f); chain(Y) ] ==> chain(%i. f(Y(i)))" 

109 
apply (rule chainI) 

110 
apply (erule monofunE [THEN spec, THEN spec, THEN mp]) 

111 
apply (erule chainE) 

112 
done 

113 

114 
(*  *) 

115 
(* monotone functions map upper bound to upper bounds *) 

116 
(*  *) 

117 

118 
lemma ub2ub_monofun: 

119 
"[ monofun(f); range(Y) < u] ==> range(%i. f(Y(i))) < f(u)" 

120 
apply (rule ub_rangeI) 

121 
apply (erule monofunE [THEN spec, THEN spec, THEN mp]) 

122 
apply (erule ub_rangeD) 

123 
done 

124 

125 
(*  *) 

126 
(* left to right: monofun(f) & contlub(f) ==> cont(f) *) 

127 
(*  *) 

128 

129 
lemma monocontlub2cont: 

130 
"[monofun(f);contlub(f)] ==> cont(f)" 

131 
apply (unfold cont) 

132 
apply (intro strip) 

133 
apply (rule thelubE) 

134 
apply (erule ch2ch_monofun) 

135 
apply assumption 

136 
apply (erule contlubE [THEN spec, THEN mp, symmetric]) 

137 
apply assumption 

138 
done 

139 

140 
(*  *) 

141 
(* first a lemma about binary chains *) 

142 
(*  *) 

143 

144 
lemma binchain_cont: "[ cont(f); x << y ] 

145 
==> range(%i::nat. f(if i = 0 then x else y)) << f(y)" 

146 
apply (rule subst) 

147 
prefer 2 apply (erule contE [THEN spec, THEN mp]) 

148 
apply (erule bin_chain) 

149 
apply (rule_tac y = "y" in arg_cong) 

150 
apply (erule lub_bin_chain [THEN thelubI]) 

151 
done 

152 

153 
(*  *) 

154 
(* right to left: cont(f) ==> monofun(f) & contlub(f) *) 

155 
(* part1: cont(f) ==> monofun(f *) 

156 
(*  *) 

157 

158 
lemma cont2mono: "cont(f) ==> monofun(f)" 

159 
apply (unfold monofun) 

160 
apply (intro strip) 

161 
apply (drule binchain_cont [THEN is_ub_lub]) 

162 
apply (auto split add: split_if_asm) 

163 
done 

164 

165 
(*  *) 

166 
(* right to left: cont(f) ==> monofun(f) & contlub(f) *) 

167 
(* part2: cont(f) ==> contlub(f) *) 

168 
(*  *) 

169 

170 
lemma cont2contlub: "cont(f) ==> contlub(f)" 

171 
apply (unfold contlub) 

172 
apply (intro strip) 

173 
apply (rule thelubI [symmetric]) 

174 
apply (erule contE [THEN spec, THEN mp]) 

175 
apply assumption 

176 
done 

177 

178 
(*  *) 

179 
(* monotone functions map finite chains to finite chains *) 

180 
(*  *) 

181 

182 
lemma monofun_finch2finch: 

183 
"[ monofun f; finite_chain Y ] ==> finite_chain (%n. f (Y n))" 

184 
apply (unfold finite_chain_def) 

185 
apply (force elim!: ch2ch_monofun simp add: max_in_chain_def) 

186 
done 

187 

188 
(*  *) 

189 
(* The same holds for continuous functions *) 

190 
(*  *) 

191 

192 
lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard] 

193 
(* [ cont ?f; finite_chain ?Y ] ==> finite_chain (%n. ?f (?Y n)) *) 

194 

195 

196 
(*  *) 

197 
(* The following results are about a curried function that is monotone *) 

198 
(* in both arguments *) 

199 
(*  *) 

200 

201 
lemma ch2ch_MF2L: 

202 
"[monofun(MF2); chain(F)] ==> chain(%i. MF2 (F i) x)" 

203 
apply (erule ch2ch_monofun [THEN ch2ch_fun]) 

204 
apply assumption 

205 
done 

206 

207 

208 
lemma ch2ch_MF2R: 

209 
"[monofun(MF2(f)); chain(Y)] ==> chain(%i. MF2 f (Y i))" 

210 
apply (erule ch2ch_monofun) 

211 
apply assumption 

212 
done 

213 

214 
lemma ch2ch_MF2LR: 

215 
"[monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)] ==> 

216 
chain(%i. MF2(F(i))(Y(i)))" 

217 
apply (rule chainI) 

218 
apply (rule trans_less) 

219 
apply (erule ch2ch_MF2L [THEN chainE]) 

220 
apply assumption 

221 
apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec) 

222 
apply (erule chainE) 

223 
done 

224 

225 

226 
lemma ch2ch_lubMF2R: 

227 
"[monofun(MF2::('a::po=>'b::po=>'c::cpo)); 

228 
!f. monofun(MF2(f)::('b::po=>'c::cpo)); 

229 
chain(F);chain(Y)] ==> 

230 
chain(%j. lub(range(%i. MF2 (F j) (Y i))))" 

231 
apply (rule lub_mono [THEN chainI]) 

232 
apply (rule ch2ch_MF2R, erule spec) 

233 
apply assumption 

234 
apply (rule ch2ch_MF2R, erule spec) 

235 
apply assumption 

236 
apply (intro strip) 

237 
apply (rule chainE) 

238 
apply (erule ch2ch_MF2L) 

239 
apply assumption 

240 
done 

241 

242 

243 
lemma ch2ch_lubMF2L: 

244 
"[monofun(MF2::('a::po=>'b::po=>'c::cpo)); 

245 
!f. monofun(MF2(f)::('b::po=>'c::cpo)); 

246 
chain(F);chain(Y)] ==> 

247 
chain(%i. lub(range(%j. MF2 (F j) (Y i))))" 

248 
apply (rule lub_mono [THEN chainI]) 

249 
apply (erule ch2ch_MF2L) 

250 
apply assumption 

251 
apply (erule ch2ch_MF2L) 

252 
apply assumption 

253 
apply (intro strip) 

254 
apply (rule chainE) 

255 
apply (rule ch2ch_MF2R, erule spec) 

256 
apply assumption 

257 
done 

258 

259 

260 
lemma lub_MF2_mono: 

261 
"[monofun(MF2::('a::po=>'b::po=>'c::cpo)); 

262 
!f. monofun(MF2(f)::('b::po=>'c::cpo)); 

263 
chain(F)] ==> 

264 
monofun(% x. lub(range(% j. MF2 (F j) (x))))" 

265 
apply (rule monofunI) 

266 
apply (intro strip) 

267 
apply (rule lub_mono) 

268 
apply (erule ch2ch_MF2L) 

269 
apply assumption 

270 
apply (erule ch2ch_MF2L) 

271 
apply assumption 

272 
apply (intro strip) 

273 
apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec) 

274 
apply assumption 

275 
done 

276 

277 
lemma ex_lubMF2: 

278 
"[monofun(MF2::('a::po=>'b::po=>'c::cpo)); 

279 
!f. monofun(MF2(f)::('b::po=>'c::cpo)); 

280 
chain(F); chain(Y)] ==> 

281 
lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) = 

282 
lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))" 

283 
apply (rule antisym_less) 

284 
apply (rule is_lub_thelub[OF _ ub_rangeI]) 

285 
apply (erule ch2ch_lubMF2R) 

286 
apply (assumption+) 

287 
apply (rule lub_mono) 

288 
apply (rule ch2ch_MF2R, erule spec) 

289 
apply assumption 

290 
apply (erule ch2ch_lubMF2L) 

291 
apply (assumption+) 

292 
apply (intro strip) 

293 
apply (rule is_ub_thelub) 

294 
apply (erule ch2ch_MF2L) 

295 
apply assumption 

296 
apply (rule is_lub_thelub[OF _ ub_rangeI]) 

297 
apply (erule ch2ch_lubMF2L) 

298 
apply (assumption+) 

299 
apply (rule lub_mono) 

300 
apply (erule ch2ch_MF2L) 

301 
apply assumption 

302 
apply (erule ch2ch_lubMF2R) 

303 
apply (assumption+) 

304 
apply (intro strip) 

305 
apply (rule is_ub_thelub) 

306 
apply (rule ch2ch_MF2R, erule spec) 

307 
apply assumption 

308 
done 

309 

310 

311 
lemma diag_lubMF2_1: 

312 
"[monofun(MF2::('a::po=>'b::po=>'c::cpo)); 

313 
!f. monofun(MF2(f)::('b::po=>'c::cpo)); 

314 
chain(FY);chain(TY)] ==> 

315 
lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) = 

316 
lub(range(%i. MF2(FY(i))(TY(i))))" 

317 
apply (rule antisym_less) 

318 
apply (rule is_lub_thelub[OF _ ub_rangeI]) 

319 
apply (erule ch2ch_lubMF2L) 

320 
apply (assumption+) 

321 
apply (rule lub_mono3) 

322 
apply (erule ch2ch_MF2L) 

323 
apply (assumption+) 

324 
apply (erule ch2ch_MF2LR) 

325 
apply (assumption+) 

326 
apply (rule allI) 

327 
apply (rule_tac m = "i" and n = "ia" in nat_less_cases) 

328 
apply (rule_tac x = "ia" in exI) 

329 
apply (rule chain_mono) 

330 
apply (erule allE) 

331 
apply (erule ch2ch_MF2R) 

332 
apply (assumption+) 

333 
apply (erule ssubst) 

334 
apply (rule_tac x = "ia" in exI) 

335 
apply (rule refl_less) 

336 
apply (rule_tac x = "i" in exI) 

337 
apply (rule chain_mono) 

338 
apply (erule ch2ch_MF2L) 

339 
apply (assumption+) 

340 
apply (rule lub_mono) 

341 
apply (erule ch2ch_MF2LR) 

342 
apply (assumption+) 

343 
apply (erule ch2ch_lubMF2L) 

344 
apply (assumption+) 

345 
apply (intro strip) 

346 
apply (rule is_ub_thelub) 

347 
apply (erule ch2ch_MF2L) 

348 
apply assumption 

349 
done 

350 

351 
lemma diag_lubMF2_2: 

352 
"[monofun(MF2::('a::po=>'b::po=>'c::cpo)); 

353 
!f. monofun(MF2(f)::('b::po=>'c::cpo)); 

354 
chain(FY);chain(TY)] ==> 

355 
lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) = 

356 
lub(range(%i. MF2(FY(i))(TY(i))))" 

357 
apply (rule trans) 

358 
apply (rule ex_lubMF2) 

359 
apply (assumption+) 

360 
apply (erule diag_lubMF2_1) 

361 
apply (assumption+) 

362 
done 

363 

364 

365 
(*  *) 

366 
(* The following results are about a curried function that is continuous *) 

367 
(* in both arguments *) 

368 
(*  *) 

369 

370 
lemma contlub_CF2: 

371 
assumes prem1: "cont(CF2)" 

372 
assumes prem2: "!f. cont(CF2(f))" 

373 
assumes prem3: "chain(FY)" 

374 
assumes prem4: "chain(TY)" 

375 
shows "CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))" 

376 
apply (subst prem1 [THEN cont2contlub, THEN contlubE, THEN spec, THEN mp]) 

377 
apply assumption 

378 
apply (subst thelub_fun) 

379 
apply (rule prem1 [THEN cont2mono [THEN ch2ch_monofun]]) 

380 
apply assumption 

381 
apply (rule trans) 

382 
apply (rule prem2 [THEN spec, THEN cont2contlub, THEN contlubE, THEN spec, THEN mp, THEN ext, THEN arg_cong, THEN arg_cong]) 

383 
apply (rule prem4) 

384 
apply (rule diag_lubMF2_2) 

385 
apply (auto simp add: cont2mono prems) 

386 
done 

387 

388 
(*  *) 

389 
(* The following results are about application for functions in 'a=>'b *) 

390 
(*  *) 

391 

392 
lemma monofun_fun_fun: "f1 << f2 ==> f1(x) << f2(x)" 

393 
apply (erule less_fun [THEN iffD1, THEN spec]) 

394 
done 

395 

396 
lemma monofun_fun_arg: "[monofun(f); x1 << x2] ==> f(x1) << f(x2)" 

397 
apply (erule monofunE [THEN spec, THEN spec, THEN mp]) 

398 
apply assumption 

399 
done 

400 

401 
lemma monofun_fun: "[monofun(f1); monofun(f2); f1 << f2; x1 << x2] ==> f1(x1) << f2(x2)" 

402 
apply (rule trans_less) 

403 
apply (erule monofun_fun_arg) 

404 
apply assumption 

405 
apply (erule monofun_fun_fun) 

406 
done 

407 

408 

409 
(*  *) 

410 
(* The following results are about the propagation of monotonicity and *) 

411 
(* continuity *) 

412 
(*  *) 

413 

414 
lemma mono2mono_MF1L: "[monofun(c1)] ==> monofun(%x. c1 x y)" 

415 
apply (rule monofunI) 

416 
apply (intro strip) 

417 
apply (erule monofun_fun_arg [THEN monofun_fun_fun]) 

418 
apply assumption 

419 
done 

420 

421 
lemma cont2cont_CF1L: "[cont(c1)] ==> cont(%x. c1 x y)" 

422 
apply (rule monocontlub2cont) 

423 
apply (erule cont2mono [THEN mono2mono_MF1L]) 

424 
apply (rule contlubI) 

425 
apply (intro strip) 

426 
apply (frule asm_rl) 

427 
apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst]) 

428 
apply assumption 

429 
apply (subst thelub_fun) 

430 
apply (rule ch2ch_monofun) 

431 
apply (erule cont2mono) 

432 
apply assumption 

433 
apply (rule refl) 

434 
done 

435 

436 
(********* Note "(%x.%y.c1 x y) = c1" ***********) 

437 

438 
lemma mono2mono_MF1L_rev: "!y. monofun(%x. c1 x y) ==> monofun(c1)" 

439 
apply (rule monofunI) 

440 
apply (intro strip) 

441 
apply (rule less_fun [THEN iffD2]) 

442 
apply (blast dest: monofunE) 

443 
done 

444 

445 
lemma cont2cont_CF1L_rev: "!y. cont(%x. c1 x y) ==> cont(c1)" 

446 
apply (rule monocontlub2cont) 

447 
apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev]) 

448 
apply (erule spec) 

449 
apply (rule contlubI) 

450 
apply (intro strip) 

451 
apply (rule ext) 

452 
apply (subst thelub_fun) 

453 
apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev, THEN ch2ch_monofun]) 

454 
apply (erule spec) 

455 
apply assumption 

456 
apply (blast dest: cont2contlub [THEN contlubE]) 

457 
done 

458 

459 
(*  *) 

460 
(* What D.A.Schmidt calls continuity of abstraction *) 

461 
(* never used here *) 

462 
(*  *) 

463 

464 
lemma contlub_abstraction: 

465 
"[chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)] ==> 

466 
(%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))" 

467 
apply (rule trans) 

468 
prefer 2 apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp]) 

469 
prefer 2 apply (assumption) 

470 
apply (erule cont2cont_CF1L_rev) 

471 
apply (rule ext) 

472 
apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp, symmetric]) 

473 
apply (erule spec) 

474 
apply assumption 

475 
done 

476 

477 
lemma mono2mono_app: "[monofun(ft);!x. monofun(ft(x));monofun(tt)] ==> 

478 
monofun(%x.(ft(x))(tt(x)))" 

479 
apply (rule monofunI) 

480 
apply (intro strip) 

481 
apply (rule_tac ?f1.0 = "ft(x)" and ?f2.0 = "ft(y)" in monofun_fun) 

482 
apply (erule spec) 

483 
apply (erule spec) 

484 
apply (erule monofunE [THEN spec, THEN spec, THEN mp]) 

485 
apply assumption 

486 
apply (erule monofunE [THEN spec, THEN spec, THEN mp]) 

487 
apply assumption 

488 
done 

489 

490 

491 
lemma cont2contlub_app: "[cont(ft);!x. cont(ft(x));cont(tt)] ==> contlub(%x.(ft(x))(tt(x)))" 

492 
apply (rule contlubI) 

493 
apply (intro strip) 

494 
apply (rule_tac f3 = "tt" in contlubE [THEN spec, THEN mp, THEN ssubst]) 

495 
apply (erule cont2contlub) 

496 
apply assumption 

497 
apply (rule contlub_CF2) 

498 
apply (assumption+) 

499 
apply (erule cont2mono [THEN ch2ch_monofun]) 

500 
apply assumption 

501 
done 

502 

503 

504 
lemma cont2cont_app: "[cont(ft); !x. cont(ft(x)); cont(tt)] ==> cont(%x.(ft(x))(tt(x)))" 

505 
apply (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) 

506 
done 

507 

508 

509 
lemmas cont2cont_app2 = cont2cont_app[OF _ allI] 

510 
(* [ cont ?ft; !!x. cont (?ft x); cont ?tt ] ==> *) 

511 
(* cont (%x. ?ft x (?tt x)) *) 

512 

513 

514 
(*  *) 

515 
(* The identity function is continuous *) 

516 
(*  *) 

517 

518 
lemma cont_id: "cont(% x. x)" 

519 
apply (rule contI) 

520 
apply (intro strip) 

521 
apply (erule thelubE) 

522 
apply (rule refl) 

523 
done 

524 

525 
(*  *) 

526 
(* constant functions are continuous *) 

527 
(*  *) 

528 

529 
lemma cont_const: "cont(%x. c)" 

530 
apply (unfold cont) 

531 
apply (intro strip) 

532 
apply (blast intro: is_lubI ub_rangeI dest: ub_rangeD) 

533 
done 

534 

535 

536 
lemma cont2cont_app3: "[cont(f); cont(t) ] ==> cont(%x. f(t(x)))" 

537 
apply (best intro: cont2cont_app2 cont_const) 

538 
done 

539 

540 
(*  *) 

541 
(* A nonemptyness result for Cfun *) 

542 
(*  *) 

543 

544 
lemma CfunI: "?x:Collect cont" 

545 
apply (rule CollectI) 

546 
apply (rule cont_const) 

547 
done 

548 

549 
(*  *) 

550 
(* some properties of flat *) 

551 
(*  *) 

552 

553 
lemma flatdom2monofun: "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" 

554 

555 
apply (unfold monofun) 

556 
apply (intro strip) 

557 
apply (drule ax_flat [THEN spec, THEN spec, THEN mp]) 

558 
apply auto 

559 
done 

560 

561 
declare range_composition [simp del] 

562 
lemma chfindom_monofun2cont: "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" 

563 
apply (rule monocontlub2cont) 

564 
apply assumption 

565 
apply (rule contlubI) 

566 
apply (intro strip) 

567 
apply (frule chfin2finch) 

568 
apply (rule antisym_less) 

569 
apply (clarsimp simp add: finite_chain_def maxinch_is_thelub) 

570 
apply (rule is_ub_thelub) 

571 
apply (erule ch2ch_monofun) 

572 
apply assumption 

573 
apply (drule monofun_finch2finch[COMP swap_prems_rl]) 

574 
apply assumption 

575 
apply (simp add: finite_chain_def) 

576 
apply (erule conjE) 

577 
apply (erule exE) 

578 
apply (simp add: maxinch_is_thelub) 

579 
apply (erule monofunE [THEN spec, THEN spec, THEN mp]) 

580 
apply (erule is_ub_thelub) 

581 
done 

582 

583 
lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard] 

584 
(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *) 

585 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

586 
end 