src/HOLCF/Cprod.thy
changeset 17837 2922be3544f8
parent 17834 28414668b43d
child 18077 f1f4f951ec8d
     1.1 --- a/src/HOLCF/Cprod.thy	Tue Oct 11 23:47:29 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Wed Oct 12 01:43:37 2005 +0200
     1.3 @@ -274,6 +274,9 @@
     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 +by (rule compactI, simp add: less_cprod)
     1.9 +
    1.10  lemma lub_cprod2: 
    1.11    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.12  apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)