# HG changeset patch
# User huffman
# Date 1200337480 -3600
# Node ID 098469c6c351c3f1c3784f373f1ba44aa23ed8e9
# Parent  8161f137b0e9b766f2c00360cbfb43301a4d215a
simplified chfin instance proof

diff -r 8161f137b0e9 -r 098469c6c351 src/HOLCF/Cprod.thy
--- 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)