author  huffman 
Thu, 31 Jan 2008 21:21:22 +0100  
changeset 26023  29c1e3e98276 
parent 25923  5fe4b543512e 
child 26026  f9647c040b58 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Pcpo.thy 
2 
ID: $Id$ 

3 
Author: Franz Regensburger 

4 
*) 

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

5 

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

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

7 

15577  8 
theory Pcpo 
9 
imports Porder 

10 
begin 

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

11 

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

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

13 

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

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

15 

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

17 
 {* class axiom: *} 
16626  18 
cpo: "chain S \<Longrightarrow> \<exists>x. range S << x" 
2394  19 

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

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

16626  22 
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S << l" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

23 
by (blast dest: cpo intro: lubI) 
15563  24 

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

25 
text {* Properties of the lub *} 
15563  26 

16626  27 
lemma is_ub_thelub: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

28 
by (blast dest: cpo intro: lubI [THEN is_ub_lub]) 
15563  29 

16626  30 
lemma is_lub_thelub: 
31 
"\<lbrakk>chain (S::nat \<Rightarrow> 'a::cpo); range S < x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" 

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

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

16626  34 
lemma lub_range_mono: 
35 
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain (X::nat \<Rightarrow> 'a::cpo)\<rbrakk> 

36 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 

15563  37 
apply (erule is_lub_thelub) 
38 
apply (rule ub_rangeI) 

16626  39 
apply (subgoal_tac "\<exists>j. X i = Y j") 
15563  40 
apply clarsimp 
41 
apply (erule is_ub_thelub) 

42 
apply auto 

43 
done 

44 

16626  45 
lemma lub_range_shift: 
46 
"chain (Y::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" 

15563  47 
apply (rule antisym_less) 
48 
apply (rule lub_range_mono) 

49 
apply fast 

50 
apply assumption 

51 
apply (erule chain_shift) 

52 
apply (rule is_lub_thelub) 

53 
apply assumption 

54 
apply (rule ub_rangeI) 

17813  55 
apply (rule_tac y="Y (i + j)" in trans_less) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

56 
apply (erule chain_mono) 
15563  57 
apply (rule le_add1) 
17813  58 
apply (rule is_ub_thelub) 
59 
apply (erule chain_shift) 

15563  60 
done 
61 

16626  62 
lemma maxinch_is_thelub: 
63 
"chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = ((Y i)::'a::cpo))" 

15563  64 
apply (rule iffI) 
65 
apply (fast intro!: thelubI lub_finch1) 

66 
apply (unfold max_in_chain_def) 

67 
apply (safe intro!: antisym_less) 

25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

68 
apply (fast elim!: chain_mono) 
15563  69 
apply (drule sym) 
70 
apply (force elim!: is_ub_thelub) 

71 
done 

72 

16626  73 
text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *} 
15563  74 

16626  75 
lemma lub_mono: 
25923  76 
"\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
16626  77 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
15563  78 
apply (erule is_lub_thelub) 
79 
apply (rule ub_rangeI) 

80 
apply (rule trans_less) 

25923  81 
apply (erule meta_spec) 
15563  82 
apply (erule is_ub_thelub) 
83 
done 

84 

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

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

16626  87 
lemma lub_equal: 
88 
"\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<forall>k. X k = Y k\<rbrakk> 

89 
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" 

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

90 
by (simp only: expand_fun_eq [symmetric]) 
15563  91 

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

92 
text {* more results about mono and = of lubs of chains *} 
3326  93 

16626  94 
lemma lub_mono2: 
17813  95 
"\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain (X::nat \<Rightarrow> 'a::cpo); chain Y\<rbrakk> 
16626  96 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
15563  97 
apply (erule exE) 
17813  98 
apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))") 
99 
apply (thin_tac "\<forall>i>j. X i = Y i") 

100 
apply (simp only: lub_range_shift) 

16626  101 
apply simp 
15563  102 
done 
103 

16626  104 
lemma lub_equal2: 
105 
"\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain (X::nat \<Rightarrow> 'a::cpo); chain Y\<rbrakk> 

106 
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" 

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

107 
by (blast intro: antisym_less lub_mono2 sym) 
15563  108 

16626  109 
lemma lub_mono3: 
110 
"\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk> 

111 
\<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)" 

17813  112 
apply (erule is_lub_thelub) 
15563  113 
apply (rule ub_rangeI) 
114 
apply (erule allE) 

