author  haftmann 
Fri, 08 May 2009 13:34:27 +0200  
changeset 31071  845a6acd3bf3 
parent 31024  0fdf666e08bf 
child 31076  99fe356cbbc2 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Pcpo.thy 
2 
Author: Franz Regensburger 

3 
*) 

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

4 

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

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

6 

15577  7 
theory Pcpo 
8 
imports Porder 

9 
begin 

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

10 

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

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

12 

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

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

14 

29614
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29138
diff
changeset

15 
class cpo = po + 
31071  16 
assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S << x" 
17 
begin 

2394  18 

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

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

31071  21 
lemma cpo_lubI: "chain S \<Longrightarrow> range S << (\<Squnion>i. S i)" 
22 
by (fast dest: cpo elim: lubI) 

26026  23 

31071  24 
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S << l" 
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 

31071  29 
lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)" 
30 
by (blast dest: cpo intro: lubI [THEN is_ub_lub]) 

15563  31 

16626  32 
lemma is_lub_thelub: 
31071  33 
"\<lbrakk>chain S; range S < x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" 
34 
by (blast dest: cpo intro: lubI [THEN is_lub_lub]) 

15563  35 

16626  36 
lemma lub_range_mono: 
31071  37 
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> 
16626  38 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
15563  39 
apply (erule is_lub_thelub) 
40 
apply (rule ub_rangeI) 

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

44 
apply auto 

45 
done 

46 

16626  47 
lemma lub_range_shift: 
31071  48 
"chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" 
15563  49 
apply (rule antisym_less) 
50 
apply (rule lub_range_mono) 

51 
apply fast 

52 
apply assumption 

53 
apply (erule chain_shift) 

54 
apply (rule is_lub_thelub) 

55 
apply assumption 

56 
apply (rule ub_rangeI) 

17813  57 
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

58 
apply (erule chain_mono) 
15563  59 
apply (rule le_add1) 
17813  60 
apply (rule is_ub_thelub) 
61 
apply (erule chain_shift) 

15563  62 
done 
63 

16626  64 
lemma maxinch_is_thelub: 
31071  65 
"chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)" 
15563  66 
apply (rule iffI) 
67 
apply (fast intro!: thelubI lub_finch1) 

68 
apply (unfold max_in_chain_def) 

69 
apply (safe intro!: antisym_less) 

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

70 
apply (fast elim!: chain_mono) 
15563  71 
apply (drule sym) 
72 
apply (force elim!: is_ub_thelub) 

73 
done 

74 

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

16626  77 
lemma lub_mono: 
31071  78 
"\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
16626  79 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
15563  80 
apply (erule is_lub_thelub) 
81 
apply (rule ub_rangeI) 

82 
apply (rule trans_less) 

25923  83 
apply (erule meta_spec) 
15563  84 
apply (erule is_ub_thelub) 
85 
done 

86 

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

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

16626  89 
lemma lub_equal: 
31071  90 
"\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk> 
16626  91 
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" 
31071  92 
by (simp only: expand_fun_eq [symmetric]) 
15563  93 

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

94 
text {* more results about mono and = of lubs of chains *} 
3326  95 

16626  96 
lemma lub_mono2: 
31071  97 
"\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk> 
16626  98 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
15563  99 
apply (erule exE) 
17813  100 
apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))") 
101 
apply (thin_tac "\<forall>i>j. X i = Y i") 

102 
apply (simp only: lub_range_shift) 

16626  103 
apply simp 
15563  104 
done 
105 

16626  106 
lemma lub_equal2: 
31071  107 
"\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk> 
16626  108 
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" 
31071  109 
by (blast intro: antisym_less lub_mono2 sym) 
15563  110 

16626  111 
lemma lub_mono3: 
31071  112 
"\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk> 
16626  113 
\<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)" 
17813  114 
apply (erule is_lub_thelub) 
15563  115 
apply (rule ub_rangeI) 
116 
apply (erule allE) 

117 
apply (erule exE) 

16626  118 
apply (erule trans_less) 
119 
apply (erule is_ub_thelub) 

15563  120 
done 
121 

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

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

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

