author  huffman 
Tue, 08 Mar 2005 00:00:49 +0100  
changeset 15588  14e3228f18cc 
parent 15577  e16da3068ad6 
child 15600  a59f07556a8d 
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 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

15 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

17 
of default class po 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

19 

15565  20 
defaultsort po 
243
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 
consts 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

23 
monofun :: "('a => 'b) => bool"  "monotonicity" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

24 
contlub :: "('a::cpo => 'b::cpo) => bool"  "first cont. def" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

25 
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

26 

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

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

28 

15565  29 
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

30 

15565  31 
contlub: "contlub(f) == ! Y. chain(Y) > 
3842  32 
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

33 

15565  34 
cont: "cont(f) == ! Y. chain(Y) > 
3842  35 
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

36 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

37 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

38 
the main purpose of cont.thy is to show: 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

39 
@{prop "monofun(f) & contlub(f) == cont(f)"} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

41 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

42 
text {* access to definition *} 
15565  43 

44 
lemma contlubI: 

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

46 
contlub(f)" 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

47 
by (unfold contlub) 
15565  48 

49 
lemma contlubE: 

50 
" contlub(f)==> 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

52 
by (unfold contlub) 
15565  53 

54 
lemma contI: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

56 
by (unfold cont) 
15565  57 

58 
lemma contE: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

60 
by (unfold cont) 
15565  61 

62 
lemma monofunI: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

64 
by (unfold monofun) 
15565  65 

66 
lemma monofunE: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

68 
by (unfold monofun) 
15565  69 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

70 
text {* monotone functions map chains to chains *} 
15565  71 

72 
lemma ch2ch_monofun: 

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

74 
apply (rule chainI) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

75 
apply (erule monofunE [rule_format]) 
15565  76 
apply (erule chainE) 
77 
done 

78 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

79 
text {* monotone functions map upper bound to upper bounds *} 
15565  80 

81 
lemma ub2ub_monofun: 

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

83 
apply (rule ub_rangeI) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

84 
apply (erule monofunE [rule_format]) 
15565  85 
apply (erule ub_rangeD) 
86 
done 

87 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

88 
text {* left to right: @{prop "monofun(f) & contlub(f) ==> cont(f)"} *} 
15565  89 

90 
lemma monocontlub2cont: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

92 
apply (rule contI [rule_format]) 
15565  93 
apply (rule thelubE) 
94 
apply (erule ch2ch_monofun) 

95 
apply assumption 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

96 
apply (erule contlubE [rule_format, symmetric]) 
15565  97 
apply assumption 
98 
done 

99 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

100 
text {* first a lemma about binary chains *} 
15565  101 

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

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

104 
apply (rule subst) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

105 
prefer 2 apply (erule contE [rule_format]) 
15565  106 
apply (erule bin_chain) 
107 
apply (rule_tac y = "y" in arg_cong) 

108 
apply (erule lub_bin_chain [THEN thelubI]) 

109 
done 

110 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

111 
text {* right to left: @{prop "cont(f) ==> monofun(f) & contlub(f)"} *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

112 
text {* part1: @{prop "cont(f) ==> monofun(f)"} *} 
15565  113 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

115 
apply (rule monofunI [rule_format]) 
15565  116 
apply (drule binchain_cont [THEN is_ub_lub]) 
117 
apply (auto split add: split_if_asm) 

118 
done 

119 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

120 
text {* right to left: @{prop "cont(f) ==> monofun(f) & contlub(f)"} *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

121 
text {* part2: @{prop "cont(f) ==> contlub(f)"} *} 
15565  122 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

124 
apply (rule contlubI [rule_format]) 
15565  125 
apply (rule thelubI [symmetric]) 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

126 
apply (erule contE [rule_format]) 
15565  127 
apply assumption 
128 
done 

129 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

130 
text {* monotone functions map finite chains to finite chains *} 
15565  131 

132 
lemma monofun_finch2finch: 

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

134 
apply (unfold finite_chain_def) 

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

136 
done 

137 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

138 
text {* The same holds for continuous functions *} 
15565  139 

140 
lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard] 

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

142 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

143 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

144 
The following results are about a curried function that is monotone 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

145 
in both arguments 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

146 
*} 
15565  147 

148 
lemma ch2ch_MF2L: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

150 
by (erule ch2ch_monofun [THEN ch2ch_fun]) 
15565  151 

152 
lemma ch2ch_MF2R: 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

154 
by (erule ch2ch_monofun) 
15565  155 

156 
lemma ch2ch_MF2LR: 

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

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

159 
apply (rule chainI) 

160 
apply (rule trans_less) 

161 
apply (erule ch2ch_MF2L [THEN chainE]) 

162 
apply assumption 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

163 
apply (rule monofunE [rule_format], erule spec) 
15565  164 
apply (erule chainE) 
165 
done 

166 

167 
lemma ch2ch_lubMF2R: 

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

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

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

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

172 
apply (rule lub_mono [THEN chainI]) 

173 
apply (rule ch2ch_MF2R, erule spec) 

174 
apply assumption 

