author  huffman 
Thu, 30 Sep 2010 18:46:19 0700  
changeset 39808  1410c84013b9 
parent 39144  23b1e6759359 
child 40003  427106657e04 
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 

36452  11 
default_sort cpo 
29531  12 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
33506
diff
changeset

13 
subsection {* Unit type is a pcpo *} 
29531  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 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

35 
instantiation prod :: (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 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

44 
instance prod :: (po, po) po 
29531  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 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
33506
diff
changeset

61 
subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *} 
29531  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 

35919  87 
lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y" 
88 
unfolding below_prod_def by simp 

89 

90 
lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y" 

91 
unfolding below_prod_def by simp 

92 

29531  93 
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

94 
by (simp add: monofun_def below_prod_def) 
29531  95 

96 
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

97 
by (simp add: monofun_def below_prod_def) 
29531  98 

31112  99 
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] 
100 

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

102 

103 
lemma prod_chain_cases: 

104 
assumes "chain Y" 

105 
obtains A B 

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

107 
proof 

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

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

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

111 
qed 

112 

29531  113 
subsection {* Product type is a cpo *} 
114 

115 
lemma is_lub_Pair: 

31112  116 
"\<lbrakk>range A << x; range B << y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) << (x, y)" 
29531  117 
apply (rule is_lubI [OF ub_rangeI]) 
31112  118 
apply (simp add: is_ub_lub) 
29531  119 
apply (frule ub2ub_monofun [OF monofun_fst]) 
120 
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

121 
apply (simp add: below_prod_def is_lub_lub) 
29531  122 
done 
123 

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

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

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

128 

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

131 
assumes S: "chain S" 

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

133 
proof  

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

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

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

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

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

143 
using is_lub_Pair [OF 1 2] by simp 

144 
qed 

145 

146 
lemma thelub_cprod: 

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

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

149 
by (rule lub_cprod [THEN thelubI]) 

150 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

151 
instance prod :: (cpo, cpo) cpo 
29531  152 
proof 
153 
fix S :: "nat \<Rightarrow> ('a \<times> 'b)" 

154 
assume "chain S" 

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

156 
by (rule lub_cprod) 

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

158 
qed 

159 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

160 
instance prod :: (finite_po, finite_po) finite_po .. 
29531  161 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

162 
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo 
29531  163 
proof 
164 
fix x y :: "'a \<times> 'b" 

165 
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

166 
unfolding below_prod_def Pair_fst_snd_eq 
29531  167 
by simp 
168 
qed 

169 

170 
subsection {* Product type is pointed *} 

171 

172 
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

173 
by (simp add: below_prod_def) 
29531  174 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

175 
instance prod :: (pcpo, pcpo) pcpo 
29531  176 
by intro_classes (fast intro: minimal_cprod) 
177 

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

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

180 

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

181 
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

182 
unfolding inst_cprod_pcpo by simp 
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 fst_strict [simp]: "fst \<bottom> = \<bottom>" 
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

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

186 

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

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

189 

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

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

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

192 

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

193 
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

194 
unfolding split_def by simp 
29531  195 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
33506
diff
changeset

196 
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *} 
29531  197 

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

199 
apply (rule contI) 

200 
apply (rule is_lub_Pair) 

201 
apply (erule cpo_lubI) 

202 
apply (rule lub_const) 

203 
done 

204 

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

206 
apply (rule contI) 

207 
apply (rule is_lub_Pair) 

208 
apply (rule lub_const) 

209 
apply (erule cpo_lubI) 

210 
done 

211 

35914  212 
lemma cont_fst: "cont fst" 
213 
apply (rule contI) 

29531  214 
apply (simp add: thelub_cprod) 
35914  215 
apply (erule cpo_lubI [OF ch2ch_fst]) 
29531  216 
done 
217 

218 
lemma cont_snd: "cont snd" 

35914  219 
apply (rule contI) 
220 
apply (simp add: thelub_cprod) 

221 
apply (erule cpo_lubI [OF ch2ch_snd]) 

29531  222 
done 
223 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36452
diff
changeset

224 
lemma cont2cont_Pair [simp, cont2cont]: 
29531  225 
assumes f: "cont (\<lambda>x. f x)" 
226 
assumes g: "cont (\<lambda>x. g x)" 

227 
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

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

229 
apply (rule cont_apply [OF g cont_pair2]) 
29533  230 
apply (rule cont_const) 
29531  231 
done 
232 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36452
diff
changeset

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

234 

37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36452
diff
changeset

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

236 

39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

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

238 
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

239 
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

240 
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

241 
assumes g: "cont (\<lambda>x. g x)" 
39144  242 
shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)" 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

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

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

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

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

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

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

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

250 

39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

251 
lemma prod_contI: 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

252 
assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

253 
assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

254 
shows "cont f" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

255 
proof  
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

256 
have "cont (\<lambda>(x, y). f (x, y))" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

257 
by (intro cont2cont_prod_case f1 f2 cont2cont) 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

258 
thus "cont f" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

259 
by (simp only: split_eta) 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

260 
qed 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

261 

1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

262 
lemma prod_cont_iff: 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

263 
"cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

264 
apply safe 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

265 
apply (erule cont_compose [OF _ cont_pair1]) 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

266 
apply (erule cont_compose [OF _ cont_pair2]) 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

267 
apply (simp only: prod_contI) 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

268 
done 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

269 

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

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

271 
"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

272 
by (drule cont_compose [OF _ cont_pair1], simp) 
29531  273 

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

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

275 
"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

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

277 

39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

278 
lemma cont2cont_prod_case' [simp, cont2cont]: 
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset

279 
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

280 
assumes g: "cont (\<lambda>x. g x)" 
39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

281 
shows "cont (\<lambda>x. prod_case (f x) (g x))" 
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset

282 
using assms by (simp add: cont2cont_prod_case prod_cont_iff) 
29531  283 

39144  284 
text {* The simple version (due to Joachim Breitner) is needed if 
285 
either element type of the pair is not a cpo. *} 

286 

287 
lemma cont2cont_split_simple [simp, cont2cont]: 

288 
assumes "\<And>a b. cont (\<lambda>x. f x a b)" 

289 
shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)" 

290 
using assms by (cases p) auto 

291 

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

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

293 

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

294 
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

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

296 

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

297 
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

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

299 

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

300 
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

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

302 

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

303 
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

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

305 

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

306 
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

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

308 

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

309 
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

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

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

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

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

314 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset

315 
instance prod :: (chfin, chfin) chfin 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

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

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

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

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

320 

29531  321 
end 