author  huffman 
Mon, 11 May 2009 12:25:20 0700  
changeset 31112  4dcda8ca5d59 
parent 31076  99fe356cbbc2 
child 33506  afb577487b15 
permissions  rwrr 
29531  1 
(* Title: HOLCF/Product_Cpo.thy 
2 
Author: Franz Regensburger 

3 
*) 

4 

5 
header {* The cpo of cartesian products *} 

6 

7 
theory Product_Cpo 

29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

8 
imports Adm 
29531  9 
begin 
10 

11 
defaultsort cpo 

12 

13 
subsection {* Type @{typ unit} is a pcpo *} 

14 

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

15 
instantiation unit :: below 
29531  16 
begin 
17 

18 
definition 

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

19 
below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True" 
29531  20 

21 
instance .. 

22 
end 

23 

24 
instance unit :: discrete_cpo 

25 
by intro_classes simp 

26 

27 
instance unit :: finite_po .. 

28 

29 
instance unit :: pcpo 

30 
by intro_classes simp 

31 

32 

33 
subsection {* Product type is a partial order *} 

34 

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

35 
instantiation "*" :: (below, below) below 
29531  36 
begin 
37 

38 
definition 

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

39 
below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" 
29531  40 

41 
instance .. 

42 
end 

43 

44 
instance "*" :: (po, po) po 

45 
proof 

46 
fix x :: "'a \<times> 'b" 

47 
show "x \<sqsubseteq> x" 

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

48 
unfolding below_prod_def by simp 
29531  49 
next 
50 
fix x y :: "'a \<times> 'b" 

51 
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" 

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

52 
unfolding below_prod_def Pair_fst_snd_eq 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

53 
by (fast intro: below_antisym) 
29531  54 
next 
55 
fix x y z :: "'a \<times> 'b" 

56 
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" 

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

57 
unfolding below_prod_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

58 
by (fast intro: below_trans) 
29531  59 
qed 
60 

61 
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} 

62 

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

63 
lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

64 
unfolding below_prod_def by simp 
29531  65 

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

66 
lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

67 
unfolding below_prod_def by simp 
29531  68 

69 
text {* Pair @{text "(_,_)"} is monotone in both arguments *} 

70 

71 
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" 

72 
by (simp add: monofun_def) 

73 

74 
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" 

75 
by (simp add: monofun_def) 

76 

77 
lemma monofun_pair: 

78 
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" 

79 
by simp 

80 

31112  81 
lemma ch2ch_Pair [simp]: 
82 
"chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))" 

83 
by (rule chainI, simp add: chainE) 

84 

29531  85 
text {* @{term fst} and @{term snd} are monotone *} 
86 

87 
lemma monofun_fst: "monofun fst" 

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

88 
by (simp add: monofun_def below_prod_def) 
29531  89 

90 
lemma monofun_snd: "monofun snd" 

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

91 
by (simp add: monofun_def below_prod_def) 
29531  92 

31112  93 
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] 
94 

95 
lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd] 

96 

97 
lemma prod_chain_cases: 

98 
assumes "chain Y" 

99 
obtains A B 

100 
where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))" 

101 
proof 

102 
from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst) 

103 
from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd) 

104 
show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp 

105 
qed 

106 

29531  107 
subsection {* Product type is a cpo *} 
108 

109 
lemma is_lub_Pair: 

31112  110 
"\<lbrakk>range A << x; range B << y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) << (x, y)" 
29531  111 
apply (rule is_lubI [OF ub_rangeI]) 
31112  112 
apply (simp add: is_ub_lub) 
29531  113 
apply (frule ub2ub_monofun [OF monofun_fst]) 
114 
apply (drule ub2ub_monofun [OF monofun_snd]) 

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

115 
apply (simp add: below_prod_def is_lub_lub) 
29531  116 
done 
117 

31112  118 
lemma thelub_Pair: 
119 
"\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk> 

120 
\<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)" 

121 
by (fast intro: thelubI is_lub_Pair elim: thelubE) 

122 

29531  123 
lemma lub_cprod: 
124 
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" 

125 
assumes S: "chain S" 

126 
shows "range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 

127 
proof  

31112  128 
from `chain S` have "chain (\<lambda>i. fst (S i))" 
129 
by (rule ch2ch_fst) 

29531  130 
hence 1: "range (\<lambda>i. fst (S i)) << (\<Squnion>i. fst (S i))" 
131 
by (rule cpo_lubI) 

31112  132 
from `chain S` have "chain (\<lambda>i. snd (S i))" 
133 
by (rule ch2ch_snd) 

29531  134 
hence 2: "range (\<lambda>i. snd (S i)) << (\<Squnion>i. snd (S i))" 
135 
by (rule cpo_lubI) 

136 
show "range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 

137 
using is_lub_Pair [OF 1 2] by simp 

138 
qed 

139 

140 
lemma thelub_cprod: 

141 
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) 

142 
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 

143 
by (rule lub_cprod [THEN thelubI]) 

144 

145 
instance "*" :: (cpo, cpo) cpo 

146 
proof 

147 
fix S :: "nat \<Rightarrow> ('a \<times> 'b)" 

148 
assume "chain S" 

149 
hence "range S << (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 

150 
by (rule lub_cprod) 

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

152 
qed 

153 

154 
instance "*" :: (finite_po, finite_po) finite_po .. 

155 

156 
instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo 

157 
proof 

158 
fix x y :: "'a \<times> 'b" 

