simplified chfin instance proof
authorhuffman
Mon Jan 14 20:04:40 2008 +0100 (2008-01-14)
changeset 25905098469c6c351
parent 25904 8161f137b0e9
child 25906 2179c6661218
simplified chfin instance proof
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Jan 14 19:26:41 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:04:40 2008 +0100
     1.3 @@ -163,29 +163,6 @@
     1.4  
     1.5  instance "*" :: (finite_po, finite_po) finite_po ..
     1.6  
     1.7 -instance "*" :: (chfin, chfin) chfin
     1.8 -proof (intro_classes, clarify)
     1.9 -  fix Y :: "nat \<Rightarrow> 'a \<times> 'b"
    1.10 -  assume Y: "chain Y"
    1.11 -  from Y have "chain (\<lambda>i. fst (Y i))"
    1.12 -    by (rule ch2ch_monofun [OF monofun_fst])
    1.13 -  hence "\<exists>m. max_in_chain m (\<lambda>i. fst (Y i))"
    1.14 -    by (rule chfin [rule_format])
    1.15 -  then obtain m where m: "max_in_chain m (\<lambda>i. fst (Y i))" ..
    1.16 -  from Y have "chain (\<lambda>i. snd (Y i))"
    1.17 -    by (rule ch2ch_monofun [OF monofun_snd])
    1.18 -  hence "\<exists>n. max_in_chain n (\<lambda>i. snd (Y i))"
    1.19 -    by (rule chfin [rule_format])
    1.20 -  then obtain n where n: "max_in_chain n (\<lambda>i. snd (Y i))" ..
    1.21 -  from m have m': "max_in_chain (max m n) (\<lambda>i. fst (Y i))"
    1.22 -    by (rule maxinch_mono [OF _ le_maxI1])
    1.23 -  from n have n': "max_in_chain (max m n) (\<lambda>i. snd (Y i))"
    1.24 -    by (rule maxinch_mono [OF _ le_maxI2])
    1.25 -  from m' n' have "max_in_chain (max m n) Y"
    1.26 -    unfolding max_in_chain_def Pair_fst_snd_eq by fast
    1.27 -  thus "\<exists>n. max_in_chain n Y" ..
    1.28 -qed
    1.29 -
    1.30  subsection {* Product type is pointed *}
    1.31  
    1.32  lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
    1.33 @@ -363,6 +340,12 @@
    1.34  apply (drule compact_csnd, simp)
    1.35  done
    1.36  
    1.37 +instance "*" :: (chfin, chfin) chfin
    1.38 +apply (intro_classes, clarify)
    1.39 +apply (erule compact_imp_max_in_chain)
    1.40 +apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
    1.41 +done
    1.42 +
    1.43  lemma lub_cprod2: 
    1.44    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.45  apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)