# 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 \ 'a \ 'b" - assume Y: "chain Y" - from Y have "chain (\i. fst (Y i))" - by (rule ch2ch_monofun [OF monofun_fst]) - hence "\m. max_in_chain m (\i. fst (Y i))" - by (rule chfin [rule_format]) - then obtain m where m: "max_in_chain m (\i. fst (Y i))" .. - from Y have "chain (\i. snd (Y i))" - by (rule ch2ch_monofun [OF monofun_snd]) - hence "\n. max_in_chain n (\i. snd (Y i))" - by (rule chfin [rule_format]) - then obtain n where n: "max_in_chain n (\i. snd (Y i))" .. - from m have m': "max_in_chain (max m n) (\i. fst (Y i))" - by (rule maxinch_mono [OF _ le_maxI1]) - from n have n': "max_in_chain (max m n) (\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 "\n. max_in_chain n Y" .. -qed - subsection {* Product type is pointed *} lemma minimal_cprod: "(\, \) \ 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="\i. Y i" in cprodE, simp) +done + lemma lub_cprod2: "chain S \ range S <<| <\i. cfst\(S i), \i. csnd\(S i)>" apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)