175 
apply (rule ch2ch_MF2R, erule spec) 

176 
apply assumption 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

177 
apply (rule allI) 
15565  178 
apply (rule chainE) 
179 
apply (erule ch2ch_MF2L) 

180 
apply assumption 

181 
done 

182 

183 
lemma ch2ch_lubMF2L: 

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

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

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

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

188 
apply (rule lub_mono [THEN chainI]) 

189 
apply (erule ch2ch_MF2L) 

190 
apply assumption 

191 
apply (erule ch2ch_MF2L) 

192 
apply assumption 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

193 
apply (rule allI) 
15565  194 
apply (rule chainE) 
195 
apply (rule ch2ch_MF2R, erule spec) 

196 
apply assumption 

197 
done 

198 

199 
lemma lub_MF2_mono: 

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

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

202 
chain(F)] ==> 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

204 
apply (rule monofunI [rule_format]) 
15565  205 
apply (rule lub_mono) 
206 
apply (erule ch2ch_MF2L) 

207 
apply assumption 

208 
apply (erule ch2ch_MF2L) 

209 
apply assumption 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

210 
apply (rule allI) 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

211 
apply (rule monofunE [rule_format], erule spec) 
15565  212 
apply assumption 
213 
done 

214 

215 
lemma ex_lubMF2: 

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

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

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

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

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

221 
apply (rule antisym_less) 

222 
apply (rule is_lub_thelub[OF _ ub_rangeI]) 

223 
apply (erule ch2ch_lubMF2R) 

224 
apply (assumption+) 

225 
apply (rule lub_mono) 

226 
apply (rule ch2ch_MF2R, erule spec) 

227 
apply assumption 

228 
apply (erule ch2ch_lubMF2L) 

229 
apply (assumption+) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

230 
apply (rule allI) 
15565  231 
apply (rule is_ub_thelub) 
232 
apply (erule ch2ch_MF2L) 

233 
apply assumption 

234 
apply (rule is_lub_thelub[OF _ ub_rangeI]) 

235 
apply (erule ch2ch_lubMF2L) 

236 
apply (assumption+) 

237 
apply (rule lub_mono) 

238 
apply (erule ch2ch_MF2L) 

239 
apply assumption 

240 
apply (erule ch2ch_lubMF2R) 

241 
apply (assumption+) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

242 
apply (rule allI) 
15565  243 
apply (rule is_ub_thelub) 
244 
apply (rule ch2ch_MF2R, erule spec) 

245 
apply assumption 

246 
done 

247 

248 
lemma diag_lubMF2_1: 

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

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

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

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

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

254 
apply (rule antisym_less) 

255 
apply (rule is_lub_thelub[OF _ ub_rangeI]) 

256 
apply (erule ch2ch_lubMF2L) 

257 
apply (assumption+) 

258 
apply (rule lub_mono3) 

259 
apply (erule ch2ch_MF2L) 

260 
apply (assumption+) 

261 
apply (erule ch2ch_MF2LR) 

262 
apply (assumption+) 

263 
apply (rule allI) 

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

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

266 
apply (rule chain_mono) 

267 
apply (erule allE) 

268 
apply (erule ch2ch_MF2R) 

269 
apply (assumption+) 

270 
apply (erule ssubst) 

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

272 
apply (rule refl_less) 

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

274 
apply (rule chain_mono) 

275 
apply (erule ch2ch_MF2L) 

276 
apply (assumption+) 

277 
apply (rule lub_mono) 

278 
apply (erule ch2ch_MF2LR) 

279 
apply (assumption+) 

280 
apply (erule ch2ch_lubMF2L) 

281 
apply (assumption+) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

282 
apply (rule allI) 
15565  283 
apply (rule is_ub_thelub) 
284 
apply (erule ch2ch_MF2L) 

285 
apply assumption 

286 
done 

287 

288 
lemma diag_lubMF2_2: 

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

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

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

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

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

294 
apply (rule trans) 

295 
apply (rule ex_lubMF2) 

296 
apply (assumption+) 

297 
apply (erule diag_lubMF2_1) 

298 
apply (assumption+) 

299 
done 

300 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

301 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

302 
The following results are about a curried function that is continuous 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

303 
in both arguments 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

304 
*} 
15565  305 

306 
lemma contlub_CF2: 

307 
assumes prem1: "cont(CF2)" 

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

309 
assumes prem3: "chain(FY)" 

310 
assumes prem4: "chain(TY)" 

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

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

313 
apply assumption 

314 
apply (subst thelub_fun) 

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

316 
apply assumption 

317 
apply (rule trans) 

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

319 
apply (rule prem4) 

320 
apply (rule diag_lubMF2_2) 

321 
apply (auto simp add: cont2mono prems) 

322 
done 

323 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

324 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

325 
The following results are about application for functions in @{typ "'a=>'b"} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

326 
*} 
15565  327 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

329 
by (erule less_fun [THEN iffD1, THEN spec]) 
15565  330 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

332 
by (erule monofunE [THEN spec, THEN spec, THEN mp]) 
15565  333 

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

335 
apply (rule trans_less) 

