author  huffman 
Wed, 02 Mar 2005 22:57:08 +0100  
changeset 15563  9e125b675253 
parent 14981  e73f8140af78 
child 15576  efb95d0d01f7 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Pcpo.thy 
2 
ID: $Id$ 

3 
Author: Franz Regensburger 

15563  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
2640  5 

6 
introduction of the classes cpo and pcpo 

7 
*) 

15563  8 
theory Pcpo = Porder: 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

9 

2640  10 
(* The class cpo of chain complete partial orders *) 
11 
(* ********************************************** *) 

12 
axclass cpo < po 

13 
(* class axiom: *) 

15563  14 
cpo: "chain S ==> ? x. range S << x" 
2394  15 

2640  16 
(* The class pcpo of pointed cpos *) 
17 
(* ****************************** *) 

18 
axclass pcpo < cpo 

19 

15563  20 
least: "? x.!y. x<<y" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

21 

2394  22 
consts 
2640  23 
UU :: "'a::pcpo" 
2394  24 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12030
diff
changeset

25 
syntax (xsymbols) 
15563  26 
UU :: "'a::pcpo" ("\<bottom>") 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

27 

2640  28 
defs 
15563  29 
UU_def: "UU == @x.!y. x<<y" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

30 

3326  31 
(* further useful classes for HOLCF domains *) 
32 

33 
axclass chfin<cpo 

34 

15563  35 
chfin: "!Y. chain Y>(? n. max_in_chain n Y)" 
3326  36 

37 
axclass flat<pcpo 

38 

15563  39 
ax_flat: "! x y. x << y > (x = UU)  (x=y)" 
40 

41 
(* Title: HOLCF/Pcpo.ML 

42 
ID: $Id$ 

43 
Author: Franz Regensburger 

44 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

45 

46 
introduction of the classes cpo and pcpo 

47 
*) 

48 

49 

50 
(*  *) 

51 
(* derive the old rule minimal *) 

52 
(*  *) 

53 

54 
lemma UU_least: "ALL z. UU << z" 

55 
apply (unfold UU_def) 

56 
apply (rule some_eq_ex [THEN iffD2]) 

57 
apply (rule least) 

58 
done 

59 

60 
lemmas minimal = UU_least [THEN spec, standard] 

61 

62 
declare minimal [iff] 

63 

64 
(*  *) 