159 
show "x \<sqsubseteq> y \<longleftrightarrow> x = y" 

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

160 
unfolding below_prod_def Pair_fst_snd_eq 
29531  161 
by simp 
162 
qed 

163 

164 
subsection {* Product type is pointed *} 

165 

166 
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" 

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

167 
by (simp add: below_prod_def) 
29531  168 

169 
instance "*" :: (pcpo, pcpo) pcpo 

170 
by intro_classes (fast intro: minimal_cprod) 

171 

172 
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" 

173 
by (rule minimal_cprod [THEN UU_I, symmetric]) 

174 

29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

175 
lemma Pair_defined_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

176 
unfolding inst_cprod_pcpo by simp 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

177 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

178 
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

179 
unfolding inst_cprod_pcpo by (rule fst_conv) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

180 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

181 
lemma csnd_strict [simp]: "snd \<bottom> = \<bottom>" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

182 
unfolding inst_cprod_pcpo by (rule snd_conv) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

183 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

184 
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

185 
by simp 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

186 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

187 
lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

188 
unfolding split_def by simp 
29531  189 

190 
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} 

191 

192 
lemma cont_pair1: "cont (\<lambda>x. (x, y))" 

193 
apply (rule contI) 

194 
apply (rule is_lub_Pair) 

195 
apply (erule cpo_lubI) 

196 
apply (rule lub_const) 

197 
done 

198 

199 
lemma cont_pair2: "cont (\<lambda>y. (x, y))" 

200 
apply (rule contI) 

201 
apply (rule is_lub_Pair) 

202 
apply (rule lub_const) 

203 
apply (erule cpo_lubI) 

204 
done 

205 

206 
lemma contlub_fst: "contlub fst" 

207 
apply (rule contlubI) 

208 
apply (simp add: thelub_cprod) 

209 
done 

210 

211 
lemma contlub_snd: "contlub snd" 

212 
apply (rule contlubI) 

213 
apply (simp add: thelub_cprod) 

214 
done 

215 

216 
lemma cont_fst: "cont fst" 

217 
apply (rule monocontlub2cont) 

218 
apply (rule monofun_fst) 

219 
apply (rule contlub_fst) 

220 
done 

221 

222 
lemma cont_snd: "cont snd" 

223 
apply (rule monocontlub2cont) 

224 
apply (rule monofun_snd) 

225 
apply (rule contlub_snd) 

226 
done 

227 

228 
lemma cont2cont_Pair [cont2cont]: 

229 
assumes f: "cont (\<lambda>x. f x)" 

230 
assumes g: "cont (\<lambda>x. g x)" 

231 
shows "cont (\<lambda>x. (f x, g x))" 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

232 
apply (rule cont_apply [OF f cont_pair1]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

233 
apply (rule cont_apply [OF g cont_pair2]) 
29533  234 
apply (rule cont_const) 
29531  235 
done 
236 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

237 
lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

238 

85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

239 
lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

240 

85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

241 
lemma cont2cont_split: 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

242 
assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

243 
assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

244 
assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

245 
assumes g: "cont (\<lambda>x. g x)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

246 
shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

247 
unfolding split_def 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

248 
apply (rule cont_apply [OF g]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

249 
apply (rule cont_apply [OF cont_fst f2]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

250 
apply (rule cont_apply [OF cont_snd f3]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

251 
apply (rule cont_const) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

252 
apply (rule f1) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

253 
done 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

254 

85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

255 
lemma cont_fst_snd_D1: 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

256 
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

257 
by (drule cont_compose [OF _ cont_pair1], simp) 
29531  258 

31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

259 
lemma cont_fst_snd_D2: 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

260 
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

261 
by (drule cont_compose [OF _ cont_pair2], simp) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

262 

85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

263 
lemma cont2cont_split' [cont2cont]: 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

264 
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

265 
assumes g: "cont (\<lambda>x. g x)" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

266 
shows "cont (\<lambda>x. split (f x) (g x))" 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

267 
proof  
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

268 
note f1 = f [THEN cont_fst_snd_D1] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

269 
note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

270 
note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2] 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

271 
show ?thesis 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

272 
unfolding split_def 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

273 
apply (rule cont_apply [OF g]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

274 
apply (rule cont_apply [OF cont_fst f2]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

275 
apply (rule cont_apply [OF cont_snd f3]) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

276 
apply (rule cont_const) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

277 
apply (rule f1) 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

278 
done 
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

279 
qed 
29531  280 

29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

281 
subsection {* Compactness and chainfiniteness *} 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

282 

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

283 
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

284 
unfolding below_prod_def by simp 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

285 

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

286 
lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

287 
unfolding below_prod_def by simp 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

288 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

289 
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

290 
by (rule compactI, simp add: fst_below_iff) 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

291 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

292 
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

293 
by (rule compactI, simp add: snd_below_iff) 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

294 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

295 
lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31041
diff
changeset

296 
by (rule compactI, simp add: below_prod_def) 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

297 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

298 
lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

299 
apply (safe intro!: compact_Pair) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

300 
apply (drule compact_fst, simp) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

301 
apply (drule compact_snd, simp) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

302 
done 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

303 

08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

304 
instance "*" :: (chfin, chfin) chfin 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

305 
apply intro_classes 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

306 
apply (erule compact_imp_max_in_chain) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

307 
apply (case_tac "\<Squnion>i. Y i", simp) 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

308 
done 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

309 

29531  310 
end 