336 
apply (erule monofun_fun_arg) 

337 
apply assumption 

338 
apply (erule monofun_fun_fun) 

339 
done 

340 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

341 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

342 
The following results are about the propagation of monotonicity and 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

343 
continuity 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

344 
*} 
15565  345 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

347 
apply (rule monofunI [rule_format]) 
15565  348 
apply (erule monofun_fun_arg [THEN monofun_fun_fun]) 
349 
apply assumption 

350 
done 

351 

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

353 
apply (rule monocontlub2cont) 

354 
apply (erule cont2mono [THEN mono2mono_MF1L]) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

355 
apply (rule contlubI [rule_format]) 
15565  356 
apply (frule asm_rl) 
357 
apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst]) 

358 
apply assumption 

359 
apply (subst thelub_fun) 

360 
apply (rule ch2ch_monofun) 

361 
apply (erule cont2mono) 

362 
apply assumption 

363 
apply (rule refl) 

364 
done 

365 

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

367 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

369 
apply (rule monofunI [rule_format]) 
15565  370 
apply (rule less_fun [THEN iffD2]) 
371 
apply (blast dest: monofunE) 

372 
done 

373 

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

375 
apply (rule monocontlub2cont) 

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

377 
apply (erule spec) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

378 
apply (rule contlubI [rule_format]) 
15565  379 
apply (rule ext) 
380 
apply (subst thelub_fun) 

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

382 
apply (erule spec) 

383 
apply assumption 

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

385 
done 

386 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

387 
text {* 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

388 
What D.A.Schmidt calls continuity of abstraction 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

389 
never used here 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

390 
*} 
15565  391 

392 
lemma contlub_abstraction: 

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

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

395 
apply (rule trans) 

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

397 
prefer 2 apply (assumption) 

398 
apply (erule cont2cont_CF1L_rev) 

399 
apply (rule ext) 

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

401 
apply (erule spec) 

402 
apply assumption 

403 
done 

404 

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

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

407 
apply (rule monofunI [rule_format]) 
15565  408 
apply (rule_tac ?f1.0 = "ft(x)" and ?f2.0 = "ft(y)" in monofun_fun) 
409 
apply (erule spec) 

410 
apply (erule spec) 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

411 
apply (erule monofunE [rule_format]) 
15565  412 
apply assumption 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

413 
apply (erule monofunE [rule_format]) 
15565  414 
apply assumption 
415 
done 

416 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

418 
apply (rule contlubI [rule_format]) 
15565  419 
apply (rule_tac f3 = "tt" in contlubE [THEN spec, THEN mp, THEN ssubst]) 
420 
apply (erule cont2contlub) 

421 
apply assumption 

422 
apply (rule contlub_CF2) 

423 
apply (assumption+) 

424 
apply (erule cont2mono [THEN ch2ch_monofun]) 

425 
apply assumption 

426 
done 

427 

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

429 
apply (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) 

430 
done 

431 

432 
lemmas cont2cont_app2 = cont2cont_app[OF _ allI] 

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

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

435 

436 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

437 
text {* The identity function is continuous *} 
15565  438 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

440 
apply (rule contI [rule_format]) 
15565  441 
apply (erule thelubE) 
442 
apply (rule refl) 

443 
done 

444 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

445 
text {* constant functions are continuous *} 
15565  446 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

448 
apply (rule contI [rule_format]) 
15565  449 
apply (blast intro: is_lubI ub_rangeI dest: ub_rangeD) 
450 
done 

451 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

452 
lemma cont2cont_app3: "[cont(f); cont(t) ] ==> cont(%x. f(t(x)))" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

453 
by (best intro: cont2cont_app2 cont_const) 
15565  454 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

455 
text {* A nonemptiness result for Cfun *} 
15565  456 

457 
lemma CfunI: "?x:Collect cont" 

458 
apply (rule CollectI) 

459 
apply (rule cont_const) 

460 
done 

461 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

462 
text {* some properties of flat *} 
15565  463 

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

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

465 
apply (rule monofunI [rule_format]) 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

466 
apply (drule ax_flat [rule_format]) 
15565  467 
apply auto 
468 
done 

469 

470 
declare range_composition [simp del] 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

471 

15565  472 
lemma chfindom_monofun2cont: "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" 
473 
apply (rule monocontlub2cont) 

474 
apply assumption 

15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

475 
apply (rule contlubI [rule_format]) 
15565  476 
apply (frule chfin2finch) 
477 
apply (rule antisym_less) 

478 
apply (clarsimp simp add: finite_chain_def maxinch_is_thelub) 

479 
apply (rule is_ub_thelub) 

480 
apply (erule ch2ch_monofun) 

481 
apply assumption 

482 
apply (drule monofun_finch2finch[COMP swap_prems_rl]) 

483 
apply assumption 

484 
apply (simp add: finite_chain_def) 

485 
apply (erule conjE) 

486 
apply (erule exE) 

487 
apply (simp add: maxinch_is_thelub) 

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

489 
apply (erule is_ub_thelub) 

490 
done 

491 

492 
lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard] 

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

494 

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

495 
end 