116 apply (rule is_lub_thelub) |
116 apply (rule is_lub_thelub) |
117 apply (rule ch2ch_monofun [OF monofun_snd S]) |
117 apply (rule ch2ch_monofun [OF monofun_snd S]) |
118 apply (erule monofun_snd [THEN ub2ub_monofun]) |
118 apply (erule monofun_snd [THEN ub2ub_monofun]) |
119 done |
119 done |
120 |
120 |
121 lemma directed_lub_cprod: |
|
122 fixes S :: "('a::dcpo \<times> 'b::dcpo) set" |
|
123 assumes S: "directed S" |
|
124 shows "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)" |
|
125 apply (rule is_lubI) |
|
126 apply (rule is_ubI) |
|
127 apply (rule_tac t=x in surjective_pairing [THEN ssubst]) |
|
128 apply (rule monofun_pair) |
|
129 apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_fst S] imageI]) |
|
130 apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_snd S] imageI]) |
|
131 apply (rule_tac t=u in surjective_pairing [THEN ssubst]) |
|
132 apply (rule monofun_pair) |
|
133 apply (rule is_lub_thelub') |
|
134 apply (rule dir2dir_monofun [OF monofun_fst S]) |
|
135 apply (erule ub2ub_monofun' [OF monofun_fst]) |
|
136 apply (rule is_lub_thelub') |
|
137 apply (rule dir2dir_monofun [OF monofun_snd S]) |
|
138 apply (erule ub2ub_monofun' [OF monofun_snd]) |
|
139 done |
|
140 |
|
141 lemma thelub_cprod: |
121 lemma thelub_cprod: |
142 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
122 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
143 \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
123 \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
144 by (rule lub_cprod [THEN thelubI]) |
124 by (rule lub_cprod [THEN thelubI]) |
145 |
125 |
150 hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
130 hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
151 by (rule lub_cprod) |
131 by (rule lub_cprod) |
152 thus "\<exists>x. range S <<| x" .. |
132 thus "\<exists>x. range S <<| x" .. |
153 qed |
133 qed |
154 |
134 |
155 instance "*" :: (dcpo, dcpo) dcpo |
|
156 proof |
|
157 fix S :: "('a \<times> 'b) set" |
|
158 assume "directed S" |
|
159 hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)" |
|
160 by (rule directed_lub_cprod) |
|
161 thus "\<exists>x. S <<| x" .. |
|
162 qed |
|
163 |
|
164 instance "*" :: (finite_po, finite_po) finite_po .. |
135 instance "*" :: (finite_po, finite_po) finite_po .. |
165 |
136 |
166 subsection {* Product type is pointed *} |
137 subsection {* Product type is pointed *} |
167 |
138 |
168 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
139 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |