author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58880 | 0baae4311a9f |
child 61424 | c3658c18b7bc |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Product_Cpo.thy |
29531 | 2 |
Author: Franz Regensburger |
3 |
*) |
|
4 |
||
58880 | 5 |
section {* The cpo of cartesian products *} |
29531 | 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 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
216 |
lemma cont2cont_case_prod: |
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))" |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
236 |
by (intro cont2cont_case_prod f1 f2 cont2cont) |
39808
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 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
249 |
lemma cont2cont_case_prod' [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)" |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
252 |
shows "cont (\<lambda>x. case_prod (f x) (g x))" |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
253 |
using assms by (simp add: cont2cont_case_prod 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 |
||
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
265 |
lemma adm_case_prod [simp]: |
40619 | 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)" |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
44066
diff
changeset
|
268 |
unfolding case_prod_beta using assms . |
40619 | 269 |
|
29535
08824fad8879
add strictness and compactness lemmas to Product_Cpo.thy
huffman
parents:
29533
diff
changeset
|
270 |
subsection {* Compactness and chain-finiteness *} |
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 |