author  huffman 
Sat, 27 Nov 2010 16:08:10 0800  
changeset 40774  0437dbc127b3 
parent 40771  src/HOLCF/Pcpo.thy@1c6f7d4b110e 
child 41429  cf5f025bc3c7 
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)" 
40771  22 
by (fast dest: cpo elim: is_lub_lub) 
26026  23 

31071  24 
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S << l" 
40771  25 
by (blast dest: cpo intro: is_lub_lub) 
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)" 
40771  30 
by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1]) 
15563  31 

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

39969  36 
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)" 
37 
by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) 

38 

40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

39 
lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

40 
by (simp add: lub_below_iff) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

41 

ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

42 
lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)" 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

43 
by (erule below_trans, erule is_ub_thelub) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

44 

16626  45 
lemma lub_range_mono: 
31071  46 
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> 
16626  47 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

48 
apply (erule lub_below) 
16626  49 
apply (subgoal_tac "\<exists>j. X i = Y j") 
15563  50 
apply clarsimp 
51 
apply (erule is_ub_thelub) 

52 
apply auto 

53 
done 

54 

16626  55 
lemma lub_range_shift: 
31071  56 
"chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

57 
apply (rule below_antisym) 
15563  58 
apply (rule lub_range_mono) 
59 
apply fast 

60 
apply assumption 

61 
apply (erule chain_shift) 

40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

62 
apply (rule lub_below) 
15563  63 
apply assumption 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

64 
apply (rule_tac i="i" in below_lub) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

65 
apply (erule chain_shift) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

66 
apply (erule chain_mono) 
15563  67 
apply (rule le_add1) 
68 
done 

69 

16626  70 
lemma maxinch_is_thelub: 
31071  71 
"chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)" 
15563  72 
apply (rule iffI) 
40771  73 
apply (fast intro!: lub_eqI lub_finch1) 
15563  74 
apply (unfold max_in_chain_def) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

75 
apply (safe intro!: below_antisym) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

76 
apply (fast elim!: chain_mono) 
15563  77 
apply (drule sym) 
78 
apply (force elim!: is_ub_thelub) 

79 
done 

80 

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

16626  83 
lemma lub_mono: 
31071  84 
"\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
16626  85 
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

86 
by (fast elim: lub_below below_lub) 
15563  87 

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

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

35492  90 
lemma lub_eq: 
91 
"(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" 

92 
by simp 

93 

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

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

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

98 
apply (rule chainI) 

25923  99 
apply (rule lub_mono [OF 2 2]) 
16203  100 
apply (rule chainE [OF 1]) 
101 
done 

102 

16201  103 
lemma diag_lub: 
104 
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" 

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

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

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

107 
proof (rule below_antisym) 
16201  108 
have 3: "chain (\<lambda>i. Y i i)" 
109 
apply (rule chainI) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

110 
apply (rule below_trans) 
16201  111 
apply (rule chainE [OF 1]) 
112 
apply (rule chainE [OF 2]) 

113 
done 

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

16203  115 
by (rule ch2ch_lub [OF 1 2]) 
16201  116 
show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

117 
apply (rule lub_below [OF 4]) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

118 
apply (rule lub_below [OF 2]) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40498
diff
changeset

119 
apply (rule below_lub [OF 3]) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

120 
apply (rule below_trans) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25921
diff
changeset

121 
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

122 
apply (rule chain_mono [OF 2 le_maxI2]) 
16201  123 
done 
124 
show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" 

25923  125 
apply (rule lub_mono [OF 3 4]) 
16201  126 
apply (rule is_ub_thelub [OF 2]) 
127 
done 

128 
qed 

129 

130 
lemma ex_lub: 

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

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

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

31071  134 
by (simp add: diag_lub 1 2) 
16201  135 

31071  136 
end 
16201  137 

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

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

139 

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

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

141 

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

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

143 
assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" 
31071  144 
begin 
25723  145 

31071  146 
definition UU :: 'a where 
25723  147 
"UU = (THE x. \<forall>y. x \<sqsubseteq> y)" 
148 

149 
notation (xsymbols) 

150 
UU ("\<bottom>") 

151 

152 
text {* derive the old rule minimal *} 

153 

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

155 
apply (unfold UU_def) 

156 
apply (rule theI') 

157 
apply (rule ex_ex1I) 

158 
apply (rule least) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

159 
apply (blast intro: below_antisym) 
25723  160 
done 
161 

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

163 
by (rule UU_least [THEN spec]) 

164 

31071  165 
end 
166 

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

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

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

169 
setup {* 
33523  170 
Reorient_Proc.add 
31024
0fdf666e08bf
reimplement reorientation simproc using theory data
huffman
parents:
29634
diff
changeset

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

172 
*} 
25723  173 

33523  174 
simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc 
25723  175 

31071  176 
context pcpo 
177 
begin 

178 

25723  179 
text {* useful lemmas about @{term \<bottom>} *} 
180 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

181 
lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)" 
25723  182 
by (simp add: po_eq_conv) 
183 

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

185 
by simp 

186 

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

188 
by (subst eq_UU_iff) 

189 

40045  190 
lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" 
191 
by (simp only: eq_UU_iff lub_below_iff) 

192 

25723  193 
lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>" 
40045  194 
by (simp add: lub_eq_bottom_iff) 
15563  195 

16626  196 
lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>" 
40045  197 
by simp 
15563  198 

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

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

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

206 

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

207 
subsection {* Chainfinite and flat cpos *} 
15563  208 

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

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

210 

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

213 
begin 

25814  214 

31071  215 
subclass cpo 
216 
apply default 

217 
apply (frule chfin) 

218 
apply (blast intro: lub_finch1) 

219 
done 

15563  220 

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

223 

224 
end 

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

225 

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

228 
begin 

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

229 

31071  230 
subclass chfin 
231 
apply default 

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

234 
apply simp 
15563  235 
apply simp 
236 
apply (erule exE) 

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

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

239 
apply (blast dest: chain_mono ax_flat) 
15563  240 
done 
241 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

242 
lemma flat_below_iff: 
25826  243 
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)" 
31071  244 
by (safe dest!: ax_flat) 
25826  245 

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

15563  248 

31071  249 
end 
15563  250 

40091
1ca61fbd8a79
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents:
40089
diff
changeset

251 
subsection {* Discrete cpos *} 
26023  252 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

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

254 
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" 
31071  255 
begin 
26023  256 

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

258 
proof qed simp_all 
26023  259 

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

261 

262 
lemma discrete_chain_const: 

31071  263 
assumes S: "chain S" 
26023  264 
shows "\<exists>x. S = (\<lambda>i. x)" 
265 
proof (intro exI ext) 

266 
fix i :: nat 

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

268 
hence "S 0 = S i" by simp 

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

270 
qed 

271 

40091
1ca61fbd8a79
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents:
40089
diff
changeset

272 
subclass chfin 
26023  273 
proof 
274 
fix S :: "nat \<Rightarrow> 'a" 

275 
assume S: "chain S" 

40091
1ca61fbd8a79
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents:
40089
diff
changeset

276 
hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const) 
1ca61fbd8a79
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents:
40089
diff
changeset

277 
hence "max_in_chain 0 S" 
1ca61fbd8a79
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents:
40089
diff
changeset

278 
unfolding max_in_chain_def by auto 
1ca61fbd8a79
make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
huffman
parents:
40089
diff
changeset

279 
thus "\<exists>i. max_in_chain i S" .. 
26023  280 
qed 
281 

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

283 

16626  284 
end 