65 
(* in cpo's everthing equal to THE lub has lub properties for every chain *) 

66 
(*  *) 

67 

68 
lemma thelubE: "[ chain(S); lub(range(S)) = (l::'a::cpo) ] ==> range(S) << l " 

69 
apply (blast dest: cpo intro: lubI) 

70 
done 

71 

72 
(*  *) 

73 
(* Properties of the lub *) 

74 
(*  *) 

75 

76 

77 
lemma is_ub_thelub: "chain (S::nat => 'a::cpo) ==> S(x) << lub(range(S))" 

78 
apply (blast dest: cpo intro: lubI [THEN is_ub_lub]) 

79 
done 

80 

81 
lemma is_lub_thelub: "[ chain (S::nat => 'a::cpo); range(S) < x ] ==> lub(range S) << x" 

82 
apply (blast dest: cpo intro: lubI [THEN is_lub_lub]) 

83 
done 

84 

85 
lemma lub_range_mono: "[ range X <= range Y; chain Y; chain (X::nat=>'a::cpo) ] ==> lub(range X) << lub(range Y)" 

86 
apply (erule is_lub_thelub) 

87 
apply (rule ub_rangeI) 

88 
apply (subgoal_tac "? j. X i = Y j") 

89 
apply clarsimp 

90 
apply (erule is_ub_thelub) 

91 
apply auto 

92 
done 

93 

94 
lemma lub_range_shift: "chain (Y::nat=>'a::cpo) ==> lub(range (%i. Y(i + j))) = lub(range Y)" 

95 
apply (rule antisym_less) 

96 
apply (rule lub_range_mono) 

97 
apply fast 

98 
apply assumption 

99 
apply (erule chain_shift) 

100 
apply (rule is_lub_thelub) 

101 
apply assumption 

102 
apply (rule ub_rangeI) 

103 
apply (rule trans_less) 

104 
apply (rule_tac [2] is_ub_thelub) 

105 
apply (erule_tac [2] chain_shift) 

106 
apply (erule chain_mono3) 

107 
apply (rule le_add1) 

108 
done 

109 

110 
lemma maxinch_is_thelub: "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))" 

111 
apply (rule iffI) 

112 
apply (fast intro!: thelubI lub_finch1) 

113 
apply (unfold max_in_chain_def) 

114 
apply (safe intro!: antisym_less) 

115 
apply (fast elim!: chain_mono3) 

116 
apply (drule sym) 

117 
apply (force elim!: is_ub_thelub) 

118 
done 

119 

120 

121 
(*  *) 

122 
(* the << relation between two chains is preserved by their lubs *) 

123 
(*  *) 

124 

125 
lemma lub_mono: "[chain(C1::(nat=>'a::cpo));chain(C2); ALL k. C1(k) << C2(k)] 

126 
==> lub(range(C1)) << lub(range(C2))" 

127 
apply (erule is_lub_thelub) 

128 
apply (rule ub_rangeI) 

129 
apply (rule trans_less) 

130 
apply (erule spec) 

131 
apply (erule is_ub_thelub) 

132 
done 

133 

134 
(*  *) 

135 
(* the = relation between two chains is preserved by their lubs *) 

136 
(*  *) 

137 

138 
lemma lub_equal: "[ chain(C1::(nat=>'a::cpo));chain(C2);ALL k. C1(k)=C2(k)] 

139 
==> lub(range(C1))=lub(range(C2))" 

140 
apply (rule antisym_less) 

141 
apply (rule lub_mono) 

142 
apply assumption 

143 
apply assumption 

144 
apply (intro strip) 

145 
apply (rule antisym_less_inverse [THEN conjunct1]) 

146 
apply (erule spec) 

147 
apply (rule lub_mono) 

148 
apply assumption 

149 
apply assumption 

150 
apply (intro strip) 

151 
apply (rule antisym_less_inverse [THEN conjunct2]) 

152 
apply (erule spec) 

153 
done 

154 

155 
(*  *) 

156 
(* more results about mono and = of lubs of chains *) 

157 
(*  *) 

3326  158 

15563  159 
lemma lub_mono2: "[EX j. ALL i. j<i > X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)] 
160 
==> lub(range(X))<<lub(range(Y))" 

161 
apply (erule exE) 

162 
apply (rule is_lub_thelub) 

163 
apply assumption 

164 
apply (rule ub_rangeI) 

165 
(* apply (intro strip) *) 

166 
apply (case_tac "j<i") 

167 
apply (rule_tac s = "Y (i) " and t = "X (i) " in subst) 

168 
apply (rule sym) 

169 
apply fast 

170 
apply (rule is_ub_thelub) 

171 
apply assumption 

172 
apply (rule_tac y = "X (Suc (j))" in trans_less) 

173 
apply (rule chain_mono) 

174 
apply assumption 

175 
apply (rule not_less_eq [THEN subst]) 

176 
apply assumption 

177 
apply (rule_tac s = "Y (Suc (j))" and t = "X (Suc (j))" in subst) 

178 
apply (simp (no_asm_simp)) 

179 
apply (erule is_ub_thelub) 

180 
done 

181 

182 
lemma lub_equal2: "[EX j. ALL i. j<i > X(i)=Y(i); chain(X::nat=>'a::cpo); chain(Y)] 

183 
==> lub(range(X))=lub(range(Y))" 

184 
apply (blast intro: antisym_less lub_mono2 sym) 

185 
done 

186 

187 
lemma lub_mono3: "[chain(Y::nat=>'a::cpo);chain(X); 

188 
ALL i. EX j. Y(i)<< X(j)]==> lub(range(Y))<<lub(range(X))" 

189 
apply (rule is_lub_thelub) 

190 
apply assumption 

191 
apply (rule ub_rangeI) 

192 
(* apply (intro strip) *) 

193 
apply (erule allE) 

194 
apply (erule exE) 

195 
apply (rule trans_less) 

196 
apply (rule_tac [2] is_ub_thelub) 

197 
prefer 2 apply (assumption) 

198 
apply assumption 

199 
done 

200 

201 
(*  *) 

202 
(* usefull lemmas about UU *) 

203 
(*  *) 

204 

205 
lemma eq_UU_iff: "(x=UU)=(x<<UU)" 

206 
apply (rule iffI) 

207 
apply (erule ssubst) 

208 
apply (rule refl_less) 

209 
apply (rule antisym_less) 

210 
apply assumption 

211 
apply (rule minimal) 

212 
done 

213 

214 
lemma UU_I: "x << UU ==> x = UU" 

215 
apply (subst eq_UU_iff) 

216 
apply assumption 

217 
done 

218 

219 
lemma not_less2not_eq: "~(x::'a::po)<<y ==> ~x=y" 

