author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 16070 | 4a83dd540b88 |
child 16201 | 7bb51c8196cb |
permissions | -rw-r--r-- |
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 new-style theories, and combined numbered files
huffman
parents:
15563
diff
changeset
|
7 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15563
diff
changeset
|
8 |
header {* Classes cpo and pcpo *} |
efb95d0d01f7
converted to new-style 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 Higher-Order 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 |
||
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
128 |
subsection {* Pointed cpos *} |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
129 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
130 |
text {* The class pcpo of pointed cpos *} |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
131 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
132 |
axclass pcpo < cpo |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
133 |
least: "? x.!y. x<<y" |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
134 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
135 |
consts |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
136 |
UU :: "'a::pcpo" |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
137 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
138 |
syntax (xsymbols) |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
139 |
UU :: "'a::pcpo" ("\<bottom>") |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
140 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
141 |
defs |
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset
|
142 |
UU_def: "UU == THE x. ALL y. x<<y" |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
143 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
144 |
text {* derive the old rule minimal *} |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
145 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
146 |
lemma UU_least: "ALL z. UU << z" |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
147 |
apply (unfold UU_def) |
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset
|
148 |
apply (rule theI') |
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset
|
149 |
apply (rule ex_ex1I) |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
150 |
apply (rule least) |
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15640
diff
changeset
|
151 |
apply (blast intro: antisym_less) |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
152 |
done |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
153 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
154 |
lemmas minimal = UU_least [THEN spec, standard] |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
155 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
156 |
declare minimal [iff] |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
157 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
158 |
text {* useful lemmas about @{term UU} *} |
15563 | 159 |
|
160 |
lemma eq_UU_iff: "(x=UU)=(x<<UU)" |
|
161 |
apply (rule iffI) |
|
162 |
apply (erule ssubst) |
|
163 |
apply (rule refl_less) |
|
164 |
apply (rule antisym_less) |
|
165 |
apply assumption |
|
166 |
apply (rule minimal) |
|
167 |
done |
|
168 |
||
169 |
lemma UU_I: "x << UU ==> x = UU" |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
170 |
by (subst eq_UU_iff) |
15563 | 171 |
|
172 |
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
|
173 |
by auto |
15563 | 174 |
|
175 |
lemma chain_UU_I: "[|chain(Y);lub(range(Y))=UU|] ==> ALL i. Y(i)=UU" |
|
176 |
apply (rule allI) |
|
177 |
apply (rule antisym_less) |
|
178 |
apply (rule_tac [2] minimal) |
|
179 |
apply (erule subst) |
|
180 |
apply (erule is_ub_thelub) |
|
181 |
done |
|
182 |
||
183 |
lemma chain_UU_I_inverse: "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" |
|
184 |
apply (rule lub_chain_maxelem) |
|
185 |
apply (erule spec) |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
186 |
apply simp |
15563 | 187 |
done |
188 |
||
189 |
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
|
190 |
by (blast intro: chain_UU_I_inverse) |
15563 | 191 |
|
192 |
lemma notUU_I: "[| x<<y; ~x=UU |] ==> ~y=UU" |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
193 |
by (blast intro: UU_I) |
15563 | 194 |
|
195 |
lemma chain_mono2: |
|
196 |
"[|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
|
197 |
by (blast dest: notUU_I chain_mono) |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
198 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
199 |
subsection {* Chain-finite and flat cpos *} |
15563 | 200 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
201 |
text {* further useful classes for HOLCF domains *} |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
202 |
|
15640
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
203 |
axclass chfin < po |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
204 |
chfin: "!Y. chain Y-->(? n. max_in_chain n Y)" |
15563 | 205 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
206 |
axclass flat < pcpo |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
207 |
ax_flat: "! x y. x << y --> (x = UU) | (x=y)" |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
208 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
209 |
text {* some properties for chfin and flat *} |
15563 | 210 |
|
15640
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
211 |
text {* chfin types are cpo *} |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
212 |
|
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
213 |
lemma chfin_imp_cpo: |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
214 |
"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
|
215 |
apply (frule chfin [rule_format]) |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
216 |
apply (blast intro: lub_finch1) |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
217 |
done |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
218 |
|
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
219 |
instance chfin < cpo |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
220 |
by intro_classes (rule chfin_imp_cpo) |
2d1d6ea579a1
chfin now a subclass of po, proved instance chfin < cpo
huffman
parents:
15588
diff
changeset
|
221 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
222 |
text {* flat types are chfin *} |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
223 |
|
15563 | 224 |
lemma flat_imp_chfin: |
225 |
"ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)" |
|
226 |
apply (unfold max_in_chain_def) |
|
227 |
apply clarify |
|
228 |
apply (case_tac "ALL i. Y (i) =UU") |
|
229 |
apply (rule_tac x = "0" in exI) |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
230 |
apply simp |
15563 | 231 |
apply simp |
232 |
apply (erule exE) |
|
233 |
apply (rule_tac x = "i" in exI) |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
234 |
apply clarify |
15563 | 235 |
apply (erule le_imp_less_or_eq [THEN disjE]) |
236 |
apply safe |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
237 |
apply (blast dest: chain_mono ax_flat [rule_format]) |
15563 | 238 |
done |
239 |
||
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
240 |
instance flat < chfin |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
241 |
by intro_classes (rule flat_imp_chfin) |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
242 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
243 |
text {* flat subclass of chfin @{text "-->"} @{text adm_flat} not needed *} |
15563 | 244 |
|
245 |
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
|
246 |
by (safe dest!: ax_flat [rule_format]) |
15563 | 247 |
|
248 |
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
|
249 |
by (simp add: chfin finite_chain_def) |
15563 | 250 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
251 |
text {* lemmata for improved admissibility introdution rule *} |
15563 | 252 |
|
253 |
lemma infinite_chain_adm_lemma: |
|
254 |
"[|chain Y; ALL i. P (Y i); |
|
255 |
(!!Y. [| chain Y; ALL i. P (Y i); ~ finite_chain Y |] ==> P (lub(range Y))) |
|
256 |
|] ==> P (lub (range Y))" |
|
257 |
apply (case_tac "finite_chain Y") |
|
258 |
prefer 2 apply fast |
|
259 |
apply (unfold finite_chain_def) |
|
260 |
apply safe |
|
261 |
apply (erule lub_finch1 [THEN thelubI, THEN ssubst]) |
|
262 |
apply assumption |
|
263 |
apply (erule spec) |
|
264 |
done |
|
265 |
||
266 |
lemma increasing_chain_adm_lemma: |
|
267 |
"[|chain Y; ALL i. P (Y i); |
|
268 |
(!!Y. [| chain Y; ALL i. P (Y i); |
|
269 |
ALL i. EX j. i < j & Y i ~= Y j & Y i << Y j|] |
|
270 |
==> P (lub (range Y))) |] ==> P (lub (range Y))" |
|
271 |
apply (erule infinite_chain_adm_lemma) |
|
272 |
apply assumption |
|
273 |
apply (erule thin_rl) |
|
274 |
apply (unfold finite_chain_def) |
|
275 |
apply (unfold max_in_chain_def) |
|
276 |
apply (fast dest: le_imp_less_or_eq elim: chain_mono) |
|
277 |
done |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15563
diff
changeset
|
278 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
279 |
end |