126 
apply (rule chainI) 

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

130 

16201  131 
lemma diag_lub: 
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 
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 

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

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

31071  163 
by (simp add: diag_lub 1 2) 
16201  164 

31071  165 
end 
16201  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 

29614
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29138
diff
changeset

171 
class pcpo = cpo + 
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29138
diff
changeset

172 
assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" 
31071  173 
begin 
25723  174 

31071  175 
definition UU :: 'a where 
25723  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 

31071  194 
end 
195 

31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

196 
text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *} 
16739  197 

31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

198 
setup {* 
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

199 
ReorientProc.add 
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

200 
(fn Const(@{const_name UU}, _) => true  _ => false) 
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

201 
*} 
25723  202 

31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

203 
simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc 
25723  204 

31071  205 
context pcpo 
206 
begin 

207 

25723  208 
text {* useful lemmas about @{term \<bottom>} *} 
209 

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

211 
by (simp add: po_eq_conv) 

212 

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

214 
by simp 

215 

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

217 
by (subst eq_UU_iff) 

218 

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

15563  220 
apply (rule allI) 
16626  221 
apply (rule UU_I) 
15563  222 
apply (erule subst) 
223 
apply (erule is_ub_thelub) 

224 
done 

225 

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

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

229 
apply simp 
15563  230 
done 
231 

16626  232 
lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>" 
31071  233 
by (blast intro: chain_UU_I_inverse) 
15563  234 

16626  235 
lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>" 
31071  236 
by (blast intro: UU_I) 
15563  237 

16627  238 
lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>" 
31071  239 
by (blast dest: notUU_I chain_mono_less) 
240 

241 
end 

15588
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 
subsection {* Chainfinite and flat cpos *} 
15563  244 

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

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

246 

31071  247 
class chfin = po + 
248 
assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y" 

249 
begin 

25814  250 

31071  251 
subclass cpo 
252 
apply default 

253 
apply (frule chfin) 

254 
apply (blast intro: lub_finch1) 

255 
done 

15563  256 

31071  257 
lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y" 
258 
by (simp add: chfin finite_chain_def) 

259 

260 
end 

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

261 

31071  262 
class finite_po = finite + po 
263 
begin 

25814  264 

31071  265 
subclass chfin 
266 
apply default 

25814  267 
apply (drule finite_range_imp_finch) 
268 
apply (rule finite) 

269 
apply (simp add: finite_chain_def) 

270 
done 

271 

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

273 

31071  274 
class flat = pcpo + 
275 
assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y" 

276 
begin 

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

277 

31071  278 
subclass chfin 
279 
apply default 

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

282 
apply simp 
15563  283 
apply simp 
284 
apply (erule exE) 

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

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

287 
apply (blast dest: chain_mono ax_flat) 
15563  288 
done 
289 

25826  290 
lemma flat_less_iff: 
291 
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)" 

31071  292 
by (safe dest!: ax_flat) 
25826  293 

31071  294 
lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)" 
295 
by (safe dest!: ax_flat) 

15563  296 

31071  297 
end 
15563  298 

26023  299 
text {* Discrete cpos *} 
300 

29614
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29138
diff
changeset

301 
class discrete_cpo = sq_ord + 
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29138
diff
changeset

302 
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" 
31071  303 
begin 
26023  304 

31071  305 
subclass po 
29614
1f7b1b0df292
simplified handling of base sort, dropped axclass
haftmann
parents:
29138
diff
changeset

306 
proof qed simp_all 
26023  307 

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

309 

310 
lemma discrete_chain_const: 

31071  311 
assumes S: "chain S" 
26023  312 
shows "\<exists>x. S = (\<lambda>i. x)" 
313 
proof (intro exI ext) 

314 
fix i :: nat 

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

316 
hence "S 0 = S i" by simp 

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

318 
qed 

319 

31071  320 
subclass cpo 
26023  321 
proof 
322 
fix S :: "nat \<Rightarrow> 'a" 

323 
assume S: "chain S" 

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

325 
by (rule discrete_chain_const) 

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

327 
by (fast intro: lub_const) 

328 
qed 

329 

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

331 

16626  332 
end 