author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 54863  82acc20ded73 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Pcpo.thy 
2640  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 

41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

146 
definition bottom :: "'a" 
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

147 
where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)" 
25723  148 

149 
notation (xsymbols) 

41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

150 
bottom ("\<bottom>") 
25723  151 

41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

152 
lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" 
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

153 
unfolding bottom_def 
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

154 
apply (rule the1I2) 
25723  155 
apply (rule ex_ex1I) 
156 
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

157 
apply (blast intro: below_antisym) 
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

158 
apply simp 
25723  159 
done 
160 

41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

161 
end 
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

162 

cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

163 
text {* Old "UU" syntax: *} 
25723  164 

41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

165 
syntax UU :: logic 
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

166 

cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

167 
translations "UU" => "CONST bottom" 
31071  168 

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

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

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

171 
setup {* 
33523  172 
Reorient_Proc.add 
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
40774
diff
changeset

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

174 
*} 
25723  175 

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

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

179 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset

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

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset

183 
lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)" 
25723  184 
by simp 
185 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset

186 
lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" 
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset

187 
by (subst eq_bottom_iff) 
25723  188 

40045  189 
lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset

190 
by (simp only: eq_bottom_iff lub_below_iff) 
40045  191 

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

192 
subsection {* Chainfinite and flat cpos *} 
15563  193 

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

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

195 

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

198 
begin 

25814  199 

31071  200 
subclass cpo 
201 
apply default 

202 
apply (frule chfin) 

203 
apply (blast intro: lub_finch1) 

204 
done 

15563  205 

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

208 

209 
end 

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

210 

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

213 
begin 

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

214 

31071  215 
subclass chfin 
216 
apply default 

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

219 
apply simp 
15563  220 
apply simp 
221 
apply (erule exE) 

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

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

224 
apply (blast dest: chain_mono ax_flat) 
15563  225 
done 
226 

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

227 
lemma flat_below_iff: 
25826  228 
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)" 
31071  229 
by (safe dest!: ax_flat) 
25826  230 

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

15563  233 

31071  234 
end 
15563  235 

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

236 
subsection {* Discrete cpos *} 
26023  237 

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

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

239 
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" 
31071  240 
begin 
26023  241 

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

243 
proof qed simp_all 
26023  244 

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

246 

247 
lemma discrete_chain_const: 

31071  248 
assumes S: "chain S" 
26023  249 
shows "\<exists>x. S = (\<lambda>i. x)" 
250 
proof (intro exI ext) 

251 
fix i :: nat 

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

253 
hence "S 0 = S i" by simp 

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

255 
qed 

256 

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

257 
subclass chfin 
26023  258 
proof 
259 
fix S :: "nat \<Rightarrow> 'a" 

260 
assume S: "chain S" 

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

261 
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

262 
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

263 
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

264 
thus "\<exists>i. max_in_chain i S" .. 
26023  265 
qed 
266 

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

268 

16626  269 
end 