115 
apply (erule exE) 

16626  116 
apply (erule trans_less) 
117 
apply (erule is_ub_thelub) 

15563  118 
done 
119 

16203  120 
lemma ch2ch_lub: 
121 
fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" 

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

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

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

125 
apply (rule chainI) 

25923  126 
apply (rule lub_mono [OF 2 2]) 
16203  127 
apply (rule chainE [OF 1]) 
128 
done 

129 

16201  130 
lemma diag_lub: 
131 
fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" 

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

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

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

135 
proof (rule antisym_less) 

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

137 
apply (rule chainI) 

138 
apply (rule trans_less) 

139 
apply (rule chainE [OF 1]) 

140 
apply (rule chainE [OF 2]) 

141 
done 

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

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

146 
apply (rule ub_rangeI) 

16203  147 
apply (rule lub_mono3 [rule_format, OF 2 3]) 
16201  148 
apply (rule exI) 
149 
apply (rule trans_less) 

25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

150 
apply (rule chain_mono [OF 1 le_maxI1]) 
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

151 
apply (rule chain_mono [OF 2 le_maxI2]) 
16201  152 
done 
153 
show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" 

25923  154 
apply (rule lub_mono [OF 3 4]) 
16201  155 
apply (rule is_ub_thelub [OF 2]) 
156 
done 

157 
qed 

158 

159 
lemma ex_lub: 

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

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

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

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

164 
by (simp add: diag_lub 1 2) 

165 

166 

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

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

168 

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

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

170 

25723  171 
axclass pcpo < cpo 
172 
least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" 

173 

174 
definition 

175 
UU :: "'a::pcpo" where 

176 
"UU = (THE x. \<forall>y. x \<sqsubseteq> y)" 

177 

178 
notation (xsymbols) 

179 
UU ("\<bottom>") 

180 

181 
text {* derive the old rule minimal *} 

182 

183 
lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z" 

184 
apply (unfold UU_def) 

185 
apply (rule theI') 

186 
apply (rule ex_ex1I) 

187 
apply (rule least) 

188 
apply (blast intro: antisym_less) 

189 
done 

190 

191 
lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" 

192 
by (rule UU_least [THEN spec]) 

193 

194 
lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)" 

195 
by auto 

16739  196 

25723  197 
ML_setup {* 
198 
local 

199 
val meta_UU_reorient = thm "UU_reorient" RS eq_reflection; 

200 
fun reorient_proc sg _ (_ $ t $ u) = 

201 
case u of 

202 
Const("Pcpo.UU",_) => NONE 

203 
 Const("HOL.zero", _) => NONE 

204 
 Const("HOL.one", _) => NONE 

205 
 Const("Numeral.number_of", _) $ _ => NONE 

206 
 _ => SOME meta_UU_reorient; 

207 
in 

208 
val UU_reorient_simproc = 

209 
Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc 

210 
end; 

211 

212 
Addsimprocs [UU_reorient_simproc]; 

213 
*} 

214 

215 
text {* useful lemmas about @{term \<bottom>} *} 

216 

217 
lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)" 

218 
by (simp add: po_eq_conv) 

219 

220 
lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)" 

221 
by simp 

222 

223 
lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" 

224 
by (subst eq_UU_iff) 

225 

226 
lemma not_less2not_eq: "\<not> (x::'a::po) \<sqsubseteq> y \<Longrightarrow> x \<noteq> y" 

227 
by auto 

228 

229 
lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>" 

15563  230 
apply (rule allI) 
16626  231 
apply (rule UU_I) 
15563  232 
apply (erule subst) 
233 
apply (erule is_ub_thelub) 

234 
done 

235 

16626  236 
lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>" 
15563  237 
apply (rule lub_chain_maxelem) 
238 
apply (erule spec) 

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

239 
apply simp 
15563  240 
done 
241 

16626  242 
lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

243 
by (blast intro: chain_UU_I_inverse) 
15563  244 

16626  245 
lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

246 
by (blast intro: UU_I) 
15563  247 

16627  248 
lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>" 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

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

250 

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

251 
subsection {* Chainfinite and flat cpos *} 
15563  252 

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

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

254 

25814  255 
axclass finite_po < finite, po 
256 

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

257 
axclass chfin < po 
25921  258 
chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y" 
15563  259 

25723  260 
axclass flat < pcpo 
25920  261 
ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

262 

25814  263 
text {* finite partial orders are chainfinite and directedcomplete *} 
264 

