1(*  Title:      HOL/HOLCF/Product_Cpo.thy
2    Author:     Franz Regensburger
3*)
4
5section \<open>The cpo of cartesian products\<close>
6
7theory Product_Cpo
8  imports Adm
9begin
10
11default_sort cpo
12
13
14subsection \<open>Unit type is a pcpo\<close>
15
16instantiation unit :: discrete_cpo
17begin
18
19definition below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
20
21instance
22  by standard simp
23
24end
25
26instance unit :: pcpo
27  by standard simp
28
29
30subsection \<open>Product type is a partial order\<close>
31
32instantiation prod :: (below, below) below
33begin
34
35definition below_prod_def: "(\<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
36
37instance ..
38
39end
40
41instance prod :: (po, po) po
42proof
43  fix x :: "'a \<times> 'b"
44  show "x \<sqsubseteq> x"
45    by (simp add: below_prod_def)
46next
47  fix x y :: "'a \<times> 'b"
48  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x"
49  then show "x = y"
50    unfolding below_prod_def prod_eq_iff
51    by (fast intro: below_antisym)
52next
53  fix x y z :: "'a \<times> 'b"
54  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z"
55  then show "x \<sqsubseteq> z"
56    unfolding below_prod_def
57    by (fast intro: below_trans)
58qed
59
60
61subsection \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
62
63lemma prod_belowI: "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
64  by (simp add: below_prod_def)
65
66lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
67  by (simp add: below_prod_def)
68
69text \<open>Pair \<open>(_,_)\<close>  is monotone in both arguments\<close>
70
71lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
72  by (simp add: monofun_def)
73
74lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
75  by (simp add: monofun_def)
76
77lemma monofun_pair: "x1 \<sqsubseteq> x2 \<Longrightarrow> y1 \<sqsubseteq> y2 \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
78  by simp
79
80lemma ch2ch_Pair [simp]: "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
81  by (rule chainI, simp add: chainE)
82
83text \<open>\<^term>\<open>fst\<close> and \<^term>\<open>snd\<close> are monotone\<close>
84
85lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
86  by (simp add: below_prod_def)
87
88lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"
89  by (simp add: below_prod_def)
90
91lemma monofun_fst: "monofun fst"
92  by (simp add: monofun_def below_prod_def)
93
94lemma monofun_snd: "monofun snd"
95  by (simp add: monofun_def below_prod_def)
96
97lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
98
99lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
100
101lemma prod_chain_cases:
102  assumes chain: "chain Y"
103  obtains A B
104  where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
105proof
106  from chain show "chain (\<lambda>i. fst (Y i))"
107    by (rule ch2ch_fst)
108  from chain show "chain (\<lambda>i. snd (Y i))"
109    by (rule ch2ch_snd)
110  show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))"
111    by simp
112qed
113
114
115subsection \<open>Product type is a cpo\<close>
116
117lemma is_lub_Pair: "range A <<| x \<Longrightarrow> range B <<| y \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
118  by (simp add: is_lub_def is_ub_def below_prod_def)
119
120lemma lub_Pair: "chain A \<Longrightarrow> chain B \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
121  for A :: "nat \<Rightarrow> 'a::cpo" and B :: "nat \<Rightarrow> 'b::cpo"
122  by (fast intro: lub_eqI is_lub_Pair elim: thelubE)
123
124lemma is_lub_prod:
125  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
126  assumes "chain S"
127  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
128  using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI)
129
130lemma lub_prod: "chain S \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
131  for S :: "nat \<Rightarrow> 'a::cpo \<times> 'b::cpo"
132  by (rule is_lub_prod [THEN lub_eqI])
133
134instance prod :: (cpo, cpo) cpo
135proof
136  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
137  assume "chain S"
138  then have "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
139    by (rule is_lub_prod)
140  then show "\<exists>x. range S <<| x" ..
141qed
142
143instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo
144proof
145  fix x y :: "'a \<times> 'b"
146  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
147    by (simp add: below_prod_def prod_eq_iff)
148qed
149
150
151subsection \<open>Product type is pointed\<close>
152
153lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
154  by (simp add: below_prod_def)
155
156instance prod :: (pcpo, pcpo) pcpo
157  by intro_classes (fast intro: minimal_prod)
158
159lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
160  by (rule minimal_prod [THEN bottomI, symmetric])
161
162lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
163  by (simp add: inst_prod_pcpo)
164
165lemma fst_strict [simp]: "fst \<bottom> = \<bottom>"
166  unfolding inst_prod_pcpo by (rule fst_conv)
167
168lemma snd_strict [simp]: "snd \<bottom> = \<bottom>"
169  unfolding inst_prod_pcpo by (rule snd_conv)
170
171lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
172  by simp
173
174lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
175  by (simp add: split_def)
176
177
178subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
179
180lemma cont_pair1: "cont (\<lambda>x. (x, y))"
181  apply (rule contI)
182  apply (rule is_lub_Pair)
183   apply (erule cpo_lubI)
184  apply (rule is_lub_const)
185  done
186
187lemma cont_pair2: "cont (\<lambda>y. (x, y))"
188  apply (rule contI)
189  apply (rule is_lub_Pair)
190   apply (rule is_lub_const)
191  apply (erule cpo_lubI)
192  done
193
194lemma cont_fst: "cont fst"
195  apply (rule contI)
196  apply (simp add: lub_prod)
197  apply (erule cpo_lubI [OF ch2ch_fst])
198  done
199
200lemma cont_snd: "cont snd"
201  apply (rule contI)
202  apply (simp add: lub_prod)
203  apply (erule cpo_lubI [OF ch2ch_snd])
204  done
205
206lemma cont2cont_Pair [simp, cont2cont]:
207  assumes f: "cont (\<lambda>x. f x)"
208  assumes g: "cont (\<lambda>x. g x)"
209  shows "cont (\<lambda>x. (f x, g x))"
210  apply (rule cont_apply [OF f cont_pair1])
211  apply (rule cont_apply [OF g cont_pair2])
212  apply (rule cont_const)
213  done
214
215lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
216
217lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
218
219lemma cont2cont_case_prod:
220  assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
221  assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
222  assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
223  assumes g: "cont (\<lambda>x. g x)"
224  shows "cont (\<lambda>x. case g x of (a, b) \<Rightarrow> f x a b)"
225  unfolding split_def
226  apply (rule cont_apply [OF g])
227   apply (rule cont_apply [OF cont_fst f2])
228   apply (rule cont_apply [OF cont_snd f3])
229   apply (rule cont_const)
230  apply (rule f1)
231  done
232
233lemma prod_contI:
234  assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
235  assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
236  shows "cont f"
237proof -
238  have "cont (\<lambda>(x, y). f (x, y))"
239    by (intro cont2cont_case_prod f1 f2 cont2cont)
240  then show "cont f"
241    by (simp only: case_prod_eta)
242qed
243
244lemma prod_cont_iff: "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
245  apply safe
246    apply (erule cont_compose [OF _ cont_pair1])
247   apply (erule cont_compose [OF _ cont_pair2])
248  apply (simp only: prod_contI)
249  done
250
251lemma cont2cont_case_prod' [simp, cont2cont]:
252  assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
253  assumes g: "cont (\<lambda>x. g x)"
254  shows "cont (\<lambda>x. case_prod (f x) (g x))"
255  using assms by (simp add: cont2cont_case_prod prod_cont_iff)
256
257text \<open>The simple version (due to Joachim Breitner) is needed if
258  either element type of the pair is not a cpo.\<close>
259
260lemma cont2cont_split_simple [simp, cont2cont]:
261  assumes "\<And>a b. cont (\<lambda>x. f x a b)"
262  shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
263  using assms by (cases p) auto
264
265text \<open>Admissibility of predicates on product types.\<close>
266
267lemma adm_case_prod [simp]:
268  assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
269  shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
270  unfolding case_prod_beta using assms .
271
272
273subsection \<open>Compactness and chain-finiteness\<close>
274
275lemma fst_below_iff: "fst x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
276  for x :: "'a \<times> 'b"
277  by (simp add: below_prod_def)
278
279lemma snd_below_iff: "snd x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
280  for x :: "'a \<times> 'b"
281  by (simp add: below_prod_def)
282
283lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
284  by (rule compactI) (simp add: fst_below_iff)
285
286lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
287  by (rule compactI) (simp add: snd_below_iff)
288
289lemma compact_Pair: "compact x \<Longrightarrow> compact y \<Longrightarrow> compact (x, y)"
290  by (rule compactI) (simp add: below_prod_def)
291
292lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
293  apply (safe intro!: compact_Pair)
294   apply (drule compact_fst, simp)
295  apply (drule compact_snd, simp)
296  done
297
298instance prod :: (chfin, chfin) chfin
299  apply intro_classes
300  apply (erule compact_imp_max_in_chain)
301  apply (case_tac "\<Squnion>i. Y i", simp)
302  done
303
304end
305