220 
apply auto 

221 
done 

222 

223 
lemma chain_UU_I: "[chain(Y);lub(range(Y))=UU] ==> ALL i. Y(i)=UU" 

224 
apply (rule allI) 

225 
apply (rule antisym_less) 

226 
apply (rule_tac [2] minimal) 

227 
apply (erule subst) 

228 
apply (erule is_ub_thelub) 

229 
done 

230 

231 

232 
lemma chain_UU_I_inverse: "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" 

233 
apply (rule lub_chain_maxelem) 

234 
apply (erule spec) 

235 
apply (rule allI) 

236 
apply (rule antisym_less_inverse [THEN conjunct1]) 

237 
apply (erule spec) 

238 
done 

239 

240 
lemma chain_UU_I_inverse2: "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> EX i.~ Y(i)=UU" 

241 
apply (blast intro: chain_UU_I_inverse) 

242 
done 

243 

244 
lemma notUU_I: "[ x<<y; ~x=UU ] ==> ~y=UU" 

245 
apply (blast intro: UU_I) 

246 
done 

247 

248 
lemma chain_mono2: 

249 
"[EX j. ~Y(j)=UU;chain(Y::nat=>'a::pcpo)] ==> EX j. ALL i. j<i>~Y(i)=UU" 

250 
apply (blast dest: notUU_I chain_mono) 

251 
done 

252 

253 
(**************************************) 

254 
(* some properties for chfin and flat *) 

255 
(**************************************) 

256 

257 
(*  *) 

258 
(* flat types are chfin *) 

259 
(*  *) 

260 

261 
(*Used only in an "instance" declaration (Fun1.thy)*) 

262 
lemma flat_imp_chfin: 

263 
"ALL Y::nat=>'a::flat. chain Y > (EX n. max_in_chain n Y)" 

264 
apply (unfold max_in_chain_def) 

265 
apply clarify 

266 
apply (case_tac "ALL i. Y (i) =UU") 

267 
apply (rule_tac x = "0" in exI) 

268 
apply (simp (no_asm_simp)) 

269 
apply simp 

270 
apply (erule exE) 

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

272 
apply (intro strip) 

273 
apply (erule le_imp_less_or_eq [THEN disjE]) 

274 
apply safe 

275 
apply (blast dest: chain_mono ax_flat [THEN spec, THEN spec, THEN mp]) 

276 
done 

277 

278 
(* flat subclass of chfin > adm_flat not needed *) 

279 

280 
lemma flat_eq: "(a::'a::flat) ~= UU ==> a << b = (a = b)" 

281 
apply (safe intro!: refl_less) 

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

283 
apply (fast intro!: refl_less ax_flat [THEN spec, THEN spec, THEN mp]) 

284 
done 

285 

286 
lemma chfin2finch: "chain (Y::nat=>'a::chfin) ==> finite_chain Y" 

287 
apply (force simp add: chfin finite_chain_def) 

288 
done 

289 

290 
(*  *) 

291 
(* lemmata for improved admissibility introdution rule *) 

292 
(*  *) 

293 

294 
lemma infinite_chain_adm_lemma: 

295 
"[chain Y; ALL i. P (Y i); 

296 
(!!Y. [ chain Y; ALL i. P (Y i); ~ finite_chain Y ] ==> P (lub(range Y))) 

297 
] ==> P (lub (range Y))" 

298 
(* apply (cut_tac prems) *) 

299 
apply (case_tac "finite_chain Y") 

300 
prefer 2 apply fast 

301 
apply (unfold finite_chain_def) 

302 
apply safe 

303 
apply (erule lub_finch1 [THEN thelubI, THEN ssubst]) 

304 
apply assumption 

305 
apply (erule spec) 

306 
done 

307 

308 
lemma increasing_chain_adm_lemma: 

309 
"[chain Y; ALL i. P (Y i); 

310 
(!!Y. [ chain Y; ALL i. P (Y i); 

311 
ALL i. EX j. i < j & Y i ~= Y j & Y i << Y j] 

312 
==> P (lub (range Y))) ] ==> P (lub (range Y))" 

313 
(* apply (cut_tac prems) *) 

314 
apply (erule infinite_chain_adm_lemma) 

315 
apply assumption 

316 
apply (erule thin_rl) 

317 
apply (unfold finite_chain_def) 

318 
apply (unfold max_in_chain_def) 

319 
apply (fast dest: le_imp_less_or_eq elim: chain_mono) 

320 
done 

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

321 
end 