add theorem cpair_defined_iff
authorhuffman
Tue Jul 26 18:22:03 2005 +0200 (2005-07-26)
changeset 16916da331e0a4a81
parent 16915 bca4c3b1afca
child 16917 1fe50b19daba
add theorem cpair_defined_iff
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Tue Jul 26 15:29:37 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Tue Jul 26 18:22:03 2005 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4  
     1.5  subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
     1.6  
     1.7 -lemma contlub_pair1: "contlub (\<lambda>x. (x,y))"
     1.8 +lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
     1.9  apply (rule contlubI)
    1.10  apply (subst thelub_cprod)
    1.11  apply (erule monofun_pair1 [THEN ch2ch_monofun])
    1.12 @@ -252,11 +252,14 @@
    1.13  lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
    1.14  by (simp add: cpair_eq_pair less_cprod_def)
    1.15  
    1.16 +lemma cpair_defined_iff: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
    1.17 +by (simp add: inst_cprod_pcpo cpair_eq_pair)
    1.18 +
    1.19  lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
    1.20 -by (simp add: cpair_eq_pair inst_cprod_pcpo)
    1.21 +by (simp add: cpair_defined_iff)
    1.22  
    1.23  lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
    1.24 -by (simp add: cpair_eq_pair inst_cprod_pcpo)
    1.25 +by (rule cpair_strict [symmetric])
    1.26  
    1.27  lemma defined_cpair_rev: 
    1.28   "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"