src/HOLCF/Cprod.thy
changeset 25879 98b93782c3b1
parent 25827 c2adeb1bae5c
child 25905 098469c6c351
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Jan 10 05:11:09 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Jan 10 05:15:43 2008 +0100
     1.3 @@ -342,9 +342,27 @@
     1.4  lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
     1.5  by (auto simp add: po_eq_conv less_cprod)
     1.6  
     1.7 -lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
     1.8 +lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
     1.9 +by (simp add: less_cprod)
    1.10 +
    1.11 +lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
    1.12 +by (simp add: less_cprod)
    1.13 +
    1.14 +lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
    1.15 +by (rule compactI, simp add: cfst_less_iff)
    1.16 +
    1.17 +lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
    1.18 +by (rule compactI, simp add: csnd_less_iff)
    1.19 +
    1.20 +lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
    1.21  by (rule compactI, simp add: less_cprod)
    1.22  
    1.23 +lemma compact_cpair_iff [simp]: "compact <x, y> = (compact x \<and> compact y)"
    1.24 +apply (safe intro!: compact_cpair)
    1.25 +apply (drule compact_cfst, simp)
    1.26 +apply (drule compact_csnd, simp)
    1.27 +done
    1.28 +
    1.29  lemma lub_cprod2: 
    1.30    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.31  apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)