author | huffman |
Thu, 15 Jan 2009 08:11:50 -0800 | |
changeset 29535 | 08824fad8879 |
parent 29533 | 7f4a32134447 |
child 31041 | 85b4843d9939 |
permissions | -rw-r--r-- |
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 |
||
15 |
instantiation unit :: sq_ord |
|
16 |
begin |
|
17 |
||
18 |
definition |
|
19 |
less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True" |
|
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 |
||
35 |
instantiation "*" :: (sq_ord, sq_ord) sq_ord |
|
36 |
begin |
|
37 |
||
38 |
definition |
|
39 |
less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" |
|
40 |
||
41 |
instance .. |
|
42 |
end |
|
43 |
||
44 |
instance "*" :: (po, po) po |
|
45 |
proof |
|
46 |
fix x :: "'a \<times> 'b" |
|
47 |
show "x \<sqsubseteq> x" |
|
48 |
unfolding less_cprod_def by simp |
|
49 |
next |
|
50 |
fix x y :: "'a \<times> 'b" |
|
51 |
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" |
|
52 |
unfolding less_cprod_def Pair_fst_snd_eq |
|
53 |
by (fast intro: antisym_less) |
|
54 |
next |
|
55 |
fix x y z :: "'a \<times> 'b" |
|
56 |
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" |
|
57 |
unfolding less_cprod_def |
|
58 |
by (fast intro: trans_less) |
|
59 |
qed |
|
60 |
||
61 |
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
|
62 |
||
63 |
lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q" |
|
64 |
unfolding less_cprod_def by simp |
|
65 |
||
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
66 |
lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d" |
29531 | 67 |
unfolding less_cprod_def by simp |
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 |
||
81 |
text {* @{term fst} and @{term snd} are monotone *} |
|
82 |
||
83 |
lemma monofun_fst: "monofun fst" |
|
84 |
by (simp add: monofun_def less_cprod_def) |
|
85 |
||
86 |
lemma monofun_snd: "monofun snd" |
|
87 |
by (simp add: monofun_def less_cprod_def) |
|
88 |
||
89 |
subsection {* Product type is a cpo *} |
|
90 |
||
91 |
lemma is_lub_Pair: |
|
92 |
"\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)" |
|
93 |
apply (rule is_lubI [OF ub_rangeI]) |
|
94 |
apply (simp add: less_cprod_def is_ub_lub) |
|
95 |
apply (frule ub2ub_monofun [OF monofun_fst]) |
|
96 |
apply (drule ub2ub_monofun [OF monofun_snd]) |
|
97 |
apply (simp add: less_cprod_def is_lub_lub) |
|
98 |
done |
|
99 |
||
100 |
lemma lub_cprod: |
|
101 |
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" |
|
102 |
assumes S: "chain S" |
|
103 |
shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
104 |
proof - |
|
105 |
have "chain (\<lambda>i. fst (S i))" |
|
106 |
using monofun_fst S by (rule ch2ch_monofun) |
|
107 |
hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))" |
|
108 |
by (rule cpo_lubI) |
|
109 |
have "chain (\<lambda>i. snd (S i))" |
|
110 |
using monofun_snd S by (rule ch2ch_monofun) |
|
111 |
hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))" |
|
112 |
by (rule cpo_lubI) |
|
113 |
show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
114 |
using is_lub_Pair [OF 1 2] by simp |
|
115 |
qed |
|
116 |
||
117 |
lemma thelub_cprod: |
|
118 |
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
|
119 |
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
120 |
by (rule lub_cprod [THEN thelubI]) |
|
121 |
||
122 |
instance "*" :: (cpo, cpo) cpo |
|
123 |
proof |
|
124 |
fix S :: "nat \<Rightarrow> ('a \<times> 'b)" |
|
125 |
assume "chain S" |
|
126 |
hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
127 |
by (rule lub_cprod) |
|
128 |
thus "\<exists>x. range S <<| x" .. |
|
129 |
qed |
|
130 |
||
131 |
instance "*" :: (finite_po, finite_po) finite_po .. |
|
132 |
||
133 |
instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo |
|
134 |
proof |
|
135 |
fix x y :: "'a \<times> 'b" |
|
136 |
show "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
|
137 |
unfolding less_cprod_def Pair_fst_snd_eq |
|
138 |
by simp |
|
139 |
qed |
|
140 |
||
141 |
subsection {* Product type is pointed *} |
|
142 |
||
143 |
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
|
144 |
by (simp add: less_cprod_def) |
|
145 |
||
146 |
instance "*" :: (pcpo, pcpo) pcpo |
|
147 |
by intro_classes (fast intro: minimal_cprod) |
|
148 |
||
149 |
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" |
|
150 |
by (rule minimal_cprod [THEN UU_I, symmetric]) |
|
151 |
||
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
152 |
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
|
153 |
unfolding inst_cprod_pcpo by simp |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
154 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
155 |
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
156 |
unfolding inst_cprod_pcpo by (rule fst_conv) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
157 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
158 |
lemma csnd_strict [simp]: "snd \<bottom> = \<bottom>" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
159 |
unfolding inst_cprod_pcpo by (rule snd_conv) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
160 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
161 |
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
162 |
by simp |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
163 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
164 |
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
|
165 |
unfolding split_def by simp |
29531 | 166 |
|
167 |
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
|
168 |
||
169 |
lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
|
170 |
apply (rule contI) |
|
171 |
apply (rule is_lub_Pair) |
|
172 |
apply (erule cpo_lubI) |
|
173 |
apply (rule lub_const) |
|
174 |
done |
|
175 |
||
176 |
lemma cont_pair2: "cont (\<lambda>y. (x, y))" |
|
177 |
apply (rule contI) |
|
178 |
apply (rule is_lub_Pair) |
|
179 |
apply (rule lub_const) |
|
180 |
apply (erule cpo_lubI) |
|
181 |
done |
|
182 |
||
183 |
lemma contlub_fst: "contlub fst" |
|
184 |
apply (rule contlubI) |
|
185 |
apply (simp add: thelub_cprod) |
|
186 |
done |
|
187 |
||
188 |
lemma contlub_snd: "contlub snd" |
|
189 |
apply (rule contlubI) |
|
190 |
apply (simp add: thelub_cprod) |
|
191 |
done |
|
192 |
||
193 |
lemma cont_fst: "cont fst" |
|
194 |
apply (rule monocontlub2cont) |
|
195 |
apply (rule monofun_fst) |
|
196 |
apply (rule contlub_fst) |
|
197 |
done |
|
198 |
||
199 |
lemma cont_snd: "cont snd" |
|
200 |
apply (rule monocontlub2cont) |
|
201 |
apply (rule monofun_snd) |
|
202 |
apply (rule contlub_snd) |
|
203 |
done |
|
204 |
||
205 |
lemma cont2cont_Pair [cont2cont]: |
|
206 |
assumes f: "cont (\<lambda>x. f x)" |
|
207 |
assumes g: "cont (\<lambda>x. g x)" |
|
208 |
shows "cont (\<lambda>x. (f x, g x))" |
|
29533 | 209 |
apply (rule cont2cont_apply [OF _ cont_pair1 f]) |
210 |
apply (rule cont2cont_apply [OF _ cont_pair2 g]) |
|
211 |
apply (rule cont_const) |
|
29531 | 212 |
done |
213 |
||
29533 | 214 |
lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst] |
29531 | 215 |
|
29533 | 216 |
lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd] |
29531 | 217 |
|
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
218 |
subsection {* Compactness and chain-finiteness *} |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
219 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
220 |
lemma fst_less_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
221 |
unfolding less_cprod_def by simp |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
222 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
223 |
lemma snd_less_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y = x \<sqsubseteq> (fst x, y)" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
224 |
unfolding less_cprod_def by simp |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
225 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
226 |
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
227 |
by (rule compactI, simp add: fst_less_iff) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
228 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
229 |
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
230 |
by (rule compactI, simp add: snd_less_iff) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
231 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
232 |
lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
233 |
by (rule compactI, simp add: less_cprod_def) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
234 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
235 |
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
|
236 |
apply (safe intro!: compact_Pair) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
237 |
apply (drule compact_fst, simp) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
238 |
apply (drule compact_snd, simp) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
239 |
done |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
240 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
241 |
instance "*" :: (chfin, chfin) chfin |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
242 |
apply intro_classes |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
243 |
apply (erule compact_imp_max_in_chain) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
244 |
apply (case_tac "\<Squnion>i. Y i", simp) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
245 |
done |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
246 |
|
29531 | 247 |
end |