author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16203  b3268fe39838 
child 16626  d28314d2dce3 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Pcpo.thy 
2 
ID: $Id$ 

3 
Author: Franz Regensburger 

4 

16070
4a83dd540b88
removed LICENCE note  everything is subject to Isabelle licence as
wenzelm
parents:
15930
diff
changeset

5 
Introduction of the classes cpo and pcpo. 
2640  6 
*) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15563
diff
changeset

7 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15563
diff
changeset

8 
header {* Classes cpo and pcpo *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15563
diff
changeset

9 

15577  10 
theory Pcpo 
11 
imports Porder 

12 
begin 

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

13 

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

14 
subsection {* Complete partial orders *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

15 

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

16 
text {* The class cpo of chain complete partial orders *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

17 

2640  18 
axclass cpo < po 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

19 
 {* class axiom: *} 
15563  20 
cpo: "chain S ==> ? x. range S << x" 
2394  21 

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

22 
text {* in cpo's everthing equal to THE lub has lub properties for every chain *} 
15563  23 

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

24 
lemma thelubE: "[ chain(S); lub(range(S)) = (l::'a::cpo) ] ==> range(S) << l" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

25 
by (blast dest: cpo intro: lubI) 
15563  26 

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

27 
text {* Properties of the lub *} 
15563  28 

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

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

30 
by (blast dest: cpo intro: lubI [THEN is_ub_lub]) 
15563  31 

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

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

33 
by (blast dest: cpo intro: lubI [THEN is_lub_lub]) 
15563  34 

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

36 
apply (erule is_lub_thelub) 

37 
apply (rule ub_rangeI) 

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

39 
apply clarsimp 

40 
apply (erule is_ub_thelub) 

41 
apply auto 

42 
done 

43 

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

45 
apply (rule antisym_less) 

46 
apply (rule lub_range_mono) 

47 
apply fast 

48 
apply assumption 

49 
apply (erule chain_shift) 

50 
apply (rule is_lub_thelub) 

51 
apply assumption 

52 
apply (rule ub_rangeI) 

53 
apply (rule trans_less) 

54 
apply (rule_tac [2] is_ub_thelub) 

55 
apply (erule_tac [2] chain_shift) 

56 
apply (erule chain_mono3) 

57 
apply (rule le_add1) 

58 
done 

59 

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

61 
apply (rule iffI) 

62 
apply (fast intro!: thelubI lub_finch1) 

63 
apply (unfold max_in_chain_def) 

64 
apply (safe intro!: antisym_less) 

65 
apply (fast elim!: chain_mono3) 

66 
apply (drule sym) 

67 
apply (force elim!: is_ub_thelub) 

68 
done 

69 

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

70 
text {* the @{text "<<"} relation between two chains is preserved by their lubs *} 
15563  71 

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

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

74 
apply (erule is_lub_thelub) 

75 
apply (rule ub_rangeI) 

76 
apply (rule trans_less) 

77 
apply (erule spec) 

78 
apply (erule is_ub_thelub) 

79 
done 

80 

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

81 
text {* the = relation between two chains is preserved by their lubs *} 
15563  82 

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

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

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

85 
by (simp only: expand_fun_eq [symmetric]) 
15563  86 

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

87 
text {* more results about mono and = of lubs of chains *} 
3326  88 

15563  89 
lemma lub_mono2: "[EX j. ALL i. j<i > X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)] 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

90 
==> lub(range(X))<<lub(range(Y))" 
15563  91 
apply (erule exE) 
92 
apply (rule is_lub_thelub) 

93 
apply assumption 

94 
apply (rule ub_rangeI) 

95 
apply (case_tac "j<i") 

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

97 
apply (rule sym) 

98 
apply fast 

99 
apply (rule is_ub_thelub) 

100 
apply assumption 

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

102 
apply (rule chain_mono) 

103 
apply assumption 

104 
apply (rule not_less_eq [THEN subst]) 

105 
apply assumption 

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

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

107 
apply (simp) 
15563  108 
apply (erule is_ub_thelub) 
109 
done 

110 

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

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

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

113 
by (blast intro: antisym_less lub_mono2 sym) 
15563  114 

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

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

117 
apply (rule is_lub_thelub) 

118 
apply assumption 

119 
apply (rule ub_rangeI) 

120 
apply (erule allE) 

121 
apply (erule exE) 

122 
apply (rule trans_less) 

123 
apply (rule_tac [2] is_ub_thelub) 

124 
prefer 2 apply (assumption) 

125 
apply assumption 

126 
done 

127 

16203  128 
lemma ch2ch_lub: 
129 
fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" 

130 
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 

131 
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" 

132 
shows "chain (\<lambda>i. \<Squnion>j. Y i j)" 

133 
apply (rule chainI) 

134 
apply (rule lub_mono [rule_format, OF 2 2]) 

135 
apply (rule chainE [OF 1]) 

136 
done 

137 

16201  138 
lemma diag_lub: 
139 
fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" 

140 
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 

141 
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" 

142 
shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)" 

143 
proof (rule antisym_less) 

144 
have 3: "chain (\<lambda>i. Y i i)" 

145 
apply (rule chainI) 

146 
apply (rule trans_less) 

147 
apply (rule chainE [OF 1]) 

148 
apply (rule chainE [OF 2]) 

149 
done 

150 
have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)" 

16203  151 
by (rule ch2ch_lub [OF 1 2]) 
16201  152 
show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" 
153 
apply (rule is_lub_thelub [OF 4]) 

154 
apply (rule ub_rangeI) 

16203  155 
apply (rule lub_mono3 [rule_format, OF 2 3]) 
16201  156 
apply (rule exI) 
157 
apply (rule trans_less) 

158 
apply (rule chain_mono3 [OF 1 le_maxI1]) 

159 
apply (rule chain_mono3 [OF 2 le_maxI2]) 

160 
done 

161 
show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" 

16203  162 
apply (rule lub_mono [rule_format, OF 3 4]) 
16201  163 
apply (rule is_ub_thelub [OF 2]) 
164 
done 

165 
qed 

166 

167 
lemma ex_lub: 

168 
fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" 

169 
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 

170 
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" 

171 
shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)" 

172 
by (simp add: diag_lub 1 2) 

173 

174 

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

175 
subsection {* Pointed cpos *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

176 

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

177 
text {* The class pcpo of pointed cpos *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

178 

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

179 
axclass pcpo < cpo 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

180 
least: "? x.!y. x<<y" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

181 

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

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

183 
UU :: "'a::pcpo" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

184 

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

185 
syntax (xsymbols) 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

186 
UU :: "'a::pcpo" ("\<bottom>") 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

187 

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

188 
defs 
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset

189 
UU_def: "UU == THE x. ALL y. x<<y" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

190 

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

191 
text {* derive the old rule minimal *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

192 

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

193 
lemma UU_least: "ALL z. UU << z" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

194 
apply (unfold UU_def) 
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset

195 
apply (rule theI') 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset

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

197 
apply (rule least) 
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset

198 
apply (blast intro: antisym_less) 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

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

200 

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

201 
lemmas minimal = UU_least [THEN spec, standard] 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

202 

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

203 
declare minimal [iff] 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

204 

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

205 
text {* useful lemmas about @{term UU} *} 
15563  206 

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

208 
apply (rule iffI) 

209 
apply (erule ssubst) 

210 
apply (rule refl_less) 

211 
apply (rule antisym_less) 

212 
apply assumption 

213 
apply (rule minimal) 

214 
done 

215 

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

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

217 
by (subst eq_UU_iff) 
15563  218 

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

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

220 
by auto 
15563  221 

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

223 
apply (rule allI) 

224 
apply (rule antisym_less) 

225 
apply (rule_tac [2] minimal) 

226 
apply (erule subst) 

227 
apply (erule is_ub_thelub) 

228 
done 

229 

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

231 
apply (rule lub_chain_maxelem) 

232 
apply (erule spec) 

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

233 
apply simp 
15563  234 
done 
235 

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

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

237 
by (blast intro: chain_UU_I_inverse) 
15563  238 

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

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

240 
by (blast intro: UU_I) 
15563  241 

242 
lemma chain_mono2: 

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

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

244 
by (blast dest: notUU_I chain_mono) 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

245 

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

246 
subsection {* Chainfinite and flat cpos *} 
15563  247 

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

248 
text {* further useful classes for HOLCF domains *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

249 

15640
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

250 
axclass chfin < po 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

251 
chfin: "!Y. chain Y>(? n. max_in_chain n Y)" 
15563  252 

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

253 
axclass flat < pcpo 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

254 
ax_flat: "! x y. x << y > (x = UU)  (x=y)" 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

255 

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

256 
text {* some properties for chfin and flat *} 
15563  257 

15640
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

258 
text {* chfin types are cpo *} 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

259 

2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

260 
lemma chfin_imp_cpo: 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

261 
"chain (S::nat=>'a::chfin) ==> EX x. range S << x" 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

262 
apply (frule chfin [rule_format]) 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

263 
apply (blast intro: lub_finch1) 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

264 
done 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

265 

2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

266 
instance chfin < cpo 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

267 
by intro_classes (rule chfin_imp_cpo) 
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset

268 

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

269 
text {* flat types are chfin *} 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

270 

15563  271 
lemma flat_imp_chfin: 
272 
"ALL Y::nat=>'a::flat. chain Y > (EX n. max_in_chain n Y)" 

273 
apply (unfold max_in_chain_def) 

274 
apply clarify 

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

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

276 
apply simp 
15563  277 
apply simp 
278 
apply (erule exE) 

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

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

280 
apply clarify 
15563  281 
apply (erule le_imp_less_or_eq [THEN disjE]) 
282 
apply safe 

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

283 
apply (blast dest: chain_mono ax_flat [rule_format]) 
15563  284 
done 
285 

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

286 
instance flat < chfin 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

287 
by intro_classes (rule flat_imp_chfin) 
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

288 

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

289 
text {* flat subclass of chfin @{text ">"} @{text adm_flat} not needed *} 
15563  290 

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

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

292 
by (safe dest!: ax_flat [rule_format]) 
15563  293 

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

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

295 
by (simp add: chfin finite_chain_def) 
15563  296 

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

297 
text {* lemmata for improved admissibility introdution rule *} 
15563  298 

299 
lemma infinite_chain_adm_lemma: 

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

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

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

303 
apply (case_tac "finite_chain Y") 

304 
prefer 2 apply fast 

305 
apply (unfold finite_chain_def) 

306 
apply safe 

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

308 
apply assumption 

309 
apply (erule spec) 

310 
done 

311 

312 
lemma increasing_chain_adm_lemma: 

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

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

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

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

317 
apply (erule infinite_chain_adm_lemma) 

318 
apply assumption 

319 
apply (erule thin_rl) 

320 
apply (unfold finite_chain_def) 

321 
apply (unfold max_in_chain_def) 

322 
apply (fast dest: le_imp_less_or_eq elim: chain_mono) 

323 
done 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15563
diff
changeset

324 

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

325 
end 