|
1 (* Title: HOLCF/Product_Cpo.thy |
|
2 Author: Franz Regensburger |
|
3 *) |
|
4 |
|
5 header {* The cpo of cartesian products *} |
|
6 |
|
7 theory Product_Cpo |
|
8 imports Adm |
|
9 begin |
|
10 |
|
11 default_sort cpo |
|
12 |
|
13 subsection {* Unit type is a pcpo *} |
|
14 |
|
15 instantiation unit :: discrete_cpo |
|
16 begin |
|
17 |
|
18 definition |
|
19 below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True" |
|
20 |
|
21 instance proof |
|
22 qed simp |
|
23 |
|
24 end |
|
25 |
|
26 instance unit :: pcpo |
|
27 by intro_classes simp |
|
28 |
|
29 |
|
30 subsection {* Product type is a partial order *} |
|
31 |
|
32 instantiation prod :: (below, below) below |
|
33 begin |
|
34 |
|
35 definition |
|
36 below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" |
|
37 |
|
38 instance .. |
|
39 end |
|
40 |
|
41 instance prod :: (po, po) po |
|
42 proof |
|
43 fix x :: "'a \<times> 'b" |
|
44 show "x \<sqsubseteq> x" |
|
45 unfolding below_prod_def by simp |
|
46 next |
|
47 fix x y :: "'a \<times> 'b" |
|
48 assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" |
|
49 unfolding below_prod_def Pair_fst_snd_eq |
|
50 by (fast intro: below_antisym) |
|
51 next |
|
52 fix x y z :: "'a \<times> 'b" |
|
53 assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" |
|
54 unfolding below_prod_def |
|
55 by (fast intro: below_trans) |
|
56 qed |
|
57 |
|
58 subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *} |
|
59 |
|
60 lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q" |
|
61 unfolding below_prod_def by simp |
|
62 |
|
63 lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d" |
|
64 unfolding below_prod_def by simp |
|
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 |
|
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 |
|
82 text {* @{term fst} and @{term snd} are monotone *} |
|
83 |
|
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 |
|
90 lemma monofun_fst: "monofun fst" |
|
91 by (simp add: monofun_def below_prod_def) |
|
92 |
|
93 lemma monofun_snd: "monofun snd" |
|
94 by (simp add: monofun_def below_prod_def) |
|
95 |
|
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 |
|
110 subsection {* Product type is a cpo *} |
|
111 |
|
112 lemma is_lub_Pair: |
|
113 "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)" |
|
114 unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp |
|
115 |
|
116 lemma lub_Pair: |
|
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)" |
|
119 by (fast intro: lub_eqI is_lub_Pair elim: thelubE) |
|
120 |
|
121 lemma is_lub_prod: |
|
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))" |
|
125 using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI) |
|
126 |
|
127 lemma lub_prod: |
|
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))" |
|
130 by (rule is_lub_prod [THEN lub_eqI]) |
|
131 |
|
132 instance prod :: (cpo, cpo) cpo |
|
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))" |
|
137 by (rule is_lub_prod) |
|
138 thus "\<exists>x. range S <<| x" .. |
|
139 qed |
|
140 |
|
141 instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo |
|
142 proof |
|
143 fix x y :: "'a \<times> 'b" |
|
144 show "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
|
145 unfolding below_prod_def Pair_fst_snd_eq |
|
146 by simp |
|
147 qed |
|
148 |
|
149 subsection {* Product type is pointed *} |
|
150 |
|
151 lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
|
152 by (simp add: below_prod_def) |
|
153 |
|
154 instance prod :: (pcpo, pcpo) pcpo |
|
155 by intro_classes (fast intro: minimal_prod) |
|
156 |
|
157 lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" |
|
158 by (rule minimal_prod [THEN UU_I, symmetric]) |
|
159 |
|
160 lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" |
|
161 unfolding inst_prod_pcpo by simp |
|
162 |
|
163 lemma fst_strict [simp]: "fst \<bottom> = \<bottom>" |
|
164 unfolding inst_prod_pcpo by (rule fst_conv) |
|
165 |
|
166 lemma snd_strict [simp]: "snd \<bottom> = \<bottom>" |
|
167 unfolding inst_prod_pcpo by (rule snd_conv) |
|
168 |
|
169 lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>" |
|
170 by simp |
|
171 |
|
172 lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>" |
|
173 unfolding split_def by simp |
|
174 |
|
175 subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *} |
|
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) |
|
181 apply (rule is_lub_const) |
|
182 done |
|
183 |
|
184 lemma cont_pair2: "cont (\<lambda>y. (x, y))" |
|
185 apply (rule contI) |
|
186 apply (rule is_lub_Pair) |
|
187 apply (rule is_lub_const) |
|
188 apply (erule cpo_lubI) |
|
189 done |
|
190 |
|
191 lemma cont_fst: "cont fst" |
|
192 apply (rule contI) |
|
193 apply (simp add: lub_prod) |
|
194 apply (erule cpo_lubI [OF ch2ch_fst]) |
|
195 done |
|
196 |
|
197 lemma cont_snd: "cont snd" |
|
198 apply (rule contI) |
|
199 apply (simp add: lub_prod) |
|
200 apply (erule cpo_lubI [OF ch2ch_snd]) |
|
201 done |
|
202 |
|
203 lemma cont2cont_Pair [simp, cont2cont]: |
|
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))" |
|
207 apply (rule cont_apply [OF f cont_pair1]) |
|
208 apply (rule cont_apply [OF g cont_pair2]) |
|
209 apply (rule cont_const) |
|
210 done |
|
211 |
|
212 lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst] |
|
213 |
|
214 lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd] |
|
215 |
|
216 lemma cont2cont_prod_case: |
|
217 assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)" |
|
218 assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)" |
|
219 assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)" |
|
220 assumes g: "cont (\<lambda>x. g x)" |
|
221 shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)" |
|
222 unfolding split_def |
|
223 apply (rule cont_apply [OF g]) |
|
224 apply (rule cont_apply [OF cont_fst f2]) |
|
225 apply (rule cont_apply [OF cont_snd f3]) |
|
226 apply (rule cont_const) |
|
227 apply (rule f1) |
|
228 done |
|
229 |
|
230 lemma prod_contI: |
|
231 assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))" |
|
232 assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))" |
|
233 shows "cont f" |
|
234 proof - |
|
235 have "cont (\<lambda>(x, y). f (x, y))" |
|
236 by (intro cont2cont_prod_case f1 f2 cont2cont) |
|
237 thus "cont f" |
|
238 by (simp only: split_eta) |
|
239 qed |
|
240 |
|
241 lemma prod_cont_iff: |
|
242 "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))" |
|
243 apply safe |
|
244 apply (erule cont_compose [OF _ cont_pair1]) |
|
245 apply (erule cont_compose [OF _ cont_pair2]) |
|
246 apply (simp only: prod_contI) |
|
247 done |
|
248 |
|
249 lemma cont2cont_prod_case' [simp, cont2cont]: |
|
250 assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))" |
|
251 assumes g: "cont (\<lambda>x. g x)" |
|
252 shows "cont (\<lambda>x. prod_case (f x) (g x))" |
|
253 using assms by (simp add: cont2cont_prod_case prod_cont_iff) |
|
254 |
|
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 |
|
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 |
|
270 subsection {* Compactness and chain-finiteness *} |
|
271 |
|
272 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)" |
|
273 unfolding below_prod_def by simp |
|
274 |
|
275 lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)" |
|
276 unfolding below_prod_def by simp |
|
277 |
|
278 lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)" |
|
279 by (rule compactI, simp add: fst_below_iff) |
|
280 |
|
281 lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)" |
|
282 by (rule compactI, simp add: snd_below_iff) |
|
283 |
|
284 lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)" |
|
285 by (rule compactI, simp add: below_prod_def) |
|
286 |
|
287 lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y" |
|
288 apply (safe intro!: compact_Pair) |
|
289 apply (drule compact_fst, simp) |
|
290 apply (drule compact_snd, simp) |
|
291 done |
|
292 |
|
293 instance prod :: (chfin, chfin) chfin |
|
294 apply intro_classes |
|
295 apply (erule compact_imp_max_in_chain) |
|
296 apply (case_tac "\<Squnion>i. Y i", simp) |
|
297 done |
|
298 |
|
299 end |