159 hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)" |
159 hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)" |
160 by (rule directed_lub_cprod) |
160 by (rule directed_lub_cprod) |
161 thus "\<exists>x. S <<| x" .. |
161 thus "\<exists>x. S <<| x" .. |
162 qed |
162 qed |
163 |
163 |
|
164 instance "*" :: (finite_po, finite_po) finite_po .. |
|
165 |
|
166 instance "*" :: (chfin, chfin) chfin |
|
167 proof (intro_classes, clarify) |
|
168 fix Y :: "nat \<Rightarrow> 'a \<times> 'b" |
|
169 assume Y: "chain Y" |
|
170 from Y have "chain (\<lambda>i. fst (Y i))" |
|
171 by (rule ch2ch_monofun [OF monofun_fst]) |
|
172 hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))" |
|
173 by (rule chfin [rule_format]) |
|
174 then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" .. |
|
175 from Y have "chain (\<lambda>i. snd (Y i))" |
|
176 by (rule ch2ch_monofun [OF monofun_snd]) |
|
177 hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))" |
|
178 by (rule chfin [rule_format]) |
|
179 then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" .. |
|
180 from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))" |
|
181 by (rule maxinch_mono [OF _ le_maxI1]) |
|
182 from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))" |
|
183 by (rule maxinch_mono [OF _ le_maxI2]) |
|
184 from m' n' have "max_in_chain (max m n) Y" |
|
185 unfolding max_in_chain_def Pair_fst_snd_eq by fast |
|
186 thus "\<exists>n. max_in_chain n Y" .. |
|
187 qed |
|
188 |
164 subsection {* Product type is pointed *} |
189 subsection {* Product type is pointed *} |
165 |
190 |
166 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
191 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
167 by (simp add: less_cprod_def) |
192 by (simp add: less_cprod_def) |
168 |
193 |