91 lemma monofun_snd: "monofun snd" |
91 lemma monofun_snd: "monofun snd" |
92 by (simp add: monofun_def less_cprod_def) |
92 by (simp add: monofun_def less_cprod_def) |
93 |
93 |
94 subsection {* Product type is a cpo *} |
94 subsection {* Product type is a cpo *} |
95 |
95 |
|
96 lemma is_lub_Pair: |
|
97 "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)" |
|
98 apply (rule is_lubI [OF ub_rangeI]) |
|
99 apply (simp add: less_cprod_def is_ub_lub) |
|
100 apply (frule ub2ub_monofun [OF monofun_fst]) |
|
101 apply (drule ub2ub_monofun [OF monofun_snd]) |
|
102 apply (simp add: less_cprod_def is_lub_lub) |
|
103 done |
|
104 |
96 lemma lub_cprod: |
105 lemma lub_cprod: |
97 fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" |
106 fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)" |
98 assumes S: "chain S" |
107 assumes S: "chain S" |
99 shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
108 shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
100 apply (rule is_lubI) |
109 proof - |
101 apply (rule ub_rangeI) |
110 have "chain (\<lambda>i. fst (S i))" |
102 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst]) |
111 using monofun_fst S by (rule ch2ch_monofun) |
103 apply (rule monofun_pair) |
112 hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))" |
104 apply (rule is_ub_thelub) |
113 by (rule thelubE [OF _ refl]) |
105 apply (rule ch2ch_monofun [OF monofun_fst S]) |
114 have "chain (\<lambda>i. snd (S i))" |
106 apply (rule is_ub_thelub) |
115 using monofun_snd S by (rule ch2ch_monofun) |
107 apply (rule ch2ch_monofun [OF monofun_snd S]) |
116 hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))" |
108 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst]) |
117 by (rule thelubE [OF _ refl]) |
109 apply (rule monofun_pair) |
118 show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
110 apply (rule is_lub_thelub) |
119 using is_lub_Pair [OF 1 2] by simp |
111 apply (rule ch2ch_monofun [OF monofun_fst S]) |
120 qed |
112 apply (erule monofun_fst [THEN ub2ub_monofun]) |
|
113 apply (rule is_lub_thelub) |
|
114 apply (rule ch2ch_monofun [OF monofun_snd S]) |
|
115 apply (erule monofun_snd [THEN ub2ub_monofun]) |
|
116 done |
|
117 |
121 |
118 lemma thelub_cprod: |
122 lemma thelub_cprod: |
119 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
123 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
120 \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
124 \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
121 by (rule lub_cprod [THEN thelubI]) |
125 by (rule lub_cprod [THEN thelubI]) |
143 by (rule minimal_cprod [THEN UU_I, symmetric]) |
147 by (rule minimal_cprod [THEN UU_I, symmetric]) |
144 |
148 |
145 |
149 |
146 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
150 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
147 |
151 |
148 lemma contlub_pair1: "contlub (\<lambda>x. (x, y))" |
|
149 apply (rule contlubI) |
|
150 apply (subst thelub_cprod) |
|
151 apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
|
152 apply simp |
|
153 done |
|
154 |
|
155 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" |
|
156 apply (rule contlubI) |
|
157 apply (subst thelub_cprod) |
|
158 apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
|
159 apply simp |
|
160 done |
|
161 |
|
162 lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
152 lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
163 apply (rule monocontlub2cont) |
153 apply (rule contI) |
164 apply (rule monofun_pair1) |
154 apply (rule is_lub_Pair) |
165 apply (rule contlub_pair1) |
155 apply (erule thelubE [OF _ refl]) |
|
156 apply (rule lub_const) |
166 done |
157 done |
167 |
158 |
168 lemma cont_pair2: "cont (\<lambda>y. (x, y))" |
159 lemma cont_pair2: "cont (\<lambda>y. (x, y))" |
169 apply (rule monocontlub2cont) |
160 apply (rule contI) |
170 apply (rule monofun_pair2) |
161 apply (rule is_lub_Pair) |
171 apply (rule contlub_pair2) |
162 apply (rule lub_const) |
|
163 apply (erule thelubE [OF _ refl]) |
172 done |
164 done |
173 |
165 |
174 lemma contlub_fst: "contlub fst" |
166 lemma contlub_fst: "contlub fst" |
175 apply (rule contlubI) |
167 apply (rule contlubI) |
176 apply (simp add: thelub_cprod) |
168 apply (simp add: thelub_cprod) |