author | huffman |
Fri, 22 Oct 2010 06:58:45 -0700 | |
changeset 40089 | 8adc57fb8454 |
parent 40003 | 427106657e04 |
child 40090 | d57357cda8bb |
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 |
||
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 :: pcpo |
|
28 |
by intro_classes simp |
|
29 |
||
30 |
||
31 |
subsection {* Product type is a partial order *} |
|
32 |
||
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset
|
33 |
instantiation prod :: (below, below) below |
29531 | 34 |
begin |
35 |
||
36 |
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
|
37 |
below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" |
29531 | 38 |
|
39 |
instance .. |
|
40 |
end |
|
41 |
||
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset
|
42 |
instance prod :: (po, po) po |
29531 | 43 |
proof |
44 |
fix x :: "'a \<times> 'b" |
|
45 |
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
|
46 |
unfolding below_prod_def by simp |
29531 | 47 |
next |
48 |
fix x y :: "'a \<times> 'b" |
|
49 |
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
|
50 |
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
|
51 |
by (fast intro: below_antisym) |
29531 | 52 |
next |
53 |
fix x y z :: "'a \<times> 'b" |
|
54 |
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
|
55 |
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
|
56 |
by (fast intro: below_trans) |
29531 | 57 |
qed |
58 |
||
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
33506
diff
changeset
|
59 |
subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *} |
29531 | 60 |
|
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
|
61 |
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
|
62 |
unfolding below_prod_def by simp |
29531 | 63 |
|
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
|
64 |
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
|
65 |
unfolding below_prod_def by simp |
29531 | 66 |
|
67 |
text {* Pair @{text "(_,_)"} is monotone in both arguments *} |
|
68 |
||
69 |
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" |
|
70 |
by (simp add: monofun_def) |
|
71 |
||
72 |
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" |
|
73 |
by (simp add: monofun_def) |
|
74 |
||
75 |
lemma monofun_pair: |
|
76 |
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" |
|
77 |
by simp |
|
78 |
||
31112 | 79 |
lemma ch2ch_Pair [simp]: |
80 |
"chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))" |
|
81 |
by (rule chainI, simp add: chainE) |
|
82 |
||
29531 | 83 |
text {* @{term fst} and @{term snd} are monotone *} |
84 |
||
35919 | 85 |
lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y" |
86 |
unfolding below_prod_def by simp |
|
87 |
||
88 |
lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y" |
|
89 |
unfolding below_prod_def by simp |
|
90 |
||
29531 | 91 |
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
|
92 |
by (simp add: monofun_def below_prod_def) |
29531 | 93 |
|
94 |
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
|
95 |
by (simp add: monofun_def below_prod_def) |
29531 | 96 |
|
31112 | 97 |
lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] |
98 |
||
99 |
lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd] |
|
100 |
||
101 |
lemma prod_chain_cases: |
|
102 |
assumes "chain Y" |
|
103 |
obtains A B |
|
104 |
where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))" |
|
105 |
proof |
|
106 |
from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst) |
|
107 |
from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd) |
|
108 |
show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp |
|
109 |
qed |
|
110 |
||
29531 | 111 |
subsection {* Product type is a cpo *} |
112 |
||
113 |
lemma is_lub_Pair: |
|
31112 | 114 |
"\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)" |
29531 | 115 |
apply (rule is_lubI [OF ub_rangeI]) |
31112 | 116 |
apply (simp add: is_ub_lub) |
29531 | 117 |
apply (frule ub2ub_monofun [OF monofun_fst]) |
118 |
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
|
119 |
apply (simp add: below_prod_def is_lub_lub) |
29531 | 120 |
done |
121 |
||
31112 | 122 |
lemma thelub_Pair: |
123 |
"\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk> |
|
124 |
\<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)" |
|
125 |
by (fast intro: thelubI is_lub_Pair elim: thelubE) |
|
126 |
||
29531 | 127 |
lemma lub_cprod: |
128 |
fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" |
|
129 |
assumes S: "chain S" |
|
130 |
shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
131 |
proof - |
|
31112 | 132 |
from `chain S` have "chain (\<lambda>i. fst (S i))" |
133 |
by (rule ch2ch_fst) |
|
29531 | 134 |
hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))" |
135 |
by (rule cpo_lubI) |
|
31112 | 136 |
from `chain S` have "chain (\<lambda>i. snd (S i))" |
137 |
by (rule ch2ch_snd) |
|
29531 | 138 |
hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))" |
139 |
by (rule cpo_lubI) |
|
140 |
show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
141 |
using is_lub_Pair [OF 1 2] by simp |
|
142 |
qed |
|
143 |
||
144 |
lemma thelub_cprod: |
|
145 |
"chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
|
146 |
\<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
147 |
by (rule lub_cprod [THEN thelubI]) |
|
148 |
||
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset
|
149 |
instance prod :: (cpo, cpo) cpo |
29531 | 150 |
proof |
151 |
fix S :: "nat \<Rightarrow> ('a \<times> 'b)" |
|
152 |
assume "chain S" |
|
153 |
hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
|
154 |
by (rule lub_cprod) |
|
155 |
thus "\<exists>x. range S <<| x" .. |
|
156 |
qed |
|
157 |
||
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset
|
158 |
instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo |
29531 | 159 |
proof |
160 |
fix x y :: "'a \<times> 'b" |
|
161 |
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
|
162 |
unfolding below_prod_def Pair_fst_snd_eq |
29531 | 163 |
by simp |
164 |
qed |
|
165 |
||
166 |
subsection {* Product type is pointed *} |
|
167 |
||
168 |
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
|
169 |
by (simp add: below_prod_def) |
29531 | 170 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset
|
171 |
instance prod :: (pcpo, pcpo) pcpo |
29531 | 172 |
by intro_classes (fast intro: minimal_cprod) |
173 |
||
174 |
lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" |
|
175 |
by (rule minimal_cprod [THEN UU_I, symmetric]) |
|
176 |
||
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
177 |
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
|
178 |
unfolding inst_cprod_pcpo by simp |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
179 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
180 |
lemma fst_strict [simp]: "fst \<bottom> = \<bottom>" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
181 |
unfolding inst_cprod_pcpo by (rule fst_conv) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
182 |
|
33506 | 183 |
lemma snd_strict [simp]: "snd \<bottom> = \<bottom>" |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
184 |
unfolding inst_cprod_pcpo by (rule snd_conv) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
185 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
186 |
lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>" |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
187 |
by simp |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
188 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
189 |
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
|
190 |
unfolding split_def by simp |
29531 | 191 |
|
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
33506
diff
changeset
|
192 |
subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *} |
29531 | 193 |
|
194 |
lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
|
195 |
apply (rule contI) |
|
196 |
apply (rule is_lub_Pair) |
|
197 |
apply (erule cpo_lubI) |
|
198 |
apply (rule lub_const) |
|
199 |
done |
|
200 |
||
201 |
lemma cont_pair2: "cont (\<lambda>y. (x, y))" |
|
202 |
apply (rule contI) |
|
203 |
apply (rule is_lub_Pair) |
|
204 |
apply (rule lub_const) |
|
205 |
apply (erule cpo_lubI) |
|
206 |
done |
|
207 |
||
35914 | 208 |
lemma cont_fst: "cont fst" |
209 |
apply (rule contI) |
|
29531 | 210 |
apply (simp add: thelub_cprod) |
35914 | 211 |
apply (erule cpo_lubI [OF ch2ch_fst]) |
29531 | 212 |
done |
213 |
||
214 |
lemma cont_snd: "cont snd" |
|
35914 | 215 |
apply (rule contI) |
216 |
apply (simp add: thelub_cprod) |
|
217 |
apply (erule cpo_lubI [OF ch2ch_snd]) |
|
29531 | 218 |
done |
219 |
||
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36452
diff
changeset
|
220 |
lemma cont2cont_Pair [simp, cont2cont]: |
29531 | 221 |
assumes f: "cont (\<lambda>x. f x)" |
222 |
assumes g: "cont (\<lambda>x. g x)" |
|
223 |
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
|
224 |
apply (rule cont_apply [OF f cont_pair1]) |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
225 |
apply (rule cont_apply [OF g cont_pair2]) |
29533 | 226 |
apply (rule cont_const) |
29531 | 227 |
done |
228 |
||
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36452
diff
changeset
|
229 |
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
|
230 |
|
37079
0cd15d8c90a0
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman
parents:
36452
diff
changeset
|
231 |
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
|
232 |
|
39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
233 |
lemma cont2cont_prod_case: |
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
234 |
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
|
235 |
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
|
236 |
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
|
237 |
assumes g: "cont (\<lambda>x. g x)" |
39144 | 238 |
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
|
239 |
unfolding split_def |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
240 |
apply (rule cont_apply [OF g]) |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
241 |
apply (rule cont_apply [OF cont_fst f2]) |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
242 |
apply (rule cont_apply [OF cont_snd f3]) |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
243 |
apply (rule cont_const) |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
244 |
apply (rule f1) |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
245 |
done |
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
246 |
|
39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
247 |
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
|
248 |
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
|
249 |
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
|
250 |
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
|
251 |
proof - |
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
252 |
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
|
253 |
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
|
254 |
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
|
255 |
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
|
256 |
qed |
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
257 |
|
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
258 |
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
|
259 |
"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
|
260 |
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
|
261 |
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
|
262 |
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
|
263 |
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
|
264 |
done |
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
265 |
|
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39144
diff
changeset
|
266 |
lemma cont2cont_prod_case' [simp, cont2cont]: |
31041
85b4843d9939
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
huffman
parents:
29535
diff
changeset
|
267 |
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
|
268 |
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
|
269 |
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
|
270 |
using assms by (simp add: cont2cont_prod_case prod_cont_iff) |
29531 | 271 |
|
39144 | 272 |
text {* The simple version (due to Joachim Breitner) is needed if |
273 |
either element type of the pair is not a cpo. *} |
|
274 |
||
275 |
lemma cont2cont_split_simple [simp, cont2cont]: |
|
276 |
assumes "\<And>a b. cont (\<lambda>x. f x a b)" |
|
277 |
shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)" |
|
278 |
using assms by (cases p) auto |
|
279 |
||
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
280 |
subsection {* Compactness and chain-finiteness *} |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
281 |
|
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 |
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
|
283 |
unfolding below_prod_def by simp |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
284 |
|
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 |
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
|
286 |
unfolding below_prod_def by simp |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
287 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
288 |
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
|
289 |
by (rule compactI, simp add: fst_below_iff) |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
290 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
291 |
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
|
292 |
by (rule compactI, simp add: snd_below_iff) |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
293 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
294 |
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
|
295 |
by (rule compactI, simp add: below_prod_def) |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
296 |
|
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
297 |
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
|
298 |
apply (safe intro!: compact_Pair) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
299 |
apply (drule compact_fst, simp) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
300 |
apply (drule compact_snd, simp) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
301 |
done |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
302 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37079
diff
changeset
|
303 |
instance prod :: (chfin, chfin) chfin |
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
304 |
apply intro_classes |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
305 |
apply (erule compact_imp_max_in_chain) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
306 |
apply (case_tac "\<Squnion>i. Y i", simp) |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
307 |
done |
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
308 |
|
29531 | 309 |
end |