author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44066  d74182c93f04 
child 55414  eab03e9cee8a 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Product_Cpo.thy 
29531  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 

40090  15 
instantiation unit :: discrete_cpo 
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 

40090  21 
instance proof 
22 
qed simp 

29531  23 

40090  24 
end 
29531  25 

26 
instance unit :: pcpo 

27 
by intro_classes simp 

28 

29 

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

31 

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

32 
instantiation prod :: (below, below) below 
29531  33 
begin 
34 

35 
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

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

38 
instance .. 

39 
end 

40 

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

41 
instance prod :: (po, po) po 
29531  42 
proof 
43 
fix x :: "'a \<times> 'b" 

44 
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

45 
unfolding below_prod_def by simp 
29531  46 
next 
47 
fix x y :: "'a \<times> 'b" 

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

44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset

49 
unfolding below_prod_def prod_eq_iff 
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

50 
by (fast intro: below_antisym) 
29531  51 
next 
52 
fix x y z :: "'a \<times> 'b" 

53 
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

54 
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

55 
by (fast intro: below_trans) 
29531  56 
qed 
57 

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

58 
subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *} 
29531  59 

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

60 
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

61 
unfolding below_prod_def by simp 
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 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

64 
unfolding below_prod_def by simp 
29531  65 

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

67 

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

69 
by (simp add: monofun_def) 

70 

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

72 
by (simp add: monofun_def) 

73 

74 
lemma monofun_pair: 

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

76 
by simp 

77 

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

80 
by (rule chainI, simp add: chainE) 

81 

29531  82 
text {* @{term fst} and @{term snd} are monotone *} 
83 

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

86 

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

88 
unfolding below_prod_def by simp 

89 

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

91 
by (simp add: monofun_def below_prod_def) 
29531  92 

93 
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

94 
by (simp add: monofun_def below_prod_def) 
29531  95 

31112  96 
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] 
97 

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

99 

100 
lemma prod_chain_cases: 

101 
assumes "chain Y" 

102 
obtains A B 

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

104 
proof 

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

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

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

108 
qed 

109 

29531  110 
subsection {* Product type is a cpo *} 
111 

112 
lemma is_lub_Pair: 

31112  113 
"\<lbrakk>range A << x; range B << y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) << (x, y)" 
40771  114 
unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp 
29531  115 

40771  116 
lemma lub_Pair: 
31112  117 
"\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk> 
118 
\<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)" 

40771  119 
by (fast intro: lub_eqI is_lub_Pair elim: thelubE) 
31112  120 

40771  121 
lemma is_lub_prod: 
29531  122 
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" 
123 
assumes S: "chain S" 

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

40771  125 
using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI) 
29531  126 

40771  127 
lemma lub_prod: 
29531  128 
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) 
129 
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" 

40771  130 
by (rule is_lub_prod [THEN lub_eqI]) 
29531  131 

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

132 
instance prod :: (cpo, cpo) cpo 
29531  133 
proof 
134 
fix S :: "nat \<Rightarrow> ('a \<times> 'b)" 

135 
assume "chain S" 

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

40771  137 
by (rule is_lub_prod) 
29531  138 
thus "\<exists>x. range S << x" .. 
139 
qed 

140 

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

141 
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo 
29531  142 
proof 
143 
fix x y :: "'a \<times> 'b" 

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

44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset

145 
unfolding below_prod_def prod_eq_iff 
29531  146 
by simp 
147 
qed 

148 

149 
subsection {* Product type is pointed *} 

150 

40771  151 
lemma minimal_prod: "(\<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

152 
by (simp add: below_prod_def) 
29531  153 

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

154 
instance prod :: (pcpo, pcpo) pcpo 
40771  155 
by intro_classes (fast intro: minimal_prod) 
29531  156 

40771  157 
lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40774
diff
changeset

158 
by (rule minimal_prod [THEN bottomI, symmetric]) 
29531  159 

40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40090
diff
changeset

160 
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" 
40771  161 
unfolding inst_prod_pcpo by simp 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

162 

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

163 
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>" 
40771  164 
unfolding inst_prod_pcpo by (rule fst_conv) 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

165 

33506  166 
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>" 
40771  167 
unfolding inst_prod_pcpo by (rule snd_conv) 
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset

168 

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

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

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

171 

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

172 
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

173 
unfolding split_def by simp 
29531  174 

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

175 
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *} 
29531  176 

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

178 
apply (rule contI) 

179 
apply (rule is_lub_Pair) 

180 
apply (erule cpo_lubI) 

40771  181 
apply (rule is_lub_const) 
29531  182 
done 
183 

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

185 
apply (rule contI) 

186 
apply (rule is_lub_Pair) 

40771  187 
apply (rule is_lub_const) 
29531  188 
apply (erule cpo_lubI) 
189 
done 

190 

35914  191 
lemma cont_fst: "cont fst" 
192 
apply (rule contI) 

40771  193 
apply (simp add: lub_prod) 
35914  194 
apply (erule cpo_lubI [OF ch2ch_fst]) 
29531  195 
done 
196 

197 
lemma cont_snd: "cont snd" 

35914  198 
apply (rule contI) 
40771  199 
apply (simp add: lub_prod) 
35914  200 
apply (erule cpo_lubI [OF ch2ch_snd]) 
29531  201 
done 
202 

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

203 
lemma cont2cont_Pair [simp, cont2cont]: 
29531  204 
assumes f: "cont (\<lambda>x. f x)" 
205 
assumes g: "cont (\<lambda>x. g x)" 

206 
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

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

208 
apply (rule cont_apply [OF g cont_pair2]) 
29533  209 
apply (rule cont_const) 
29531  210 
done 
211 

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

212 
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

213 

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

214 
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

215 

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

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

217 
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

218 
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

219 
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

220 
assumes g: "cont (\<lambda>x. g x)" 
39144  221 
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

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

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

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

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

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

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

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

229 

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

230 
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

231 
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

232 
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

233 
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

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

235 
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

236 
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

237 
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

238 
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

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

240 

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

241 
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

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

243 
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

244 
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

245 
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

246 
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

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

248 

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

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

250 
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

251 
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

252 
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

253 
using assms by (simp add: cont2cont_prod_case prod_cont_iff) 
29531  254 

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

257 

258 
lemma cont2cont_split_simple [simp, cont2cont]: 

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

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

261 
using assms by (cases p) auto 

262 

40619  263 
text {* Admissibility of predicates on product types. *} 
264 

265 
lemma adm_prod_case [simp]: 

266 
assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))" 

267 
shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)" 

268 
unfolding prod_case_beta using assms . 

269 

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

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

271 

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

272 
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

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

274 

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

275 
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

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

277 

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

278 
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

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

280 

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

281 
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

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

283 

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

284 
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

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

286 

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

287 
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

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

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

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

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

292 

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

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

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

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

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

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

298 

29531  299 
end 