265 
instance finite_po < chfin 

25921  266 
apply intro_classes 
25814  267 
apply (drule finite_range_imp_finch) 
268 
apply (rule finite) 

269 
apply (simp add: finite_chain_def) 

270 
done 

271 

25906
2179c6661218
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
huffman
parents:
25826
diff
changeset

272 
instance finite_po < cpo 
25814  273 
apply intro_classes 
25906
2179c6661218
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
huffman
parents:
25826
diff
changeset

274 
apply (drule directed_chain) 
25814  275 
apply (drule directed_finiteD [OF _ finite subset_refl]) 
276 
apply (erule bexE, rule exI) 

277 
apply (erule (1) is_lub_maximal) 

278 
done 

279 

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

280 
text {* some properties for chfin and flat *} 
15563  281 

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

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

283 

25921  284 
instance chfin < cpo 
285 
apply intro_classes 

286 
apply (frule chfin) 

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

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

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

289 

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

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

291 

25920  292 
instance flat < chfin 
293 
apply intro_classes 

15563  294 
apply (unfold max_in_chain_def) 
16626  295 
apply (case_tac "\<forall>i. Y i = \<bottom>") 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

296 
apply simp 
15563  297 
apply simp 
298 
apply (erule exE) 

16626  299 
apply (rule_tac x="i" in exI) 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

300 
apply clarify 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

301 
apply (blast dest: chain_mono ax_flat) 
15563  302 
done 
303 

16627  304 
text {* flat subclass of chfin; @{text adm_flat} not needed *} 
15563  305 

25826  306 
lemma flat_less_iff: 
307 
fixes x y :: "'a::flat" 

308 
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)" 

25920  309 
by (safe dest!: ax_flat) 
25826  310 

16626  311 
lemma flat_eq: "(a::'a::flat) \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)" 
25920  312 
by (safe dest!: ax_flat) 
15563  313 

16626  314 
lemma chfin2finch: "chain (Y::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> finite_chain Y" 
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

315 
by (simp add: chfin finite_chain_def) 
15563  316 

26023  317 
text {* Discrete cpos *} 
318 

319 
axclass discrete_cpo < sq_ord 

320 
discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" 

321 

322 
instance discrete_cpo < po 

323 
by (intro_classes, simp_all) 

324 

325 
text {* In a discrete cpo, every chain is constant *} 

326 

327 
lemma discrete_chain_const: 

328 
assumes S: "chain (S::nat \<Rightarrow> 'a::discrete_cpo)" 

329 
shows "\<exists>x. S = (\<lambda>i. x)" 

330 
proof (intro exI ext) 

331 
fix i :: nat 

332 
have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono) 

333 
hence "S 0 = S i" by simp 

334 
thus "S i = S 0" by (rule sym) 

335 
qed 

336 

337 
instance discrete_cpo < cpo 

338 
proof 

339 
fix S :: "nat \<Rightarrow> 'a" 

340 
assume S: "chain S" 

341 
hence "\<exists>x. S = (\<lambda>i. x)" 

342 
by (rule discrete_chain_const) 

343 
thus "\<exists>x. range S << x" 

344 
by (fast intro: lub_const) 

345 
qed 

346 

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

347 
text {* lemmata for improved admissibility introdution rule *} 
15563  348 

349 
lemma infinite_chain_adm_lemma: 

16626  350 
"\<lbrakk>chain Y; \<forall>i. P (Y i); 
351 
\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> 

352 
\<Longrightarrow> P (\<Squnion>i. Y i)" 

15563  353 
apply (case_tac "finite_chain Y") 
354 
prefer 2 apply fast 

355 
apply (unfold finite_chain_def) 

356 
apply safe 

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

358 
apply assumption 

359 
apply (erule spec) 

360 
done 

361 

362 
lemma increasing_chain_adm_lemma: 

16626  363 
"\<lbrakk>chain Y; \<forall>i. P (Y i); \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); 
364 
\<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk> 

365 
\<Longrightarrow> P (\<Squnion>i. Y i)" 

15563  366 
apply (erule infinite_chain_adm_lemma) 
367 
apply assumption 

368 
apply (erule thin_rl) 

369 
apply (unfold finite_chain_def) 

370 
apply (unfold max_in_chain_def) 

25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

371 
apply (fast dest: le_imp_less_or_eq elim: chain_mono_less) 
15563  372 
done 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15563
diff
changeset

373 

16626  374 
end 