# HG changeset patch
# User huffman
# Date 1122394923 -7200
# Node ID da331e0a4a81265939ff8c60d8bd95dfeea4ff97
# Parent  bca4c3b1afca6f51d7f2d6c26c39d19067a90cf8
add theorem cpair_defined_iff

diff -r bca4c3b1afca -r da331e0a4a81 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Tue Jul 26 15:29:37 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Tue Jul 26 18:22:03 2005 +0200
@@ -132,7 +132,7 @@
 
 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
 
-lemma contlub_pair1: "contlub (\<lambda>x. (x,y))"
+lemma contlub_pair1: "contlub (\<lambda>x. (x, y))"
 apply (rule contlubI)
 apply (subst thelub_cprod)
 apply (erule monofun_pair1 [THEN ch2ch_monofun])
@@ -252,11 +252,14 @@
 lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
 by (simp add: cpair_eq_pair less_cprod_def)
 
+lemma cpair_defined_iff: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
+by (simp add: inst_cprod_pcpo cpair_eq_pair)
+
 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
-by (simp add: cpair_eq_pair inst_cprod_pcpo)
+by (simp add: cpair_defined_iff)
 
 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
-by (simp add: cpair_eq_pair inst_cprod_pcpo)
+by (rule cpair_strict [symmetric])
 
 lemma defined_cpair_rev: 
  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"