--- a/src/HOLCF/Cprod.thy Mon Jan 14 19:26:41 2008 +0100
+++ b/src/HOLCF/Cprod.thy Mon Jan 14 20:04:40 2008 +0100
@@ -163,29 +163,6 @@
instance "*" :: (finite_po, finite_po) finite_po ..
-instance "*" :: (chfin, chfin) chfin
-proof (intro_classes, clarify)
- fix Y :: "nat \<Rightarrow> 'a \<times> 'b"
- assume Y: "chain Y"
- from Y have "chain (\<lambda>i. fst (Y i))"
- by (rule ch2ch_monofun [OF monofun_fst])
- hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))"
- by (rule chfin [rule_format])
- then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" ..
- from Y have "chain (\<lambda>i. snd (Y i))"
- by (rule ch2ch_monofun [OF monofun_snd])
- hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))"
- by (rule chfin [rule_format])
- then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" ..
- from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))"
- by (rule maxinch_mono [OF _ le_maxI1])
- from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))"
- by (rule maxinch_mono [OF _ le_maxI2])
- from m' n' have "max_in_chain (max m n) Y"
- unfolding max_in_chain_def Pair_fst_snd_eq by fast
- thus "\<exists>n. max_in_chain n Y" ..
-qed
-
subsection {* Product type is pointed *}
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
@@ -363,6 +340,12 @@
apply (drule compact_csnd, simp)
done
+instance "*" :: (chfin, chfin) chfin
+apply (intro_classes, clarify)
+apply (erule compact_imp_max_in_chain)
+apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
+done
+
lemma lub_cprod2:
"chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)